Proof System for Admissible Fragments

This file defines a proof system for admissible fragments of Lω₁ω. The system is Prop-valued (no proof terms) and operates on sentences.

Main Definitions

• Derivable A T φ: Derivability of sentence φ from theory T in fragment A.
• AConsistent A T: Theory T is consistent in fragment A (cannot derive ⊥).

Main Results

• Derivable.mono: Derivability is monotone in the theory.
• AConsistent.mono: Consistency is antitone in the theory.
• AConsistent.no_contradiction: No consistent theory contains both φ and ¬φ.

Design Notes

The system is sentence-level (not bounded formulas with parameters). The quantifier rules use the omega-rule: all_intro requires derivability of all substitution instances, and all_elim extracts one instance.

inductive FirstOrder.Language.Derivable {L : Language} (A : L.AdmissibleFragment) : Set L.Sentenceω → L.Sentenceω → Prop

Derivability in an admissible fragment. Prop-valued (no proof terms).

The system includes structural rules, propositional rules, infinitary connective rules, quantifier rules (omega-rule), equality rules, and classical logic (LEM).

• assumption {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φ : L.Sentenceω} : φ ∈ T → φ ∈ A.formulas → Derivable A T φ
• weaken {L : Language} {A : L.AdmissibleFragment} {T T' : Set L.Sentenceω} {φ : L.Sentenceω} : T ⊆ T' → Derivable A T φ → Derivable A T' φ
• falsum_elim {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φ : L.Sentenceω} : Derivable A T BoundedFormulaω.falsum → φ ∈ A.formulas → Derivable A T φ
• imp_intro {L : Language} {A : L.AdmissibleFragment} {φ : L.Sentenceω} {T : Set L.Sentenceω} {ψ : L.Sentenceω} : φ ∈ A.formulas → Derivable A (T ∪ {φ}) ψ → Derivable A T (BoundedFormulaω.imp φ ψ)
• imp_elim {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φ ψ : L.Sentenceω} : Derivable A T (BoundedFormulaω.imp φ ψ) → Derivable A T φ → Derivable A T ψ
• not_not_elim {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φ : L.Sentenceω} : Derivable A T (BoundedFormulaω.not φ).not → Derivable A T φ
• iInf_intro {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φs : ℕ → L.BoundedFormulaω Empty 0} : (∀ (k : ℕ), Derivable A T (φs k)) → BoundedFormulaω.iInf φs ∈ A.formulas → Derivable A T (BoundedFormulaω.iInf φs)
• iInf_elim {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φs : ℕ → L.BoundedFormulaω Empty 0} (k : ℕ) : Derivable A T (BoundedFormulaω.iInf φs) → Derivable A T (φs k)
• iSup_intro {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φs : ℕ → L.BoundedFormulaω Empty 0} (k : ℕ) : Derivable A T (φs k) → BoundedFormulaω.iSup φs ∈ A.formulas → Derivable A T (BoundedFormulaω.iSup φs)
• iSup_elim {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φs : ℕ → L.BoundedFormulaω Empty 0} {ψ : L.Sentenceω} : Derivable A T (BoundedFormulaω.iSup φs) → (∀ (k : ℕ), Derivable A (T ∪ {φs k}) ψ) → Derivable A T ψ
• all_intro {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} (φ : L.BoundedFormulaω Empty 1) : (∀ (t : L.Term Empty), Derivable A T (BoundedFormulaω.subst φ.openBounds fun (x : Fin 1) => t)) → φ.all ∈ A.formulas → Derivable A T φ.all
• all_elim {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} (φ : L.BoundedFormulaω Empty 1) (t : L.Term Empty) : Derivable A T φ.all → Derivable A T (BoundedFormulaω.subst φ.openBounds fun (x : Fin 1) => t)
• eq_refl {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} (t : L.Term (Empty ⊕ Fin 0)) : BoundedFormulaω.equal t t ∈ A.formulas → Derivable A T (BoundedFormulaω.equal t t)
• eq_subst {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} (t₁ t₂ : L.Term Empty) (φ : L.Formulaω (Fin 1)) : Derivable A T (BoundedFormulaω.equal (Term.relabel Sum.inl t₁) (Term.relabel Sum.inl t₂)) → Derivable A T (BoundedFormulaω.subst φ fun (x : Fin 1) => t₁) → (BoundedFormulaω.subst φ fun (x : Fin 1) => t₂) ∈ A.formulas → Derivable A T (BoundedFormulaω.subst φ fun (x : Fin 1) => t₂)
• em {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} (φ : L.Sentenceω) : φ ∈ A.formulas → Derivable A T (BoundedFormulaω.or φ (BoundedFormulaω.not φ))

def FirstOrder.Language.AConsistent {L : Language} (A : L.AdmissibleFragment) (T : Set L.Sentenceω) : Prop

A theory is A-consistent if ⊥ is not derivable from it.

Equations

• FirstOrder.Language.AConsistent A T = ¬FirstOrder.Language.Derivable A T FirstOrder.Language.BoundedFormulaω.falsum

Basic lemmas

theorem FirstOrder.Language.Derivable.mono {L : Language} {φ : L.Sentenceω} {A : L.AdmissibleFragment} {T T' : Set L.Sentenceω} (h : T ⊆ T') (hd : Derivable A T φ) : Derivable A T' φ

Derivability is monotone in the theory.

theorem FirstOrder.Language.AConsistent.mono {L : Language} {A : L.AdmissibleFragment} {T T' : Set L.Sentenceω} (h : T' ⊆ T) (hc : AConsistent A T) : AConsistent A T'

Consistency is antitone: subsets of consistent sets are consistent.

theorem FirstOrder.Language.AConsistent.no_falsum {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} (hc : AConsistent A T) (hT : T ⊆ A.formulas) : BoundedFormulaω.falsum ∉ T

A consistent theory does not contain ⊥.

theorem FirstOrder.Language.AConsistent.no_contradiction {L : Language} {φ : L.Sentenceω} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} (hc : AConsistent A T) (hφ : φ ∈ T) (hφA : φ ∈ A.formulas) : BoundedFormulaω.not φ ∉ T

