therefore
Sign up
Open navigation
All proofs
Project-declaredLean 4.32.1 Β· mathlib@520045ab

Ch Sigma1 mem iff

LO.FirstOrder.Arithmetic.chSigma1_mem_iff

formal logicmetatheoryproof theoryinduction scheme delta1

Plain-language statement

mem_iff math (C = Hierarchy 𝚺 1). Mirrors chUniv_mem_iff, threading the IsSigma1 K side condition through isSigma1_iff_hierarchy.

Exact Lean statement

theorem chSigma1_mem_iff (Ο† : _root_.LO.FirstOrder.ArithmeticSemiformula β„• 0) :
    InductionSigma1R (βŒœΟ†βŒ : β„•)
      ↔ βˆƒ Οƒ ∈ InductionScheme β„’β‚’α΅£ (Arithmetic.Hierarchy 𝚺 1), Ο† = (Οƒ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• 0)

Formal artifact

Lean source

Canonical source
Full Lean sourceLean 4
theorem chSigma1_mem_iff (Ο† : _root_.LO.FirstOrder.ArithmeticSemiformula β„• 0) :    InductionSigma1R (βŒœΟ†βŒ : β„•)      ↔ βˆƒ Οƒ ∈ InductionScheme β„’β‚’α΅£ (Arithmetic.Hierarchy 𝚺 1), Ο† = (Οƒ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• 0) := by  rw [mem_inductionScheme_sigma1_iff]  constructor  Β· rintro ⟨m, -, b, -, hp, hU, hsh, hbv, K, -, hKsemi, hKsig, hsubst⟩    obtain ⟨γ, rfl⟩ := Bootstrapping.IsSemiformula.sound hKsemi    have hbsemi : Bootstrapping.IsSemiformula β„’β‚’α΅£ m b := hbv β–Έ hU.isSemiformula    obtain ⟨β, rfl⟩ := Bootstrapping.IsSemiformula.sound hbsemi    refine ⟨γ, hierarchy_of_isSigma1 Ξ³ hKsig, ?_⟩    have hΞ²Ξ³ : Ξ² β‡œ (fun i : Fin m ↦ (&↑i : SyntacticTerm β„’β‚’α΅£)) = succInd Ξ³ := by      apply (Semiformula.quote_inj_iff (L := β„’β‚’α΅£) (V := β„•)).mp      have e := Bootstrapping.subst_fvarVec_quote' (V := β„•) Ξ²      simp only [natCast_nat] at e      rw [← e, hsubst, indBodyVal_quote]    have hΞ²free : Ξ².freeVariables = βˆ… := by      have hsΞ² : Rewriting.shift Ξ² = Ξ² :=        (Semiformula.quote_inj_iff (L := β„’β‚’α΅£) (V := β„•)).mp          (by rw [Semiformula.quote_shift (V := β„•) Ξ²]; exact hsh)      have step : βˆ€ x, Ξ².FVar? x β†’ 1 ≀ x ∧ Ξ².FVar? (x - 1) := by        intro x hx        rw [← hsΞ²] at hx        rcases Semiformula.fvar?_rew hx with (⟨i, hi⟩ | ⟨z, hz, hi⟩)        Β· simp [Rew.shift_bvar, Semiterm.FVar?] at hi        Β· have hxz : x = z + 1 := by            simpa [Rew.shift_fvar, Semiterm.FVar?, Semiterm.freeVariables_fvar] using hi          exact ⟨by omega, by rw [hxz]; simpa using hz⟩      by_contra hne      classical      have hnem := Finset.nonempty_of_ne_empty hne      obtain ⟨hge, hpred⟩ := step (Ξ².freeVariables.min' hnem) (Ξ².freeVariables.min'_mem hnem)      exact absurd (Ξ².freeVariables.min'_le _ hpred) (by omega)    have hΟ† : Ο† = (βˆ€ΒΉ* Ξ² : _root_.LO.FirstOrder.ArithmeticSemiformula β„• 0) := by      apply (Semiformula.quote_inj_iff (L := β„’β‚’α΅£) (V := β„•)).mp      rw [hp, Bootstrapping.quote_allClosure (V := β„•) Ξ²]; simp    rw [hΟ†]    exact closure_inversion Ξ² Ξ³ hΞ²free hbv hΞ²Ξ³  Β· rintro ⟨ψ, hψ, rfl⟩    set Ο‡ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• 0 := succInd ψ with hΟ‡    set b : β„• := (⌜(Rew.fixitr 0 Ο‡.fvSup β–Ή Ο‡ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• (0 + Ο‡.fvSup))⌝ : β„•) with hb    have hcode : (βŒœΟ‡.univCl'⌝ : β„•) = Bootstrapping.qqAlls b ((0 + Ο‡.fvSup : β„•)) := by      rw [hb, Bootstrapping.quote_univCl' (V := β„•) Ο‡]; simp    have hs : Bootstrapping.subst β„’β‚’α΅£ (Bootstrapping.fvarVec (0 + Ο‡.fvSup : β„•)) b        = indBodyVal (⌜ψ⌝ : β„•) := by      rw [hb]      have hsub := Bootstrapping.subst_fvarVec_quote' (V := β„•)        (Rew.fixitr 0 Ο‡.fvSup β–Ή Ο‡ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• (0 + Ο‡.fvSup))      simp only [natCast_nat] at hsub      rw [hsub, Bootstrapping.quote_subst_fvar_fixitr Ο‡,        show (⌜ψ⌝ : β„•) = (⌜ψ⌝ : Bootstrapping.Semiformula β„• β„’β‚’α΅£ 1).val from rfl,        indBodyVal_eq, indBody_quote, hΟ‡]      rfl    refine ⟨(0 + Ο‡.fvSup : β„•), ?_, b, ?_, ?_, ?_, ?_, ?_, (⌜ψ⌝ : β„•), ?_, ?_, ?_, ?_⟩    Β· rw [hcode]; exact Bootstrapping.index_le_qqAlls _ _    Β· rw [hcode]; exact Bootstrapping.le_qqAlls _ _    Β· exact hcode    Β· rw [hb]      exact (Semiformula.quote_isSemiformula (V := β„•)        (Rew.fixitr 0 Ο‡.fvSup β–Ή Ο‡ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• (0 + Ο‡.fvSup))).isUFormula    Β· rw [hb]      have hnf : βˆ€ x, Β¬(Rew.fixitr 0 Ο‡.fvSup β–Ή Ο‡ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• (0 + Ο‡.fvSup)).FVar? x := by        intro x        rw [Rew.eq_bind (Rew.fixitr 0 Ο‡.fvSup)]        simp only [Function.comp_def, Rew.fixitr_bvar, Rew.fixitr_fvar, Fin.natAdd_mk, zero_add]        intro hh        rcases Semiformula.fvar?_rew hh with (⟨z, hz⟩ | ⟨z, hz, hx⟩)        Β· simp at hz        Β· have : z < Ο‡.fvSup := Semiformula.lt_fvSup_of_fvar? hz          simp [this] at hx      have hshift : Rewriting.shift (Rew.fixitr 0 Ο‡.fvSup β–Ή Ο‡ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• (0 + Ο‡.fvSup))          = (Rew.fixitr 0 Ο‡.fvSup β–Ή Ο‡ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• (0 + Ο‡.fvSup)) :=        Semiformula.rew_eq_self_of (by simp) (fun x hx ↦ absurd hx (hnf x))      rw [← Semiformula.quote_shift (V := β„•)        (Rew.fixitr 0 Ο‡.fvSup β–Ή Ο‡ : _root_.LO.FirstOrder.ArithmeticSemiformula β„• (0 + Ο‡.fvSup)), hshift]    Β· rw [hb]; exact (Bootstrapping.bv_quote_fixitr Ο‡).trans (zero_add _).symm    Β· rw [hs]; exact le_indBodyVal _    Β· simp    Β· -- the new side condition: `IsSigma1 ⌜ψ⌝` from `Hierarchy 𝚺 1 ψ`      exact isSigma1_of_hierarchy hψ    Β· exact hs
Project
Foundation
License
Apache-2.0
Commit
8dcdb3196454
Source
Foundation/FirstOrder/Incompleteness/InductionSchemeDelta1.lean:1292-1371

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.1

Computable Pred iff decoded pred

ComputablePred.iff_decoded_pred

Plain-language statement

Computability of a predicate on a Primcodable type is equivalent to the computability of the corresponding predicate on β„• obtained by decoding.

formal logicmetatheoryproof theory

Source project: Foundation

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.1

Bv quote fixitr

LO.FirstOrder.Arithmetic.Bootstrapping.bv_quote_fixitr

Plain-language statement

bv-pin bridge (over β„•): bv ⌜fixitr 0 (fvSup Ο‡) β–Ή Ο‡βŒ = fvSup Ο‡. - ≀ is immediate from quote_univCl_eq + bv_qqAlls (closing fvSup quantifiers reaches a sentence, whose bv is 0). - β‰₯ is by level-factoring: were the body an IsSemiformula j for some j < fvSup, IsSemiformula.sound + castLE-invariance would re-express Ο‡ as `Ξ³ β‡œ ![...

formal logicmetatheoryproof theory

Source project: Foundation

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.1

Conj

LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.conj

Plain-language statement

Crucial inducion for formalized Ξ£1\Sigma_1-completeness.

formal logicmetatheoryproof theory

Source project: Foundation

Person-level attribution pending.

View proof record