Exclusion

This file defines exclusion between states and what it determines in unilateral truthmaker semantics. Given an exclusion relation, two states conflict when a part of one excludes a part of the other, and a state is possible when it does not conflict with itself. Plebani, Rosella and Saitta, and independently Champollion and Bernard, derive possibility in this way, while Fine takes the possible states as given. Fine constrains exclusion by three conditions and negates a proposition P by fusing states that together exclude its verifiers. This gives the exclusive negation −P, and its regular closure, the exclusionary negation ∼P.

Main definitions

• Truthmaker.Conflict excl s t: some part of s excludes some part of t.
• Truthmaker.possible excl: the states that do not conflict with themselves.
• Truthmaker.PossibleFusion excl: two possible states that do not conflict have a possible fusion.
• Truthmaker.UpwardExclusion, Truthmaker.DownwardExclusion, Truthmaker.NullExclusion: Fine's conditions on exclusion.
• Truthmaker.Excludes excl Q P: every verifier of Q excludes a verifier of P, and every verifier of P is excluded by a verifier of Q.
• Truthmaker.exclusiveNeg, Truthmaker.exclusionaryNeg: Fine's negations −P and ∼P.
• Truthmaker.ClassicalExclusion excl P: Fine's classical exclusion over the possible states P.

Main results

• Truthmaker.isConjunctivePart_iff_excludes: containment is exclusion with parthood in place of exclusion.
• Truthmaker.mem_possible_iff_forall: a state is possible exactly when no two of its parts conflict.
• Truthmaker.coe_upperClosure_exclusionaryNeg: under Upward Exclusion, the states containing a verifier of ∼P are those that conflict with every verifier of P, the polar of P under conflict.
• Truthmaker.sSup_exclusiveNeg: the subject-matter of −P is the fusion of the excluders of verifiers of P.
• Truthmaker.forall_exists_conflict_iff: the half of Downward Exclusion that rules out emergent exclusion says that a state conflicting with a fusion conflicts with one of its members.
• Truthmaker.exclusionaryNeg_singleton: the negation of a single state is the regular closure of its excluders.
• Truthmaker.exclusionaryNeg_regularClosure: negation does not see regular closure.
• Truthmaker.exclusionaryNeg_regularClosure_iUnion, Truthmaker.exclusionaryNeg_iSups: the de Morgan laws for the exclusionary negation.
• Truthmaker.exclusionaryNeg_exclusionaryNeg: double negation holds of every regular proposition if it holds of every single state.
• Truthmaker.ClassicalExclusion.exclusive, Truthmaker.ClassicalExclusion.exhaustive: under classical exclusion a single state paired with its negation is exclusive and exhaustive.
• Truthmaker.Canonical.possible_excl: in the canonical space, where a literal excludes its mirror image, the derived possibility is Fine's consistency.
• Truthmaker.RedBlueGreen.exclusionaryNeg_exclusionaryNeg_ne: double negation can fail.

Implementation notes

Fine's published Downward Exclusion condition omits the regular closure of the excluders, which Champollion and Bernard report as a typo. It is stated here with the closure. The de Morgan laws are proved by computing the inexact verifiers and the subject-matter of each side, which determine a regular proposition (Truthmaker.regularClosure_eq_iff). Fine states that negation does not see regular closure for regular propositions only and his de Morgan laws for regular ones, but they hold without regularity. The law for conjunctions needs no distributivity, only that the conjuncts have verifiers and that the null state verifies none of them.

References

• 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)
• L. Champollion and T. Bernard, Negation and modality in unilateral truthmaker semantics (2024)

def Truthmaker.Excludes {S : Type u_1} (excl : S → S → Prop) (Q P : Set S) : Prop

A proposition Q excludes P when every verifier of Q excludes a verifier of P and every verifier of P is excluded by a verifier of Q.

Equations

• Truthmaker.Excludes excl Q P = (Q ⊆ {q : S | ∃ p ∈ P, excl q p} ∧ P ⊆ {p : S | ∃ q ∈ Q, excl q p})

Conflict and possibility

theorem Truthmaker.isConjunctivePart_iff_excludes {S : Type u_1} [Preorder S] {s t : Set S} : IsConjunctivePart t s ↔ Excludes (fun (x1 x2 : S) => x1 ≥ x2) s t

