$\Delta_1$-definability of the induction schemata, and of 𝗜𝚺₁ and 𝗣𝗔

This file discharges the two axioms that previously sat in Examples.lean: PA_delta1Definable : 𝗣𝗔.Δ₁ and ISigma1_delta1Definable : 𝗜𝚺₁.Δ₁.

The route:

𝗣𝗔  = 𝗣𝗔⁻ + InductionScheme ℒₒᵣ Set.univ
𝗜𝚺₁ = 𝗣𝗔⁻ + InductionScheme ℒₒᵣ (Arithmetic.Hierarchy 𝚺 1)

𝗣𝗔⁻ is a finite set of sentences, so Theory.Δ₁.ofFinite gives 𝗣𝗔⁻.Δ₁. Theory.Δ₁.add/.ofEq then reduce both headline instances to the single obligation (InductionScheme ℒₒᵣ C).Δ₁, which is the mathematical content of this file.

Internal iterated universal quantifier qqAlls

qqAlls p k = ^∀ ^∀ … ^∀ p (k quantifiers), the internal counterpart of the meta universal closure ∀¹*. This is part (a) of arithmetizing univCl (part (b), the free→bound fixitr rewrite, is still open). The headline of this section is quote_allClosure: ⌜∀¹* φ⌝ = qqAlls ⌜φ⌝ n.

def LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls.blueprint : PR.Blueprint 1

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : PR.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p k : V) : V

qqAlls p k = ^∀ ^∀ ... ^∀ p (k universal quantifiers).

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls p k = LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls.construction.result ![p] k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : qqAlls p 0 = p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p k : V) : qqAlls p (k + 1) = qqAll (qqAlls p k)

def LO.FirstOrder.Arithmetic.qqAllsDef : 𝚺₁.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ qqAlls via qqAllsDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ qqAlls

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m : ℕ} (Γ : SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Function₂ qqAlls

theorem LO.FirstOrder.Arithmetic.Bootstrapping.le_qqAll {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : p ≤ qqAll p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p k : V) : qqAlls (qqAll p) k = qqAll (qqAlls p k)

^∀ commutes through the closure

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqAlls_succ' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p k : V) : qqAlls p (k + 1) = qqAlls (qqAll p) k

pushing one more ^∀ onto the body equals one more layer of closure

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.le_qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p k : V) : p ≤ qqAlls p k

theorem LO.FirstOrder.Arithmetic.Bootstrapping.succ_le_qqAll {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : p + 1 ≤ qqAll p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.index_le_qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p k : V) : k ≤ qqAlls p k

the number of quantifiers is bounded by the closure code (bounds ∃ m ≤ p)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.isUFormula_qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p k : V} : IsUFormula L (qqAlls p k) ↔ IsUFormula L p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.bv_qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p k : V} (hp : IsUFormula L p) : bv L (qqAlls p k) = bv L p - k

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k p : V} (h : IsSemiformula L (n + k) p) : IsSemiformula L n (Bootstrapping.qqAlls p k)

closing k variables of an (n+k)-formula yields an n-formula

theorem LO.FirstOrder.Arithmetic.Bootstrapping.quote_allClosure {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : FirstOrder.Semiformula L ℕ n) : ⌜∀¹* φ⌝ = qqAlls ⌜φ⌝ ↑n

