def LO.FirstOrder.Theory.Consistencyₐ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : Theory ℒₒᵣ) [T.Delta1Definable] (φ : V) : Prop

Equations

• T.Consistencyₐ φ = ¬T.Provableₐ (⌜ℒₒᵣ⌝.neg φ)

Instances For

• LO.Arith.consistencyₐ_definable

theorem LO.FirstOrder.Theory.Consistencyₐ.quote_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : Theory ℒₒᵣ) [T.Delta1Definable] {φ : Sentence ℒₒᵣ} : T.Consistencyₐ ⌜φ⌝ ↔ ¬T.Provableₐ ⌜∼φ⌝

def LO.FirstOrder.Theory.consistencyₐ (T : Theory ℒₒᵣ) [T.Delta1Definable] : 𝚷₁.Semisentence 1

Equations

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

theorem LO.Arith.consistencyₐ_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] : 𝚷₁-Predicate T.Consistencyₐ via T.consistencyₐ

@[simp]

theorem LO.Arith.eval_consistencyₐ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] (v : Fin 1 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val T.consistencyₐ) ↔ T.Consistencyₐ (v 0)

instance LO.Arith.consistencyₐ_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] : 𝚷₁-Predicate T.Consistencyₐ