Truthmaker content

This file defines conjunctive parthood, the containment relation of Kit Fine's theory of truthmaker content. States are ordered by parthood, with fusion as join, and a unilateral proposition is the set of states that exactly verify it, so a proposition over states S is a Set S. Conjunction is the pointwise fusion s ⊻ t, disjunction is the union s ∪ t, and Fine's entailment of t by s is the inclusion s ⊆ t.

A state inexactly verifies s when some part of it exactly verifies s, that is, when it lies in upperClosure s. Inexact verification obeys the classical clauses: upperClosure_sups and upperClosure_union say that the inexact verifiers of s ⊻ t and s ∪ t are the common and the pooled inexact verifiers of s and t.

Main definitions

• Truthmaker.IsConjunctivePart t s: every verifier of s contains a verifier of t, and every verifier of t is part of a verifier of s.
• Truthmaker.regularClosure: the closure operator sending s to the states that contain a verifier of s and are part of the fusion of its verifiers. Its closed sets are Fine's regular propositions, and the regular closure of s ∪ t is his disjunction in a regular domain.

Main results

• Truthmaker.isConjunctivePart_iff: conjunctive parthood compares upper and lower closures.
• Truthmaker.IsConjunctivePart.antisymm: conjunctive parthood is antisymmetric on convex propositions.
• Truthmaker.isConjunctivePart_singleton_right_iff: parts of a single state are its parts.
• Truthmaker.isConjunctivePart_sups_left: a conjunct is a conjunctive part of a conjunction.
• Truthmaker.isConjunctivePart_union_left_iff: s contains s ∨ t only when every verifier of t is part of a verifier of s, so disjunction introduction fails for containment.
• Truthmaker.isConjunctivePart_iff_sups_eq: a closed convex proposition contains t exactly when conjoining t leaves it unchanged.
• Truthmaker.isClosed_regularClosure_iff: the regular propositions are those closed under nonempty fusions and convex.
• Truthmaker.isConjunctivePart_regularClosure_iff: regular closure does not change containment.
• Truthmaker.regularClosure_eq_iff: a regular proposition is determined by its inexact verifiers and its subject-matter.
• Truthmaker.regularClosure_sups, Truthmaker.regularClosure_iSups: in a distributive space, regular closure distributes over conjunction.
• Truthmaker.regularClosure_union_sups: disjunction distributes over conjunction in a regular domain.

Implementation notes

Fine defines conjunctive parthood only between propositions with a verifier. The relation here is total, and the empty proposition is a conjunctive part only of itself. Fine's closure condition asks for closure under arbitrary nonempty fusions, which isClosed_regularClosure_iff states and of which SupClosed is the finitary version. Fine states the distribution of regular closure over conjunction, and the distribution of disjunction over conjunction, for regular propositions, but his proofs apply them to unions and to sets of excluders that need not be regular. They are stated here for arbitrary nonempty propositions. His distributivity assumption is mathlib's Order.Frame.

References

• K. Fine, A Theory of Truthmaker Content I: Conjunction, Disjunction and Negation (2017)
• K. Fine, Truthmaker Semantics (2017)
• M. Jago, Truthmaker Semantics (2026)

def Truthmaker.IsConjunctivePart {S : Type u_1} [Preorder S] (t s : Set S) : Prop

A proposition t is a conjunctive part of s, or s contains t, if every verifier of s contains a verifier of t and every verifier of t is part of a verifier of s.

Equations

• Truthmaker.IsConjunctivePart t s = (s ⊆ ↑(upperClosure t) ∧ t ⊆ ↑(lowerClosure s))

theorem Truthmaker.isConjunctivePart_iff {S : Type u_1} [Preorder S] {s t : Set S} : IsConjunctivePart t s ↔ upperClosure t ≤ upperClosure s ∧ lowerClosure t ≤ lowerClosure s

Conjunctive parthood asks that every inexact verifier of s inexactly verify t, and that every state below a verifier of t lie below a verifier of s.

theorem Truthmaker.IsConjunctivePart.refl {S : Type u_1} [Preorder S] (s : Set S) : IsConjunctivePart s s

theorem Truthmaker.IsConjunctivePart.rfl {S : Type u_1} [Preorder S] {s : Set S} : IsConjunctivePart s s

theorem Truthmaker.IsConjunctivePart.trans {S : Type u_1} [Preorder S] {s t u : Set S} (hut : IsConjunctivePart u t) (hts : IsConjunctivePart t s) : IsConjunctivePart u s

