Bilateral truthmaker propositions

This file defines Kit Fine's bilateral propositions. A bilateral proposition pairs a set of verifiers with a set of falsifiers. Negation swaps the two sets, conjunction fuses verifiers and pools falsifiers, and disjunction pools verifiers and fuses falsifiers.

The possible states form a lower set P, and two states are compatible when their fusion is possible. A proposition is exclusive when no verifier is compatible with a falsifier, and exhaustive when every possible state is compatible with a verifier or a falsifier. The maximal possible states are the worlds, and a proposition is true at a world containing one of its verifiers. When the states form a complete lattice, the subject-matter of a proposition is the fusion of all its verifiers and falsifiers.

Main definitions

• Truthmaker.BilProp: a set of verifiers and a set of falsifiers, with negation as an InvolutiveNeg instance.
• Truthmaker.BilProp.conj, Truthmaker.BilProp.disj: conjunction and disjunction.
• Truthmaker.BilProp.Exclusive, Truthmaker.BilProp.Exhaustive: the two halves of bivalence.
• Truthmaker.BilProp.subjectMatter: the fusion of all verifiers and falsifiers.
• Truthmaker.Canonical.possible, Truthmaker.Canonical.atom: Fine's canonical space, whose states are sets of literals, and its atomic propositions.
• Truthmaker.Canonical.mirror: the literal with the same atom and the opposite polarity.

Main results

• Truthmaker.BilProp.neg_conj, Truthmaker.BilProp.neg_disj: De Morgan's laws.
• Truthmaker.BilProp.Exclusive.conj, Truthmaker.BilProp.Exhaustive.conj: conjunction preserves exclusivity and exhaustivity, and so do negation and disjunction.
• Truthmaker.BilProp.exclusive_iff: a proposition is exclusive exactly when no possible state makes it both true and false.
• Truthmaker.BilProp.exhaustive_iff: when every possible state is part of a world, a proposition is exhaustive exactly when it is true or false at every world.
• Truthmaker.Canonical.maximal_possible_iff, Truthmaker.Canonical.exists_le_maximal_possible: the worlds of the canonical space contain exactly one of each literal and its mirror, and every consistent set of literals is part of one.
• Truthmaker.BilProp.subjectMatter_neg, Truthmaker.BilProp.subjectMatter_conj: negation keeps the subject-matter, and conjunction fuses subject-matters.
• Truthmaker.Canonical.mem_upperClosure_disj_neg_atom, Truthmaker.Canonical.subjectMatter_disj_neg_atom_injective: the excluded middle a ∨ ¬a of an atom is true at every world, yet distinct atoms give excluded middles with distinct subject-matters, each an impossible state.

Implementation notes

Fine defines conjunction only between propositions with a verifier and disjunction only between propositions with a falsifier. Here both are total, and the subject-matter lemmas carry the nonemptiness hypotheses instead.

References

• K. Fine, A Theory of Truthmaker Content I: Conjunction, Disjunction and Negation (2017)
• K. Fine, A Theory of Truthmaker Content II: Subject-matter, Common Content, Remainder and Ground (2017)
• K. Fine, Truthmaker Semantics (2017)

structure Truthmaker.BilProp (S : Type u_1) : Type u_1

A bilateral proposition is a set of verifying states together with a set of falsifying states.

• ver : Set S

  The states that exactly verify the proposition.

• fal : Set S

  The states that exactly falsify the proposition.

theorem Truthmaker.BilProp.ext_iff {S : Type u_1} {x y : BilProp S} : x = y ↔ x.ver = y.ver ∧ x.fal = y.fal

theorem Truthmaker.BilProp.ext {S : Type u_1} {x y : BilProp S} (ver : x.ver = y.ver) (fal : x.fal = y.fal) : x = y

@[instance_reducible]

instance Truthmaker.BilProp.instInvolutiveNeg {S : Type u_1} : InvolutiveNeg (BilProp S)

The negation of a bilateral proposition swaps its verifiers and its falsifiers.

Equations

• Truthmaker.BilProp.instInvolutiveNeg = { neg := fun (A : Truthmaker.BilProp S) => { ver := A.fal, fal := A.ver }, neg_neg := ⋯ }

