Documentation

Linglib.Logic.Trivalent.Pointwise

Trivalent propositions #

A trivalent proposition is a function W → SignType, true, false or undefined at each world. Its worlds split into a positive extension, a negative extension and a gap, and Beaver and Krahmer's assertion operator applied pointwise collapses the gap into the negative extension. Strong Kleene conjunction and disjunction of propositions are the pointwise ⊓ and ⊔. A trivalent proposition is also a conditional event in de Finetti's sense, fixed by where it is defined and where it is true. This file adds the extensions, bivalence, the conditional-event decomposition, and the three families of trivalent quantifiers.

Main definitions #

Trivalent.posExt, Trivalent.negExt, Trivalent.gapExt: the three extensions.
Trivalent.IsBivalent: the proposition is never 0.
Trivalent.forallWeak, Trivalent.existsWeak: the Weak Kleene quantifiers, undefined as soon as any instance is.
Trivalent.forallStrong, Trivalent.existsStrong: the Strong Kleene quantifiers, the indexed ⊓ and ⊔.
Trivalent.forallHaug, Trivalent.existsHaug: Haug's quantifiers, undefined only when every instance is, with existsHaug_meetWeak_presuppose as Quantifier Projection.

Main results #

Trivalent.indicator_support_ofProp_eq_one, Trivalent.indicator_ofProp_eq_indicator_ofProp_iff: every trivalent proposition is the conditional event of its truth on its definedness, and two conditional events coincide exactly when they have the same condition and agree on it.

Each family is the quantifier of a theory of how a presupposition projects from the scope of a quantifier. Over the domain's subtype, the Weak Kleene quantifiers project universally, as Chemla's experiments support, Haug's existentially, as Mayr and Sauerland argue for a semantic projection that pragmatics then strengthens, and the Strong Kleene existential of Kleene and Fox is defined exactly where some instance is true or every instance is false; Spector and Sudo delimit when each reading surfaces.

Implementation notes #

The Strong Kleene quantifiers are explicit definitions rather than ⨅ and ⨆, because a CompleteLinearOrder instance on SignType would carry a second LinearOrder parent that instance search prefers, making every later ⊓ noncomputable.

References #

Extensions #

def Trivalent.posExt {W : Type u_1} (p : W → SignType) :

Set W

The positive extension collects the worlds where the proposition is true.

Equations

Trivalent.posExt p = {w : W | p w = 1}

Instances For

def Trivalent.negExt {W : Type u_1} (p : W → SignType) :

Set W

The negative extension collects the worlds where the proposition is false.

Equations

Trivalent.negExt p = {w : W | p w = -1}

Instances For

def Trivalent.gapExt {W : Type u_1} (p : W → SignType) :

Set W

The extension gap collects the worlds where the proposition is neither true nor false.

Equations

Trivalent.gapExt p = {w : W | p w = 0}

Instances For

@[simp]

theorem Trivalent.mem_posExt {W : Type u_1} {p : W → SignType} {w : W} :

w ∈ posExt p ↔ p w = 1

@[simp]

theorem Trivalent.mem_negExt {W : Type u_1} {p : W → SignType} {w : W} :

w ∈ negExt p ↔ p w = -1

@[simp]

theorem Trivalent.mem_gapExt {W : Type u_1} {p : W → SignType} {w : W} :

w ∈ gapExt p ↔ p w = 0

@[instance_reducible]

instance Trivalent.instDecidablePredMemSetPosExt {W : Type u_1} (p : W → SignType) :

DecidablePred fun (x : W) => x ∈ posExt p

Equations

Trivalent.instDecidablePredMemSetPosExt p w = Trivalent.instDecidablePredMemSetPosExt._aux_1 p w

@[instance_reducible]

instance Trivalent.instDecidablePredMemSetNegExt {W : Type u_1} (p : W → SignType) :

DecidablePred fun (x : W) => x ∈ negExt p

Equations

Trivalent.instDecidablePredMemSetNegExt p w = Trivalent.instDecidablePredMemSetNegExt._aux_1 p w

@[instance_reducible]

instance Trivalent.instDecidablePredMemSetGapExt {W : Type u_1} (p : W → SignType) :

DecidablePred fun (x : W) => x ∈ gapExt p

Equations

Trivalent.instDecidablePredMemSetGapExt p w = Trivalent.instDecidablePredMemSetGapExt._aux_1 p w

