Proof-theoretic consistency over a Henkin-closed sentence set

The relational kernel adapter for syntactic Barwise completeness (issue #19B).

HenkinClosed P names the memberships a sentence set P ⊆ L[[ℕ]].Sentenceω must have for the family of P-bounded P-consistent sets to be a consistency property in the countable-completion kernel's sense. HenkinClosedMin P is the weaker interface the family constructor actually consumes — components, constant instances, the closed atoms, and only the kernel's negated targets rather than the negation of every member — and HenkinClosed.toMin derives it from the full closure. HenkinClosedMin.consistencyPropertyEqOn inhabits ConsistencyPropertyEqOn P from that family using only the rules of Derivable; exists_countable_model_of_aconsistent then runs the fair enumeration and the quotient term model. Both are re-exported in the HenkinClosed namespace with their published statements unchanged.

The closure is external syntactic saturation, not an admissibility notion: nothing here mentions an admissible set. Admissibility enters only when internalizing the construction and showing its codes remain inside the admissible language.

Why this engine

The kernel's ConsistencyPropertyEqOn has no extension and no chain_closure field. Both would be needed by a Zorn-style maximal-consistent construction, and chain closure is false for AConsistent: with ℕ constants, the sets {¬⋀ₖ U(cₖ)} ∪ {U(cₖ) | k ≤ n} are each consistent and form a chain whose union derives ⊥ by the ω-rule. scripts/check_chain_closure_counterexample.lean keeps that fact executable. The fair enumeration adds one closure target at a time and never claims the union is in the family, so it needs neither field.

Substitution

The one-hole templates for equality symmetry, transitivity and relation congruence are closed terms substituted into a Fin 1-formula; Derivable.eq_subst already takes the target's membership φ.subst t₂ ∈ P as a premise, and HenkinClosed supplies it for closed atoms. No general substitution closure is imposed on P.

Scope

Relational base L, Language.{0, 0}, auxiliary constants present in the model. Forgetting the constants, the source-fragment adapter (L_A(C) in L[[ℕ]]), and arbitrary languages are separate steps.

structure FirstOrder.Language.HenkinClosed {L : Language} (P : Set (L.withConstants ℕ).Sentenceω) : Prop

Henkin closure of a sentence set over L[[ℕ]]: exactly the memberships the proof-theoretic consistency family needs to discharge the kernel's fields.

• falsum_mem : BoundedFormulaω.falsum ∈ P
• not_mem (φ : (L.withConstants ℕ).Sentenceω) : φ ∈ P → BoundedFormulaω.not φ ∈ P
• imp_left (φ ψ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.imp φ ψ ∈ P → φ ∈ P
• imp_right (φ ψ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.imp φ ψ ∈ P → ψ ∈ P
• iInf_comp (φs : ℕ → (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.iInf φs ∈ P → ∀ (k : ℕ), φs k ∈ P
• iSup_comp (φs : ℕ → (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.iSup φs ∈ P → ∀ (k : ℕ), φs k ∈ P
• all_inst (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : φ.all ∈ P → ∀ (c : ℕ), instConst c φ ∈ P
• constEq_mem (a b : ℕ) : constEq a b ∈ P
• relInst_mem (l : ℕ) (R : L.Relations l) (g : Fin l → ℕ) : relInst R g ∈ P

structure FirstOrder.Language.HenkinClosedMin {L : Language} (P : Set (L.withConstants ℕ).Sentenceω) : Prop

The minimal Henkin closure: exactly the memberships the family constructor HenkinClosedMin.consistencyPropertyEqOn consumes. Instead of negation of every member, only the kernel's actual negated targets: the negated antecedent of a member implication, the negated consequent of a member negated implication, the negated components of a member negated conjunction or disjunction, and the negated constant instances of a member negated universal — the closure targets of the generated universe GenU. HenkinClosed.toMin shows the full closure implies it; falsum_mem is not consumed by the kernel and is not required.

Enlarging P strengthens the hypothesis AConsistent P T (more side conditions are discharged), so this weaker interface is the honest consumer contract.

• imp_left (φ ψ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.imp φ ψ ∈ P → φ ∈ P
• imp_right (φ ψ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.imp φ ψ ∈ P → ψ ∈ P
• iInf_comp (φs : ℕ → (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.iInf φs ∈ P → ∀ (k : ℕ), φs k ∈ P
• iSup_comp (φs : ℕ → (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.iSup φs ∈ P → ∀ (k : ℕ), φs k ∈ P
• all_inst (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : φ.all ∈ P → ∀ (c : ℕ), instConst c φ ∈ P
• not_imp_left (φ ψ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.imp φ ψ ∈ P → BoundedFormulaω.not φ ∈ P
• not_neg_imp_right (φ ψ : (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.imp φ ψ).not ∈ P → BoundedFormulaω.not ψ ∈ P
• not_neg_iInf_comp (φs : ℕ → (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.iInf φs).not ∈ P → ∀ (k : ℕ), BoundedFormulaω.not (φs k) ∈ P
• not_neg_iSup_comp (φs : ℕ → (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.iSup φs).not ∈ P → ∀ (k : ℕ), BoundedFormulaω.not (φs k) ∈ P
• not_neg_all_inst (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : φ.all.not ∈ P → ∀ (c : ℕ), BoundedFormulaω.not (instConst c φ) ∈ P
• constEq_mem (a b : ℕ) : constEq a b ∈ P
• relInst_mem (l : ℕ) (R : L.Relations l) (g : Fin l → ℕ) : relInst R g ∈ P

theorem FirstOrder.Language.HenkinClosed.toMin {L : Language} {P : Set (L.withConstants ℕ).Sentenceω} (hP : HenkinClosed P) : HenkinClosedMin P

The full closure implies the minimal one: every negated target is the negation of a member.

def FirstOrder.Language.HenkinClosed.aconsistentSets {L : Language} (P : Set (L.withConstants ℕ).Sentenceω) : Set (Set (L.withConstants ℕ).Sentenceω)

The proof-theoretic family: P-bounded P-consistent sets.

Equations

• FirstOrder.Language.HenkinClosed.aconsistentSets P = {S : Set (L.withConstants ℕ).Sentenceω | S ⊆ P ∧ FirstOrder.Language.AConsistent P S}

theorem FirstOrder.Language.HenkinClosed.union_singleton_subset {L : Language} {P S : Set (L.withConstants ℕ).Sentenceω} (hS : S ⊆ P) {φ : (L.withConstants ℕ).Sentenceω} (hφ : φ ∈ P) : S ∪ {φ} ⊆ P

theorem FirstOrder.Language.HenkinClosedMin.mem_of_not_mem {L : Language} {P : Set (L.withConstants ℕ).Sentenceω} (hP : HenkinClosedMin P) {φ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.not φ ∈ P) : φ ∈ P

¬φ ∈ P gives φ ∈ P, since φ.not = φ.imp ⊥.

def FirstOrder.Language.HenkinClosedMin.consistencyPropertyEqOn {L : Language} {P : Set (L.withConstants ℕ).Sentenceω} (hP : HenkinClosedMin P) [L.IsRelational] : ConsistencyPropertyEqOn P

The proof-theoretic consistency property over a minimally Henkin-closed P. No extension, no chain_closure: the kernel does not ask for them.

Equations

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

theorem FirstOrder.Language.HenkinClosedMin.exists_countable_model_of_aconsistent {L : Language} {P : Set (L.withConstants ℕ).Sentenceω} (hP : HenkinClosedMin P) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hPc : P.Countable) {T : Set (L.withConstants ℕ).Sentenceω} (hT : T ⊆ P) (hcons : AConsistent P T) : ∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M) (_ : Countable M), Theoryω.Model T M

Syntactic model existence over the relational core (countable P), minimal closure. A P-consistent T ⊆ P has a countable L[[ℕ]]-model. No chain closure and no extension hypothesis: the fair enumeration never needs them.

This is the kernel adapter, stated explicitly over a relational base with the auxiliary constants still present. It is not yet the Barwise theorem over an arbitrary language.

theorem FirstOrder.Language.HenkinClosed.mem_of_not_mem {L : Language} {P : Set (L.withConstants ℕ).Sentenceω} (hP : HenkinClosed P) {φ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.not φ ∈ P) : φ ∈ P

¬φ ∈ P gives φ ∈ P, since φ.not = φ.imp ⊥.

def FirstOrder.Language.HenkinClosed.consistencyPropertyEqOn {L : Language} {P : Set (L.withConstants ℕ).Sentenceω} (hP : HenkinClosed P) [L.IsRelational] : ConsistencyPropertyEqOn P

The proof-theoretic consistency property over a Henkin-closed P, through the minimal closure.

Equations

• hP.consistencyPropertyEqOn = ⋯.consistencyPropertyEqOn

theorem FirstOrder.Language.HenkinClosed.exists_countable_model_of_aconsistent {L : Language} {P : Set (L.withConstants ℕ).Sentenceω} (hP : HenkinClosed P) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hPc : P.Countable) {T : Set (L.withConstants ℕ).Sentenceω} (hT : T ⊆ P) (hcons : AConsistent P T) : ∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M) (_ : Countable M), Theoryω.Model T M

Syntactic model existence over the relational core (countable P). The full-closure form of HenkinClosedMin.exists_countable_model_of_aconsistent, kept as the published kernel adapter.