The internal iterated-^∀ computes the universal-closure code: ⌜∀¹* φ⌝ = qqAlls ⌜φ⌝ n.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.quote_univCl {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (ψ : FirstOrder.Semiformula L ℕ 0) : ⌜ψ.univCl⌝ = ⌜ψ.univCl'⌝

The Gödel code of a sentence univCl ψ agrees with that of its 0-ary semiformula unfolding univCl' ψ (which prepends fvSup ψ universals to the fixitr-rewritten body).

theorem LO.FirstOrder.Arithmetic.Bootstrapping.quote_univCl' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (ψ : FirstOrder.Semiformula L ℕ 0) : ⌜ψ.univCl'⌝ = qqAlls ⌜(Rewriting.app (Rew.fixitr 0 ψ.fvSup)) ψ⌝ ↑(0 + ψ.fvSup)

⌜univCl' ψ⌝ = qqAlls ⌜fixitr 0 (fvSup ψ) ▹ ψ⌝ (fvSup ψ): the universal closure is the internal iterated-^∀ applied to the freevar-free fixitr-image of ψ.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.quote_univCl_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (ψ : FirstOrder.Semiformula L ℕ 0) : ⌜ψ.univCl⌝ = qqAlls ⌜(Rewriting.app (Rew.fixitr 0 ψ.fvSup)) ψ⌝ ↑(0 + ψ.fvSup)

Combined: the code of the universal closure of ψ.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.quote_subst_fvar_fixitr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : FirstOrder.Semiformula L ℕ 0) : ⌜(Rewriting.app (Rew.fixitr 0 φ.fvSup)) φ ⇜ fun (x : Fin (0 + φ.fvSup)) => FirstOrder.Semiterm.fvar ↑x⌝ = ⌜φ⌝

Closure inversion at the code level. Substituting the free-variable atoms &0 … &(m-1) back into the fixitr-image recovers ⌜φ⌝. This is the DECODE direction: the recognizer can recover ⌜succInd ψ⌝ (hence ψ) from the freevar-free closure body using the already-proven internal subst, with no need for an internal fixitr. Meta witness: subst_comp_fixitr.

theorem LO.FirstOrder.Semiformula.fvar?_fvSup_pred {L : Language} {n : ℕ} (φ : Semiformula L ℕ n) (h : 0 < φ.fvSup) : φ.FVar? (φ.fvSup - 1)

Sup attained. The largest free-variable index of φ is fvSup φ - 1 (when φ has free variables). Together with lt_fvSup_of_fvar? this pins fvSup as exactly the count of universals in univCl', and is what the recognizer's bv b = m clause checks (no over-recognition by padding leading ∀s).

castLE-invariance of the Gödel code and free variables

Raising the de Bruijn level of a (semi)term/(semi)formula by Rew.castLE changes neither its raw Gödel code (the underlying variable indices are preserved) nor its set of free variables. These are the bookkeeping lemmas behind the bv-pin bridge below: an IsSemiformula j-witness of a code that "really" sits at level n ≥ j factors through castLE, letting us read off the free-variable budget.

theorem LO.FirstOrder.Semiterm.quote_castLE {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) {n' : ℕ} (h : n ≤ n') : ⌜(Rew.castLE h) t⌝ = ⌜t⌝

theorem LO.FirstOrder.Semiterm.freeVariables_castLE {L : Language} {n : ℕ} (t : SyntacticSemiterm L n) {n' : ℕ} (h : n ≤ n') : ((Rew.castLE h) t).freeVariables = freeVariables t

theorem LO.FirstOrder.Semiformula.quote_castLE {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiformula L ℕ n) {n' : ℕ} (h : n ≤ n') : ⌜(Rewriting.app (Rew.castLE h)) φ⌝ = ⌜φ⌝

theorem LO.FirstOrder.Semiformula.freeVariables_castLE {L : Language} {n : ℕ} (φ : Semiformula L ℕ n) {n' : ℕ} (h : n ≤ n') : ((Rewriting.app (Rew.castLE h)) φ).freeVariables = φ.freeVariables

The bv-pin bridge

The recognizer pins the number of leading universals m to fvSup of the core formula via a clause forcing bv b = m. Soundness of that pin rests on the bridge below: the freevar-free universal-closure body uses exactly fvSup χ bound slots, so closing fewer than fvSup χ quantifiers cannot reach a sentence — forbidding over-recognition by vacuous leading ∀s.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.bv_quote_fixitr {L : Language} [L.Encodable] [L.LORDefinable] (χ : FirstOrder.Semiformula L ℕ 0) : bv L ⌜(Rewriting.app (Rew.fixitr 0 χ.fvSup)) χ⌝ = χ.fvSup

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 γ ⇜ ![&0, …, &(j-1)] with γ free-variable-free, forcing fvSup χ ≤ j < fvSup χ.

Internal free-variable vector fvarVec

