Satisfaction and partial truth for prenex formulas with a $\Delta_0$ matrix

PrenexSatisfied Γ s e p says that Q₀ x₀ ⋯ Q_{s-1} x_{s-1} θ holds under the assignment e, where p codes the $\Delta_0$ matrix θ and the quantifiers alternate starting with Γ. PartialTrue Γ s is the partial truth predicate for the codes of such sentences.

References

• [HP98, 0.30, 1.64, 1.66, Lemma I.1.68, Theorem I.1.70, Definition I.1.74, Theorem I.1.75, Corollary I.1.76]

def FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Polarity → ℕ → V → V → Prop

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied x✝ 0 = FFL.FirstOrder.Arithmetic.Bootstrapping.BoundedSatisfied
• FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied FFL.Polarity.sigma s.succ = fun (e p : V) => ∃ (x : V), FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied 𝚷 s (adjoin x e) p
• FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied FFL.Polarity.pi s.succ = fun (e p : V) => ∀ (x : V), FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied 𝚺 s (adjoin x e) p

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.zero_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : Polarity} {e p : V} : PrenexSatisfied Γ 0 e p ↔ BoundedSatisfied e p

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.sigma_succ_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s : ℕ} {e p : V} : PrenexSatisfied 𝚺 (s + 1) e p ↔ ∃ (x : V), PrenexSatisfied 𝚷 s (adjoin x e) p

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.pi_succ_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s : ℕ} {e p : V} : PrenexSatisfied 𝚷 (s + 1) e p ↔ ∀ (x : V), PrenexSatisfied 𝚺 s (adjoin x e) p

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.not_prenexSatisfied_of_not_isBounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : Polarity} {s : ℕ} {e p : V} (h : ¬IsBounded p) : ¬PrenexSatisfied Γ s e p

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.prenexSatisfied' (Γ : Polarity) (s : ℕ) : { Γ := Γ.coe, rank := s + 1 }.Semisentence 2

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.prenexSatisfied (Γ : Polarity) (s : ℕ) [NeZero s] : { Γ := Γ.coe, rank := s }.Semisentence 2

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.prenexSatisfied Γ 0 = absurd FFL.FirstOrder.Arithmetic.Bootstrapping.prenexSatisfied._proof_1 ⋯
• FFL.FirstOrder.Arithmetic.Bootstrapping.prenexSatisfied Γ s.succ = FFL.FirstOrder.Arithmetic.Bootstrapping.prenexSatisfied' Γ s

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.sigma_defined' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) : { Γ := 𝚺, rank := s + 1 }.DefinedRel (PrenexSatisfied 𝚺 (s + 1)) (prenexSatisfied' 𝚺 s)

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.pi_defined' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) : { Γ := 𝚷, rank := s + 1 }.DefinedRel (PrenexSatisfied 𝚷 (s + 1)) (prenexSatisfied' 𝚷 s)

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.sigma_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) [NeZero s] : { Γ := 𝚺, rank := s }.DefinedRel (PrenexSatisfied 𝚺 s) (prenexSatisfied 𝚺 s)

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.pi_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) [NeZero s] : { Γ := 𝚷, rank := s }.DefinedRel (PrenexSatisfied 𝚷 s) (prenexSatisfied 𝚷 s)

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.sigma_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) [NeZero s] : { Γ := 𝚺, rank := s }.DefinableRel (PrenexSatisfied 𝚺 s)

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PrenexSatisfied.pi_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) [NeZero s] : { Γ := 𝚷, rank := s }.DefinableRel (PrenexSatisfied 𝚷 s)

Partial truth

