Prenex normal form for the arithmetical hierarchy #
For 𝗕𝚺 s ⪯ T, every Hierarchy Γ s formula φ is T-provably equivalent to φ₀.toPrenex Γ s
for some φ₀ : ArithmeticSemisentence (n + s) in Hierarchy 𝚺 0.
References #
- [HP98]
A formula in Γ-prenex form of level s, stored as the 𝚺₀ matrix that remains after
stripping the s leading alternating quantifiers.
- matrix : HierarchySymbol.Semiformula ξ (n + s) 𝚺₀
Instances For
def
FFL.FirstOrder.Arithmetic.Prenex.val
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
(φ : Prenex Γ s ξ n)
:
Equations
- ↑φ = FFL.FirstOrder.Semiformula.toPrenex Γ s ↑φ.matrix
Instances For
@[instance_reducible]
instance
FFL.FirstOrder.Arithmetic.Prenex.instCoeTCArithmeticSemiformula
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
:
CoeTC (Prenex Γ s ξ n) (ArithmeticSemiformula ξ n)
@[instance_reducible]
instance
FFL.FirstOrder.Arithmetic.Prenex.instHTildeAlt
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
:
Equations
def
FFL.FirstOrder.Arithmetic.Prenex.ofΔ₀
{ξ : Type u_1}
{n : ℕ}
(φ : HierarchySymbol.Semiformula ξ n 𝚺₀)
(Γ : Polarity)
(s : ℕ)
:
Prenex Γ s ξ n
Equations
- FFL.FirstOrder.Arithmetic.Prenex.ofΔ₀ φ x✝ 0 = { matrix := φ }
- FFL.FirstOrder.Arithmetic.Prenex.ofΔ₀ φ x✝ s.succ = ⋯.mp (FFL.FirstOrder.Arithmetic.Prenex.ofΔ₀ φ x✝.alt s).altUp
Instances For
def
FFL.FirstOrder.Arithmetic.Prenex.rel
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n k : ℕ}
(r : ℒₒᵣ.Rel k)
(v : Fin k → ArithmeticSemiterm ξ n)
:
Prenex Γ s ξ n
Equations
Instances For
def
FFL.FirstOrder.Arithmetic.Prenex.nrel
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n k : ℕ}
(r : ℒₒᵣ.Rel k)
(v : Fin k → ArithmeticSemiterm ξ n)
:
Prenex Γ s ξ n
Equations
Instances For
@[simp]
theorem
FFL.FirstOrder.Arithmetic.Prenex.val_strictHierarchy
{Γ : Polarity}
{s n : ℕ}
{ξ : Type u_5}
{φ : Prenex Γ s ξ n}
:
StrictHierarchy Γ s ↑φ
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_sigmaInv
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
(φ : Prenex 𝚺 (s + 1) ξ n)
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_piInv
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
(φ : Prenex 𝚷 (s + 1) ξ n)
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_sigma
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
(φ : Prenex 𝚷 s ξ (n + 1))
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_pi
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
(φ : Prenex 𝚺 s ξ (n + 1))
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_altUp
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
(φ : Prenex Γ s ξ n)
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_ofΔ₀
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
(φ : HierarchySymbol.Semiformula ξ n 𝚺₀)
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_verum
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_falsum
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_rel
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
{k : ℕ}
(r : ℒₒᵣ.Rel k)
(v : Fin k → ArithmeticSemiterm ξ n)
(e : Fin n → V)
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_nrel
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{V : Type u_4}
[ORingStructure V]
{f : ξ → V}
{k : ℕ}
(r : ℒₒᵣ.Rel k)
(v : Fin k → ArithmeticSemiterm ξ n)
(e : Fin n → V)
:
@[irreducible]
def
FFL.FirstOrder.Arithmetic.Prenex.ball
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
:
ArithmeticSemiterm ξ n → Prenex Γ s ξ (n + 1) → Prenex Γ s ξ n
Equations
- One or more equations did not get rendered due to their size.
- FFL.FirstOrder.Arithmetic.Prenex.ball x✝¹ x✝ = ∼FFL.FirstOrder.Arithmetic.Prenex.bexs x✝¹ (∼x✝)
Instances For
@[irreducible]
def
FFL.FirstOrder.Arithmetic.Prenex.bexs
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
:
ArithmeticSemiterm ξ n → Prenex Γ s ξ (n + 1) → Prenex Γ s ξ n
Equations
- One or more equations did not get rendered due to their size.
- FFL.FirstOrder.Arithmetic.Prenex.bexs x✝¹ x✝ = ∼FFL.FirstOrder.Arithmetic.Prenex.ball x✝¹ (∼x✝)
Instances For
@[simp]
theorem
FFL.FirstOrder.Arithmetic.Prenex.ball_zero
{Γ : Polarity}
{ξ : Type u_1}
{n : ℕ}
{u : ArithmeticSemiterm ξ n}
{φ : Prenex Γ 0 ξ (n + 1)}
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.ball_succ_sigma
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{u : ArithmeticSemiterm ξ n}
{φ : Prenex 𝚺 (s + 1) ξ (n + 1)}
:
@[simp]
theorem
FFL.FirstOrder.Arithmetic.Prenex.bexs_zero
{Γ : Polarity}
{ξ : Type u_1}
{n : ℕ}
{u : ArithmeticSemiterm ξ n}
{φ : Prenex Γ 0 ξ (n + 1)}
:
theorem
FFL.FirstOrder.Arithmetic.Prenex.bexs_succ_sigma
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
{u : ArithmeticSemiterm ξ n}
{φ : Prenex 𝚺 (s + 1) ξ (n + 1)}
:
bexs u φ = (bexs (Rew.bShift u)
(φ.sigmaInv.rew
(Rew.subst (Semiterm.bvar 1 :> Semiterm.bvar 0 :> fun (x : Fin n) => Semiterm.bvar x.succ.succ)))).sigma
@[irreducible]
Equations
Instances For
@[irreducible]
Equations
Instances For
@[instance_reducible]
instance
FFL.FirstOrder.Arithmetic.Prenex.instHWedge
{Γ : Polarity}
{s : ℕ}
{ξ : Type u_1}
{n : ℕ}
:
Equations
@[instance_reducible]
Equations
theorem
FFL.FirstOrder.Arithmetic.Prenex.models_exists_prenex
{ξ : Type u_1}
{Γ Γ' : Polarity}
{s n : ℕ}
{φ : ArithmeticSemiformula ξ n}
(h : Hierarchy Γ s φ)
:
∃ (φ' : Prenex Γ s ξ n),
∀ (V : Type u_5) [inst : ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗕 Γ' s] (e : Fin n → V) (f : ξ → V),
(Semiformula.Eval e f) φ ↔ (Semiformula.Eval e f) ↑φ'
theorem
FFL.FirstOrder.Arithmetic.exists_prenex_of_hierarchy
{Γ : Polarity}
{s : ℕ}
(T : ArithmeticTheory)
[𝗕𝚺s ⪯ T]
{n : ℕ}
{φ : ArithmeticSemisentence n}
(h : Hierarchy Γ s φ)
:
theorem
FFL.FirstOrder.Arithmetic.exists_matrix_provable
{Γ : Polarity}
{s : ℕ}
(T : ArithmeticTheory)
[𝗕𝚺s ⪯ T]
{n : ℕ}
{φ : ArithmeticSemisentence n}
(h : Hierarchy Γ s φ)
:
∃ (φ₀ : 𝚺₀.Semisentence (n + s)), T ⊢ ∀¹* (φ 🡘 Semiformula.toPrenex Γ s ↑φ₀)
theorem
FFL.FirstOrder.Arithmetic.exists_strictHierarchy_of_hierarchy
{Γ : Polarity}
{s : ℕ}
(T : ArithmeticTheory)
[𝗕𝚺s ⪯ T]
{n : ℕ}
{φ : ArithmeticSemisentence n}
(h : Hierarchy Γ s φ)
:
∃ (ψ : ArithmeticSemisentence n), StrictHierarchy Γ s ψ ∧ T ⊢ ∀¹* (φ 🡘 ψ)