Champollion and Bernard (2024): Negation and modality in unilateral truthmaker semantics

Champollion and Bernard give a unilateral truthmaker semantics in which negation comes from a primitive exclusion relation between events rather than from a second set of falsifiers. Two events conflict when a part of one excludes a part of the other (Truthmaker.Conflict), and an event is possible when it does not conflict with itself (Truthmaker.possible, Lemma 4.1), so possibility, which Fine takes as primitive, is derived. The worlds are the maximal possible events. Under the axioms of Harmony and Rashōmon, the latter Plebani, Rosella and Saitta's Possible Fusion, a world conflicts with every event it does not contain (conflict_of_not_le, Theorem 8.4). An event verifies the negation of φ when it fuses, for each verifier of φ, an event excluding a part of that verifier (neg). Every world then contains a verifier of exactly one of φ and its negation (mem_upperClosure_neg_iff, Theorems 9.2–9.4), so φ paired with its negation is exclusive and exhaustive in Fine's sense (exclusive_mk_neg, exhaustive_mk_neg).

The paper departs from Fine in admitting emergent exclusion, where an event excludes the fusion of two events without conflicting with either. Such an event verifies ¬(P ∧ Q) but not ¬P ∨ ¬Q (mem_neg_sups_diff), as the third egg's being in a basket with room for two does (eggs_mem_neg_sups_diff). The two sides of de Morgan's law still hold at the same worlds (mem_upperClosure_neg_sups_iff). Emergent exclusion is exactly the failure of a state that conflicts with a fusion to conflict with one of its members (Truthmaker.forall_exists_conflict_iff). Fine's Downward Exclusion rules it out (Truthmaker.DownwardExclusion.exists_conflict), and under it his negation obeys the law exactly (Truthmaker.exclusionaryNeg_iSups). Under Fine's Upward Exclusion the paper's negation is contained in Fine's exclusive negation (neg_subset_exclusiveNeg), Rashōmon is Fine's second condition on classical exclusion (possibleFusion_iff_exists_le_excl), and the paper's axioms make exclusion classical (classicalExclusion_possible). Cumulativity of exclusion adds the further verifiers of ¬(P ∧ Q) that Ciardelli, Zhang and Champollion's counterfactual data call for (neg_sups_neg_subset). In the canonical frame a literal excludes its mirror image. There the derived possibility is Fine's consistency (Truthmaker.Canonical.possible_excl), negation recovers Fine's falsifiers (neg_ver_atom, neg_ver_conj_atom), and the axioms hold.

Implementation notes

The paper takes events to form a complete distributive lattice. No proof here uses distributivity. Symmetry of exclusion is needed only for Plenitude, which the paper states with the event before the world while Harmony puts the world first. The paper's paraphrase of Fine's third condition on classical exclusion speaks of a possible state where Fine has an impossible one. Occurrence (Theorems 8.1–8.2), the definitions of necessity, and the results about a formula language (Theorems 9.8–9.9) are not formalized.

References

• L. Champollion and T. Bernard, Negation and modality in unilateral truthmaker semantics (2024)
• K. Fine, A Theory of Truthmaker Content I: Conjunction, Disjunction and Negation (2017)
• M. Plebani, G. Rosella and V. Saitta, Truthmakers, Incompatibility, and Modality (2022)
• I. Ciardelli, L. Zhang and L. Champollion, Two switches in the theory of counterfactuals: A study of truth conditionality and minimal change (2018)

Worlds and the axioms on exclusion

def ChampollionBernard2024.Cosmopolitan {E : Type u_1} [CompleteLattice E] (excl : E → E → Prop) : Prop

Cosmopolitanism (axiom 19), Fine's W-space condition, holds when every possible event is part of a world, a maximal possible event.

Equations

• ChampollionBernard2024.Cosmopolitan excl = ∀ e ∈ Truthmaker.possible excl, ∃ (w : E), e ≤ w ∧ Maximal (fun (x : E) => x ∈ Truthmaker.possible excl) w

def ChampollionBernard2024.Harmony {E : Type u_1} [CompleteLattice E] (excl : E → E → Prop) : Prop

Harmony (axiom 20) holds when every event that coheres with a world is possible.

Equations

• ChampollionBernard2024.Harmony excl = ∀ ⦃w e : E⦄, Maximal (fun (x : E) => x ∈ Truthmaker.possible excl) w → ¬Truthmaker.Conflict excl w e → e ∈ Truthmaker.possible excl

theorem ChampollionBernard2024.mem_possible_iff_exists_world {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} [Std.Symm excl] (hC : Cosmopolitan excl) (hH : Harmony excl) {e : E} : e ∈ Truthmaker.possible excl ↔ ∃ (w : E), ¬Truthmaker.Conflict excl e w ∧ Maximal (fun (x : E) => x ∈ Truthmaker.possible excl) w