@[simp]

theorem Truthmaker.BilProp.ver_neg {S : Type u_1} (A : BilProp S) : (-A).ver = A.fal

@[simp]

theorem Truthmaker.BilProp.fal_neg {S : Type u_1} (A : BilProp S) : (-A).fal = A.ver

def Truthmaker.BilProp.conj {S : Type u_1} [SemilatticeSup S] (A B : BilProp S) : BilProp S

The conjunction of A and B is verified by the fusion of a verifier of each and falsified by a falsifier of either.

Equations

• A.conj B = { ver := A.ver ⊻ B.ver, fal := A.fal ∪ B.fal }

def Truthmaker.BilProp.disj {S : Type u_1} [SemilatticeSup S] (A B : BilProp S) : BilProp S

The disjunction of A and B is verified by a verifier of either and falsified by the fusion of a falsifier of each.

Equations

• A.disj B = { ver := A.ver ∪ B.ver, fal := A.fal ⊻ B.fal }

@[simp]

theorem Truthmaker.BilProp.ver_conj {S : Type u_1} [SemilatticeSup S] (A B : BilProp S) : (A.conj B).ver = A.ver ⊻ B.ver

@[simp]

theorem Truthmaker.BilProp.fal_conj {S : Type u_1} [SemilatticeSup S] (A B : BilProp S) : (A.conj B).fal = A.fal ∪ B.fal

@[simp]

theorem Truthmaker.BilProp.ver_disj {S : Type u_1} [SemilatticeSup S] (A B : BilProp S) : (A.disj B).ver = A.ver ∪ B.ver

@[simp]

theorem Truthmaker.BilProp.fal_disj {S : Type u_1} [SemilatticeSup S] (A B : BilProp S) : (A.disj B).fal = A.fal ⊻ B.fal

@[simp]

theorem Truthmaker.BilProp.neg_conj {S : Type u_1} [SemilatticeSup S] (A B : BilProp S) : -A.conj B = (-A).disj (-B)

@[simp]

theorem Truthmaker.BilProp.neg_disj {S : Type u_1} [SemilatticeSup S] (A B : BilProp S) : -A.disj B = (-A).conj (-B)

def Truthmaker.BilProp.Exclusive {S : Type u_1} [SemilatticeSup S] (P : LowerSet S) (A : BilProp S) : Prop

A bilateral proposition is exclusive over the possible states P if the fusion of a verifier with a falsifier is never possible.

Equations

• Truthmaker.BilProp.Exclusive P A = ∀ ⦃s : S⦄, s ∈ A.ver → ∀ ⦃t : S⦄, t ∈ A.fal → s ⊔ t ∉ P

def Truthmaker.BilProp.Exhaustive {S : Type u_1} [SemilatticeSup S] (P : LowerSet S) (A : BilProp S) : Prop

A bilateral proposition is exhaustive over the possible states P if every possible state has a possible fusion with a verifier or with a falsifier.

Equations

• Truthmaker.BilProp.Exhaustive P A = ∀ ⦃s : S⦄, s ∈ P → (∃ t ∈ A.ver, s ⊔ t ∈ P) ∨ ∃ t ∈ A.fal, s ⊔ t ∈ P

theorem Truthmaker.BilProp.Exclusive.neg {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A : BilProp S} (h : Exclusive P A) : Exclusive P (-A)

theorem Truthmaker.BilProp.Exhaustive.neg {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A : BilProp S} (h : Exhaustive P A) : Exhaustive P (-A)

@[simp]

theorem Truthmaker.BilProp.exclusive_neg {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A : BilProp S} : Exclusive P (-A) ↔ Exclusive P A

@[simp]

theorem Truthmaker.BilProp.exhaustive_neg {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A : BilProp S} : Exhaustive P (-A) ↔ Exhaustive P A

theorem Truthmaker.BilProp.Exclusive.conj {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A B : BilProp S} (hA : Exclusive P A) (hB : Exclusive P B) : Exclusive P (A.conj B)

theorem Truthmaker.BilProp.Exhaustive.conj {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A B : BilProp S} (hA : Exhaustive P A) (hB : Exhaustive P B) : Exhaustive P (A.conj B)

