Theories as Consequence Fixed Points

Abstract

Deductively closed sets are precisely the fixed points of consequence closure, whose fixed points form a complete lattice under intersections.

Theorem 1.1 (Theories are exactly consequence fixed points).

$$\begin{array}{c}\forall Formula:\mathrm{Type},\\ Cn:\mathrm{ConsequenceOperator}\left(Formula\right),S:\mathrm{Set}\left(Formula\right),\\ \mathrm{IsTheory}\left(Cn,S\right)⟺S\in \mathrm{fixedPoints}\left(Cn\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint.theory_iff_consequence_fixedPoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

A theory contains every consequence generated from itself. Since a closure operator is extensive, the reverse inclusion already holds, so deductive closure is equivalent to equality with the consequence closure.

Thus the theories of an arbitrary Tarskian consequence operator are exactly its fixed points. The statement uses only the closure laws and imposes no finiteness condition on formulas or theories.

Lemma 1.2 (Consequence closure is a fixed point).

$$\begin{array}{c}\forall Formula:\mathrm{Type},\\ Cn:\mathrm{ConsequenceOperator}\left(Formula\right),S:\mathrm{Set}\left(Formula\right),\\ \mathrm{Cn}\left(S\right)\in \mathrm{fixedPoints}\left(Cn\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint.consequenceClosure_is_fixedPoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

Closing any set of formulas produces a deductively closed set. Applying the same consequence operator again changes nothing, by the idempotence law for closure operators.

Lemma 1.3 (Consequence closure is least above its generators).

$$\begin{array}{c}\forall Formula:\mathrm{Type},\\ Cn:\mathrm{ConsequenceOperator}\left(Formula\right),S:\mathrm{Set}\left(Formula\right),\\ \mathrm{IsLeast}\left(\{T:\mathrm{Set}\left(Formula\right)\mid S\subseteq T\wedge T\in \mathrm{fixedPoints}\left(Cn\right)\},\mathrm{Cn}\left(S\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint.consequenceClosure_isLeast_fixedPoint_above (✓ std3). ∎

Source. Repository-derived.

Commentary.

The closure of a generating set contains every generator and is itself a fixed point. If another fixed point contains the generators, closure minimality places the generated closure inside it.

Consequently the deductive closure is the least closed theory extending the chosen assumptions, not merely one closed extension among many.

Lemma 1.4 (Fixed points are closed under arbitrary intersections).

$$\begin{array}{c}\forall Formula:\mathrm{Type},\\ Cn:\mathrm{ConsequenceOperator}\left(Formula\right),families:\mathrm{Set}\left(\mathrm{Set}\left(Formula\right)\right),\\ (\forall T,T\in families,T\in \mathrm{fixedPoints}\left(Cn\right))\Rightarrow \\ \mathrm{sInf}\left(families\right)\in \mathrm{fixedPoints}\left(Cn\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint.fixedPoints_closed_under_sInf (✓ std3). ∎

Source. Repository-derived.

Commentary.

The intersection of any family of consequence fixed points is again a fixed point. No nonemptiness assumption is needed: closed sets of a closure operator are preserved by arbitrary infima.

Together with the inherited order, this intersection law supplies the meet structure behind the complete lattice of theories.

References

• Truth anchor: D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint.consequenceClosure_isLeast_fixedPoint_above
• Truth anchor: D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint.consequenceClosure_is_fixedPoint
• Truth anchor: D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint.fixedPoints_closed_under_sInf
• Truth anchor: D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint.theory_iff_consequence_fixedPoint