Consistency Bridge: From AConsistent to ConsistencyPropertyEq

This file constructs a ConsistencyPropertyEq from AConsistent, enabling the model existence theorem for proof-theoretically consistent theories in admissible fragments.

Main Results

• consistencyPropertyOfFullFragment: Constructs a ConsistencyPropertyEq from A-consistent sets in a FullBarwiseFragment (all sentences in the fragment).
• barwise_completeness_II_syntactic_full: A countable A-consistent theory in a full Barwise fragment of a countable language has a countable model.

Design Notes

The chain closure axiom for AConsistent does not follow from the proof-theoretic definition alone (infinitary derivations can draw premises from scattered chain elements). It is taken as an explicit hypothesis, factored via BarwiseFragment.

The FullBarwiseFragment wrapper isolates the strong hypothesis that ALL Lω₁ω sentences belong to the fragment. This matches the global Henkin/maximal-consistent API (e.g., extension requires deciding arbitrary sentences) without modifying the existing ConsistencyProperty infrastructure.

The verification of each consistency property axiom follows a uniform pattern: assume the relevant extension is inconsistent, use proof rules to derive ⊥ from the original set, contradicting its consistency.

structure FirstOrder.Language.BarwiseFragment (L : Language) extends L.AdmissibleFragment : Type (max (max u (u_1 + 1)) v)

A Barwise fragment extends an admissible fragment with the chain closure property for proof-theoretic consistency.

• formulas : Set L.Sentenceω
• height : Ordinal.{u_1}
• height_gt_omega : Ordinal.omega0 < self.height
• closed_neg (φ : L.Sentenceω) : φ ∈ self.formulas → BoundedFormulaω.not φ ∈ self.formulas
• closed_imp (φ ψ : L.Sentenceω) : φ ∈ self.formulas → ψ ∈ self.formulas → BoundedFormulaω.imp φ ψ ∈ self.formulas
• closed_iInf (φs : ℕ → L.Sentenceω) : (∀ (k : ℕ), φs k ∈ self.formulas) → BoundedFormulaω.iInf φs ∈ self.formulas
• closed_iSup (φs : ℕ → L.Sentenceω) : (∀ (k : ℕ), φs k ∈ self.formulas) → BoundedFormulaω.iSup φs ∈ self.formulas
• closed_quantifier_instance (φ : L.Formulaω (Fin 1)) (t : L.Term Empty) : (BoundedFormulaω.relabel Sum.inr φ).ex ∈ self.formulas → (BoundedFormulaω.subst φ fun (x : Fin 1) => t) ∈ self.formulas
• falsum_mem : BoundedFormulaω.falsum ∈ self.formulas
• closed_imp_left (φ ψ : L.Sentenceω) : BoundedFormulaω.imp φ ψ ∈ self.formulas → φ ∈ self.formulas
• closed_imp_right (φ ψ : L.Sentenceω) : BoundedFormulaω.imp φ ψ ∈ self.formulas → ψ ∈ self.formulas
• closed_iInf_component (φs : ℕ → L.Sentenceω) (k : ℕ) : BoundedFormulaω.iInf φs ∈ self.formulas → φs k ∈ self.formulas
• closed_iSup_component (φs : ℕ → L.Sentenceω) (k : ℕ) : BoundedFormulaω.iSup φs ∈ self.formulas → φs k ∈ self.formulas
• compact (S : Set L.Sentenceω) : S ⊆ self.formulas → (∀ F ⊆ self.formulas, F.Finite → F ⊆ S → ∃ (M : Type) (x : L.Structure M), Theoryω.Model F M) → ∃ (M : Type) (x : L.Structure M), Theoryω.Model S M
• chain_closure_consistent (chain : Set (Set L.Sentenceω)) : chain ⊆ {S : Set L.Sentenceω | S ⊆ self.formulas ∧ AConsistent self.toAdmissibleFragment S} → IsChain (fun (x1 x2 : Set L.Sentenceω) => x1 ⊆ x2) chain → chain.Nonempty → AConsistent self.toAdmissibleFragment (⋃₀ chain)

structure FirstOrder.Language.FullBarwiseFragment (L : Language) extends L.BarwiseFragment : Type (max (max u (u_1 + 1)) v)