A consistent theory does not contain both φ and ¬φ.

theorem FirstOrder.Language.Derivable.neg_intro {L : Language} {φ : L.Sentenceω} {T : Set L.Sentenceω} {A : L.AdmissibleFragment} (hφ : φ ∈ A.formulas) (h : Derivable A (T ∪ {φ}) BoundedFormulaω.falsum) : Derivable A T (BoundedFormulaω.not φ)

Negation introduction: if T ∪ {φ} ⊢ ⊥, then T ⊢ ¬φ.

theorem FirstOrder.Language.Derivable.neg_elim {L : Language} {T : Set L.Sentenceω} {φ : L.Sentenceω} {A : L.AdmissibleFragment} (h₁ : Derivable A T φ) (h₂ : Derivable A T (BoundedFormulaω.not φ)) : Derivable A T BoundedFormulaω.falsum

Negation elimination: if T ⊢ φ and T ⊢ ¬φ, then T ⊢ ⊥.

theorem FirstOrder.Language.Derivable.derivable_collapses_extension {L : Language} {T : Set L.Sentenceω} {χ : L.Sentenceω} {A : L.AdmissibleFragment} (hd : Derivable A T χ) (hχ : χ ∈ A.formulas) (hbot : Derivable A (T ∪ {χ}) BoundedFormulaω.falsum) : Derivable A T BoundedFormulaω.falsum

If S ⊢ χ and S ∪ {χ} ⊢ ⊥, then S ⊢ ⊥.

theorem FirstOrder.Language.Derivable.inconsistent_of_both_extensions {L : Language} {φ : L.Sentenceω} {T : Set L.Sentenceω} {A : L.AdmissibleFragment} (hφA : φ ∈ A.formulas) (h₁ : Derivable A (T ∪ {φ}) BoundedFormulaω.falsum) (h₂ : Derivable A (T ∪ {BoundedFormulaω.not φ}) BoundedFormulaω.falsum) : Derivable A T BoundedFormulaω.falsum

If S ∪ {φ} ⊢ ⊥ and S ∪ {¬φ} ⊢ ⊥, then S ⊢ ⊥.

theorem FirstOrder.Language.Derivable.imp_intro_from_neg {L : Language} {T : Set L.Sentenceω} {φ ψ : L.Sentenceω} {A : L.AdmissibleFragment} (hd : Derivable A T (BoundedFormulaω.not φ)) (hφA : φ ∈ A.formulas) (hψA : ψ ∈ A.formulas) : Derivable A T (BoundedFormulaω.imp φ ψ)

If S ⊢ ¬φ and φ, ψ ∈ A.formulas, then S ⊢ φ → ψ.

theorem FirstOrder.Language.AConsistent.extension_of_mem_formulas {L : Language} {φ : L.Sentenceω} {A : L.AdmissibleFragment} {S : Set L.Sentenceω} (_hSA : S ⊆ A.formulas) (hc : AConsistent A S) (hφA : φ ∈ A.formulas) : AConsistent A (S ∪ {φ}) ∨ AConsistent A (S ∪ {BoundedFormulaω.not φ})

If S ⊆ A.formulas, AConsistent A S, and φ ∈ A.formulas, then AConsistent A (S ∪ {φ}) ∨ AConsistent A (S ∪ {¬φ}).