fvarVec k = ⟨^&0, ^&1, …, ^&(k-1)⟩, the code of the substitution vector mapping bound var #i to free var &i. The recognizer applies subst (fvarVec m) · to invert the universal closure (undo fixitr), recovering ⌜succInd ψ⌝ from the freevar-free body — see quote_subst_fvar_fixitr. This is a 𝚺₁ vector recursion (fvarVec (k+1) = concat (fvarVec k) (^&k)).

def LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec.blueprint : PR.Blueprint 0

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : PR.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : V

fvarVec k = ⟨^&0, …, ^&(k-1)⟩.

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec k = LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec.construction.result ![] k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : fvarVec 0 = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : fvarVec (k + 1) = concat (fvarVec k) (qqFvar k)

def LO.FirstOrder.Arithmetic.fvarVecDef : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arithmetic.fvarVecDef = LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec.blueprint.resultDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ fvarVec via fvarVecDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ fvarVec

instance LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m : ℕ} (Γ : SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Function₁ fvarVec

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.len_fvarVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : len (fvarVec k) = k

theorem LO.FirstOrder.Arithmetic.Bootstrapping.nth_fvarVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k i : V) : i < k → nth (fvarVec k) i = qqFvar i

fvarVec k is the vector with i-th entry ^&i for i < k.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec_val_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (m : ℕ) : fvarVec ↑m = SemitermVec.val fun (i : Fin m) => Semiterm.fvar ↑↑i

fvarVec is the code of the typed substitution vector fun i ↦ ^&i (over a standard length).

theorem LO.FirstOrder.Arithmetic.Bootstrapping.subst_fvarVec_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (φ : ArithmeticSemiformula ℕ 0) : subst ℒₒᵣ (fvarVec ↑(0 + Semiformula.fvSup φ)) ⌜(Rewriting.app (Rew.fixitr 0 (Semiformula.fvSup φ))) φ⌝ = ⌜φ⌝

Raw closure inversion. subst (fvarVec (fvSup φ)) ⌜fixitr 0 (fvSup φ) ▹ φ⌝ = ⌜φ⌝: the internal substitution by fvarVec undoes the universal-closure fixitr at the code level. This is the recognizer's mechanism for recovering ⌜succInd ψ⌝ from the freevar-free closure body.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.subst_fvarVec_quote' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m : ℕ} (β : ArithmeticSemiformula ℕ m) : subst ℒₒᵣ (fvarVec ↑m) ⌜β⌝ = ⌜β ⇜ fun (i : Fin m) => FirstOrder.Semiterm.fvar ↑i⌝

Generalized free-ization. For any β : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ m, substituting the free-variable atoms &0 … &(m-1) for its m bound slots equals ⌜β ⇜ (&·)⌝. This is the forward recognizer's tool: once IsSemiformula.sound yields a β with ⌜β⌝ = b, this computes subst (fvarVec m) b. (Specializes to subst_fvarVec_quote when β is a fixitr-image.)

Σ₁ side condition: internal IsSigma1 predicate (for C = Hierarchy 𝚺 1)

IsSigma1 p recognizes codes of 𝚺₁ formulas over ℒₒᵣ. By Hierarchy.sigma₁_induction', over ℒₒᵣ a formula is 𝚺₁ iff built from atoms (=,≠,<,≮,⊤,⊥) by ∧, ∨, (unbounded) ∃, and bounded ∀ ∀¹[“#0 < !!(bShift t)”] φ, whose body desugars to (^#0 ^≮ u) ^⋎ φ with u = termBShift t. The recognizer is applied to a code already known to be a semiformula, so atoms are matched purely structurally (no IsUTermVec guard). Positivity (u is a bShift-image) is Δ₁: termBShift only grows codes (le_termBShift), so ∃ t < u+1, u = termBShift t is a bounded ∃ over the Δ₁ graph termBShiftGraph.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.le_termBShift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsUTerm L t) : t ≤ termBShift L t

termBShift only grows codes: t ≤ termBShift t for well-formed terms. The ^#z → ^#(z+1) bvar shift grows, ^&x is fixed, and functions recurse componentwise. Bounds the ∃ t guard in the bounded-∀ clause.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.termBShift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsUTerm L t) : IsUTerm L (Bootstrapping.termBShift L t)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.termBShiftVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k v : V} (hv : IsUTermVec L k v) : IsUTermVec L k (Bootstrapping.termBShiftVec L k v)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBV_termBShift_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsUTerm L t) (m : V) : termBV L (termBShift L t) ≤ m + 1 ↔ termBV L t ≤ m

