Truthmaker Semantics @cite{fine-2017} @cite{bondarenko-elliott-2026} @cite{jago-2026}

State-based propositions grounded in Core/Mereology.lean. Propositions are sets of verifying states, where states form a join-semilattice (the same SemilatticeSup infrastructure used for events and plural individuals).

Files in this directory

• Basic.lean (this file) — unilateral and bilateral propositions, fusion-based connectives, content parthood (Down/Up/full), bilateral pairs with exclusivity/exhaustivity, subject-matter.
• Inexact.lean — inexact truthmaking and exact/inexact entailment.
• Closure.lean — closed/convex/regular closure operators (Jago Def 4), built on Mereology.AlgClosure and Mereology.convexClosure.
• Entailment.lean — analytic entailment (AC), FDE-style consequence, bridges.

Part I: Unilateral propositions

The first part formalizes the unilateral fragment needed by @cite{bondarenko-elliott-2026}: propositions as sets of verifiers, conjunction via fusion, content parthood (Down clause), and attitude distribution. Both halves of Jago's conjunctive parthood are exposed (IsSubsumedBy, Subserves, IsContentPart).

Part II: Bilateral propositions

The second part formalizes Fine's full bilateral conception: propositions as pairs (V, F) of verifier and falsifier sets, with negation as the swap operation. The duality between conjunction and disjunction at the verification/falsification level:

Connective	Verified by	Falsified by
A ∧ B	fusion (⊔)	union (∨)
A ∨ B	union (∨)	fusion (⊔)
¬A	falsifiers	verifiers

Key ideas

1. Conjunction via fusion: p ∧ q is verified by the fusion s₁ ⊔ s₂ of verifiers of p and q (not by set intersection). This makes conjunction mereologically structured.

2. Disjunction via union: p ∨ q is verified by any verifier of either p or q. This is purely set-theoretic — no mereological structure.

3. Content parthood (Jago Def 5): q is a content part of p when both the Down clause holds (every verifier of p has a part verifying q) AND the Up clause holds (every verifier of q is part of some verifier of p). The Down-only relation IsSubsumedBy is the relation @cite{bondarenko-elliott-2026} use for monotonicity arguments.

4. Bilateral propositions: Propositions are (V, F) pairs. Negation swaps them; conjunction fuses verifiers but unions falsifiers; disjunction unions verifiers but fuses falsifiers.

5. Exclusivity/Exhaustivity: No verifier is compatible with a falsifier (exclusivity); every possible state is compatible with a verifier or falsifier (exhaustivity).

6. Subject-matter: σ(A) = the fusion of all verifiers and falsifiers of A. Two sentences can be logically equivalent but differ in subject-matter; crucially, σ(¬A) = σ(A) (negation invariance).

Citation discipline

• The encyclopedia survey @cite{jago-2026} is the entry point; specific technical claims trace back to Fine's two-part Truthmaker Content series (which are in Journal of Philosophical Logic 46(6), not the Wiley Companion chapter fine-2017). Section/page numbers internal to those papers are flagged UNVERIFIED until checked against PDFs.
• @cite{bondarenko-elliott-2026} definitions/theorem numbers are flagged UNVERIFIED since the manuscript has not been cross-checked.

@[reducible, inline]

abbrev Semantics.Truthmaker.TMProp (S : Type u_1) : Type u_1

A truthmaker proposition: a set of verifying states. A state s verifies p iff p s holds.

Equations

• Semantics.Truthmaker.TMProp S = (S → Prop)

def Semantics.Truthmaker.tmOr {S : Type u_1} (p q : TMProp S) : TMProp S

Disjunction via union. s verifies p ∨ q iff s verifies p or s verifies q. Set-theoretic — no mereological structure.

Equations

• Semantics.Truthmaker.tmOr p q s = (p s ∨ q s)

def Semantics.Truthmaker.tmAnd {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) : TMProp S

