Proof System over a Permitted Sentence Set

This file defines a proof system for Lω₁ω over a permitted sentence set P : Set L.Sentenceω. The system is Prop-valued (no proof terms) and operates on sentences.

Main Definitions

• Derivable P T φ: Derivability of sentence φ from theory T, with conclusions permitted by P.
• AConsistent P T: Theory T is P-consistent (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.

The permission parameter is a raw Set L.Sentenceω, not a fragment structure: the consumer audit (interface contract §8) established that the proof system consumes nothing but membership — its membership premises guard conclusions, never hypotheses, so no closure or distinguished-element field is required. Fragment-based callers pass their sentence set (e.g. A.formulas) and supply any needed closure facts (such as φ.not ∈ P) explicitly at the two negation lemmas that use them.

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

Derivability over a permitted sentence set. 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} {P T : Set L.Sentenceω} {φ : L.Sentenceω} : φ ∈ T → φ ∈ P → Derivable P T φ
• weaken {L : Language} {P T T' : Set L.Sentenceω} {φ : L.Sentenceω} : T ⊆ T' → Derivable P T φ → Derivable P T' φ
• falsum_elim {L : Language} {P T : Set L.Sentenceω} {φ : L.Sentenceω} : Derivable P T BoundedFormulaω.falsum → φ ∈ P → Derivable P T φ
• imp_intro {L : Language} {P : Set L.Sentenceω} {φ : L.Sentenceω} {T : Set L.Sentenceω} {ψ : L.Sentenceω} : φ ∈ P → Derivable P (T ∪ {φ}) ψ → Derivable P T (BoundedFormulaω.imp φ ψ)
• imp_elim {L : Language} {P T : Set L.Sentenceω} {φ ψ : L.Sentenceω} : Derivable P T (BoundedFormulaω.imp φ ψ) → Derivable P T φ → Derivable P T ψ
• not_not_elim {L : Language} {P T : Set L.Sentenceω} {φ : L.Sentenceω} : Derivable P T (BoundedFormulaω.not φ).not → Derivable P T φ
• iInf_intro {L : Language} {P T : Set L.Sentenceω} {φs : ℕ → L.BoundedFormulaω Empty 0} : (∀ (k : ℕ), Derivable P T (φs k)) → BoundedFormulaω.iInf φs ∈ P → Derivable P T (BoundedFormulaω.iInf φs)
• iInf_elim {L : Language} {P T : Set L.Sentenceω} {φs : ℕ → L.BoundedFormulaω Empty 0} (k : ℕ) : Derivable P T (BoundedFormulaω.iInf φs) → Derivable P T (φs k)
• iSup_intro {L : Language} {P T : Set L.Sentenceω} {φs : ℕ → L.BoundedFormulaω Empty 0} (k : ℕ) : Derivable P T (φs k) → BoundedFormulaω.iSup φs ∈ P → Derivable P T (BoundedFormulaω.iSup φs)
• iSup_elim {L : Language} {P T : Set L.Sentenceω} {φs : ℕ → L.BoundedFormulaω Empty 0} {ψ : L.Sentenceω} : Derivable P T (BoundedFormulaω.iSup φs) → (∀ (k : ℕ), Derivable P (T ∪ {φs k}) ψ) → Derivable P T ψ
• all_intro {L : Language} {P T : Set L.Sentenceω} (φ : L.BoundedFormulaω Empty 1) : (∀ (t : L.Term Empty), Derivable P T (BoundedFormulaω.subst φ.openBounds fun (x : Fin 1) => t)) → φ.all ∈ P → Derivable P T φ.all
• all_elim {L : Language} {P T : Set L.Sentenceω} (φ : L.BoundedFormulaω Empty 1) (t : L.Term Empty) : Derivable P T φ.all → Derivable P T (BoundedFormulaω.subst φ.openBounds fun (x : Fin 1) => t)
• eq_refl {L : Language} {P T : Set L.Sentenceω} (t : L.Term (Empty ⊕ Fin 0)) : BoundedFormulaω.equal t t ∈ P → Derivable P T (BoundedFormulaω.equal t t)
• eq_subst {L : Language} {P T : Set L.Sentenceω} (t₁ t₂ : L.Term Empty) (φ : L.Formulaω (Fin 1)) : Derivable P T (BoundedFormulaω.equal (Term.relabel Sum.inl t₁) (Term.relabel Sum.inl t₂)) → Derivable P T (BoundedFormulaω.subst φ fun (x : Fin 1) => t₁) → (BoundedFormulaω.subst φ fun (x : Fin 1) => t₂) ∈ P → Derivable P T (BoundedFormulaω.subst φ fun (x : Fin 1) => t₂)
• em {L : Language} {P T : Set L.Sentenceω} (φ : L.Sentenceω) : φ ∈ P → Derivable P T (BoundedFormulaω.or φ (BoundedFormulaω.not φ))

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

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

Equations

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

Basic lemmas

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

Derivability is monotone in the theory.

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

Consistency is antitone: subsets of consistent sets are consistent.

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

A consistent theory does not contain ⊥.

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

A consistent theory does not contain both φ and ¬φ. The negation's membership in the permitted set is an explicit hypothesis (fragment-based callers discharge it by closure).

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

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

theorem FirstOrder.Language.Derivable.neg_elim {L : Language} {T : Set L.Sentenceω} {φ : L.Sentenceω} {P : Set L.Sentenceω} (h₁ : Derivable P T φ) (h₂ : Derivable P T (BoundedFormulaω.not φ)) : Derivable P 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ω} {P : Set L.Sentenceω} (hd : Derivable P T χ) (hχ : χ ∈ P) (hbot : Derivable P (T ∪ {χ}) BoundedFormulaω.falsum) : Derivable P T BoundedFormulaω.falsum

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

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

If S ∪ {φ} ⊢ ⊥ and S ∪ {¬φ} ⊢ ⊥, then S ⊢ ⊥. The negation's membership in the permitted set is an explicit hypothesis.

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

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

theorem FirstOrder.Language.AConsistent.extension_of_mem_formulas {L : Language} {φ : L.Sentenceω} {P S : Set L.Sentenceω} (hc : AConsistent P S) (hφP : φ ∈ P) (hφnP : BoundedFormulaω.not φ ∈ P) : AConsistent P (S ∪ {φ}) ∨ AConsistent P (S ∪ {BoundedFormulaω.not φ})

If AConsistent P S and both φ and φ.not are permitted, then AConsistent P (S ∪ {φ}) ∨ AConsistent P (S ∪ {¬φ}).