A proposition s contains t exactly when s excludes t in the sense of Excludes, with containment of states in place of exclusion.

def Truthmaker.Conflict {S : Type u_1} [Preorder S] (excl : S → S → Prop) (s t : S) : Prop

Two states conflict when some part of the first excludes some part of the second.

Equations

• Truthmaker.Conflict excl s t = ∃ s' ≤ s, ∃ t' ≤ t, excl s' t'

theorem Truthmaker.Conflict.of_excl {S : Type u_1} [Preorder S] {excl : S → S → Prop} {s t : S} (h : excl s t) : Conflict excl s t

theorem Truthmaker.Conflict.mono {S : Type u_1} [Preorder S] {excl : S → S → Prop} {s t s' t' : S} (h : Conflict excl s t) (hs : s ≤ s') (ht : t ≤ t') : Conflict excl s' t'

theorem Truthmaker.Conflict.symm {S : Type u_1} [Preorder S] {excl : S → S → Prop} {s t : S} [Std.Symm excl] (h : Conflict excl s t) : Conflict excl t s

def Truthmaker.possible {S : Type u_1} [Preorder S] (excl : S → S → Prop) : LowerSet S

A state is possible when it does not conflict with itself, and every part of a possible state is possible.

Equations

• Truthmaker.possible excl = { carrier := {s : S | ¬Truthmaker.Conflict excl s s}, lower' := ⋯ }

theorem Truthmaker.mem_possible {S : Type u_1} [Preorder S] {excl : S → S → Prop} {s : S} : s ∈ possible excl ↔ ¬Conflict excl s s

theorem Truthmaker.mem_possible_iff_forall {S : Type u_1} [Preorder S] {excl : S → S → Prop} {s : S} : s ∈ possible excl ↔ ∀ t ≤ s, ∀ u ≤ s, ¬Conflict excl t u

A state is possible exactly when no two of its parts conflict.

def Truthmaker.UpwardExclusion {S : Type u_1} [Preorder S] (excl : S → S → Prop) : Prop

Upward Exclusion holds when a state that excludes p excludes every state containing p.

Equations

• Truthmaker.UpwardExclusion excl = ∀ ⦃q p p' : S⦄, excl q p → p ≤ p' → excl q p'

theorem Truthmaker.UpwardExclusion.conflict_iff {S : Type u_1} [Preorder S] {excl : S → S → Prop} {s t : S} (hU : UpwardExclusion excl) : Conflict excl s t ↔ ∃ s' ≤ s, excl s' t

Under Upward Exclusion, a state conflicts with t exactly when some part of it excludes t.

theorem Truthmaker.sup_not_mem_possible {S : Type u_1} [SemilatticeSup S] {excl : S → S → Prop} {s t : S} (h : excl s t) : s ⊔ t ∉ possible excl

Two states one of which excludes the other have an impossible fusion.

theorem Truthmaker.not_conflict_of_sup_mem_possible {S : Type u_1} [SemilatticeSup S] {excl : S → S → Prop} {s t : S} (h : s ⊔ t ∈ possible excl) : ¬Conflict excl s t

Two states with a possible fusion do not conflict.

def Truthmaker.PossibleFusion {S : Type u_1} [SemilatticeSup S] (excl : S → S → Prop) : Prop

Possible Fusion holds when two possible states that do not conflict have a possible fusion.

Equations

• Truthmaker.PossibleFusion excl = ∀ ⦃s : S⦄, s ∈ Truthmaker.possible excl → ∀ ⦃t : S⦄, t ∈ Truthmaker.possible excl → ¬Truthmaker.Conflict excl s t → s ⊔ t ∈ Truthmaker.possible excl

theorem Truthmaker.possibleFusion_iff {S : Type u_1} [SemilatticeSup S] {excl : S → S → Prop} : PossibleFusion excl ↔ ∀ s ∈ possible excl, ∀ t ∈ possible excl, s ⊔ t ∈ possible excl ↔ ¬Conflict excl s t

Possible Fusion holds exactly when two possible states have a possible fusion just when they do not conflict.

Fine's exclusion conditions and negations

def Truthmaker.DownwardExclusion {S : Type u_1} [CompleteLattice S] (excl : S → S → Prop) : Prop

Downward Exclusion holds when every state that excludes the fusion of P lies in the regular closure of the excluders of members of P.

Equations

• Truthmaker.DownwardExclusion excl = ∀ ⦃P : Set S⦄ ⦃q : S⦄, excl q (sSup P) → q ∈ Truthmaker.regularClosure {r : S | ∃ p ∈ P, excl r p}

def Truthmaker.NullExclusion {S : Type u_1} [CompleteLattice S] (excl : S → S → Prop) : Prop

Null Exclusion holds when the null state neither excludes nor is excluded, and every other state excludes some state and is excluded by some state.

Equations

• Truthmaker.NullExclusion excl = ((∀ (s : S), ¬excl ⊥ s ∧ ¬excl s ⊥) ∧ ∀ (s : S), s ≠ ⊥ → (∃ (t : S), excl s t) ∧ ∃ (t : S), excl t s)

def Truthmaker.exclusiveNeg {S : Type u_1} [CompleteLattice S] (excl : S → S → Prop) (P : Set S) : Set S

The exclusive negation of P is verified by the fusions of propositions that exclude P.

Equations

• Truthmaker.exclusiveNeg excl P = {q : S | ∃ (Q : Set S), Truthmaker.Excludes excl Q P ∧ sSup Q = q}

def Truthmaker.exclusionaryNeg {S : Type u_1} [CompleteLattice S] (excl : S → S → Prop) (P : Set S) : Set S

The exclusionary negation of P is the regular closure of its exclusive negation.

Equations

• Truthmaker.exclusionaryNeg excl P = Truthmaker.regularClosure (Truthmaker.exclusiveNeg excl P)

theorem Truthmaker.sSup_image_mem_exclusiveNeg {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} {f : S → S} (hf : ∀ p ∈ P, excl (f p) p) : sSup (f '' P) ∈ exclusiveNeg excl P

The fusion of a choice of an excluder for each verifier of P verifies the exclusive negation of P.

theorem Truthmaker.exclusiveNeg_nonempty_iff {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} : (exclusiveNeg excl P).Nonempty ↔ ∀ p ∈ P, ∃ (r : S), excl r p

A proposition has an exclusive negation with a verifier exactly when every verifier of it has an excluder.

theorem Truthmaker.exclusiveNeg_nonempty {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} (hN : NullExclusion excl) (hP : ⊥ ∉ P) : (exclusiveNeg excl P).Nonempty

Under Null Exclusion, a proposition that the null state does not verify has an exclusive negation with a verifier.

@[simp]

theorem Truthmaker.exclusiveNeg_empty {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} : exclusiveNeg excl ∅ = {⊥}

theorem Truthmaker.mem_upperClosure_exclusiveNeg {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} {x : S} : x ∈ upperClosure (exclusiveNeg excl P) ↔ ∀ p ∈ P, ∃ r ≤ x, excl r p

A state contains a verifier of the exclusive negation of P exactly when, for every verifier of P, it has a part that excludes it.

theorem Truthmaker.coe_upperClosure_exclusiveNeg {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} (hU : UpwardExclusion excl) (P : Set S) : ↑(upperClosure (exclusiveNeg excl P)) = upperPolar (flip (Conflict excl)) P

Under Upward Exclusion, the states containing a verifier of the exclusive negation of P are those that conflict with every verifier of P, the polar of P under conflict.

theorem Truthmaker.coe_upperClosure_exclusionaryNeg {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} (hU : UpwardExclusion excl) (P : Set S) : ↑(upperClosure (exclusionaryNeg excl P)) = upperPolar (flip (Conflict excl)) P

Under Upward Exclusion, the states containing a verifier of the exclusionary negation of P are those that conflict with every verifier of P.

theorem Truthmaker.sSup_exclusiveNeg {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} (h : ∀ p ∈ P, ∃ (r : S), excl r p) : sSup (exclusiveNeg excl P) = sSup {r : S | ∃ p ∈ P, excl r p}

If every verifier of P has an excluder, the subject-matter of the exclusive negation of P is the fusion of all excluders of verifiers of P.

theorem Truthmaker.exclusiveNeg_iUnion {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {ι : Type u_2} (P : ι → Set S) : exclusiveNeg excl (⋃ (i : ι), P i) = Set.iSups fun (i : ι) => exclusiveNeg excl (P i)

The exclusive negation of a disjunction is the conjunction of the exclusive negations of the disjuncts.

theorem Truthmaker.exclusionaryNeg_singleton {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} (p : S) : exclusionaryNeg excl {p} = regularClosure {q : S | excl q p}

The exclusionary negation of a single state is the regular closure of its excluders.

theorem Truthmaker.exclusionaryNeg_sups_singleton {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} (hU : UpwardExclusion excl) (hD : DownwardExclusion excl) (p q : S) : exclusionaryNeg excl ({p} ⊻ {q}) = regularClosure (exclusionaryNeg excl {p} ∪ exclusionaryNeg excl {q})

Under Upward and Downward Exclusion, the exclusionary negation of the conjunction of two single states is the disjunction of their exclusionary negations.

theorem Truthmaker.exclusionaryNeg_nonempty {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} (hN : NullExclusion excl) (hP : ⊥ ∉ P) : (exclusionaryNeg excl P).Nonempty

Under Null Exclusion, a proposition that the null state does not verify has a negation with a verifier.

theorem Truthmaker.bot_not_mem_exclusionaryNeg {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} (hN : NullExclusion excl) (hP : P.Nonempty) : ⊥ ∉ exclusionaryNeg excl P

Under Null Exclusion, the null state does not verify the negation of a proposition with a verifier.

theorem Truthmaker.DownwardExclusion.exists_conflict {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} (hD : DownwardExclusion excl) {s : S} (hs : excl s (sSup P)) : ∃ p ∈ P, Conflict excl s p

Under Downward Exclusion, a state that excludes the fusion of P conflicts with a member of P.

theorem Truthmaker.exists_conflict_of_conflict_sSup {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : Set S} (hU : UpwardExclusion excl) (hD : DownwardExclusion excl) {x : S} (h : Conflict excl x (sSup P)) : ∃ p ∈ P, Conflict excl x p

Under Upward and Downward Exclusion, a state that conflicts with the fusion of P conflicts with a member of P.

theorem Truthmaker.forall_exists_conflict_iff {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} (hU : UpwardExclusion excl) : (∀ ⦃x : S⦄ ⦃P : Set S⦄, Conflict excl x (sSup P) → ∃ p ∈ P, Conflict excl x p) ↔ ∀ ⦃q : S⦄ ⦃P : Set S⦄, excl q (sSup P) → q ∈ upperClosure {r : S | ∃ p ∈ P, excl r p}

Under Upward Exclusion, a state that conflicts with a fusion always conflicts with one of its members exactly when every state that excludes a fusion has a part that excludes one of its members, the half of Downward Exclusion that rules out emergent exclusion.

theorem Truthmaker.exclusionaryNeg_regularClosure {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} (hU : UpwardExclusion excl) (hD : DownwardExclusion excl) (P : Set S) : exclusionaryNeg excl (regularClosure P) = exclusionaryNeg excl P

Under Upward and Downward Exclusion, the exclusionary negation of a proposition is that of its regular closure.

theorem Truthmaker.exclusionaryNeg_iSups {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {ι : Type u_2} (hU : UpwardExclusion excl) (hD : DownwardExclusion excl) (hN : NullExclusion excl) {P : ι → Set S} (hne : ∀ (i : ι), (P i).Nonempty) (hP : ∀ (i : ι), ⊥ ∉ P i) : exclusionaryNeg excl (Set.iSups P) = regularClosure (⋃ (i : ι), exclusionaryNeg excl (P i))

Under Upward, Downward and Null Exclusion, the exclusionary negation of the conjunction of a family of propositions with verifiers, none verified by the null state, is the disjunction of their exclusionary negations.

Classical exclusion

structure Truthmaker.ClassicalExclusion {S : Type u_1} [CompleteLattice S] (excl : S → S → Prop) (P : LowerSet S) : Prop

An exclusion relation is classical over the possible states P when a state is incompatible with the states it excludes, two incompatible possible states have a part of the first that excludes the second, and every possible state is compatible with an excluder of each impossible state.

• sup_not_mem ⦃s t : S⦄ : excl s t → s ⊔ t ∉ P

  A state and a state it excludes have an impossible fusion.

• exists_le_excl ⦃s t : S⦄ : s ∈ P → t ∈ P → s ⊔ t ∉ P → ∃ s' ≤ s, excl s' t

  Two possible states with an impossible fusion have a part of the first that excludes the second.

• exists_excl ⦃t : S⦄ : t ∉ P → ∀ s ∈ P, ∃ (t' : S), excl t' t ∧ s ⊔ t' ∈ P

  Every possible state has a possible fusion with some excluder of each impossible state.

theorem Truthmaker.ClassicalExclusion.exclusive {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : LowerSet S} (h : ClassicalExclusion excl P) (p : S) : BilProp.Exclusive P { ver := {p}, fal := exclusionaryNeg excl {p} }

Under classical exclusion, a single state paired with its exclusionary negation is exclusive.

theorem Truthmaker.ClassicalExclusion.exhaustive {S : Type u_1} [CompleteLattice S] {excl : S → S → Prop} {P : LowerSet S} (h : ClassicalExclusion excl P) (p : S) : BilProp.Exhaustive P { ver := {p}, fal := exclusionaryNeg excl {p} }

Under classical exclusion, a single state paired with its exclusionary negation is exhaustive.

theorem Truthmaker.exclusionaryNeg_regularClosure_iUnion {S : Type u_1} [Order.Frame S] {excl : S → S → Prop} {ι : Type u_2} (hU : UpwardExclusion excl) (hD : DownwardExclusion excl) (hN : NullExclusion excl) {P : ι → Set S} (hP : ∀ (i : ι), ⊥ ∉ P i) : exclusionaryNeg excl (regularClosure (⋃ (i : ι), P i)) = Set.iSups fun (i : ι) => exclusionaryNeg excl (P i)

In a distributive space, under Upward, Downward and Null Exclusion, the exclusionary negation of the disjunction of a family of propositions not verified by the null state is the conjunction of their exclusionary negations.

theorem Truthmaker.exclusionaryNeg_exclusionaryNeg {S : Type u_1} [Order.Frame S] {excl : S → S → Prop} (hU : UpwardExclusion excl) (hD : DownwardExclusion excl) (hN : NullExclusion excl) (h : ∀ (p : S), exclusionaryNeg excl (exclusionaryNeg excl {p}) = {p}) {P : Set S} (hP : regularClosure.IsClosed P) (hP' : ⊥ ∉ P) : exclusionaryNeg excl (exclusionaryNeg excl P) = P

In a distributive space, under Upward, Downward and Null Exclusion, if double exclusionary negation restores every single state, it restores every regular proposition that the null state does not verify.

The canonical space

def Truthmaker.Canonical.excl {α : Type u_2} (s t : Set (α × Bool)) : Prop

In the canonical space a literal excludes its mirror image and nothing else holds.

Equations

• Truthmaker.Canonical.excl s t = ∃ (x : α × Bool), s = {x} ∧ t = {Truthmaker.Canonical.mirror x}

instance Truthmaker.Canonical.instSymmSetProdBoolExcl {α : Type u_2} : Std.Symm excl

theorem Truthmaker.Canonical.conflict_excl_iff {α : Type u_2} {s t : Set (α × Bool)} : Conflict excl s t ↔ ∃ x ∈ s, mirror x ∈ t

theorem Truthmaker.Canonical.possible_excl {α : Type u_2} : Truthmaker.possible excl = possible

The states possible under canonical exclusion are the consistent sets of literals.

theorem Truthmaker.Canonical.possibleFusion_excl {α : Type u_2} : PossibleFusion excl

Red, blue and green

def Truthmaker.RedBlueGreen.excl (s t : Set (Fin 3)) : Prop

In Fine's example of three colours, red 0, blue 1 and green 2, a single colour excludes every state containing another colour.

Equations

• Truthmaker.RedBlueGreen.excl s t = ∃ (i : Fin 3), s = {i} ∧ ∃ j ∈ t, j ≠ i

theorem Truthmaker.RedBlueGreen.exclusionaryNeg_exclusionaryNeg_ne : exclusionaryNeg excl (exclusionaryNeg excl {{0}}) ≠ {{0}}

The exclusionary negation of the exclusionary negation of red is not red.