Conjunction via fusion (@cite{fine-2017}; @cite{bondarenko-elliott-2026}). s verifies p ∧ q iff s = s₁ ⊔ s₂ for some s₁ verifying p and s₂ verifying q. The key departure from classical conjunction (set intersection).

Equations

• Semantics.Truthmaker.tmAnd p q s = ∃ (s₁ : S) (s₂ : S), p s₁ ∧ q s₂ ∧ s = s₁ ⊔ s₂

@[reducible, inline]

abbrev Semantics.Truthmaker.IsSubsumedBy {S : Type u_1} [Preorder S] (q p : TMProp S) : Prop

Down clause of conjunctive parthood (@cite{jago-2026} Def 5; @cite{bondarenko-elliott-2026} content parthood): every verifier of p has a part verifying q.

Re-export of Mereology.IsSubsumedBy — the Down clause is a generic poset relation, not truthmaker-specific.

The Down-only relation suffices for @cite{bondarenko-elliott-2026}'s monotonicity arguments.

Equations

• Semantics.Truthmaker.IsSubsumedBy q p = Mereology.IsSubsumedBy q p

@[reducible, inline]

abbrev Semantics.Truthmaker.Subserves {S : Type u_1} [Preorder S] (q p : TMProp S) : Prop

Up clause of conjunctive parthood (@cite{jago-2026} Def 5): every verifier of q is part of some verifier of p.

Re-export of Mereology.Subserves. The Up clause is more delicate: Subserves p (tmAnd p q) requires q to be inhabited (you need a witness to fuse with) — a deliberate departure from the Fine convention that propositions are nonempty.

Equations

• Semantics.Truthmaker.Subserves q p = Mereology.Subserves q p

@[reducible, inline]

abbrev Semantics.Truthmaker.IsContentPart {S : Type u_1} [Preorder S] (q p : TMProp S) : Prop

Full conjunctive parthood (@cite{jago-2026} Def 5): q is a content part of p iff both the Down and Up clauses hold.

Re-export of Mereology.IsContentPart. Written q ≤ p in Jago's notation.

Equations

• Semantics.Truthmaker.IsContentPart q p = Mereology.IsContentPart q p

theorem Semantics.Truthmaker.IsSubsumedBy.tmAnd_left {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) : IsSubsumedBy p (tmAnd p q)

p is subsumed by p ∧ q (Down clause). If s verifies p ∧ q, then s = s₁ ⊔ s₂ with p s₁, so s₁ ≤ s is the required part.

theorem Semantics.Truthmaker.IsSubsumedBy.tmAnd_right {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) : IsSubsumedBy q (tmAnd p q)

q is subsumed by p ∧ q (symmetric to tmAnd_left).

theorem Semantics.Truthmaker.Subserves.tmAnd_left {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) (hq : ∃ (s : S), q s) : Subserves p (tmAnd p q)

p subserves p ∧ q provided q is inhabited (Up clause). Take any s verifying p; pick a witness s₂ verifying q; then s ⊔ s₂ verifies p ∧ q and s ≤ s ⊔ s₂.

theorem Semantics.Truthmaker.Subserves.tmAnd_right {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) (hp : ∃ (s : S), p s) : Subserves q (tmAnd p q)

q subserves p ∧ q provided p is inhabited.

theorem Semantics.Truthmaker.IsContentPart.tmAnd_left {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) (hq : ∃ (s : S), q s) : IsContentPart p (tmAnd p q)

p is a content part of p ∧ q whenever q is inhabited (full Jago Def 5).

theorem Semantics.Truthmaker.IsContentPart.tmAnd_right {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) (hp : ∃ (s : S), p s) : IsContentPart q (tmAnd p q)

q is a content part of p ∧ q whenever p is inhabited.

def Semantics.Truthmaker.attHolds {S : Type u_1} {E : Type u_2} [Preorder S] (σ : E → S) (p : TMProp S) (x : E) : Prop

An attitude holds when the agent's total information state has a verifier-part for the proposition. σ : E → S maps agents to their total information states.

Equations

• Semantics.Truthmaker.attHolds σ p x = ∃ (s : S), p s ∧ s ≤ σ x

