Supporting results for pointwise provable equality.

Definability of arithmetical syntax

This file constructs internal recognizers for arithmetical syntax and recursively enumerable presentations of 𝐏𝐀 and 𝐈Σ₁.

Internal iterated universal quantifier qqAlls

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

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.qqAlls.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqAlls.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : PR.Construction V blueprint

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.qqAlls.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (p k : V) : V

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

Equations

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.qqAllsDef : Σ₁.Semisentence 3

The qq Alls Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

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

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

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.le_qqAlls {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (p k : V) : p ≤ qqAlls p k

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_fvSup_pred {L : Language} {n : ℕ} (φ : Semiproposition L n) (h : 0 < fvSup φ) : HasFreeVariable φ (fvSup φ - 1)

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

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.not_hasFreeVariable_fixitr {L : Language} (χ : Semiproposition L 0) (x : ℕ) : ¬Semiformula.HasFreeVariable ((Rewriting.app (Rew.fixitr 0 (Semiformula.fvSup χ))) χ) x

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.fvarVec.blueprint : PR.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.fvarVec.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.fvarVec.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : PR.Construction V blueprint

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.fvarVec.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.fvarVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (k : V) : V

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

Equations

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

@[simp]

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

@[simp]

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.fvarVecDef : Σ₁.Semisentence 2

The fvar Vec Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

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

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

@[simp]

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.lt_q_qqBall {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (u q : V) : q < qqBall u q

@[simp]

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.qqBallDef : Σ₁.Semisentence 3

The qq Ball Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

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

def PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.blueprint : Fixpoint.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.

Equations

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

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

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.IsSigma1F.

Equations

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

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

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

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

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

Concrete ∆₁-recognizer for IsSigma1.

Equations

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.delta1 : Theory.Δ₁ 𝐏𝐀⁻

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.delta1 = PointwiseComposition.FFL.FirstOrder.Theory.Δ₁.ofFinite 𝐏𝐀⁻ PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.finite

Typed decomposition of succInd

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

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

noncomputable def PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.indBody_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (φ : ArithmeticSemiproposition 1) : indBody ⌜φ⌝ = ⌜succInd φ⌝

noncomputable def PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.indBodyVal_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (K : Bootstrapping.Semiformula V ℒₒᵣ 1) : indBodyVal K.val = (indBody K).val

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

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

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

A concrete Σ₁-graph for indBodyVal

def PointwiseComposition.FFL.FirstOrder.Arithmetic.indSubstConst0 : ℕ

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

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.indSubstConst1 : ℕ

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

Equations

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

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

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

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

The induction schema is Δ₁

def PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.chUniv : ∆₁.Semisentence 1

The ch Univ construction in FFL.FirstOrder.Arithmetic.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.chSigma1 : ∆₁.Semisentence 1

The ch Sigma1 construction in FFL.FirstOrder.Arithmetic.

Equations

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

instance PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionR.univ_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : ∆₁-Predicate InductionR fun (x : V) => True via chUniv

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

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionScheme.delta1Univ : (InductionScheme ℒₒᵣ Set.univ).Δ₁

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

Equations

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

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

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

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

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

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

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

Correctness of the Σ₁-code recognizer.

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionScheme.delta1Sigma1 : (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 PointwiseComposition.FFL.FirstOrder.Arithmetic.inductionScheme_re_univ : REPred fun (x : Sentence ℒₒᵣ) => x ∈ InductionScheme ℒₒᵣ Set.univ

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

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

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instREPeano : Theory.RE 𝐏𝐀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instREISigmaOfNatNat : Theory.RE 𝐈Σ₁

𝐏𝐀 and 𝐈Σ₁ are Δ₁

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

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instΔ₁Peano : Theory.Δ₁ 𝐏𝐀

Equations

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

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instΔ₁ISigmaOfNatNat : Theory.Δ₁ 𝐈Σ₁

Equations

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