Plebani, Rosella and Saitta (2022): Truthmakers, incompatibility, and modality

Plebani, Rosella and Saitta build truthmaker semantics on a primitive, symmetric relation of exact incompatibility between states in place of Fine's primitive set of possible states. Two states are inexactly incompatible when a part of one is exactly incompatible with a part of the other (Truthmaker.Conflict) and compatible otherwise, and a state is possible when it is compatible with itself (Truthmaker.possible). Compatibility passes to parts (Claim 1, Truthmaker.Conflict.mono), and a state is possible exactly when its parts are pairwise compatible (Claim 2, Truthmaker.mem_possible_iff_forall). In the canonical model a literal is exactly incompatible with its mirror image, and the possible states are the consistent sets of literals (Truthmaker.Canonical.possible_excl).

A state is maximal with respect to compatibility when it contains every state compatible with it (MaximalCompat), and maximal with respect to parthood when no possible state properly contains it. The first implies the second (maximal_of_maximalCompat, Claim 3) but not conversely (maximal_counterExcl, not_maximalCompat_counterExcl). Fine's condition that compatible states have a possible fusion restores the converse (maximalCompat_of_maximal, Claim 4), but it makes the null state incompatible with every impossible state (conflict_bot_of_not_mem_possible). Possible Fusion instead equates maximality with respect to parthood with a weaker maximality with respect to compatibility (maximal_iff_weakMaximalCompat, Claim 5).

The falsifiers of an atomic formula are the states exactly incompatible with all its verifiers, and the connectives follow Fine's bilateral clauses (denote). Every verifier of a formula is then inexactly incompatible with every falsifier (conflict_of_mem_ver_of_mem_fal, Theorem 1), so no possible state verifies a contradiction (not_mem_possible_of_mem_ver_conj_neg, Corollary 1).

Implementation notes

States form a complete lattice. Maximality with respect to parthood is mathlib's Maximal among the possible states, which is the paper's definition for possible states, the only ones its claims about it concern. The applications to first-degree entailment, the Routley star and Kripke frames (§§4–5) are not formalized.

References

• M. Plebani, G. Rosella and V. Saitta, Truthmakers, Incompatibility, and Modality (2022)
• K. Fine, A Theory of Truthmaker Content I: Conjunction, Disjunction and Negation (2017)

Possible worlds

def PlebaniRosellaSaitta2022.MaximalCompat {S : Type u_1} [CompleteLattice S] (excl : S → S → Prop) (s : S) : Prop

A state is maximal with respect to compatibility when every state compatible with it is part of it (def. 10).

Equations

• PlebaniRosellaSaitta2022.MaximalCompat excl s = ∀ ⦃u : S⦄, ¬Truthmaker.Conflict excl u s → u ≤ s

def PlebaniRosellaSaitta2022.WeakMaximalCompat {S : Type u_1} [CompleteLattice S] (excl : S → S → Prop) (s : S) : Prop

A state is weakly maximal with respect to compatibility when every possible state compatible with it is part of it (def. 13).

Equations

• PlebaniRosellaSaitta2022.WeakMaximalCompat excl s = ∀ ⦃u : S⦄, u ∈ Truthmaker.possible excl → ¬Truthmaker.Conflict excl u s → u ≤ s