theorem Semantics.Truthmaker.attHolds_tmAnd_imp {S : Type u_1} {E : Type u_2} [SemilatticeSup S] (σ : E → S) (p q : TMProp S) (x : E) (h : attHolds σ (tmAnd p q) x) : attHolds σ p x ∧ attHolds σ q x

Forward direction of conjunction distribution: if the agent's state verifies p ∧ q, then it verifies both p and q.

theorem Semantics.Truthmaker.attHolds_tmAnd_of {S : Type u_1} {E : Type u_2} [SemilatticeSup S] (σ : E → S) (p q : TMProp S) (x : E) (hp : attHolds σ p x) (hq : attHolds σ q x) : attHolds σ (tmAnd p q) x

Converse direction: if the agent's state has parts verifying both p and q, their fusion verifies p ∧ q and is also a part of σ x.

theorem Semantics.Truthmaker.attHolds_tmAnd_iff {S : Type u_1} {E : Type u_2} [SemilatticeSup S] (σ : E → S) (p q : TMProp S) (x : E) : attHolds σ (tmAnd p q) x ↔ attHolds σ p x ∧ attHolds σ q x

Full conjunction-distribution biconditional for upward-monotone attitudes (@cite{bondarenko-elliott-2026}, monotonicity-via-mereology theorem).

theorem Semantics.Truthmaker.isSubsumedBy_or_not_general : ¬∀ (S : Type) (x : SemilatticeSup S) (p q : TMProp S), IsSubsumedBy q (tmOr p q)

Disjunction does NOT generally satisfy content parthood. tmOr p q is verified by any verifier of p or q (set union). A verifier of p ∨ q that verifies only p need not have a part verifying q — so q is not generally subsumed by p ∨ q.

Concrete witness over Nat with p = (· = 0) and q = (· = 1).

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

A bilateral proposition: separate sets of verifiers and falsifiers.

Per @cite{fine-2017}, a bilateral model assigns each atom a pair (V, F) of a verification set V and a falsification set F. The unilateral TMProp is recovered by BilProp.toTM.

• ver : S → Prop

  States that verify (make true) the proposition.

• fal : S → Prop

  States that falsify (make false) the proposition.

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

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

def Semantics.Truthmaker.BilProp.toTM {S : Type u_1} (p : BilProp S) : TMProp S

Project a bilateral proposition to its unilateral (verifier) part.

Equations

• p.toTM = p.ver

def Semantics.Truthmaker.TMProp.toBil {S : Type u_1} (p : TMProp S) : BilProp S

Lift a unilateral proposition to bilateral with empty falsifier set. Appropriate for atoms in contexts where falsification isn't tracked.

Equations

• p.toBil = { ver := p, fal := fun (x : S) => False }

def Semantics.Truthmaker.BilProp.neg {S : Type u_1} (p : BilProp S) : BilProp S

Negation: swap verifiers and falsifiers (@cite{fine-2017}).

Equations

• p.neg = { ver := p.fal, fal := p.ver }

def Semantics.Truthmaker.BilProp.conj {S : Type u_1} [SemilatticeSup S] (p q : BilProp S) : BilProp S

Conjunction: verified by fusion, falsified by union. Defined via tmAnd / tmOr so the duality is structurally explicit: conjunction fuses verifiers but unions falsifiers.

Equations

• p.conj q = { ver := Semantics.Truthmaker.tmAnd p.ver q.ver, fal := Semantics.Truthmaker.tmOr p.fal q.fal }

def Semantics.Truthmaker.BilProp.disj {S : Type u_1} [SemilatticeSup S] (p q : BilProp S) : BilProp S

Disjunction: verified by union, falsified by fusion. Exact dual of conj.

Equations

• p.disj q = { ver := Semantics.Truthmaker.tmOr p.ver q.ver, fal := Semantics.Truthmaker.tmAnd p.fal q.fal }

@[simp]

theorem Semantics.Truthmaker.BilProp.neg_neg {S : Type u_1} (p : BilProp S) : p.neg.neg = p