theorem Truthmaker.IsConjunctivePart.antisymm {S : Type u_1} [Preorder S] {s t : Set S} (hs : s.OrdConnected) (ht : t.OrdConnected) (hts : IsConjunctivePart t s) (hst : IsConjunctivePart s t) : s = t

Two convex propositions that are conjunctive parts of each other are equal.

theorem Truthmaker.isConjunctivePart_singleton_right_iff {S : Type u_1} [Preorder S] {t : Set S} (ht : t.Nonempty) {a : S} : IsConjunctivePart t {a} ↔ ∀ b ∈ t, b ≤ a

A proposition with a verifier is a conjunctive part of the proposition verified by a alone exactly when each of its verifiers is part of a.

theorem Truthmaker.isConjunctivePart_singleton_left_iff {S : Type u_1} [Preorder S] {s : Set S} (hs : s.Nonempty) {b : S} : IsConjunctivePart {b} s ↔ ∀ a ∈ s, b ≤ a

The proposition verified by b alone is a conjunctive part of a proposition with a verifier exactly when b is part of each of its verifiers.

@[simp]

theorem Truthmaker.isConjunctivePart_singleton_singleton {S : Type u_1} [Preorder S] {a b : S} : IsConjunctivePart {b} {a} ↔ b ≤ a

theorem Truthmaker.isConjunctivePart_union_left_iff {S : Type u_1} [Preorder S] {s t : Set S} : IsConjunctivePart (s ∪ t) s ↔ t ⊆ ↑(lowerClosure s)

A proposition s contains the disjunction s ∪ t exactly when every verifier of t is part of a verifier of s.

theorem Truthmaker.isConjunctivePart_sups_left {S : Type u_1} [SemilatticeSup S] {s t : Set S} (ht : t.Nonempty) : IsConjunctivePart s (s ⊻ t)

A conjunct is a conjunctive part of a conjunction whose other conjunct has a verifier.

theorem Truthmaker.isConjunctivePart_sups_right {S : Type u_1} [SemilatticeSup S] {s t : Set S} (hs : s.Nonempty) : IsConjunctivePart t (s ⊻ t)

A conjunct is a conjunctive part of a conjunction whose other conjunct has a verifier.

theorem Truthmaker.IsConjunctivePart.sups {S : Type u_1} [SemilatticeSup S] {s t u : Set S} (hu : SupClosed u) (hs : IsConjunctivePart s u) (ht : IsConjunctivePart t u) : IsConjunctivePart (s ⊻ t) u

A sup-closed proposition that contains s and t contains their conjunction.

theorem Truthmaker.isConjunctivePart_iff_sups_eq {S : Type u_1} [SemilatticeSup S] {s t : Set S} (hs : s.Nonempty) (hsc : SupClosed s) (hso : s.OrdConnected) : IsConjunctivePart t s ↔ s ⊻ t = s

A closed, convex proposition s with a verifier contains t exactly when s ⊻ t = s.

theorem Truthmaker.IsConjunctivePart.sSup_le {S : Type u_1} [CompleteLattice S] {s t : Set S} (h : IsConjunctivePart t s) : sSup t ≤ sSup s

A conjunctive part of s has a subject-matter that is part of the subject-matter of s.

theorem Truthmaker.isConjunctivePart_iff_sSup_le {S : Type u_1} [CompleteLattice S] {s t : Set S} (hs : sSup s ∈ s) : IsConjunctivePart t s ↔ s ⊆ ↑(upperClosure t) ∧ sSup t ≤ sSup s

If s contains the fusion of its verifiers, s contains t exactly when every verifier of s contains a verifier of t and the subject-matter of t is part of that of s.

def Truthmaker.regularClosure {S : Type u_1} [CompleteLattice S] : ClosureOperator (Set S)

The regular closure of a proposition s consists of the states that contain a verifier of s and are part of the fusion of its verifiers. It is unrelated to the regular closure of possibility semantics.

Equations

• Truthmaker.regularClosure = ClosureOperator.mk' (fun (s : Set S) => ↑(upperClosure s) ∩ Set.Iic (sSup s)) ⋯ ⋯ ⋯

theorem Truthmaker.mem_regularClosure {S : Type u_1} [CompleteLattice S] {s : Set S} {x : S} : x ∈ regularClosure s ↔ (∃ a ∈ s, a ≤ x) ∧ x ≤ sSup s

@[simp]

theorem Truthmaker.regularClosure_empty {S : Type u_1} [CompleteLattice S] : regularClosure ∅ = ∅

@[simp]

theorem Truthmaker.regularClosure_singleton {S : Type u_1} [CompleteLattice S] (a : S) : regularClosure {a} = {a}