A full Barwise fragment: an admissible fragment containing ALL Lω₁ω sentences. This is a strong wrapper introduced to match the global Henkin/maximal-consistent API (ConsistencyProperty.extension requires deciding arbitrary sentences). We isolate this hypothesis here rather than modifying the global API.

• formulas : Set L.Sentenceω
• height : Ordinal.{u_1}
• height_gt_omega : Ordinal.omega0 < self.height
• closed_neg (φ : L.Sentenceω) : φ ∈ self.formulas → BoundedFormulaω.not φ ∈ self.formulas
• closed_imp (φ ψ : L.Sentenceω) : φ ∈ self.formulas → ψ ∈ self.formulas → BoundedFormulaω.imp φ ψ ∈ self.formulas
• closed_iInf (φs : ℕ → L.Sentenceω) : (∀ (k : ℕ), φs k ∈ self.formulas) → BoundedFormulaω.iInf φs ∈ self.formulas
• closed_iSup (φs : ℕ → L.Sentenceω) : (∀ (k : ℕ), φs k ∈ self.formulas) → BoundedFormulaω.iSup φs ∈ self.formulas
• closed_quantifier_instance (φ : L.Formulaω (Fin 1)) (t : L.Term Empty) : (BoundedFormulaω.relabel Sum.inr φ).ex ∈ self.formulas → (BoundedFormulaω.subst φ fun (x : Fin 1) => t) ∈ self.formulas
• falsum_mem : BoundedFormulaω.falsum ∈ self.formulas
• closed_imp_left (φ ψ : L.Sentenceω) : BoundedFormulaω.imp φ ψ ∈ self.formulas → φ ∈ self.formulas
• closed_imp_right (φ ψ : L.Sentenceω) : BoundedFormulaω.imp φ ψ ∈ self.formulas → ψ ∈ self.formulas
• closed_iInf_component (φs : ℕ → L.Sentenceω) (k : ℕ) : BoundedFormulaω.iInf φs ∈ self.formulas → φs k ∈ self.formulas
• closed_iSup_component (φs : ℕ → L.Sentenceω) (k : ℕ) : BoundedFormulaω.iSup φs ∈ self.formulas → φs k ∈ self.formulas
• compact (S : Set L.Sentenceω) : S ⊆ self.formulas → (∀ F ⊆ self.formulas, F.Finite → F ⊆ S → ∃ (M : Type) (x : L.Structure M), Theoryω.Model F M) → ∃ (M : Type) (x : L.Structure M), Theoryω.Model S M
• chain_closure_consistent (chain : Set (Set L.Sentenceω)) : chain ⊆ {S : Set L.Sentenceω | S ⊆ self.formulas ∧ AConsistent self.toAdmissibleFragment S} → IsChain (fun (x1 x2 : Set L.Sentenceω) => x1 ⊆ x2) chain → chain.Nonempty → AConsistent self.toAdmissibleFragment (⋃₀ chain)
• complete (φ : L.Sentenceω) : φ ∈ self.formulas

def FirstOrder.Language.consistentSets {L : Language} (A : L.AdmissibleFragment) : Set (Set L.Sentenceω)

The family of A-consistent subsets of the fragment's formulas.

Equations

• FirstOrder.Language.consistentSets A = {S : Set L.Sentenceω | S ⊆ A.formulas ∧ FirstOrder.Language.AConsistent A S}

noncomputable def FirstOrder.Language.consistencyPropertyOfFullFragment {L : Language} (B : L.FullBarwiseFragment) : L.ConsistencyPropertyEq

Construct a ConsistencyPropertyEq from A-consistent sets in a full Barwise fragment.

Each C0-C7 axiom is verified by assuming the extension is inconsistent and deriving a contradiction with the original set's consistency via rules of Derivable. The complete hypothesis ensures all formula membership checks are trivial.

Equations

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

theorem FirstOrder.Language.barwise_completeness_II_syntactic_full {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (B : L.FullBarwiseFragment) {T : Set L.Sentenceω} (hT : T ⊆ B.formulas) (hT_countable : T.Countable) (hcons : AConsistent B.toAdmissibleFragment T) : ∃ (M : Type u) (x : L.Structure M) (_ : Countable M), Theoryω.Model T M

Barwise Completeness II (syntactic, full fragment): A countable A-consistent theory in a full Barwise fragment of a countable language has a countable model.