theorem Truthmaker.BilProp.Exclusive.disj {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A B : BilProp S} (hA : Exclusive P A) (hB : Exclusive P B) : Exclusive P (A.disj B)

theorem Truthmaker.BilProp.Exhaustive.disj {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A B : BilProp S} (hA : Exhaustive P A) (hB : Exhaustive P B) : Exhaustive P (A.disj B)

theorem Truthmaker.BilProp.exclusive_iff {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A : BilProp S} : Exclusive P A ↔ ∀ s ∈ P, s ∈ upperClosure A.ver → s ∉ upperClosure A.fal

A proposition is exclusive exactly when no possible state contains both a verifier and a falsifier of it.

theorem Truthmaker.BilProp.Exhaustive.mem_upperClosure {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A : BilProp S} (h : Exhaustive P A) {w : S} (hw : Maximal (fun (x : S) => x ∈ P) w) : w ∈ upperClosure A.ver ∨ w ∈ upperClosure A.fal

An exhaustive proposition is true or false at every world, a maximal possible state.

theorem Truthmaker.BilProp.exhaustive_iff {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A : BilProp S} (hP : ∀ s ∈ P, ∃ (w : S), s ≤ w ∧ Maximal (fun (x : S) => x ∈ P) w) : Exhaustive P A ↔ ∀ (w : S), Maximal (fun (x : S) => x ∈ P) w → w ∈ upperClosure A.ver ∨ w ∈ upperClosure A.fal

When every possible state is part of a world, a proposition is exhaustive exactly when it is true or false at every world.

theorem Truthmaker.BilProp.Exhaustive.mem_upperClosure_disj_neg {S : Type u_1} [SemilatticeSup S] {P : LowerSet S} {A : BilProp S} (h : Exhaustive P A) {w : S} (hw : Maximal (fun (x : S) => x ∈ P) w) : w ∈ upperClosure (A.disj (-A)).ver

The excluded middle of an exhaustive proposition is true at every world.

def Truthmaker.BilProp.subjectMatter {S : Type u_1} [CompleteLattice S] (A : BilProp S) : S

The subject-matter of a bilateral proposition is the fusion of all its verifiers and all its falsifiers.

Equations

• A.subjectMatter = sSup A.ver ⊔ sSup A.fal

@[simp]

theorem Truthmaker.BilProp.subjectMatter_neg {S : Type u_1} [CompleteLattice S] (A : BilProp S) : (-A).subjectMatter = A.subjectMatter

theorem Truthmaker.BilProp.subjectMatter_conj {S : Type u_1} [CompleteLattice S] {A B : BilProp S} (hA : A.ver.Nonempty) (hB : B.ver.Nonempty) : (A.conj B).subjectMatter = A.subjectMatter ⊔ B.subjectMatter

The subject-matter of a conjunction of propositions with verifiers fuses their subject-matters.

theorem Truthmaker.BilProp.subjectMatter_disj {S : Type u_1} [CompleteLattice S] {A B : BilProp S} (hA : A.fal.Nonempty) (hB : B.fal.Nonempty) : (A.disj B).subjectMatter = A.subjectMatter ⊔ B.subjectMatter

The subject-matter of a disjunction of propositions with falsifiers fuses their subject-matters.

theorem Truthmaker.BilProp.subjectMatter_disj_neg {S : Type u_1} [CompleteLattice S] {A : BilProp S} (hv : A.ver.Nonempty) (hf : A.fal.Nonempty) : (A.disj (-A)).subjectMatter = A.subjectMatter

The excluded middle of a proposition with a verifier and a falsifier has the subject-matter of the proposition.

def Truthmaker.Canonical.mirror {α : Type u_1} (x : α × Bool) : α × Bool

The mirror image of a literal has the same atom and the opposite polarity.

Equations

• Truthmaker.Canonical.mirror x = (x.1, !x.2)

@[simp]

theorem Truthmaker.Canonical.mirror_mk {α : Type u_1} (a : α) (b : Bool) : mirror (a, b) = (a, !b)

@[simp]

theorem Truthmaker.Canonical.mirror_mirror {α : Type u_1} (x : α × Bool) : mirror (mirror x) = x