Double negation is the identity (definitional).

theorem Semantics.Truthmaker.BilProp.neg_involutive {S : Type u_1} : Function.Involutive neg

Negation is involutive (mathlib-flavored restatement of neg_neg).

@[implicit_reducible]

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

BilProp S carries an InvolutiveNeg structure — the same mathlib abstraction satisfied by Theories/Semantics/Dynamic/Bilateral/Basic.lean's BilateralDen. The two bilateral frameworks (state-based truthmaker, update-based dynamic) are unified at the swap-pair level by being instances of InvolutiveNeg.

Equations

• Semantics.Truthmaker.BilProp.instInvolutiveNeg = { neg := Semantics.Truthmaker.BilProp.neg, neg_neg := ⋯ }

theorem Semantics.Truthmaker.BilProp.isBilateral {S : Type u_1} : Core.Logic.Bilateral.IsBilateral (fun (x : BilProp S) => x.ver) (fun (x : BilProp S) => x.fal) neg

Fine-style truthmaker BilProp is a paraconsistent bilateral logic (Core.Logic.Bilateral.IsBilateral). The BilProp value IS the formula; ver/fal are field projections; neg swaps them by definition. Both axioms reduce to rfl. Cross-references the InvolutiveNeg instance above and BilateralDen.isBilateral (BUS) — three frameworks share the substrate.

@[simp]

theorem Semantics.Truthmaker.BilProp.neg_conj {S : Type u_1} [SemilatticeSup S] (p q : BilProp S) : (p.conj q).neg = p.neg.disj q.neg

De Morgan: ¬(A ∧ B) = ¬A ∨ ¬B. Definitionally true once the duality of conj and disj (fusion vs. union) is unrolled.

@[simp]

theorem Semantics.Truthmaker.BilProp.neg_disj {S : Type u_1} [SemilatticeSup S] (p q : BilProp S) : (p.disj q).neg = p.neg.conj q.neg

De Morgan: ¬(A ∨ B) = ¬A ∧ ¬B.

@[reducible, inline]

abbrev Semantics.Truthmaker.Possibility (S : Type u_1) [Preorder S] : Type u_1

The set of possible states within a state space, packaged as a LowerSet S from mathlib: the carrier is a downward-closed set (P.lower : IsLowerSet ↑P), capturing Fine's requirement that any part of a possible state is itself possible.

Possibility S = LowerSet S is just an alias to make the truthmaker-semantic role visible.

Equations

• Semantics.Truthmaker.Possibility S = LowerSet S

def Semantics.Truthmaker.compatible {S : Type u_1} [SemilatticeSup S] (P : Possibility S) (s t : S) : Prop

Two states are compatible iff their fusion is possible (@cite{fine-2017}). Incompatible states represent conflicting information — e.g., a state verifying "it's cold" and a state verifying "it's hot" are incompatible because their fusion is impossible.

Equations

• Semantics.Truthmaker.compatible P s t = (s ⊔ t ∈ P)

theorem Semantics.Truthmaker.compatible_comm {S : Type u_1} [SemilatticeSup S] {P : Possibility S} (s t : S) : compatible P s t ↔ compatible P t s

Compatibility is symmetric.

instance Semantics.Truthmaker.compatible_isSymm {S : Type u_1} [SemilatticeSup S] (P : Possibility S) : Std.Symm (compatible P)

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

Exclusivity (@cite{fine-2017}): no verifier is compatible with a falsifier. One direction of bivalence: verification and falsification are mutually incompatible.

Equations

• Semantics.Truthmaker.Exclusive P A = ∀ (s t : S), A.ver s → A.fal t → ¬Semantics.Truthmaker.compatible P s t

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

Exhaustivity (@cite{fine-2017}): every possible state is compatible with a verifier or a falsifier. The other direction of bivalence: no possible state is undecided about A.

NOTE: this is the compatibility-based formulation in Fine 2017; a parthood-based variant ("every possible state is part of a verifier or falsifier") also appears in the literature and is related but not identical — added as ExhaustivePart if needed.