theorem Trivalent.posExt_union_negExt {W : Type u_1} (p : W → SignType) :

posExt p ∪ negExt p = Function.support p

A proposition is defined where it is true or false.

theorem Trivalent.posExt_subset_support {W : Type u_1} (p : W → SignType) :

posExt p ⊆ Function.support p

theorem Trivalent.negExt_subset_support {W : Type u_1} (p : W → SignType) :

negExt p ⊆ Function.support p

theorem Trivalent.support_inter_compl_posExt {W : Type u_1} (p : W → SignType) :

Function.support p ∩ (posExt p)ᶜ = negExt p

Where a proposition is defined and not true, it is false.

theorem Trivalent.posExt_union_negExt_union_gapExt {W : Type u_1} (p : W → SignType) :

posExt p ∪ negExt p ∪ gapExt p = Set.univ

The three extensions cover the world space.

theorem Trivalent.disjoint_posExt_negExt {W : Type u_1} (p : W → SignType) :

Disjoint (posExt p) (negExt p)

The positive and negative extensions are disjoint.

def Trivalent.IsBivalent {W : Type u_1} (p : W → SignType) :

A proposition is bivalent if it takes no 0 value.

Equations

Trivalent.IsBivalent p = ∀ (w : W), p w = 1 ∨ p w = -1

Instances For

theorem Trivalent.isBivalent_iff_gapExt_eq_empty {W : Type u_1} (p : W → SignType) :

IsBivalent p ↔ gapExt p = ∅

theorem Trivalent.isBivalent_iff_forall_ne_zero {W : Type u_1} (p : W → SignType) :

IsBivalent p ↔ ∀ (w : W), p w ≠ 0

theorem Trivalent.IsBivalent.ne_zero {W : Type u_1} {p : W → SignType} (h : IsBivalent p) (w : W) :

p w ≠ 0

Presupposition and assertion #

A proposition defined where A holds and asserting B there is the indicator {w | A w}.indicator fun w ↦ ofProp (B w): the classical value of B on A and 0 elsewhere. Its defined region is its Function.support, and an indicator of an indicator is the indicator of the intersection (Set.indicator_indicator).

@[simp]

theorem Trivalent.support_ofProp {W : Type u_1} (B : W → Prop) [DecidablePred B] :

(Function.support fun (w : W) => SignType.ofProp (B w)) = Set.univ

A classical proposition is defined everywhere, so by Set.support_indicator an assertion restricted to s is defined exactly on s.

@[simp]

theorem Trivalent.indicator_apply_eq_one_iff {W : Type u_1} {s : Set W} {f : W → SignType} {w : W} :

s.indicator f w = 1 ↔ w ∈ s ∧ f w = 1

@[simp]

theorem Trivalent.indicator_apply_eq_neg_one_iff {W : Type u_1} {s : Set W} {f : W → SignType} {w : W} :

s.indicator f w = -1 ↔ w ∈ s ∧ f w = -1

theorem Trivalent.support_eq_compl_gapExt {W : Type u_1} (p : W → SignType) :

Function.support p = (gapExt p)ᶜ

The defined region of a proposition is the complement of its gap.

Conditional events #

A trivalent proposition is fixed by where it is defined and where it is true, and every such pair arises: the indicator of B on A is defined on A and true on A ∩ B. So trivalent propositions are the conditional events B | A of [dF36], conditional assertions of a two-valued content on a two-valued condition, and two of them coincide exactly when they have the same condition and agree on it.

theorem Trivalent.indicator_support_ofProp_eq_one {W : Type u_1} (p : W → SignType) :

((Function.support p).indicator fun (w : W) => SignType.ofProp (p w = 1)) = p

Every trivalent proposition is the conditional event of its truth on its definedness.

