Supporting results for pointwise provable equality.

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]

structure PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex (Γ : Polarity) (s : ℕ) (ξ : Type u_1) (n : ℕ) : Type u_1

Data and laws for Prenex in FFL.FirstOrder.Arithmetic.

• matrix : HierarchySymbol.Semiformula ξ (n + s) Σ₀

  The matrix construction in FFL.FirstOrder.Arithmetic.Prenex.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Γ s ξ n) : ArithmeticSemiformula ξ n

The val construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• ↑φ = PointwiseComposition.FFL.FirstOrder.Semiformula.toPrenex Γ s ↑φ.matrix

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.instCoeTCArithmeticSemiformula {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} : CoeTC (Prenex Γ s ξ n) (ArithmeticSemiformula ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.instCoeTCArithmeticSemiformula = { coe := PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val }

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.neg {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Γ s ξ n) : Prenex Γ.alt s ξ n

The neg construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• φ.neg = { matrix := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (∼↑φ.matrix) ⋯ }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.instHTildeAlt {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} : HTilde (Prenex Γ s ξ n) (Prenex Γ.alt s ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.instHTildeAlt = { hTilde := PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.neg }

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.rew {Γ : Polarity} {s : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ n₂ : ℕ} (φ : Prenex Γ s ξ₁ n₁) (ω : Rew ℒₒᵣ ξ₁ n₁ ξ₂ n₂) : Prenex Γ s ξ₂ n₂

The rew construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• φ.rew ω = { matrix := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.rew (ω.qpow s) φ.matrix }

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.sigma {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Π s ξ (n + 1)) : Prenex Σ (s + 1) ξ n

The sigma construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• φ.sigma = { matrix := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.rew (PointwiseComposition.FFL.FirstOrder.Rew.castLE ⋯) φ.matrix }

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.pi {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Σ s ξ (n + 1)) : Prenex Π (s + 1) ξ n

The pi construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• φ.pi = { matrix := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.rew (PointwiseComposition.FFL.FirstOrder.Rew.castLE ⋯) φ.matrix }

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.sigmaInv {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Σ (s + 1) ξ n) : Prenex Π s ξ (n + 1)

The sigma Inv construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• φ.sigmaInv = { matrix := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.rew (PointwiseComposition.FFL.FirstOrder.Rew.castLE ⋯) φ.matrix }

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.piInv {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Π (s + 1) ξ n) : Prenex Σ s ξ (n + 1)

The pi Inv construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• φ.piInv = { matrix := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.rew (PointwiseComposition.FFL.FirstOrder.Rew.castLE ⋯) φ.matrix }

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.altUp {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Γ s ξ n) : Prenex Γ.alt (s + 1) ξ n

The alt Up construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ofΔ₀ {ξ : Type u_1} {n : ℕ} (φ : HierarchySymbol.Semiformula ξ n Σ₀) (Γ : Polarity) (s : ℕ) : Prenex Γ s ξ n

The ofΔ₀ construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ofΔ₀ φ x✝ 0 = { matrix := φ }
• PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ofΔ₀ φ x✝ s.succ = ⋯.mp (PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ofΔ₀ φ x✝.alt s).altUp

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.verum {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} : Prenex Γ s ξ n

The verum construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.falsum {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} : Prenex Γ s ξ n

The falsum construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.rel {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n k : ℕ} (r : ℒₒᵣ.Rel k) (v : Fin k → ArithmeticSemiterm ξ n) : Prenex Γ s ξ n

The rel construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.nrel {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n k : ℕ} (r : ℒₒᵣ.Rel k) (v : Fin k → ArithmeticSemiterm ξ n) : Prenex Γ s ξ n

The nrel construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_hierarchy {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ : Prenex Γ s ξ n} : Hierarchy Γ s ↑φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_deltaZero {Γ : Polarity} {ξ : Type u_1} {n : ℕ} {φ : Prenex Γ 0 ξ n} : Hierarchy Σ 0 ↑φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_neg {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Γ s ξ n) : ↑(∼φ) = ∼↑φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_rew {Γ : Polarity} {s : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ n₂ : ℕ} (φ : Prenex Γ s ξ₁ n₁) (ω : Rew ℒₒᵣ ξ₁ n₁ ξ₂ n₂) : ↑(φ.rew ω) = (Rewriting.app ω) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_sigma {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ : Prenex Π s ξ (n + 1)} : ↑φ.sigma = ∃¹ ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_pi {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ : Prenex Σ s ξ (n + 1)} : ↑φ.pi = ∀¹ ↑φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_sigmaInv {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ : Prenex Σ (s + 1) ξ n} : ↑φ = ∃¹ ↑φ.sigmaInv

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_piInv {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ : Prenex Π (s + 1) ξ n} : ↑φ = ∀¹ ↑φ.piInv

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_sigmaInv {s n : ℕ} {V : Type u_4} [ORingStructure V] (φ : Prenex Σ (s + 1) Empty n) (e : Fin n → V) : (Semiformula.Evalb e) ↑φ ↔ ∃ (x : V), (Semiformula.Evalb (x :> e)) ↑φ.sigmaInv

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_piInv {s n : ℕ} {V : Type u_4} [ORingStructure V] (φ : Prenex Π (s + 1) Empty n) (e : Fin n → V) : (Semiformula.Evalb e) ↑φ ↔ ∀ (x : V), (Semiformula.Evalb (x :> e)) ↑φ.piInv

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_sigma {s n : ℕ} {V : Type u_4} [ORingStructure V] (φ : Prenex Π s Empty (n + 1)) (e : Fin n → V) : (Semiformula.Evalb e) ↑φ.sigma ↔ ∃ (x : V), (Semiformula.Evalb (x :> e)) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_pi {s n : ℕ} {V : Type u_4} [ORingStructure V] (φ : Prenex Σ s Empty (n + 1)) (e : Fin n → V) : (Semiformula.Evalb e) ↑φ.pi ↔ ∀ (x : V), (Semiformula.Evalb (x :> e)) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_altUp {Γ : Polarity} {s n : ℕ} {V : Type u_4} [ORingStructure V] (φ : Prenex Γ s Empty n) (e : Fin n → V) : (Semiformula.Evalb e) ↑φ.altUp ↔ (Semiformula.Evalb e) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_ofΔ₀ {Γ : Polarity} {s n : ℕ} {V : Type u_4} [ORingStructure V] (φ : Σ₀.Semisentence n) (e : Fin n → V) : (Semiformula.Evalb e) ↑(ofΔ₀ φ Γ s) ↔ (Semiformula.Evalb e) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_verum {Γ : Polarity} {s n : ℕ} {V : Type u_4} [ORingStructure V] (e : Fin n → V) : (Semiformula.Evalb e) ↑verum ↔ (Semiformula.Evalb e) ⊤

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_falsum {Γ : Polarity} {s n : ℕ} {V : Type u_4} [ORingStructure V] (e : Fin n → V) : (Semiformula.Evalb e) ↑falsum ↔ (Semiformula.Evalb e) ⊥

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_rel {Γ : Polarity} {s n : ℕ} {V : Type u_4} [ORingStructure V] {k : ℕ} (r : ℒₒᵣ.Rel k) (v : Fin k → ArithmeticSemiterm Empty n) (e : Fin n → V) : (Semiformula.Evalb e) ↑(rel r v) ↔ (Semiformula.Evalb e) (Semiformula.rel r v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_nrel {Γ : Polarity} {s n : ℕ} {V : Type u_4} [ORingStructure V] {k : ℕ} (r : ℒₒᵣ.Rel k) (v : Fin k → ArithmeticSemiterm Empty n) (e : Fin n → V) : (Semiformula.Evalb e) ↑(nrel r v) ↔ (Semiformula.Evalb e) (Semiformula.nrel r v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.provable_iff_sigmaInv {s n : ℕ} {T : ArithmeticTheory} {φ : ArithmeticSemiformula Empty n} {φ' : Prenex Σ (s + 1) Empty n} (hφ' : T ⊢ ∀¹* (φ ⇔ₗ ↑φ')) : T ⊢ ∀¹* (φ ⇔ₗ ∃¹ ↑φ'.sigmaInv)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.provable_iff_piInv {s n : ℕ} {T : ArithmeticTheory} {φ : ArithmeticSemiformula Empty n} {φ' : Prenex Π (s + 1) Empty n} (hφ' : T ⊢ ∀¹* (φ ⇔ₗ ↑φ')) : T ⊢ ∀¹* (φ ⇔ₗ ∀¹ ↑φ'.piInv)

@[irreducible]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ball {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} : ArithmeticSemiterm ξ n → Prenex Γ s ξ (n + 1) → Prenex Γ s ξ n

The ball construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ball x✝¹ x✝ = ∼PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.bexs x✝¹ (∼x✝)

@[irreducible]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.bexs {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} : ArithmeticSemiterm ξ n → Prenex Γ s ξ (n + 1) → Prenex Γ s ξ n

The bexs construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.bexs x✝¹ x✝ = ∼PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ball x✝¹ (∼x✝)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ball_zero {Γ : Polarity} {ξ : Type u_1} {n : ℕ} {u : ArithmeticSemiterm ξ n} {φ : Prenex Γ 0 ξ (n + 1)} : ball u φ = { matrix := HierarchySymbol.Semiformula.mkSigma (“(∀¹[!!(Semiterm.bvar 0) < !!(Rew.bShift u)] !↑φ)”) ⋯ }

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ball_succ_sigma {s : ℕ} {ξ : Type u_1} {n : ℕ} {u : ArithmeticSemiterm ξ n} {φ : Prenex Σ (s + 1) ξ (n + 1)} : ball u φ = (ball (Rew.bShift u) (bexs (‘(!!(Semiterm.bvar 1) + 1)’) (φ.sigmaInv.rew (Rew.subst (Semiterm.bvar 0 :> Semiterm.bvar 1 :> fun (x : Fin n) => Semiterm.bvar x.succ.succ.succ))))).sigma

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.ball_succ_pi {s : ℕ} {ξ : Type u_1} {n : ℕ} {u : ArithmeticSemiterm ξ n} {φ : Prenex Π (s + 1) ξ (n + 1)} : ball u φ = ∼bexs u (∼φ)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.bexs_zero {Γ : Polarity} {ξ : Type u_1} {n : ℕ} {u : ArithmeticSemiterm ξ n} {φ : Prenex Γ 0 ξ (n + 1)} : bexs u φ = { matrix := HierarchySymbol.Semiformula.mkSigma (“(∃¹[!!(Semiterm.bvar 0) < !!(Rew.bShift u)] !↑φ)”) ⋯ }

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.bexs_succ_pi {s : ℕ} {ξ : Type u_1} {n : ℕ} {u : ArithmeticSemiterm ξ n} {φ : Prenex Π (s + 1) ξ (n + 1)} : bexs u φ = ∼ball u (∼φ)

@[irreducible]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.and {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} : Prenex Γ s ξ n → Prenex Γ s ξ n → Prenex Γ s ξ n

The and construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• One or more equations did not get rendered due to their size.
• x✝¹.and x✝ = { matrix := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑x✝¹ ⋏ ↑x✝) ⋯ }
• x✝¹.and x✝ = ∼(∼x✝¹).or (∼x✝)

@[irreducible]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.or {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} : Prenex Γ s ξ n → Prenex Γ s ξ n → Prenex Γ s ξ n

The or construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• x✝¹.or x✝ = { matrix := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑x✝¹ ⋎ ↑x✝) ⋯ }
• x✝¹.or x✝ = (x✝¹.sigmaInv.or x✝.sigmaInv).sigma
• x✝¹.or x✝ = ∼(∼x✝¹).and (∼x✝)

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.instHWedge {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} : HWedge (Prenex Γ s ξ n) (Prenex Γ s ξ n) (Prenex Γ s ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.instHWedge = { hWedge := PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.and }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.instHVee {Γ : Polarity} {s : ℕ} {ξ : Type u_1} {n : ℕ} : HVee (Prenex Γ s ξ n) (Prenex Γ s ξ n) (Prenex Γ s ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.instHVee = { hVee := PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.or }

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.and_zero {Γ : Polarity} {ξ : Type u_1} {n : ℕ} {φ ψ : Prenex Γ 0 ξ n} : φ ⋏ ψ = { matrix := HierarchySymbol.Semiformula.mkSigma (↑φ ⋏ ↑ψ) ⋯ }

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.and_succ_sigma {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ ψ : Prenex Σ (s + 1) ξ n} : φ ⋏ ψ = (bexs (‘(!!(Semiterm.bvar 0) + 1)’) (φ.sigmaInv.rew (Rew.subst (Semiterm.bvar 0 :> fun (x : Fin n) => Semiterm.bvar x.succ.succ))) ⋏ bexs (‘(!!(Semiterm.bvar 0) + 1)’) (ψ.sigmaInv.rew (Rew.subst (Semiterm.bvar 0 :> fun (x : Fin n) => Semiterm.bvar x.succ.succ)))).sigma

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.and_succ_pi {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ ψ : Prenex Π (s + 1) ξ n} : φ ⋏ ψ = ∼(∼φ ⋎ ∼ψ)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.or_zero {Γ : Polarity} {ξ : Type u_1} {n : ℕ} {φ ψ : Prenex Γ 0 ξ n} : φ ⋎ ψ = { matrix := HierarchySymbol.Semiformula.mkSigma (↑φ ⋎ ↑ψ) ⋯ }

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.or_succ_sigma {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ ψ : Prenex Σ (s + 1) ξ n} : φ ⋎ ψ = (φ.sigmaInv ⋎ ψ.sigmaInv).sigma

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.or_succ_pi {s : ℕ} {ξ : Type u_1} {n : ℕ} {φ ψ : Prenex Π (s + 1) ξ n} : φ ⋎ ψ = ∼(∼φ ⋏ ∼ψ)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_ball {V : Type u_4} [ORingStructure V] {Γ : Polarity} {s n : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐈Σs] (u : ArithmeticSemiterm Empty n) (φ : Prenex Γ s Empty (n + 1)) (e : Fin n → V) : (Semiformula.Evalb e) ↑(ball u φ) ↔ ∀ x < Semiterm.valb e u, (Semiformula.Evalb (x :> e)) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_bexs {V : Type u_4} [ORingStructure V] {Γ : Polarity} {s n : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐈Σs] (u : ArithmeticSemiterm Empty n) (φ : Prenex Γ s Empty (n + 1)) (e : Fin n → V) : (Semiformula.Evalb e) ↑(bexs u φ) ↔ ∃ x < Semiterm.valb e u, (Semiformula.Evalb (x :> e)) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_and {V : Type u_4} [ORingStructure V] {Γ : Polarity} {s n : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐈Σs] (φ ψ : Prenex Γ s Empty n) (e : Fin n → V) : (Semiformula.Evalb e) ↑(φ ⋏ ψ) ↔ (Semiformula.Evalb e) ↑φ ∧ (Semiformula.Evalb e) ↑ψ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_or {V : Type u_4} [ORingStructure V] {Γ : Polarity} {s n : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐈Σs] (φ ψ : Prenex Γ s Empty n) (e : Fin n → V) : (Semiformula.Evalb e) ↑(φ ⋎ ψ) ↔ (Semiformula.Evalb e) ↑φ ∨ (Semiformula.Evalb e) ↑ψ

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.exs {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Σ (s + 1) ξ (n + 1)) : Prenex Σ (s + 1) ξ n

The exs construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.all {s : ℕ} {ξ : Type u_1} {n : ℕ} (φ : Prenex Π (s + 1) ξ (n + 1)) : Prenex Π (s + 1) ξ n

The all construction in FFL.FirstOrder.Arithmetic.Prenex.

Equations

• φ.all = ∼(∼φ).exs

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_exs {s n : ℕ} {V : Type u_4} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σs] (φ : Prenex Σ (s + 1) Empty (n + 1)) (e : Fin n → V) : (Semiformula.Evalb e) ↑φ.exs ↔ ∃ (x : V), (Semiformula.Evalb (x :> e)) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_all {s n : ℕ} {V : Type u_4} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σs] (φ : Prenex Π (s + 1) Empty (n + 1)) (e : Fin n → V) : (Semiformula.Evalb e) ↑φ.all ↔ ∀ (x : V), (Semiformula.Evalb (x :> e)) ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.models_exists_prenex {Γ : Polarity} {s n : ℕ} {φ : ArithmeticSemisentence n} (h : Hierarchy Γ s φ) : ∃ (φ' : Prenex Γ s Empty n), ∀ (V : Type u_5) [inst : ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σs] (e : Fin n → V), (Semiformula.Evalb e) φ ↔ (Semiformula.Evalb e) ↑φ'

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.exists_prenex_of_hierarchy {Γ : Polarity} {s : ℕ} (T : ArithmeticTheory) [𝐈Σs ≼ T] {n : ℕ} {φ : ArithmeticSemisentence n} (h : Hierarchy Γ s φ) : ∃ (φ' : Prenex Γ s Empty n), T ⊢ ∀¹* (φ ⇔ₗ ↑φ')

theorem PointwiseComposition.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 ↑φ₀)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Prenex.val_strictHierarchy {Γ : Polarity} {s n : ℕ} {ξ : Type u_1} {φ : Prenex Γ s ξ n} : StrictHierarchy Γ s ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.exists_strictHierarchy_of_hierarchy {Γ : Polarity} {s n : ℕ} (T : ArithmeticTheory) [𝐈Σs ≼ T] {φ : ArithmeticSemisentence n} (h : Hierarchy Γ s φ) : ∃ (ψ : ArithmeticSemisentence n), StrictHierarchy Γ s ψ ∧ T ⊢ ∀¹* (φ ⇔ₗ ψ)