def FFL.FirstOrder.Arithmetic.Bootstrapping.PartialTrue {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : Polarity) (s : ℕ) (x : V) : Prop

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.partialTrue' (Γ : Polarity) (s : ℕ) : { Γ := Γ.coe, rank := s + 1 }.Semisentence 1

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.partialTrue (Γ : Polarity) (s : ℕ) [NeZero s] : { Γ := Γ.coe, rank := s }.Semisentence 1

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.partialTrue Γ 0 = absurd FFL.FirstOrder.Arithmetic.Bootstrapping.prenexSatisfied._proof_1 ⋯
• FFL.FirstOrder.Arithmetic.Bootstrapping.partialTrue Γ s.succ = FFL.FirstOrder.Arithmetic.Bootstrapping.partialTrue' Γ s

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PartialTrue.sigma_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) [NeZero s] : { Γ := 𝚺, rank := s }.DefinedPred (PartialTrue 𝚺 s) (partialTrue 𝚺 s)

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PartialTrue.pi_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) [NeZero s] : { Γ := 𝚷, rank := s }.DefinedPred (PartialTrue 𝚷 s) (partialTrue 𝚷 s)

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PartialTrue.sigma_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) [NeZero s] : { Γ := 𝚺, rank := s }.DefinablePred (PartialTrue 𝚺 s)

instance FFL.FirstOrder.Arithmetic.Bootstrapping.PartialTrue.pi_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : ℕ) [NeZero s] : { Γ := 𝚷, rank := s }.DefinablePred (PartialTrue 𝚷 s)

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.PartialTrue.zero_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : Polarity} {x : V} : PartialTrue Γ 0 x ↔ BoundedTrue x

Agreement with truth in models of 𝗜𝚺₁

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.prenexSatisfied_quote_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : Polarity} {s k : ℕ} (φ : ℬ[<, ℒₒᵣ].Prenex Γ s Empty k) (v : Fin k → V) : PrenexSatisfied Γ s (matrixToVec v) ⌜φ.matrix.val⌝ ↔ (Semiformula.Evalb v) ↑φ

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_toPrenex {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : Polarity} {s n : ℕ} (θ : ArithmeticSemisentence (n + s)) : ⌜Semiformula.toPrenex Γ s θ⌝ = qqToPrenex Γ s ⌜θ⌝

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.partialTrue_quote_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : Polarity} {s : ℕ} (φ : ℬ[<, ℒₒᵣ].Prenex Γ s Empty 0) : PartialTrue Γ s ⌜↑φ⌝ ↔ V↓[ℒₒᵣ] ⊧ ↑φ

theorem FFL.FirstOrder.Arithmetic.ISigma1.provable_partialTrue_iff {Γ : Polarity} {s : ℕ} [NeZero s] (φ : ℬ[<, ℒₒᵣ].Prenex Γ s Empty 0) : 𝗜𝚺₁ ⊢ ↑(Bootstrapping.partialTrue Γ s)/[⌜↑φ⌝] 🡘 ↑φ

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.provable_partialTrue_iff_of_hierarchy {Γ : Polarity} {s : ℕ} [NeZero s] {σ : ArithmeticSentence} (T : ArithmeticTheory) [𝗕𝚺s ⪯ T] [𝗜𝚺₁ ⪯ T] (h : ℬ[<, ℒₒᵣ].Hierarchy Γ s σ) : T ⊢ ↑(partialTrue Γ s)/[⌜↑h.prenex⌝] 🡘 σ

theorem FFL.FirstOrder.Arithmetic.Peano.provable_partialTrue_iff_of_hierarchy {Γ : Polarity} {s : ℕ} [NeZero s] {σ : ArithmeticSentence} (h : ℬ[<, ℒₒᵣ].Hierarchy Γ s σ) : 𝗣𝗔 ⊢ ↑(Bootstrapping.partialTrue Γ s)/[⌜↑h.prenex⌝] 🡘 σ

theorem FFL.FirstOrder.Arithmetic.ISigma1.provable_partialTrue_iff_of_hierarchy {Γ : Polarity} {σ : ArithmeticSentence} (h : ℬ[<, ℒₒᵣ].Hierarchy Γ 1 σ) : 𝗜𝚺₁ ⊢ ↑(Bootstrapping.partialTrue Γ 1)/[⌜↑h.prenex⌝] 🡘 σ

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.provable_boundedTrue_iff_of_hierarchy {Γ : Polarity} {σ : ArithmeticSentence} (T : ArithmeticTheory) [𝗜𝚺₁ ⪯ T] (h : ℬ[<, ℒₒᵣ].Hierarchy Γ 0 σ) : T ⊢ ↑boundedTrue/[⌜σ⌝] 🡘 σ