theorem Trivalent.indicator_ofProp_eq_indicator_ofProp_iff {W : Type u_1} {A A' : Set W} {B B' : W → Prop} [DecidablePred B] [DecidablePred B'] :

((A.indicator fun (w : W) => SignType.ofProp (B w)) = A'.indicator fun (w : W) => SignType.ofProp (B' w)) ↔ A = A' ∧ A ∩ {w : W | B w} = A' ∩ {w : W | B' w}

Two conditional events coincide exactly when they have the same condition and agree on it.

Extensions under assertion #

Asserting a proposition pointwise, fun w ↦ ofProp (p w = 1), keeps its positive extension and moves its gap into the negative extension.

@[simp]

theorem Trivalent.posExt_ofProp_eq_one {W : Type u_1} (p : W → SignType) :

(posExt fun (w : W) => SignType.ofProp (p w = 1)) = posExt p

@[simp]

theorem Trivalent.negExt_ofProp_eq_one {W : Type u_1} (p : W → SignType) :

(negExt fun (w : W) => SignType.ofProp (p w = 1)) = negExt p ∪ gapExt p

@[simp]

theorem Trivalent.gapExt_ofProp_eq_one {W : Type u_1} (p : W → SignType) :

(gapExt fun (w : W) => SignType.ofProp (p w = 1)) = ∅

theorem Trivalent.isBivalent_ofProp_eq_one {W : Type u_1} (p : W → SignType) :

IsBivalent fun (w : W) => SignType.ofProp (p w = 1)

Asserting a proposition pointwise makes it bivalent.

Quantifiers #

Like the binary connectives, the trivalent quantifiers come in rival families that share one truth rule and differ only in where undefinedness projects, which forallWith and existsWith make definitional: a family is fixed by its definedness condition. The Weak Kleene quantifiers are undefined as soon as any instance is; the Strong Kleene quantifiers are defined whenever the instances settle the value, the indexed ⊓ and ⊔; and the quantifiers of [Hau14], adopted by [CB15] and [Coo23], are undefined only when every instance is, so that a quantified presupposition projects existentially. Restricted to a pair of instances the families are the binary connectives — Weak Kleene meetWeak, Strong Kleene ⊓, and, for Haug's quantifier, Belnap's skip-undefined meetBelnap (forallHaug_pair). Middle Kleene reads its operands left to right, so it has no order-free quantifier.

noncomputable def Trivalent.forallWith {ι : Sort u_2} (D : Prop) (p : ι → SignType) :

SignType

forallWith D p is the universal quantifier undefined unless D holds, and otherwise false exactly when some instance is. All the families share this truth rule (forallWith_eq_forallWith_of_defined).

Equations

Trivalent.forallWith D p = if D then if ∃ (i : ι), p i = -1 then -1 else 1 else 0

Instances For

noncomputable def Trivalent.existsWith {ι : Sort u_2} (D : Prop) (p : ι → SignType) :

SignType

existsWith D p is the existential quantifier of the family whose definedness condition is D, the dual of forallWith.

Equations

Trivalent.existsWith D p = -Trivalent.forallWith D fun (i : ι) => -p i

Instances For

theorem Trivalent.forallWith_eq_zero_iff {ι : Sort u_2} {D : Prop} {p : ι → SignType} :

forallWith D p = 0 ↔ ¬D

theorem Trivalent.forallWith_eq_neg_one_iff {ι : Sort u_2} {D : Prop} {p : ι → SignType} :

forallWith D p = -1 ↔ D ∧ ∃ (i : ι), p i = -1

theorem Trivalent.forallWith_eq_one_iff {ι : Sort u_2} {D : Prop} {p : ι → SignType} :

forallWith D p = 1 ↔ D ∧ ∀ (i : ι), p i ≠ -1

theorem Trivalent.existsWith_eq_zero_iff {ι : Sort u_2} {D : Prop} {p : ι → SignType} :

existsWith D p = 0 ↔ ¬D

theorem Trivalent.existsWith_eq_one_iff {ι : Sort u_2} {D : Prop} {p : ι → SignType} :

existsWith D p = 1 ↔ D ∧ ∃ (i : ι), p i = 1

theorem Trivalent.existsWith_eq_neg_one_iff {ι : Sort u_2} {D : Prop} {p : ι → SignType} :

existsWith D p = -1 ↔ D ∧ ∀ (i : ι), p i ≠ 1

theorem Trivalent.forallWith_eq_forallWith_of_defined {ι : Sort u_2} {D D' : Prop} {p : ι → SignType} (hD : D) (hD' : D') :

forallWith D p = forallWith D' p

Any two families agree wherever both are defined, since they share one truth rule.

theorem Trivalent.forallWith_congr {ι : Sort u_2} {D D' : Prop} {p : ι → SignType} (h : D ↔ D') :

forallWith D p = forallWith D' p

theorem Trivalent.existsWith_congr {ι : Sort u_2} {D D' : Prop} {p : ι → SignType} (h : D ↔ D') :

existsWith D p = existsWith D' p

noncomputable def Trivalent.forallWeak {ι : Sort u_2} (p : ι → SignType) :

SignType

The Weak Kleene universal quantifier is undefined when any instance is, and otherwise classical.

Equations

Trivalent.forallWeak p = Trivalent.forallWith (∀ (i : ι), p i ≠ 0) p

Instances For

noncomputable def Trivalent.existsWeak {ι : Sort u_2} (p : ι → SignType) :

SignType

The Weak Kleene existential quantifier is the dual of forallWeak.

Equations

Trivalent.existsWeak p = Trivalent.existsWith (∀ (i : ι), p i ≠ 0) p

Instances For

@[simp]

theorem Trivalent.forallWeak_eq_zero_iff {ι : Sort u_2} {p : ι → SignType} :

forallWeak p = 0 ↔ ∃ (i : ι), p i = 0

@[simp]

theorem Trivalent.forallWeak_eq_one_iff {ι : Sort u_2} {p : ι → SignType} :

forallWeak p = 1 ↔ ∀ (i : ι), p i = 1

@[simp]

theorem Trivalent.forallWeak_eq_neg_one_iff {ι : Sort u_2} {p : ι → SignType} :

forallWeak p = -1 ↔ (∀ (i : ι), p i ≠ 0) ∧ ∃ (i : ι), p i = -1

@[simp]

theorem Trivalent.existsWeak_eq_zero_iff {ι : Sort u_2} {p : ι → SignType} :

existsWeak p = 0 ↔ ∃ (i : ι), p i = 0

@[simp]

theorem Trivalent.existsWeak_eq_one_iff {ι : Sort u_2} {p : ι → SignType} :

existsWeak p = 1 ↔ (∀ (i : ι), p i ≠ 0) ∧ ∃ (i : ι), p i = 1

@[simp]

theorem Trivalent.existsWeak_eq_neg_one_iff {ι : Sort u_2} {p : ι → SignType} :

existsWeak p = -1 ↔ ∀ (i : ι), p i = -1

noncomputable def Trivalent.forallStrong {ι : Sort u_2} (p : ι → SignType) :

SignType

The Strong Kleene universal quantifier is the indexed ⊓, false when any instance is, true when all are, and undefined otherwise.

Equations

Trivalent.forallStrong p = Trivalent.forallWith ((∃ (i : ι), p i = -1) ∨ ∀ (i : ι), p i = 1) p

Instances For

noncomputable def Trivalent.existsStrong {ι : Sort u_2} (p : ι → SignType) :

SignType

The Strong Kleene existential quantifier is the dual of forallStrong, the indexed ⊔.

Equations

Trivalent.existsStrong p = Trivalent.existsWith ((∃ (i : ι), p i = 1) ∨ ∀ (i : ι), p i = -1) p

Instances For

@[simp]

theorem Trivalent.forallStrong_eq_neg_one_iff {ι : Sort u_2} {p : ι → SignType} :

forallStrong p = -1 ↔ ∃ (i : ι), p i = -1

@[simp]

theorem Trivalent.forallStrong_eq_one_iff {ι : Sort u_2} {p : ι → SignType} :

forallStrong p = 1 ↔ ∀ (i : ι), p i = 1

@[simp]

theorem Trivalent.forallStrong_eq_zero_iff {ι : Sort u_2} {p : ι → SignType} :

forallStrong p = 0 ↔ (∀ (i : ι), p i ≠ -1) ∧ ∃ (i : ι), p i = 0

@[simp]

theorem Trivalent.existsStrong_eq_one_iff {ι : Sort u_2} {p : ι → SignType} :

existsStrong p = 1 ↔ ∃ (i : ι), p i = 1

@[simp]

theorem Trivalent.existsStrong_eq_neg_one_iff {ι : Sort u_2} {p : ι → SignType} :

existsStrong p = -1 ↔ ∀ (i : ι), p i = -1

@[simp]

theorem Trivalent.existsStrong_eq_zero_iff {ι : Sort u_2} {p : ι → SignType} :

existsStrong p = 0 ↔ (∀ (i : ι), p i ≠ 1) ∧ ∃ (i : ι), p i = 0

noncomputable def Trivalent.forallHaug {W : Type u_1} (p : W → SignType) :

SignType

Haug's universal quantifier skips undefined instances — undefined only when every instance is, false when some instance is, and true otherwise.

Equations

Trivalent.forallHaug p = Trivalent.forallWith (∃ (w : W), p w ≠ 0) p

Instances For

noncomputable def Trivalent.existsHaug {W : Type u_1} (p : W → SignType) :

SignType

The dual of forallHaug.

Equations

Trivalent.existsHaug p = Trivalent.existsWith (∃ (w : W), p w ≠ 0) p

Instances For

@[simp]

theorem Trivalent.forallHaug_eq_zero_iff {W : Type u_1} {p : W → SignType} :

forallHaug p = 0 ↔ ∀ (w : W), p w = 0

@[simp]

theorem Trivalent.forallHaug_eq_neg_one_iff {W : Type u_1} {p : W → SignType} :

forallHaug p = -1 ↔ ∃ (w : W), p w = -1

@[simp]

theorem Trivalent.forallHaug_eq_one_iff {W : Type u_1} {p : W → SignType} :

forallHaug p = 1 ↔ (∃ (w : W), p w ≠ 0) ∧ ∀ (w : W), p w ≠ -1

@[simp]

theorem Trivalent.existsHaug_eq_zero_iff {W : Type u_1} {p : W → SignType} :

existsHaug p = 0 ↔ ∀ (w : W), p w = 0

@[simp]

theorem Trivalent.existsHaug_eq_one_iff {W : Type u_1} {p : W → SignType} :

existsHaug p = 1 ↔ ∃ (w : W), p w = 1

@[simp]

theorem Trivalent.existsHaug_eq_neg_one_iff {W : Type u_1} {p : W → SignType} :

existsHaug p = -1 ↔ (∃ (w : W), p w ≠ 0) ∧ ∀ (w : W), p w ≠ 1

Each family restricted to a pair is its binary connective #

One lemma carries the correspondence: the gap-policy quantifier at a pair of instances is the gap-policy connective at the matching policy (forallWith_pair), and each family's pair lemma instantiates it.

theorem Trivalent.forallWith_pair (a b : SignType) {D : Prop} [Decidable D] :

(forallWith D fun (i : Bool) => bif i then a else b) = SignType.meetWith D a b

theorem Trivalent.existsWith_pair (a b : SignType) {D : Prop} [Decidable D] :

(existsWith D fun (i : Bool) => bif i then a else b) = SignType.joinWith D a b

theorem Trivalent.forallWeak_pair (a b : SignType) :

(forallWeak fun (i : Bool) => bif i then a else b) = a.meetWeak b

theorem Trivalent.existsWeak_pair (a b : SignType) :

(existsWeak fun (i : Bool) => bif i then a else b) = a.joinWeak b

theorem Trivalent.forallStrong_pair (a b : SignType) :

(forallStrong fun (i : Bool) => bif i then a else b) = min a b

theorem Trivalent.existsStrong_pair (a b : SignType) :

(existsStrong fun (i : Bool) => bif i then a else b) = max a b

theorem Trivalent.forallHaug_pair (a b : SignType) :

(forallHaug fun (i : Bool) => bif i then a else b) = a.meetBelnap b

Haug's universal quantifier restricted to a pair of instances is the conjunction of [Bel70], which skips undefined operands.

theorem Trivalent.existsHaug_pair (a b : SignType) :

(existsHaug fun (i : Bool) => bif i then a else b) = a.joinBelnap b

Dually, Haug's existential restricted to a pair is Belnap disjunction.

theorem Trivalent.existsHaug_presuppose_ne_neg_one {W : Type u_1} (p : W → SignType) :

(existsHaug fun (w : W) => max (p w) 0) ≠ -1

An existentially quantified presupposition is true or undefined, never false.

theorem Trivalent.existsHaug_meetWeak_presuppose {W : Type u_1} {φ ψ : W → SignType} (hφ : IsBivalent φ) (hψ : IsBivalent ψ) :

(existsHaug fun (w : W) => (max (φ w) 0).meetWeak (ψ w)) = (existsHaug fun (w : W) => max (φ w) 0).meetWeak (existsHaug fun (w : W) => (φ w).meetWeak (ψ w))

Quantifier Projection ([CB15]'s appendix) lets a presupposition under the existential project as an existentially quantified presupposition, over bivalent φ and ψ.