theorem Truthmaker.Canonical.mirror_involutive {α : Type u_1} : Function.Involutive mirror

theorem Truthmaker.Canonical.mirror_ne {α : Type u_1} (x : α × Bool) : mirror x ≠ x

def Truthmaker.Canonical.possible {α : Type u_1} : LowerSet (Set (α × Bool))

The possible states of the canonical space are the consistent sets of literals, those containing no literal together with its mirror image. The literal (a, true) asserts the atom a and (a, false) denies it.

Equations

• Truthmaker.Canonical.possible = { carrier := {L : Set (α × Bool) | ∀ x ∈ L, Truthmaker.Canonical.mirror x ∉ L}, lower' := ⋯ }

theorem Truthmaker.Canonical.mem_possible {α : Type u_1} {L : Set (α × Bool)} : L ∈ possible ↔ ∀ x ∈ L, mirror x ∉ L

theorem Truthmaker.Canonical.maximal_possible_iff {α : Type u_1} {w : Set (α × Bool)} : Maximal (fun (x : Set (α × Bool)) => x ∈ possible) w ↔ ∀ (x : α × Bool), x ∈ w ↔ mirror x ∉ w

The worlds of the canonical space are the sets of literals that contain exactly one of each literal and its mirror image.

theorem Truthmaker.Canonical.mem_or_mirror_mem_of_maximal {α : Type u_1} {w : Set (α × Bool)} (hw : Maximal (fun (x : Set (α × Bool)) => x ∈ possible) w) (x : α × Bool) : x ∈ w ∨ mirror x ∈ w

A world of the canonical space contains every literal or its mirror image.

theorem Truthmaker.Canonical.exists_le_maximal_possible {α : Type u_1} {L : Set (α × Bool)} (hL : L ∈ possible) : ∃ (w : Set (α × Bool)), L ⊆ w ∧ Maximal (fun (x : Set (α × Bool)) => x ∈ possible) w

Every consistent set of literals is part of a world, so the canonical space is a W-space.

def Truthmaker.Canonical.atom {α : Type u_1} (a : α) : BilProp (Set (α × Bool))

The atomic proposition a is verified by its assertion and falsified by its denial.

Equations

• Truthmaker.Canonical.atom a = { ver := {{(a, true)}}, fal := {{(a, false)}} }

@[simp]

theorem Truthmaker.Canonical.ver_atom {α : Type u_1} (a : α) : (atom a).ver = {{(a, true)}}

@[simp]

theorem Truthmaker.Canonical.fal_atom {α : Type u_1} (a : α) : (atom a).fal = {{(a, false)}}

theorem Truthmaker.Canonical.exclusive_atom {α : Type u_1} (a : α) : BilProp.Exclusive possible (atom a)

theorem Truthmaker.Canonical.exhaustive_atom {α : Type u_1} (a : α) : BilProp.Exhaustive possible (atom a)

theorem Truthmaker.Canonical.subjectMatter_atom {α : Type u_1} (a : α) : (atom a).subjectMatter = {(a, true), (a, false)}

theorem Truthmaker.Canonical.mem_upperClosure_disj_neg_atom {α : Type u_1} (a : α) {w : Set (α × Bool)} (hw : Maximal (fun (x : Set (α × Bool)) => x ∈ possible) w) : w ∈ upperClosure ((atom a).disj (-atom a)).ver

The excluded middle of an atom is true at every world of the canonical space.

theorem Truthmaker.Canonical.subjectMatter_disj_neg_atom {α : Type u_1} (a : α) : ((atom a).disj (-atom a)).subjectMatter = {(a, true), (a, false)}

theorem Truthmaker.Canonical.subjectMatter_disj_neg_atom_not_mem {α : Type u_1} (a : α) : ((atom a).disj (-atom a)).subjectMatter ∉ possible

The subject-matter of the excluded middle of an atom is an impossible state.

theorem Truthmaker.Canonical.subjectMatter_disj_neg_atom_injective {α : Type u_1} : Function.Injective fun (a : α) => ((atom a).disj (-atom a)).subjectMatter

Excluded middles of distinct atoms have distinct subject-matters.