The fragment-relative consistency property and Henkin completion (issue #8 tranche 2, commit 2)

ConsistencyPropertyEqOn U: a family of U-bounded sentence sets closed under the C0–C4 decompositions, the atomic equality/relation congruence fields specialized to constant indices (constEq/relInst — the relational-core term model consumes nothing more; arbitrary closed terms convert to constants at the term-model boundary via exists_eq_constTerm), and the two minimal quantifier fields (universal instantiation + a fresh witness for a negated universal — the negated-universal field is the existential witness rule; the forward constructor-level truth lemma needs no separate existential rule).

HenkinComplete U S: the truth-lemma-facing completion predicate — the same closure, but stated on S itself (targets are in S, not "consistently addable"). The fair enumeration (commit 3) produces an S* ⊇ S₀ with HenkinComplete U S*.

Deliberately absent (per the audit, §5–§6b): no extension, no chain_closure (Finding 1), no general C6 (a countable U cannot close under arbitrary substitution templates), and no finiteness — finiteness belongs to the inseparable-pair instance (commit 4).

The fragment-relative consistency property

structure FirstOrder.Language.ConsistencyPropertyEqOn {L : Language} (U : Set (L.withConstants ℕ).Sentenceω) : Type

ConsistencyPropertyEqOn U: a U-bounded consistency family with atomic equality / relation congruence and minimal quantifier fields.

• sets : Set (Set (L.withConstants ℕ).Sentenceω)

  The family of consistent sets.

• subset_U (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → S ⊆ U

  Every consistent set lives in the enumeration universe U.

• C0_no_falsum (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → BoundedFormulaω.falsum ∉ S

  (C0a) No consistent set contains ⊥.

• C0_no_contradiction (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φ : (L.withConstants ℕ).Sentenceω), ¬(φ ∈ S ∧ BoundedFormulaω.not φ ∈ S)

  (C0b) No consistent set contains a sentence and its negation.

• C1_imp (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φ ψ : (L.withConstants ℕ).Sentenceω), BoundedFormulaω.imp φ ψ ∈ S → S ∪ {BoundedFormulaω.not φ} ∈ self.sets ∨ S ∪ {ψ} ∈ self.sets

  (C1) Implication.

• C1_neg_imp (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φ ψ : (L.withConstants ℕ).Sentenceω), (BoundedFormulaω.imp φ ψ).not ∈ S → S ∪ {φ} ∈ self.sets ∧ S ∪ {BoundedFormulaω.not ψ} ∈ self.sets

  (C1') Negated implication.

• C2_not_not (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φ : (L.withConstants ℕ).Sentenceω), (BoundedFormulaω.not φ).not ∈ S → S ∪ {φ} ∈ self.sets

  (C2) Double negation.

• C3_iInf (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φs : ℕ → (L.withConstants ℕ).Sentenceω), BoundedFormulaω.iInf φs ∈ S → ∀ (k : ℕ), S ∪ {φs k} ∈ self.sets

  (C3) Countable conjunction.

• C3_neg_iInf (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φs : ℕ → (L.withConstants ℕ).Sentenceω), (BoundedFormulaω.iInf φs).not ∈ S → ∃ (k : ℕ), S ∪ {BoundedFormulaω.not (φs k)} ∈ self.sets

  (C3') Negated conjunction.

• C4_iSup (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φs : ℕ → (L.withConstants ℕ).Sentenceω), BoundedFormulaω.iSup φs ∈ S → ∃ (k : ℕ), S ∪ {φs k} ∈ self.sets

  (C4) Countable disjunction.

• C4_neg_iSup (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φs : ℕ → (L.withConstants ℕ).Sentenceω), (BoundedFormulaω.iSup φs).not ∈ S → ∀ (k : ℕ), S ∪ {BoundedFormulaω.not (φs k)} ∈ self.sets

  (C4') Negated disjunction.

• eq_refl (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (c : ℕ), S ∪ {constEq c c} ∈ self.sets

  Atomic equality reflexivity (constant indices).

• eq_symm (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (a b : ℕ), constEq a b ∈ S → S ∪ {constEq b a} ∈ self.sets

  Atomic equality symmetry (constant indices).

• eq_trans (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (a b d : ℕ), constEq a b ∈ S → constEq b d ∈ S → S ∪ {constEq a d} ∈ self.sets

  Atomic equality transitivity (constant indices).

• rel_congr (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (l : ℕ) (R : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ), relInst R g ∈ S → constEq (g i) b ∈ S → S ∪ {relInst R (Function.update g i b)} ∈ self.sets

  Atomic relation congruence (one-coordinate replacement).

• all_inst (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1), φ.all ∈ S → ∀ (c : ℕ), S ∪ {instConst c φ} ∈ self.sets

  Universal instantiation (fresh-witness-free): a universal admits every constant instance.

• neg_all_witness (S : Set (L.withConstants ℕ).Sentenceω) : S ∈ self.sets → ∀ (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1), φ.all.not ∈ S → ∃ (c : ℕ), S ∪ {BoundedFormulaω.not (instConst c φ)} ∈ self.sets

  Negated-universal witness (the sole existential rule).

The Henkin completion predicate

structure FirstOrder.Language.HenkinComplete {L : Language} (U S : Set (L.withConstants ℕ).Sentenceω) : Prop

HenkinComplete U S: the truth-lemma-facing completion — the same closure as ConsistencyPropertyEqOn but with every target present in S.

• subset_U : S ⊆ U
• no_falsum : BoundedFormulaω.falsum ∉ S
• no_contradiction (φ : (L.withConstants ℕ).Sentenceω) : ¬(φ ∈ S ∧ BoundedFormulaω.not φ ∈ S)
• imp (φ ψ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.imp φ ψ ∈ S → BoundedFormulaω.not φ ∈ S ∨ ψ ∈ S
• neg_imp (φ ψ : (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.imp φ ψ).not ∈ S → φ ∈ S ∧ BoundedFormulaω.not ψ ∈ S
• not_not (φ : (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.not φ).not ∈ S → φ ∈ S
• iInf (φs : ℕ → (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.iInf φs ∈ S → ∀ (k : ℕ), φs k ∈ S
• neg_iInf (φs : ℕ → (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.iInf φs).not ∈ S → ∃ (k : ℕ), BoundedFormulaω.not (φs k) ∈ S
• iSup (φs : ℕ → (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.iSup φs ∈ S → ∃ (k : ℕ), φs k ∈ S
• neg_iSup (φs : ℕ → (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.iSup φs).not ∈ S → ∀ (k : ℕ), BoundedFormulaω.not (φs k) ∈ S
• eq_refl (c : ℕ) : constEq c c ∈ S
• eq_symm (a b : ℕ) : constEq a b ∈ S → constEq b a ∈ S
• eq_trans (a b d : ℕ) : constEq a b ∈ S → constEq b d ∈ S → constEq a d ∈ S
• rel_congr (l : ℕ) (R : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) : relInst R g ∈ S → constEq (g i) b ∈ S → relInst R (Function.update g i b) ∈ S
• all_inst (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : φ.all ∈ S → ∀ (c : ℕ), instConst c φ ∈ S
• neg_all_witness (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : φ.all.not ∈ S → ∃ (c : ℕ), BoundedFormulaω.not (instConst c φ) ∈ S