Closure Conditions on Truthmaker Propositions @cite{jago-2026}

Jago Def 4: A truthmaker proposition (a set of states P : Set S) may satisfy three closure conditions:

• Closed (P^⊔): closed under nonempty fusion — if Q ⊆ P is nonempty, then ⊔Q ∈ P.
• Convex (P^∼): convex under parthood — if s, u ∈ P and s ≤ t ≤ u, then t ∈ P.
• Regular (P^*): both closed and convex.

Closures are not redefined here — they are imported from Core/Mereology.lean:

• Mereology.AlgClosure P is P^⊔ (Jago: closed under fusion).
• Mereology.algClosureOp : ClosureOperator (α → Prop) bundles it.
• Mereology.convexClosure P is P^∼ (Jago: convex under parthood).
• Mereology.convexClosureOp : ClosureOperator (Set α) bundles it.
• Mereology.IsConvex is the convex predicate.
• The regular closure P^* is convexClosure (AlgClosure P).

This file provides the truthmaker-flavored vocabulary (IsClosed, IsRegular, regularClose) and the bridges to mathlib's ClosureOperator.IsClosed API.

CAVEAT: IsClosed here is the finitary version (closed under binary fusion via AlgClosure's inductive definition). Jago's encyclopedia text is "closed under nonempty fusion" of arbitrary subsets. Over a SemilatticeSup with no infinitary sSup, these coincide on finite witnesses; for infinitary closure use LowerSet-style packaging.

@[reducible, inline]

abbrev Semantics.Truthmaker.IsClosed {S : Type u_1} [SemilatticeSup S] (p : TMProp S) : Prop

A proposition is closed under (finite, nonempty) fusion iff it is fixed by AlgClosure — equivalently CUM. Truthmaker-flavored alias for Mereology.CUM.

Equations

• Semantics.Truthmaker.IsClosed p = Mereology.CUM p

theorem Semantics.Truthmaker.isClosed_algClosure {S : Type u_1} [SemilatticeSup S] (p : TMProp S) : IsClosed (Mereology.AlgClosure p)

The closed closure p^⊔ = AlgClosure p is itself closed. Re-export of Mereology.algClosure_cum.

@[reducible, inline]

abbrev Semantics.Truthmaker.IsConvex {S : Type u_1} [PartialOrder S] (p : TMProp S) : Prop

A proposition is convex iff it lies between any two of its members in the partial order. Re-export of Mereology.IsConvex.

Equations

• Semantics.Truthmaker.IsConvex p = Mereology.IsConvex p

@[reducible, inline]

abbrev Semantics.Truthmaker.convexClose {S : Type u_1} [PartialOrder S] (p : TMProp S) : TMProp S

Convex closure of a TMProp. Re-export of Mereology.convexClosure (recall Set α = α → Prop = TMProp α definitionally).

Equations

• Semantics.Truthmaker.convexClose p = Mereology.convexClosure p

theorem Semantics.Truthmaker.isConvex_convexClose {S : Type u_1} [PartialOrder S] (p : TMProp S) : IsConvex (convexClose p)

The convex closure of p is convex. Re-export of Mereology.IsConvex.convexClosure.

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

A proposition is regular iff both closed (under fusion) and convex (under parthood) — @cite{jago-2026} Def 4. Prop-shape via ∧ for mathlib uniformity.

Equations

• Semantics.Truthmaker.IsRegular p = (Semantics.Truthmaker.IsClosed p ∧ Semantics.Truthmaker.IsConvex p)

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

Regular closure: convexify the algebraic closure. regularClose p = (p^⊔)^∼ — composition of the two closure operators of Core/Mereology.lean.

Equations

• Semantics.Truthmaker.regularClose p = Semantics.Truthmaker.convexClose (Mereology.AlgClosure p)

theorem Semantics.Truthmaker.subset_regularClose {S : Type u_1} [SemilatticeSup S] (p : TMProp S) {s : S} (h : p s) : regularClose p s

p ⊆ p^*: regular closure extends the original.

theorem Semantics.Truthmaker.isConvex_regularClose {S : Type u_1} [SemilatticeSup S] (p : TMProp S) : IsConvex (regularClose p)

The regular closure is convex.