termBShift shifts the bound-variable depth up by exactly one (on well-formed terms): so t is a level-m term iff termBShift t is level-(m+1). The ←-direction recovers the lowered arity, which is how the bounded-∀ bound (a termBShift-image) is recognized as a bShift of a real term of the outer arity.

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqBall {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (u q : V) : V

Internal bounded-∀ code: qqBall u q = ^∀ ((^#0 ^≮ u) ^⋎ q), the code of ∀¹[“#0 < u”] q. Packaged as a single 𝚺₁-function (mirroring qqNLT/qqRel) so the IsSigma1 fixpoint clause is flat.

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_q_qqBall {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (u q : V) : q < qqBall u q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_u_qqBall {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (u q : V) : u < qqBall u q

def LO.FirstOrder.Arithmetic.qqBallDef : 𝚺₁.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqBall_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ qqBall via qqBallDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqBall_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ qqBall

def LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.Phi {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (C : Set V) (p : V) : Prop

Single-step operator: p is 𝚺₁ given that its immediate subformulas in C are. Atoms carry no well-formedness guard (the recognizer is applied to a code already known to be a semiformula); the bounded-∀ clause requires the bound u to be a termBShift-image of a well-formed term.

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.blueprint : Fixpoint.Blueprint 0

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Fixpoint.Construction V blueprint

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.construction = { Φ := fun (x : Fin 0 → V) => LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.Phi, defined := ⋯, monotone := ⋯ }

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.instStrongFiniteConstruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Fixpoint.Construction.StrongFinite V construction

def LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : Prop

IsSigma1 p: p codes a 𝚺₁ formula over ℒₒᵣ (assuming p is a semiformula).

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1 p = LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.construction.Fixpoint ![] p

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.isSigma1 : 𝚫₁.Semisentence 1

Concrete 𝚫₁-recognizer for IsSigma1.

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.isSigma1 = LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.blueprint.fixpointDefΔ₁

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚫₁-Predicate IsSigma1 via isSigma1

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.case_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {p : V} : IsSigma1 p ↔ p = qqVerum ∨ p = qqFalsum ∨ (∃ (k : V) (r : V) (v : V), p = qqRel k r v) ∨ (∃ (k : V) (r : V) (v : V), p = qqNRel k r v) ∨ (∃ (p₁ : V) (p₂ : V), IsSigma1 p₁ ∧ IsSigma1 p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), IsSigma1 p₁ ∧ IsSigma1 p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), IsSigma1 p₁ ∧ p = qqExs p₁) ∨ ∃ (u : V) (q : V), (∃ (t : V), IsUTerm ℒₒᵣ t ∧ u = termBShift ℒₒᵣ t) ∧ IsSigma1 q ∧ p = qqBall u q

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.case {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {p : V} : IsSigma1 p → p = qqVerum ∨ p = qqFalsum ∨ (∃ (k : V) (r : V) (v : V), p = qqRel k r v) ∨ (∃ (k : V) (r : V) (v : V), p = qqNRel k r v) ∨ (∃ (p₁ : V) (p₂ : V), IsSigma1 p₁ ∧ IsSigma1 p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), IsSigma1 p₁ ∧ IsSigma1 p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), IsSigma1 p₁ ∧ p = qqExs p₁) ∨ ∃ (u : V) (q : V), (∃ (t : V), IsUTerm ℒₒᵣ t ∧ u = termBShift ℒₒᵣ t) ∧ IsSigma1 q ∧ p = qqBall u q

Alias of the forward direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.case_iff.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.mk {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {p : V} : (p = qqVerum ∨ p = qqFalsum ∨ (∃ (k : V) (r : V) (v : V), p = qqRel k r v) ∨ (∃ (k : V) (r : V) (v : V), p = qqNRel k r v) ∨ (∃ (p₁ : V) (p₂ : V), IsSigma1 p₁ ∧ IsSigma1 p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), IsSigma1 p₁ ∧ IsSigma1 p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), IsSigma1 p₁ ∧ p = qqExs p₁) ∨ ∃ (u : V) (q : V), (∃ (t : V), IsUTerm ℒₒᵣ t ∧ u = termBShift ℒₒᵣ t) ∧ IsSigma1 q ∧ p = qqBall u q) → IsSigma1 p

Alias of the reverse direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.case_iff.

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : IsSigma1 qqVerum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.falsum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : IsSigma1 qqFalsum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k r v : V} : IsSigma1 (qqRel k r v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k r v : V} : IsSigma1 (qqNRel k r v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.and_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {p q : V} : IsSigma1 (qqAnd p q) ↔ IsSigma1 p ∧ IsSigma1 q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.or_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {p q : V} : IsSigma1 (qqOr p q) ↔ IsSigma1 p ∧ IsSigma1 q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.ex_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {p : V} : IsSigma1 (qqExs p) ↔ IsSigma1 p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.of_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {p : V} (h : IsSigma1 (qqAll p)) : ∃ (u : V) (q : V), (∃ (t : V), IsUTerm ℒₒᵣ t ∧ u = termBShift ℒₒᵣ t) ∧ IsSigma1 q ∧ p = qqOr (qqBvar 0 ^≮ u) q

Inversion of the bounded-∀ clause: a ^∀-headed 𝚺₁ code is a qqBall.

B1 — 𝗣𝗔⁻ is Δ₁ (it is finite)

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.PeanoMinus.delta1 : Theory.Δ₁ 𝗣𝗔⁻

Equations

• LO.FirstOrder.Arithmetic.PeanoMinus.delta1 = LO.FirstOrder.Theory.Δ₁.ofFinite 𝗣𝗔⁻ LO.FirstOrder.Arithmetic.PeanoMinus.finite

Typed decomposition of succInd

The crux relates the code ⌜univCl (succInd φ)⌝ to internal primitives. The macro !φ t in formula position desugars to φ ⇜ ![t] (Rew.substs, not embSubsts as an earlier handoff claimed), so ⌜succInd φ⌝ collapses under the already-present typed_quote_substs/map_imply/ LCWQIsoGödelQuote.all simp set — no typed_quote_embSubsts bridge is needed.

theorem LO.FirstOrder.Arithmetic.succInd_eq (φ : ArithmeticSemiformula ℕ 1) : succInd φ = φ/[↑0] 🡒 ∀¹ (φ 🡒 φ/[‘(!!(Semiterm.bvar 0) + 1)’]) 🡒 ∀¹ φ

succInd φ, simplified (the ∀ x, !φ x instances are the identity substitution φ ⇜ ![#0]).

theorem LO.FirstOrder.Arithmetic.typed_quote_succInd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (φ : ArithmeticSemiformula ℕ 1) : ⌜succInd φ⌝ = ⌜φ/[↑0]⌝ 🡒 ∀¹ (⌜φ⌝ 🡒 ⌜φ/[‘(!!(Semiterm.bvar 0) + 1)’]⌝) 🡒 ∀¹ ⌜φ⌝

The typed Gödel code of the induction axiom body, built from the typed code ⌜φ⌝ purely with the existing typed constructors (subst, 🡒, ∀¹).

noncomputable def LO.FirstOrder.Arithmetic.indBody {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (K : Bootstrapping.Semiformula V ℒₒᵣ 1) : Bootstrapping.Semiformula V ℒₒᵣ 0

The typed succInd shape as a function of the (typed) core code K = ⌜ψ⌝. The recognizer checks subst (fvarVec m) b = (indBody K).val to recover the core K and verify the body has the induction-axiom shape.

Equations

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

theorem LO.FirstOrder.Arithmetic.indBody_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (φ : ArithmeticSemiformula ℕ 1) : indBody ⌜φ⌝ = ⌜succInd φ⌝

indBody ⌜ψ⌝ = ⌜succInd ψ⌝: the typed reconstruction matches the actual code.

noncomputable def LO.FirstOrder.Arithmetic.indBodyVal {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : V

The raw V → V form of (indBody ·).val — a composition of the 𝚺₁-definable internal operations subst, imp (p ^→ q = ∼p ^⋎ q), ^∀. This is the function the recognizer's clause subst (fvarVec m) b = indBodyVal K uses (K a code with IsSemiformula ℒₒᵣ 1 K); it is the target of the eventual 𝚺₁-graph for the ch assembly.

Equations

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

theorem LO.FirstOrder.Arithmetic.indBodyVal_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (K : Bootstrapping.Semiformula V ℒₒᵣ 1) : indBodyVal K.val = (indBody K).val

indBodyVal K.val = (indBody K).val: the raw function computes the typed indBody.

theorem LO.FirstOrder.Arithmetic.le_indBodyVal {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : k ≤ indBodyVal k

k ≤ indBodyVal k: the core k sits as the bound body of the ^∀ k conclusion inside the succInd shape, so its code is below the whole axiom's code. This is the clean half of the old size race — it bounds the recovered core K by the (functionally pinned) subst (fvarVec m) b, which equals indBodyVal K.

theorem LO.FirstOrder.Arithmetic.indBodyVal_quote (γ : ArithmeticSemiformula ℕ 1) : indBodyVal ⌜γ⌝ = ⌜succInd γ⌝

indBodyVal ⌜γ⌝ = ⌜succInd γ⌝: the raw recognizer body computes the succInd shape.

instance LO.FirstOrder.Arithmetic.indBodyVal_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ indBodyVal

A concrete 𝚺₁-graph for indBodyVal

The definability tactic above only gives a Prop-level Definable witness; the ch assembly needs an extractable 𝚺₁.Semisentence with a via correctness instance, mirroring impGraph / iffGraph. The two substitution constants are the standard codes of the closed substitution vectors ![⌜‘0’⌝] and ![⌜‘#0+1’⌝]; their absoluteness (↑constant = SemitermVec.val …) is LO.FirstOrder.Semiterm.quote_eq_encode'.

def LO.FirstOrder.Arithmetic.indSubstConst0 : ℕ

Standard ℕ-code of the substitution vector ![⌜‘0’⌝] (the ψ(0) instance).

Equations

• LO.FirstOrder.Arithmetic.indSubstConst0 = Matrix.vecToNat fun (i : Fin 1) => Encodable.encode (![↑0] i)

def LO.FirstOrder.Arithmetic.indSubstConst1 : ℕ

Standard ℕ-code of the substitution vector ![⌜‘#0+1’⌝] (the ψ(x+1) instance).

Equations

• LO.FirstOrder.Arithmetic.indSubstConst1 = Matrix.vecToNat fun (i : Fin 1) => Encodable.encode (![‘(!!(LO.FirstOrder.Semiterm.bvar 0) + 1)’] i)

theorem LO.FirstOrder.Arithmetic.val_indSubstConst0 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ↑indSubstConst0 = Bootstrapping.SemitermVec.val ![⌜↑0⌝]

theorem LO.FirstOrder.Arithmetic.val_indSubstConst1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ↑indSubstConst1 = Bootstrapping.SemitermVec.val ![⌜‘(!!(Semiterm.bvar 0) + 1)’⌝]

noncomputable def LO.FirstOrder.Arithmetic.indBodyValGraph : 𝚺₁.Semisentence 2

Concrete 𝚺₁-graph of indBodyVal, a chain of the subst/imp/qqAll graphs.

Equations

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

instance LO.FirstOrder.Arithmetic.indBodyVal.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ indBodyVal via indBodyValGraph

The crux — the induction schema is Δ₁

We build a concrete recognizer ch : 𝚫₁.Semisentence 1 whose ℕ-extension recognizes exactly the codes ⌜univCl (succInd ψ)⌝. The recognizer:

R(p) := ∃ m ≤ p, ∃ b ≤ p,
   p = qqAlls b m  ∧  IsUFormula b ∧ shift b = b  ∧  bv b = m
 ∧ ∃ K ≤ subst (fvarVec m) b, IsSemiformula 1 K
   ∧ subst (fvarVec m) b = indBodyVal K

bv b = m pins m = fvSup, forbidding over-recognition by padding leading ∀s (bv_quote_fixitr); the last clause recovers ⌜succInd ψ⌝ from the freevar-free body b.

def LO.FirstOrder.Arithmetic.InductionUnivR {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : Prop

The recognizer predicate for InductionScheme ℒₒᵣ Set.univ over a model V.

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.chUniv : 𝚫₁.Semisentence 1

Concrete 𝚫₁.Semisentence 1 recognizer for the universal induction scheme.

Equations

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

instance LO.FirstOrder.Arithmetic.InductionUnivR.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚫₁-Predicate InductionUnivR via chUniv

The crux — the induction schema is Δ₁

theorem LO.FirstOrder.Arithmetic.mem_inductionScheme_univ_iff (φ : ArithmeticSemiformula ℕ 0) : (∃ σ ∈ InductionScheme ℒₒᵣ Set.univ, φ = Rewriting.emb σ) ↔ ∃ (ψ : ArithmeticSemiformula ℕ 1), φ = Semiformula.univCl' (succInd ψ)

RHS of chUniv_mem_iff reduced to a clean ∃ψ over the syntactic universal closure.

theorem LO.FirstOrder.Arithmetic.closure_inversion {m : ℕ} (β : ArithmeticSemiformula ℕ m) (γ : ArithmeticSemiformula ℕ 1) (hfree : Semiformula.freeVariables β = ∅) (hbv : Bootstrapping.bv ℒₒᵣ ⌜β⌝ = m) (hβγ : (β ⇜ fun (i : Fin m) => Semiterm.fvar ↑i) = succInd γ) : ∀¹* β = Semiformula.univCl' (succInd γ)

Closure inversion (forward keystone). A freevar-free level-m formula β whose internal bv is m and which substitutes back to succInd γ is exactly the fixitr-image, so its m-fold closure is (succInd γ).univCl'. Mirror of bv_quote_fixitr's ≥-direction inversion; the genuine remaining math.

theorem LO.FirstOrder.Arithmetic.chUniv_mem_iff (φ : ArithmeticSemiformula ℕ 0) : InductionUnivR ⌜φ⌝ ↔ ∃ σ ∈ InductionScheme ℒₒᵣ Set.univ, φ = Rewriting.emb σ

mem_iff math (C = univ). The recognizer fires on ⌜φ⌝ exactly when φ is the universal closure of succInd ψ for some one-variable ψ. Forward inverts via IsSemiformula.sound + closure_inversion; backward composes quote_univCl'/subst_fvarVec_quote'/indBodyVal_quote.

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.InductionScheme.delta1_univ : (InductionScheme ℒₒᵣ Set.univ).Δ₁

The induction schema InductionScheme ℒₒᵣ Set.univ is Δ₁, via the recognizer chUniv.

Equations

• LO.FirstOrder.Arithmetic.InductionScheme.delta1_univ = { ch := LO.FirstOrder.Arithmetic.chUniv, mem_iff := ⋯, isDelta1 := LO.FirstOrder.Arithmetic.InductionScheme.delta1_univ._proof_1 }

Correctness of IsSigma1: IsSigma1 ⌜ψ⌝ ↔ Hierarchy 𝚺 1 ψ

theorem LO.FirstOrder.Arithmetic.quote_ball {n : ℕ} (t : SyntacticSemiterm ℒₒᵣ n) (φ : ArithmeticSemiformula ℕ (n + 1)) : ⌜“(∀¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”⌝ = Bootstrapping.qqBall (Bootstrapping.termBShift ℒₒᵣ ⌜t⌝) ⌜φ⌝

The code of the bounded universal ∀¹[#0 < bShift t] φ is qqBall (termBShift ⌜t⌝) ⌜φ⌝.

theorem LO.FirstOrder.Arithmetic.termBShift_quote {n : ℕ} (s : SyntacticSemiterm ℒₒᵣ n) : ⌜Rew.bShift s⌝ = Bootstrapping.termBShift ℒₒᵣ ⌜s⌝

The raw code of bShift s is termBShift ⌜s⌝.

theorem LO.FirstOrder.Arithmetic.isSigma1_of_hierarchy {n : ℕ} {ψ : ArithmeticSemiformula ℕ n} (h : Hierarchy 𝚺 1 ψ) : Bootstrapping.IsSigma1 ⌜ψ⌝

(⟸) Every 𝚺₁ formula has a 𝚺₁-recognized code. By sigma₁_induction'.

theorem LO.FirstOrder.Arithmetic.hierarchy_of_isSigma1 {n : ℕ} (ψ : ArithmeticSemiformula ℕ n) : Bootstrapping.IsSigma1 ⌜ψ⌝ → Hierarchy 𝚺 1 ψ

(⟹) A 𝚺₁-recognized code is the code of a 𝚺₁ formula. Meta-induction on the formula: atoms are 𝚺₁ unconditionally; ∧/∨/∃ recurse; the ^∀ case is forced into the bounded shape by the recognizer (IsSigma1.of_all), and the bound is a bShift-image (positivity via termBV_termBShift_le), so Hierarchy.ball applies.

theorem LO.FirstOrder.Arithmetic.isSigma1_iff_hierarchy {n : ℕ} (ψ : ArithmeticSemiformula ℕ n) : Bootstrapping.IsSigma1 ⌜ψ⌝ ↔ Hierarchy 𝚺 1 ψ

Correctness of the 𝚺₁-code recognizer: IsSigma1 ⌜ψ⌝ ↔ Hierarchy 𝚺 1 ψ.

The C = Hierarchy 𝚺 1 recognizer = chUniv + the IsSigma1 K side condition

def LO.FirstOrder.Arithmetic.InductionSigma1R {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : Prop

The recognizer for InductionScheme ℒₒᵣ (Hierarchy 𝚺 1): InductionUnivR plus the side condition IsSigma1 K on the recovered core K.

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.chSigma1 : 𝚫₁.Semisentence 1

Concrete 𝚫₁.Semisentence 1 recognizer for the 𝚺₁ induction scheme.

Equations

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

instance LO.FirstOrder.Arithmetic.InductionSigma1R.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚫₁-Predicate InductionSigma1R via chSigma1

theorem LO.FirstOrder.Arithmetic.mem_inductionScheme_sigma1_iff (φ : ArithmeticSemiformula ℕ 0) : (∃ σ ∈ InductionScheme ℒₒᵣ (Hierarchy 𝚺 1), φ = Rewriting.emb σ) ↔ ∃ (ψ : ArithmeticSemiformula ℕ 1), Hierarchy 𝚺 1 ψ ∧ φ = Semiformula.univCl' (succInd ψ)

RHS of chSigma1_mem_iff reduced to a clean ∃ψ (with the 𝚺₁ side condition).

theorem LO.FirstOrder.Arithmetic.chSigma1_mem_iff (φ : ArithmeticSemiformula ℕ 0) : InductionSigma1R ⌜φ⌝ ↔ ∃ σ ∈ InductionScheme ℒₒᵣ (Hierarchy 𝚺 1), φ = Rewriting.emb σ

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

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.InductionScheme.delta1_sigma1 : (InductionScheme ℒₒᵣ (Hierarchy 𝚺 1)).Δ₁

The induction schema InductionScheme ℒₒᵣ (Hierarchy 𝚺 1) is Δ₁, via chSigma1.

Equations

• LO.FirstOrder.Arithmetic.InductionScheme.delta1_sigma1 = { ch := LO.FirstOrder.Arithmetic.chSigma1, mem_iff := ⋯, isDelta1 := LO.FirstOrder.Arithmetic.InductionScheme.delta1_sigma1._proof_1 }

B2 / B3 — assemble the headline instances

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.PA_delta1Definable : Theory.Δ₁ 𝗣𝗔

Equations

• LO.FirstOrder.Arithmetic.PA_delta1Definable = LO.FirstOrder.Arithmetic.PeanoMinus.delta1.add LO.FirstOrder.Arithmetic.InductionScheme.delta1_univ

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.ISigma1_delta1Definable : Theory.Δ₁ 𝗜𝚺₁

Equations

• LO.FirstOrder.Arithmetic.ISigma1_delta1Definable = LO.FirstOrder.Arithmetic.PeanoMinus.delta1.add LO.FirstOrder.Arithmetic.InductionScheme.delta1_sigma1