An event is possible exactly when it coheres with some world (Theorem 8.3).

theorem ChampollionBernard2024.conflict_of_not_le {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hH : Harmony excl) (hR : Truthmaker.PossibleFusion excl) {w e : E} (hw : Maximal (fun (x : E) => x ∈ Truthmaker.possible excl) w) (he : ¬e ≤ w) : Truthmaker.Conflict excl w e

A world conflicts with every event it does not contain (Theorem 8.4).

Negation

def ChampollionBernard2024.neg {E : Type u_1} [CompleteLattice E] (excl : E → E → Prop) (φ : Set E) : Set E

An event verifies the negation of φ when it is the fusion of the values of a function sending each verifier of φ to an event that excludes some part of it (defs. 28–29).

Equations

• ChampollionBernard2024.neg excl φ = {e : E | ∃ (h : E → E), (∀ f ∈ φ, ∃ g ≤ f, excl (h f) g) ∧ sSup (h '' φ) = e}

theorem ChampollionBernard2024.neg_singleton {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (f : E) : neg excl {f} = {e : E | ∃ g ≤ f, excl e g}

The negation of a proposition with a single verifier f is verified by the events that exclude a part of f.

theorem ChampollionBernard2024.not_mem_upperClosure_neg {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} {φ : Set E} {s : E} (hs : s ∈ Truthmaker.possible excl) (hφ : s ∈ upperClosure φ) : s ∉ upperClosure (neg excl φ)

No possible event contains both a verifier of φ and a verifier of its negation. The paper states this for worlds (Theorem 9.4).

theorem ChampollionBernard2024.mem_upperClosure_or_neg {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hH : Harmony excl) (hR : Truthmaker.PossibleFusion excl) {w : E} (hw : Maximal (fun (x : E) => x ∈ Truthmaker.possible excl) w) (φ : Set E) : w ∈ upperClosure φ ∨ w ∈ upperClosure (neg excl φ)

Every world contains a verifier of φ or a verifier of its negation (Theorem 9.3).

theorem ChampollionBernard2024.mem_upperClosure_neg_iff {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hH : Harmony excl) (hR : Truthmaker.PossibleFusion excl) {w : E} (hw : Maximal (fun (x : E) => x ∈ Truthmaker.possible excl) w) {φ : Set E} : w ∈ upperClosure (neg excl φ) ↔ w ∉ upperClosure φ

A world contains a verifier of the negation of φ exactly when it contains no verifier of φ (Theorem 9.2).

theorem ChampollionBernard2024.exclusive_mk_neg {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (φ : Set E) : Truthmaker.BilProp.Exclusive (Truthmaker.possible excl) { ver := φ, fal := neg excl φ }

A proposition paired with its negation is exclusive over the possible events.

theorem ChampollionBernard2024.exhaustive_mk_neg {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hC : Cosmopolitan excl) (hH : Harmony excl) (hR : Truthmaker.PossibleFusion excl) (φ : Set E) : Truthmaker.BilProp.Exhaustive (Truthmaker.possible excl) { ver := φ, fal := neg excl φ }

A proposition paired with its negation is exhaustive over the possible events.

Emergent exclusion and de Morgan's law

theorem ChampollionBernard2024.not_mem_regularClosure_excluders {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} {P : Set E} {s : E} (hc : ∀ p ∈ P, ¬Truthmaker.Conflict excl s p) : s ∉ Truthmaker.regularClosure {r : E | ∃ p ∈ P, excl r p}

An event that coheres with every member of P is not an individual excluder of P, one in the regular closure of the excluders of its members, so if it excludes the fusion of P it is an emergent excluder (defs. 11–13).

theorem ChampollionBernard2024.mem_neg_sups_diff {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} {p q s : E} (hs : excl s (p ⊔ q)) (hp : ¬Truthmaker.Conflict excl s p) (hq : ¬Truthmaker.Conflict excl s q) : s ∈ neg excl ({p} ⊻ {q}) \ (neg excl {p} ∪ neg excl {q})

An event that excludes p ⊔ q while cohering with p and with q verifies ¬(P ∧ Q) but not ¬P ∨ ¬Q, where P is verified by p alone and Q by q alone (§7).

theorem ChampollionBernard2024.mem_upperClosure_neg_sups_iff {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hH : Harmony excl) (hR : Truthmaker.PossibleFusion excl) {w : E} (hw : Maximal (fun (x : E) => x ∈ Truthmaker.possible excl) w) (φ ψ : Set E) : w ∈ upperClosure (neg excl (φ ⊻ ψ)) ↔ w ∈ upperClosure (neg excl φ ∪ neg excl ψ)

The two sides of de Morgan's law ¬(φ ∧ ψ) ⇔ ¬φ ∨ ¬ψ hold at the same worlds (§9).

theorem ChampollionBernard2024.neg_sups_neg_subset {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hCum : ∀ ⦃e e' f f' : E⦄, excl e e' → excl f f' → excl (e ⊔ f) (e' ⊔ f')) (p q : E) : neg excl {p} ⊻ neg excl {q} ⊆ neg excl ({p} ⊻ {q})

If exclusion is cumulative, the fusion of a verifier of ¬P with a verifier of ¬Q verifies ¬(P ∧ Q), for P verified by p alone and Q by q alone (§8, fn. 27).

Comparison with Fine's unilateral semantics

theorem ChampollionBernard2024.neg_subset_exclusiveNeg {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hU : Truthmaker.UpwardExclusion excl) (φ : Set E) : neg excl φ ⊆ Truthmaker.exclusiveNeg excl φ

Under Upward Exclusion, every verifier of the paper's negation of φ verifies Fine's exclusive negation of φ.

theorem ChampollionBernard2024.possibleFusion_iff_exists_le_excl {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hU : Truthmaker.UpwardExclusion excl) : Truthmaker.PossibleFusion excl ↔ ∀ ⦃s t : E⦄, s ∈ Truthmaker.possible excl → t ∈ Truthmaker.possible excl → s ⊔ t ∉ Truthmaker.possible excl → ∃ s' ≤ s, excl s' t

Under Upward Exclusion, Rashōmon is Fine's second condition on classical exclusion over the derived possibility, that two possible events with an impossible fusion have a part of the first that excludes the second (fn. 21).

theorem ChampollionBernard2024.classicalExclusion_possible {E : Type u_1} [CompleteLattice E] {excl : E → E → Prop} (hU : Truthmaker.UpwardExclusion excl) (hC : Cosmopolitan excl) (hH : Harmony excl) (hR : Truthmaker.PossibleFusion excl) : Truthmaker.ClassicalExclusion excl (Truthmaker.possible excl)

Under Upward Exclusion, the paper's axioms make exclusion classical in Fine's sense over the derived possibility.

The basket with room for two eggs

def ChampollionBernard2024.eggsExcl (s t : Set (Fin 3)) : Prop

In a basket with room for two of the eggs 0, 1 and 2, the event of egg i's being in the basket excludes the event of the other two eggs' being in it, and conversely (§6).

Equations

• ChampollionBernard2024.eggsExcl s t = ∃ (i : Fin 3), s = {i} ∧ t = {i}ᶜ ∨ s = {i}ᶜ ∧ t = {i}

theorem ChampollionBernard2024.not_conflict_eggsExcl (i j : Fin 3) : ¬Truthmaker.Conflict eggsExcl {i} {j}

No egg's being in the basket conflicts with another's.

theorem ChampollionBernard2024.eggs_mem_neg_sups_diff : {2} ∈ neg eggsExcl ({{0}} ⊻ {{1}}) \ (neg eggsExcl {{0}} ∪ neg eggsExcl {{1}})

The third egg's being in the basket verifies egg 1 and egg 2 are not both in the basket but not either egg 1 or egg 2 is not in the basket (§7).

The canonical frame

theorem ChampollionBernard2024.neg_ver_atom {α : Type u_2} (a : α) : neg Truthmaker.Canonical.excl (Truthmaker.Canonical.atom a).ver = (Truthmaker.Canonical.atom a).fal

In the canonical frame the negation of an atom is verified by its denial alone, the atom's falsifier in Fine's bilateral semantics.

theorem ChampollionBernard2024.neg_ver_conj_atom {α : Type u_2} (a b : α) : neg Truthmaker.Canonical.excl ((Truthmaker.Canonical.atom a).conj (Truthmaker.Canonical.atom b)).ver = ((Truthmaker.Canonical.atom a).conj (Truthmaker.Canonical.atom b)).fal

In the canonical frame the negation of a conjunction of two atoms is verified exactly by the denial of either atom, its falsifiers in Fine's bilateral semantics, so de Morgan's law holds exactly there (§9).

theorem ChampollionBernard2024.harmony_canonicalExcl {α : Type u_2} : Harmony Truthmaker.Canonical.excl

theorem ChampollionBernard2024.cosmopolitan_canonicalExcl {α : Type u_2} : Cosmopolitan Truthmaker.Canonical.excl

theorem ChampollionBernard2024.mk_neg_ver_atom {α : Type u_2} (a : α) : { ver := (Truthmaker.Canonical.atom a).ver, fal := neg Truthmaker.Canonical.excl (Truthmaker.Canonical.atom a).ver } = Truthmaker.Canonical.atom a

Fine's bilateral atom is the unilateral atom paired with its negation.