Truthmaker Semantics @cite{fine-2017} @cite{bondarenko-elliott-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).

Part I: Unilateral Propositions (§§1–6)

The first part formalizes the unilateral fragment needed by @cite{bondarenko-elliott-2026}: propositions as sets of verifiers, conjunction via fusion, content parthood, and attitude distribution.

Part II: Bilateral Propositions (§§7–13)

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 key structural insight is 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: q is a content part of p when every verifier of p has a part that verifies q. This is strictly weaker than entailment.

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 of A. Two sentences can be logically equivalent but differ in subject-matter.

@[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.tmAnd {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) : TMProp S

Conjunction via fusion (Bondarenko & Elliott §3.1). s verifies p ∧ q iff s = s₁ ⊔ s₂ for some s₁ verifying p and s₂ verifying q. This is 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₂

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. This is set-theoretic — no mereological structure.

Equations

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

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

Content parthood (Bondarenko & Elliott Def 3). q is a content part of p iff every verifier of p has a part (≤) that verifies q. This is strictly weaker than entailment: p entails q requires every world satisfying p to satisfy q, while content parthood only requires every verifier of p to have a part verifying q.

Equations

• Semantics.Truthmaker.contentPart q p = ∀ (s : S), p s → ∃ (t : S), q t ∧ t ≤ s

theorem Semantics.Truthmaker.contentPart_refl {S : Type u_1} [Preorder S] (p : TMProp S) : contentPart p p

Content parthood is reflexive: p is a content part of itself.

theorem Semantics.Truthmaker.contentPart_trans {S : Type u_1} [Preorder S] (p q r : TMProp S) (hpq : contentPart p q) (hqr : contentPart q r) : contentPart p r

Content parthood is transitive.

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

p is a content part of p ∧ q. Proof: if s verifies p ∧ q, then s = s₁ ⊔ s₂ with p s₁. Since s₁ ≤ s₁ ⊔ s₂ = s (by le_sup_left), s₁ is a part of s that verifies p.

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

q is a content part of p ∧ q. Symmetric to contentPart_and_left, using le_sup_right.

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. attHolds σ p x iff ∃ s ≤ σ(x) such that p(s).

Equations

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

theorem Semantics.Truthmaker.mono_att_distrib_and {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

Upward-monotone attitudes distribute over conjunction (forward direction). If the agent's state verifies p ∧ q, then it verifies both p and q.

Proof: p ∧ q is verified by s₁ ⊔ s₂ where p(s₁) and q(s₂). Since s₁ ≤ s₁ ⊔ s₂ ≤ σ(x) and s₂ ≤ s₁ ⊔ s₂ ≤ σ(x), we have attHolds for both p and q.

theorem Semantics.Truthmaker.mono_att_distrib_and_conv {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

Conjunction distribution (converse direction). If the agent's state has parts verifying both p and q, then their fusion verifies p ∧ q and is also a part of σ(x).

This requires sup_le: s₁ ≤ σ(x) ∧ s₂ ≤ σ(x) → s₁ ⊔ s₂ ≤ σ(x).

theorem Semantics.Truthmaker.mono_att_distrib_and_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 iff for upward-monotone attitudes. Combines the forward and converse directions.

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

Disjunction does NOT generally satisfy content parthood.

In truthmaker semantics, p ∨ q is verified by any verifier of p or any verifier of q (set union). But a verifier of p ∨ q that verifies only p need not have a part verifying q. So q is not generally a content part of p ∨ q.

We state this as: there exist types and propositions where contentPart q (tmOr p q) fails.

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

A bilateral proposition: separate sets of verifiers and falsifiers.

Fine (2017 §5): "A model M for the bilateral case will be a triple (S, ⊑, |·|) in which |p| for each atom p is now a pair (V, F) of a verification set V and a falsification set F."

The unilateral TMProp is recovered by BilProp.ver.

• 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-only) part. This recovers the TMProp from Part I.

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 by leaving falsifiers empty. (No state falsifies the proposition — appropriate for atoms in contexts where falsification isn't tracked.)

Equations

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

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

Negation: swap verifiers and falsifiers (@cite{fine-2017} §5). s verifies ¬A iff s falsifies A; s falsifies ¬A iff s verifies A.

Equations

• Semantics.Truthmaker.bilNot p = { ver := p.fal, fal := p.ver }

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

Conjunction: verified by fusion, falsified by union (@cite{fine-2017} §5).

• s verifies A ∧ B iff s = s₁ ⊔ s₂ where s₁ verifies A and s₂ verifies B
• s falsifies A ∧ B iff s falsifies A or s falsifies B

Defined in terms of tmAnd/tmOr — the duality is explicit: conjunction fuses verifiers but unions falsifiers.

Equations

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

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

Disjunction: verified by union, falsified by fusion (@cite{fine-2017} §5).

• s verifies A ∨ B iff s verifies A or s verifies B
• s falsifies A ∨ B iff s = s₁ ⊔ s₂ where s₁ falsifies A and s₂ falsifies B

Exact dual of bilAnd: disjunction unions verifiers but fuses falsifiers.

Equations

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

theorem Semantics.Truthmaker.bilNot_involutive {S : Type u_1} (p : BilProp S) : bilNot (bilNot p) = p

Double negation is the identity. Definitionally true: swapping verifiers and falsifiers twice returns to the original.

theorem Semantics.Truthmaker.deMorgan_and {S : Type u_1} [SemilatticeSup S] (p q : BilProp S) : bilNot (bilAnd p q) = bilOr (bilNot p) (bilNot q)

De Morgan: ¬(A ∧ B) has the same verifiers and falsifiers as ¬A ∨ ¬B.

• Verifiers of ¬(A ∧ B) = falsifiers of A ∧ B = {s | A.fal s ∨ B.fal s}

• Verifiers of ¬A ∨ ¬B = {s | (¬A).ver s ∨ (¬B).ver s} = {s | A.fal s ∨ B.fal s}

• Falsifiers of ¬(A ∧ B) = verifiers of A ∧ B = {s | ∃ s₁ s₂,...}

• Falsifiers of ¬A ∨ ¬B = {s | ∃ s₁ s₂, (¬A).fal s₁ ∧ (¬B).fal s₂ ∧...} = {s | ∃ s₁ s₂, A.ver s₁ ∧ B.ver s₂ ∧...}

theorem Semantics.Truthmaker.deMorgan_or {S : Type u_1} [SemilatticeSup S] (p q : BilProp S) : bilNot (bilOr p q) = bilAnd (bilNot p) (bilNot q)

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

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

A possibility predicate distinguishes possible from impossible states within a state space. Fine (2017 §4): "(S, S⁰, ⊑) where S⁰ ⊆ S is the set of possible states and is required to be closed under Part (if s ∈ S⁰ and t ⊑ s then t ∈ S⁰)."

We represent this as a predicate satisfying downward closure.

• possible : S → Prop

  Which states are possible

• downClosed (s t : S) : self.possible s → t ≤ s → self.possible t

  Possible states are closed under parts (downward closed). If s is possible and t ≤ s, then t is possible.

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} §4). 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 = P.possible (s ⊔ t)

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

Compatibility is symmetric.

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

Exclusivity (@cite{fine-2017} §5): no verifier is compatible with a falsifier. If s verifies A and t falsifies A, then s ⊔ t is impossible.

This is 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} §5): every possible state is compatible with a verifier or a falsifier.

This is the other direction of bivalence: no possible state is undecided — it must be compatible with evidence for or against A.

Equations

• One or more equations did not get rendered due to their size.

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

Negation preserves exclusivity: if A is exclusive, so is ¬A. (Swap verifiers/falsifiers — the incompatibility is symmetric.)

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

Negation preserves exhaustivity: if A is exhaustive, so is ¬A.

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

Subject-matter of a proposition: the fusion of all its verifiers (@cite{fine-2017} §II.2). Two sentences can be logically equivalent (true at the same worlds) but differ in subject-matter.

Equations

• Semantics.Truthmaker.subjectMatter A = sSup {s : S | A.ver s}

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

A proposition is about another if its subject-matter is part of the other's. This gives a 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

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

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

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

Proof sketch: if s verifies A ∧ B, then s = s₁ ⊔ s₂ with s₁ verifying A and s₂ verifying B. If t falsifies A ∧ B, then t falsifies A or t falsifies B. Either way, the fusion includes a verifier-falsifier pair for the same atomic proposition, which is impossible by exclusivity of A or B plus downward closure of possibility.