Equations

• Semantics.Truthmaker.Exhaustive P A = ∀ s ∈ P, (∃ (t : S), A.ver t ∧ Semantics.Truthmaker.compatible P s t) ∨ ∃ (t : S), A.fal t ∧ Semantics.Truthmaker.compatible P s t

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

Negation preserves exclusivity.

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

Negation preserves exhaustivity.

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

If A and B are both exclusive, then A ∧ B is exclusive.

Sketch: if s verifies A ∧ B then s = s₁ ⊔ s₂ with A.ver s₁, B.ver s₂. If t falsifies A ∧ B then t falsifies A or B. Either way, the down-closure of possibility under parts contradicts exclusivity of A (or B).

noncomputable def Semantics.Truthmaker.TMProp.subjectMatter {S : Type u_1} [SupSet S] (p : TMProp S) : S

Subject-matter of a unilateral proposition: the fusion of all its verifiers (@cite{jago-2026} p. 5; cf. @cite{fine-2017}'s Truthmaker Content series in JPL 46(6) for the original presentation).

Equations

• p.subjectMatter = sSup {s : S | p s}

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

Subject-matter of a bilateral proposition: the fusion of both verifiers and falsifiers (@cite{jago-2026} p. 5).

This is the formulation that makes subjectMatter invariant under negation — the headline structural property that distinguishes truthmaker subject-matter from naive verifier-only "thick content". See BilProp.subjectMatter_neg.

Equations

• A.subjectMatter = sSup ({s : S | A.ver s} ∪ {s : S | A.fal s})

@[simp]

theorem Semantics.Truthmaker.BilProp.subjectMatter_neg {S : Type u_1} [SupSet S] (A : BilProp S) : A.neg.subjectMatter = A.subjectMatter

Negation invariance of subject-matter (@cite{jago-2026} p. 5): σ(¬A) = σ(A). The headline structural property of bilateral subject-matter, falling out structurally because BilProp.neg swaps ver and fal and Set.union_comm does the rest.

def Semantics.Truthmaker.BilProp.isAbout {S : Type u_1} [SupSet S] [Preorder S] (A B : BilProp S) : Prop

"A is about B" iff A's subject-matter is a part of B's (@cite{jago-2026}). Mereological account of aboutness: "It's raining" is about the weather; "It's raining and 2+2=4" is about the weather AND arithmetic.

Equations

• A.isAbout B = (A.subjectMatter ≤ B.subjectMatter)

@[implicit_reducible]

instance Semantics.Truthmaker.instDecidableEqTwoAtom : DecidableEq Semantics.Truthmaker.TwoAtom✝

Equations

• Semantics.Truthmaker.instDecidableEqTwoAtom x✝ y✝ = if h : Semantics.Truthmaker.TwoAtom.ctorIdx✝ x✝ = Semantics.Truthmaker.TwoAtom.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

theorem Semantics.Truthmaker.subjectMatter_distinguishes_classically_equivalent : ∃ (A : BilProp (Set Semantics.Truthmaker.TwoAtom✝)) (B : BilProp (Set Semantics.Truthmaker.TwoAtom✝)), (∀ (s : Set Semantics.Truthmaker.TwoAtom✝), A.ver s ↔ B.ver s) ∧ A.subjectMatter ≠ B.subjectMatter

The load-bearing claim of the framework (@cite{jago-2026}, @cite{fine-2017}). Two bilateral propositions can be pointwise equivalent on verifiers (= classically equivalent at every world) yet have distinct subject-matters (= mereologically different content).

Witness over Set TwoAtom: A and B share the same verifier {a}, but differ in falsifier — A has none, B has {b}. A.subjectMatter = sSup ({{a}} ∪ ∅) = {a} while B.subjectMatter = sSup ({{a}} ∪ {{b}}) = {a, b}. The two are classically equivalent on verifiers but truthmaker-distinct in subject-matter — exactly the distinction PW semantics cannot make.