Trivalent propositions

Prop3 W is a proposition valued in Trivalent: at each world it is true, false, or undefined. Its worlds split into the positive extension, the negative extension, and the extension gap; Prop3.metaAssert — the Beaver-Krahmer 𝒜 operator lifted pointwise — collapses the gap into the negative extension. As a Pi type, Prop3 W inherits its lattice structure pointwise (⊓/⊔ via Pi.instLattice).

References

[BK01] [Kri16]

@[reducible, inline]

abbrev Trivalent.Prop3 (W : Type u_1) : Type u_1

Three-valued propositions: functions from worlds to Trivalent.

Equations

• Trivalent.Prop3 W = (W → Trivalent)

Prop3 W := W → Trivalent is a Pi type: Lattice (W → Trivalent) auto-derives from Pi.instLattice, so (p ⊔ q) w = p w ⊔ q w and (p ⊓ q) w = p w ⊓ q w come for free from Pi.sup_apply/Pi.inf_apply — use ⊔/⊓ directly rather than bespoke wrappers. The only Trivalent-specific operation needing a pointwise lift is metaAssert: there is no Pi analogue of a unary collapsing operator.

def Trivalent.Prop3.metaAssert {W : Type u_1} (p : Prop3 W) : Prop3 W

Pointwise meta-assertion (Beaver-Krahmer 𝒜 operator).

Equations

• p.metaAssert w = (p w).metaAssert

@[simp]

theorem Trivalent.Prop3.metaAssert_apply {W : Type u_1} (p : Prop3 W) (w : W) : p.metaAssert w = (p w).metaAssert

Extensions

def Trivalent.Prop3.posExt {W : Type u_1} (p : Prop3 W) : Set W

Positive extension: worlds where the proposition is true.

Equations

• p.posExt = {w : W | p w = Trivalent.true}

def Trivalent.Prop3.negExt {W : Type u_1} (p : Prop3 W) : Set W

Negative extension: worlds where the proposition is false.

Equations

• p.negExt = {w : W | p w = Trivalent.false}

def Trivalent.Prop3.gapExt {W : Type u_1} (p : Prop3 W) : Set W

Extension gap: worlds where the proposition is neither true nor false.

Equations

• p.gapExt = {w : W | p w = Trivalent.indet}

@[simp]

theorem Trivalent.Prop3.mem_posExt {W : Type u_1} {p : Prop3 W} {w : W} : w ∈ p.posExt ↔ p w = true

@[simp]

theorem Trivalent.Prop3.mem_negExt {W : Type u_1} {p : Prop3 W} {w : W} : w ∈ p.negExt ↔ p w = false

@[simp]

theorem Trivalent.Prop3.mem_gapExt {W : Type u_1} {p : Prop3 W} {w : W} : w ∈ p.gapExt ↔ p w = indet

theorem Trivalent.Prop3.posExt_union_negExt_union_gapExt {W : Type u_1} (p : Prop3 W) : p.posExt ∪ p.negExt ∪ p.gapExt = Set.univ

The three extensions cover the world space.

theorem Trivalent.Prop3.disjoint_posExt_negExt {W : Type u_1} (p : Prop3 W) : Disjoint p.posExt p.negExt

The positive and negative extensions are disjoint.

def Trivalent.Prop3.isBivalent {W : Type u_1} (p : Prop3 W) : Prop

A proposition is bivalent if it takes no .indet value.

Equations

• p.isBivalent = ∀ (w : W), p w = Trivalent.true ∨ p w = Trivalent.false

theorem Trivalent.Prop3.isBivalent_iff_gapExt_eq_empty {W : Type u_1} (p : Prop3 W) : p.isBivalent ↔ p.gapExt = ∅

Extensions under meta-assertion

@[simp]

theorem Trivalent.Prop3.posExt_metaAssert {W : Type u_1} (p : Prop3 W) : p.metaAssert.posExt = p.posExt

@[simp]

theorem Trivalent.Prop3.negExt_metaAssert {W : Type u_1} (p : Prop3 W) : p.metaAssert.negExt = p.negExt ∪ p.gapExt

@[simp]

theorem Trivalent.Prop3.gapExt_metaAssert {W : Type u_1} (p : Prop3 W) : p.metaAssert.gapExt = ∅

theorem Trivalent.Prop3.isBivalent_metaAssert {W : Type u_1} (p : Prop3 W) : p.metaAssert.isBivalent

Meta-assertion produces a bivalent proposition.