theorem PlebaniRosellaSaitta2022.maximal_of_maximalCompat {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {s : S} (hs : s ∈ Truthmaker.possible excl) (h : MaximalCompat excl s) : Maximal (fun (x : S) => x ∈ Truthmaker.possible excl) s

A possible state that is maximal with respect to compatibility is maximal with respect to parthood (Claim 3).

theorem PlebaniRosellaSaitta2022.maximalCompat_of_maximal {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {s : S} (hF : ∀ ⦃s t : S⦄, ¬Truthmaker.Conflict excl s t → s ⊔ t ∈ Truthmaker.possible excl) (hs : Maximal (fun (x : S) => x ∈ Truthmaker.possible excl) s) : MaximalCompat excl s

If compatible states have a possible fusion, a state that is maximal with respect to parthood is maximal with respect to compatibility (Claim 4).

theorem PlebaniRosellaSaitta2022.conflict_bot_of_not_mem_possible {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {t : S} (hF : ∀ ⦃s t : S⦄, ¬Truthmaker.Conflict excl s t → s ⊔ t ∈ Truthmaker.possible excl) (ht : t ∉ Truthmaker.possible excl) : Truthmaker.Conflict excl ⊥ t

If compatible states have a possible fusion, the null state is incompatible with every impossible state.

theorem PlebaniRosellaSaitta2022.maximal_iff_weakMaximalCompat {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {s : S} (hR : Truthmaker.PossibleFusion excl) (hs : s ∈ Truthmaker.possible excl) : Maximal (fun (x : S) => x ∈ Truthmaker.possible excl) s ↔ WeakMaximalCompat excl s

Under Possible Fusion, a possible state is maximal with respect to parthood exactly when it is weakly maximal with respect to compatibility (Claim 5).

Maximality with respect to parthood without compatibility

def PlebaniRosellaSaitta2022.counterExcl (a b : Set (Fin 2)) : Prop

The exact incompatibility of the paper's counterexample on the subsets of {0, 1}, under which only {1} is incompatible, and only with itself.

Equations

• PlebaniRosellaSaitta2022.counterExcl a b = (a = {1} ∧ b = {1})

instance PlebaniRosellaSaitta2022.instSymmSetFinOfNatNatCounterExcl : Std.Symm counterExcl

theorem PlebaniRosellaSaitta2022.conflict_counterExcl_iff {a b : Set (Fin 2)} : Truthmaker.Conflict counterExcl a b ↔ 1 ∈ a ∧ 1 ∈ b

theorem PlebaniRosellaSaitta2022.maximal_counterExcl : Maximal (fun (x : Set (Fin 2)) => x ∈ Truthmaker.possible counterExcl) {0}

In the counterexample {0} is maximal with respect to parthood.

theorem PlebaniRosellaSaitta2022.not_maximalCompat_counterExcl : ¬MaximalCompat counterExcl {0}

In the counterexample {0} is not maximal with respect to compatibility, since {1} is compatible with it without being part of it.

Formulas

inductive PlebaniRosellaSaitta2022.Formula (A : Type u_3) : Type u_3

The formulas of a propositional language over atoms A.

• atom {A : Type u_3} (a : A) : Formula A
• neg {A : Type u_3} (φ : Formula A) : Formula A
• conj {A : Type u_3} (φ ψ : Formula A) : Formula A
• disj {A : Type u_3} (φ ψ : Formula A) : Formula A

def PlebaniRosellaSaitta2022.denote {S : Type u_1} {A : Type u_2} [CompleteLattice S] (excl : S → S → Prop) (V : A → Set S) : Formula A → Truthmaker.BilProp S

The bilateral proposition a formula expresses when V assigns verifiers to the atoms. An atom is falsified by the states exactly incompatible with all its verifiers, and the connectives follow Fine's bilateral clauses (def. 8).

Equations

• PlebaniRosellaSaitta2022.denote excl V (PlebaniRosellaSaitta2022.Formula.atom a) = { ver := V a, fal := {s : S | ∀ t ∈ V a, excl s t} }
• PlebaniRosellaSaitta2022.denote excl V φ.neg = -PlebaniRosellaSaitta2022.denote excl V φ
• PlebaniRosellaSaitta2022.denote excl V (φ.conj ψ) = (PlebaniRosellaSaitta2022.denote excl V φ).conj (PlebaniRosellaSaitta2022.denote excl V ψ)
• PlebaniRosellaSaitta2022.denote excl V (φ.disj ψ) = (PlebaniRosellaSaitta2022.denote excl V φ).disj (PlebaniRosellaSaitta2022.denote excl V ψ)

theorem PlebaniRosellaSaitta2022.conflict_of_mem_ver_of_mem_fal {S : Type u_1} {A : Type u_2} [CompleteLattice S] {excl : S → S → Prop} {s t : S} [Std.Symm excl] (V : A → Set S) (φ : Formula A) (hs : s ∈ (denote excl V φ).ver) (ht : t ∈ (denote excl V φ).fal) : Truthmaker.Conflict excl s t

Every verifier of a formula is inexactly incompatible with every falsifier of it (Theorem 1).

theorem PlebaniRosellaSaitta2022.not_mem_possible_of_mem_ver_conj_neg {S : Type u_1} {A : Type u_2} [CompleteLattice S] {excl : S → S → Prop} {s : S} [Std.Symm excl] (V : A → Set S) (φ : Formula A) (hs : s ∈ (denote excl V (φ.conj φ.neg)).ver) : s ∉ Truthmaker.possible excl

No possible state verifies a contradiction (Corollary 1).