theorem Truthmaker.sSup_mem_regularClosure {S : Type u_1} [CompleteLattice S] {s : Set S} (hs : s.Nonempty) : sSup s ∈ regularClosure s

@[simp]

theorem Truthmaker.sSup_regularClosure {S : Type u_1} [CompleteLattice S] (s : Set S) : sSup (regularClosure s) = sSup s

@[simp]

theorem Truthmaker.upperClosure_regularClosure {S : Type u_1} [CompleteLattice S] (s : Set S) : upperClosure (regularClosure s) = upperClosure s

theorem Truthmaker.regularClosure_eq_iff {S : Type u_1} [CompleteLattice S] {s t : Set S} : regularClosure s = regularClosure t ↔ upperClosure s = upperClosure t ∧ (s.Nonempty → sSup s = sSup t)

Two propositions have the same regular closure exactly when they have the same inexact verifiers and, if they have verifiers, the same subject-matter.

theorem Truthmaker.isClosed_regularClosure_iff {S : Type u_1} [CompleteLattice S] {s : Set S} : regularClosure.IsClosed s ↔ (∀ t ⊆ s, t.Nonempty → sSup t ∈ s) ∧ s.OrdConnected

The regular propositions, the closed sets of regularClosure, are those closed under nonempty fusions and convex.

theorem Truthmaker.isClosed_regularClosure_iff' {S : Type u_1} [CompleteLattice S] {s : Set S} : regularClosure.IsClosed s ↔ s.OrdConnected ∧ (s.Nonempty → sSup s ∈ s)

A proposition is regular exactly when it is convex and contains the fusion of its verifiers, if it has any.

theorem Truthmaker.supClosed_of_isClosed_regularClosure {S : Type u_1} [CompleteLattice S] {s : Set S} (hs : regularClosure.IsClosed s) : SupClosed s

theorem Truthmaker.ordConnected_of_isClosed_regularClosure {S : Type u_1} [CompleteLattice S] {s : Set S} (hs : regularClosure.IsClosed s) : s.OrdConnected

theorem Truthmaker.IsConjunctivePart.regularClosure {S : Type u_1} [CompleteLattice S] {s t : Set S} (h : IsConjunctivePart t s) : IsConjunctivePart (Truthmaker.regularClosure t) (Truthmaker.regularClosure s)

Regular closure preserves containment.

theorem Truthmaker.isConjunctivePart_regularClosure_iff {S : Type u_1} [CompleteLattice S] {s t : Set S} (hs : sSup s ∈ s) : IsConjunctivePart (regularClosure t) (regularClosure s) ↔ IsConjunctivePart t s

If s contains the fusion of its verifiers, the regular closure of s contains that of t exactly when s contains t.

theorem Truthmaker.regularClosure_sups {S : Type u_1} [Order.Frame S] {s t : Set S} (hs : s.Nonempty) (ht : t.Nonempty) : regularClosure (s ⊻ t) = regularClosure s ⊻ regularClosure t

In a distributive space, regular closure distributes over the conjunction of propositions with verifiers.

theorem Truthmaker.regularClosure_iSups {S : Type u_1} [Order.Frame S] {ι : Type u_2} {s : ι → Set S} (hs : ∀ (i : ι), (s i).Nonempty) : regularClosure (Set.iSups s) = Set.iSups fun (i : ι) => regularClosure (s i)

In a distributive space, regular closure distributes over the conjunction of a family of propositions with verifiers.

theorem Truthmaker.isClosed_regularClosure_sups {S : Type u_1} [Order.Frame S] {s t : Set S} (hs : regularClosure.IsClosed s) (ht : regularClosure.IsClosed t) : regularClosure.IsClosed (s ⊻ t)

In a distributive space, the conjunction of regular propositions is regular.

theorem Truthmaker.regularClosure_sups_union {S : Type u_1} [Order.Frame S] {s t u : Set S} (hs : s.Nonempty) (htu : (t ∪ u).Nonempty) : regularClosure s ⊻ regularClosure (t ∪ u) = regularClosure (s ⊻ t ∪ s ⊻ u)

Conjunction distributes over disjunction in a regular domain.

theorem Truthmaker.regularClosure_union_sups {S : Type u_1} [Order.Frame S] {s t u : Set S} (ht : t.Nonempty) (hu : u.Nonempty) : regularClosure (s ∪ t ⊻ u) = regularClosure (s ∪ t) ⊻ regularClosure (s ∪ u)

Disjunction distributes over conjunction in a regular domain.