Definability of arithmetical syntax

This file constructs internal recognizers for arithmetical syntax and recursively enumerable presentations of 𝗣𝗔 and 𝗜𝚺₁.

Internal iterated universal quantifier qqAlls

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

Equations

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

noncomputable def FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p k : V) : V

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem FFL.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 FFL.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 FFL.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)

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

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

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

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

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

theorem FFL.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 FFL.FirstOrder.Semiterm.freeVariables_castLE {L : Language} {n : ℕ} (t : SyntacticSemiterm L n) {n' : ℕ} (h : n ≤ n') : ((Rew.castLE h) t).freeVariables = freeVariables t

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

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

The bv-pin bridge

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.not_fvar?_fixitr {L : Language} (χ : Semiproposition L 0) (x : ℕ) : ¬Semiformula.FVar? ((Rewriting.app (Rew.fixitr 0 (Semiformula.fvSup χ))) χ) x

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_shift_fixitr {L : Language} [L.Encodable] [L.LORDefinable] (χ : Semiproposition L 0) : shift L ⌜(Rewriting.app (Rew.fixitr 0 (Semiformula.fvSup χ))) χ⌝ = ⌜(Rewriting.app (Rew.fixitr 0 (Semiformula.fvSup χ))) χ⌝

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

Pins the number of leading universals m recognized by the induction-scheme code to fvSup χ.

Internal free-variable vector fvarVec

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

Equations

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

noncomputable def FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.fvarVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : V

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

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

@[simp]

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

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

theorem FFL.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

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

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

theorem FFL.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

theorem FFL.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 FFL.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 FFL.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

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

qqBall u q = ^∀ ((^#0 ^≮ u) ^⋎ q), the code of ∀¹[“#0 < u”] q.

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

def FFL.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.

Equations

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

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

Equations

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

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

Equations

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

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

def FFL.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

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

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

Concrete 𝚫₁-recognizer for IsSigma1.

Equations

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

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

theorem FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.case_iff.

theorem FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.case_iff.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.ex_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {p : V} : IsSigma1 (qqExs p) ↔ IsSigma1 p

theorem FFL.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

𝗣𝗔⁻ is Δ₁

@[instance_reducible]

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

Equations

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

Typed decomposition of succInd

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

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

noncomputable def FFL.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 = ⌜ψ⌝.

Equations

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

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

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

The raw V → V form of (indBody ·).val.

Equations

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

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

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

theorem FFL.FirstOrder.Arithmetic.indBodyVal_quote (γ : ArithmeticSemiproposition 1) : indBodyVal ⌜γ⌝ = ⌜succInd γ⌝

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

A concrete 𝚺₁-graph for indBodyVal

def FFL.FirstOrder.Arithmetic.indSubstConst0 : ℕ

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

Equations

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

def FFL.FirstOrder.Arithmetic.indSubstConst1 : ℕ

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

Equations

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

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

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

noncomputable def FFL.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 FFL.FirstOrder.Arithmetic.indBodyVal.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ indBodyVal via indBodyValGraph

The induction schema is Δ₁

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

The recognizer predicate for InductionScheme ℒₒᵣ C over a model V, parameterized by a side condition S on the recovered core.

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.chInd (cond : 𝚫₁.Semisentence 1) : 𝚫₁.Semisentence 1

Concrete 𝚫₁.Semisentence 1 recognizer for InductionR cond.

Equations

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

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

Equations

• FFL.FirstOrder.Arithmetic.chUniv = FFL.FirstOrder.Arithmetic.chInd ⊤

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

Equations

• FFL.FirstOrder.Arithmetic.chSigma1 = FFL.FirstOrder.Arithmetic.chInd FFL.FirstOrder.Arithmetic.Bootstrapping.isSigma1

instance FFL.FirstOrder.Arithmetic.InductionR.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {S : V → Prop} {cond : 𝚫₁.Semisentence 1} [hcond : 𝚫₁-Predicate S via cond] : 𝚫₁-Predicate InductionR S via chInd cond

instance FFL.FirstOrder.Arithmetic.InductionR.univ_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚫₁-Predicate InductionR fun (x : V) => True via chUniv

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

theorem FFL.FirstOrder.Arithmetic.mem_inductionScheme_iff {C : ArithmeticSemiproposition 1 → Prop} (φ : ArithmeticSemiproposition 0) : (∃ σ ∈ InductionScheme ℒₒᵣ C, φ = Rewriting.emb σ) ↔ ∃ (ψ : ArithmeticSemiproposition 1), C ψ ∧ φ = Semiformula.univCl' (succInd ψ)

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

A freevar-free, bv-pinned formula β that substitutes back to succInd γ is exactly the fixitr-image, so its m-fold closure equals (succInd γ).univCl'.

theorem FFL.FirstOrder.Arithmetic.inductionR_quote_iff {S : ℕ → Prop} {C : ArithmeticSemiproposition 1 → Prop} (hS : ∀ (γ : ArithmeticSemiproposition 1), S ⌜γ⌝ ↔ C γ) (φ : ArithmeticSemiproposition 0) : InductionR S ⌜φ⌝ ↔ ∃ (ψ : ArithmeticSemiproposition 1), C ψ ∧ φ = Semiformula.univCl' (succInd ψ)

InductionR S fires exactly on codes of universal closures of succInd ψ for ψ with C ψ, given that S correctly recognizes the codes of C-formulas.

@[instance_reducible]

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

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

Equations

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

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

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

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

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

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

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

Correctness of the 𝚺₁-code recognizer.

@[instance_reducible]

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

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

Equations

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

𝗣𝗔 and 𝗜𝚺₁ are recursively enumerable

theorem FFL.FirstOrder.Arithmetic.inductionScheme_re_univ : REPred fun (x : Sentence ℒₒᵣ) => x ∈ InductionScheme ℒₒᵣ Set.univ

theorem FFL.FirstOrder.Arithmetic.inductionScheme_re_sigma1 : REPred fun (x : Sentence ℒₒᵣ) => x ∈ InductionScheme ℒₒᵣ (Hierarchy 𝚺 1)

instance FFL.FirstOrder.Arithmetic.instREInductionSchemeORingUnivSemiformulaNatOfNat : (InductionScheme ℒₒᵣ Set.univ).RE

instance FFL.FirstOrder.Arithmetic.instREInductionSchemeORingHierarchyNatSigmaPolarityOfNat : (InductionScheme ℒₒᵣ (Hierarchy 𝚺 1)).RE

instance FFL.FirstOrder.Arithmetic.instREPeano : Theory.RE 𝗣𝗔

instance FFL.FirstOrder.Arithmetic.instREISigmaOfNatNat : Theory.RE 𝗜𝚺₁

𝗣𝗔 and 𝗜𝚺₁ are Δ₁

TODO: remove. Not mathematically essential — RE above already suffices.

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Arithmetic.instΔ₁Peano : Theory.Δ₁ 𝗣𝗔

Equations

• FFL.FirstOrder.Arithmetic.instΔ₁Peano = FFL.FirstOrder.Arithmetic.PeanoMinus.delta1.add FFL.FirstOrder.Arithmetic.InductionScheme.delta1_univ

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Arithmetic.instΔ₁ISigmaOfNatNat : Theory.Δ₁ 𝗜𝚺₁

Equations

• FFL.FirstOrder.Arithmetic.instΔ₁ISigmaOfNatNat = FFL.FirstOrder.Arithmetic.PeanoMinus.delta1.add FFL.FirstOrder.Arithmetic.InductionScheme.delta1_sigma1