Fixpoint Construction #
instance
LO.Arith.Fixpoint.Blueprint.instCoeSemisentenceDeltaOneHAddNatOfNat
{k : ℕ}
:
Coe (LO.Arith.Fixpoint.Blueprint k) (𝚫₁.Semisentence (k + 2))
Equations
- LO.Arith.Fixpoint.Blueprint.instCoeSemisentenceDeltaOneHAddNatOfNat = { coe := LO.Arith.Fixpoint.Blueprint.core }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- φ.prBlueprint = { zero := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (“!!(LO.FirstOrder.Semiterm.bvar 0) = 0”) ⋯, succ := φ.succDef }
Instances For
Equations
- φ.limSeqDef = φ.prBlueprint.resultDef
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
LO.Arith.Fixpoint.Construction
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
(φ : LO.Arith.Fixpoint.Blueprint k)
:
Type u_1
- defined : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ.succ → V) => self.Φ (fun (x : Fin k) => v x.succ.succ) {x : V | x ∈ v 1} (v 0)) φ.core
Instances For
theorem
LO.Arith.Fixpoint.Construction.defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(self : LO.Arith.Fixpoint.Construction V φ)
:
LO.FirstOrder.Arith.HierarchySymbol.Defined
(fun (v : Fin k.succ.succ → V) => self.Φ (fun (x : Fin k) => v x.succ.succ) {x : V | x ∈ v 1} (v 0)) φ.core
theorem
LO.Arith.Fixpoint.Construction.monotone
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(self : LO.Arith.Fixpoint.Construction V φ)
{C : Set V}
{C' : Set V}
(h : C ⊆ C')
{v : Fin k → V}
{x : V}
:
self.Φ v C x → self.Φ v C' x
class
LO.Arith.Fixpoint.Construction.Finite
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
:
Instances
theorem
LO.Arith.Fixpoint.Construction.Finite.finite
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
{c : LO.Arith.Fixpoint.Construction V φ}
[self : LO.Arith.Fixpoint.Construction.Finite V c]
{C : Set V}
{v : Fin k → V}
{x : V}
:
class
LO.Arith.Fixpoint.Construction.StrongFinite
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
:
Instances
theorem
LO.Arith.Fixpoint.Construction.StrongFinite.strong_finite
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
{c : LO.Arith.Fixpoint.Construction V φ}
[self : LO.Arith.Fixpoint.Construction.StrongFinite V c]
{C : Set V}
{v : Fin k → V}
{x : V}
:
instance
LO.Arith.Fixpoint.instFiniteOfStrongFinite
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
[LO.Arith.Fixpoint.Construction.StrongFinite V c]
:
Equations
- LO.Arith.Fixpoint.instFiniteOfStrongFinite V c = { finite := ⋯ }
theorem
LO.Arith.Fixpoint.Construction.eval_formula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
(v : Fin k.succ.succ → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.core) ↔ c.Φ (fun (x : Fin k) => v x.succ.succ) {x : V | x ∈ v 1} (v 0)
theorem
LO.Arith.Fixpoint.Construction.succ_existsUnique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
(v : Fin k → V)
(s : V)
(ih : V)
:
def
LO.Arith.Fixpoint.Construction.succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
(v : Fin k → V)
(s : V)
(ih : V)
:
V
Equations
- c.succ v s ih = Classical.choose! ⋯
Instances For
theorem
LO.Arith.Fixpoint.Construction.mem_succ_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{x : V}
{v : Fin k → V}
{s : V}
{ih : V}
:
theorem
LO.Arith.Fixpoint.Construction.succ_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction
(fun (v : Fin (k + 2) → V) => c.succ (fun (x : Fin k) => v x.succ.succ) (v 1) (v 0)) φ.succDef
theorem
LO.Arith.Fixpoint.Construction.eval_succDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
(v : Fin (k + 3) → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.succDef) ↔ v 0 = c.succ (fun (x : Fin k) => v x.succ.succ.succ) (v 2) (v 1)
def
LO.Arith.Fixpoint.Construction.prConstruction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
:
LO.Arith.PR.Construction V φ.prBlueprint
Equations
Instances For
def
LO.Arith.Fixpoint.Construction.limSeq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
(v : Fin k → V)
(s : V)
:
V
Equations
- c.limSeq v s = c.prConstruction.result v s
Instances For
@[simp]
theorem
LO.Arith.Fixpoint.Construction.limSeq_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
:
theorem
LO.Arith.Fixpoint.Construction.limSeq_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
(s : V)
:
theorem
LO.Arith.Fixpoint.Construction.termSet_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction
(fun (v : Fin k.succ → V) => c.limSeq (fun (x : Fin k) => v x.succ) (v 0)) φ.limSeqDef
@[simp]
theorem
LO.Arith.Fixpoint.Construction.eval_limSeqDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
(v : Fin (k + 2) → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.limSeqDef) ↔ v 0 = c.limSeq (fun (x : Fin k) => v x.succ.succ) (v 1)
instance
LO.Arith.Fixpoint.Construction.limSeq_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
:
Equations
- ⋯ = ⋯
@[simp]
instance
LO.Arith.Fixpoint.Construction.limSeq_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{m : ℕ}
(Γ : LO.SigmaPiDelta)
:
Equations
- ⋯ = ⋯
theorem
LO.Arith.Fixpoint.Construction.mem_limSeq_succ_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
{x : V}
{s : V}
:
theorem
LO.Arith.Fixpoint.Construction.limSeq_cumulative
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
{s : V}
{s' : V}
:
theorem
LO.Arith.Fixpoint.Construction.mem_limSeq_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
[LO.Arith.Fixpoint.Construction.StrongFinite V c]
{u : V}
{s : V}
:
def
LO.Arith.Fixpoint.Construction.Fixpoint
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
(v : Fin k → V)
(x : V)
:
Instances For
theorem
LO.Arith.Fixpoint.Construction.fixpoint_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
[LO.Arith.Fixpoint.Construction.StrongFinite V c]
{x : V}
:
theorem
LO.Arith.Fixpoint.Construction.fixpoint_iff_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
{x : V}
:
theorem
LO.Arith.Fixpoint.Construction.finite_upperbound
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
(m : V)
:
∃ (s : V), ∀ z < m, c.Fixpoint v z → z ∈ c.limSeq v s
theorem
LO.Arith.Fixpoint.Construction.case
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
{x : V}
[LO.Arith.Fixpoint.Construction.Finite V c]
:
c.Fixpoint v x ↔ c.Φ v {z : V | c.Fixpoint v z} x
theorem
LO.Arith.Fixpoint.Construction.fixpoint_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
:
LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ → V) => c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0))
φ.fixpointDef
@[simp]
theorem
LO.Arith.Fixpoint.Construction.eval_fixpointDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
(v : Fin (k + 1) → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.fixpointDef) ↔ c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0)
theorem
LO.Arith.Fixpoint.Construction.fixpoint_definedΔ₁
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
[LO.Arith.Fixpoint.Construction.StrongFinite V c]
:
LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ → V) => c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0))
φ.fixpointDefΔ₁
@[simp]
theorem
LO.Arith.Fixpoint.Construction.eval_fixpointDefΔ₁
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
[LO.Arith.Fixpoint.Construction.StrongFinite V c]
(v : Fin (k + 1) → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.fixpointDefΔ₁) ↔ c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0)
theorem
LO.Arith.Fixpoint.Construction.induction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
{φ : LO.Arith.Fixpoint.Blueprint k}
(c : LO.Arith.Fixpoint.Construction V φ)
{v : Fin k → V}
{Γ : LO.SigmaPiDelta}
[LO.Arith.Fixpoint.Construction.StrongFinite V c]
{P : V → Prop}
(hP : { Γ := Γ, rank := 1 }-Predicate P)
(H : ∀ (C : Set V), (∀ x ∈ C, c.Fixpoint v x ∧ P x) → ∀ (x : V), c.Φ v C x → P x)
(x : V)
:
c.Fixpoint v x → P x