instance LO.FirstOrder.Arith.instDiagonalization (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] : LO.FirstOrder.DerivabilityCondition.Diagonalization T

Equations

• LO.FirstOrder.Arith.instDiagonalization T = { fixpoint := LO.FirstOrder.Arith.fixpoint, diag := ⋯ }

@[reducible, inline]

abbrev LO.FirstOrder.Theory.standardDP (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] (U : LO.FirstOrder.Theory ℒₒᵣ) [U.Delta1Definable] : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T U

Equations

• T.standardDP U = { prov := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val U.provableₐ, spec := ⋯ }

instance LO.FirstOrder.Arith.instHBL2StandardDP (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] (U : LO.FirstOrder.Theory ℒₒᵣ) [U.Delta1Definable] : (T.standardDP U).HBL2

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Arith.instHBL3StandardDP (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] (U : LO.FirstOrder.Theory ℒₒᵣ) [U.Delta1Definable] : (T.standardDP U).HBL3

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Arith.instHBLStandardDP (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] (U : LO.FirstOrder.Theory ℒₒᵣ) [U.Delta1Definable] : (T.standardDP U).HBL

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Arith.instGoedelSoundStandardDP (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] (U : LO.FirstOrder.Theory ℒₒᵣ) [U.Delta1Definable] [ℕ ⊧ₘ* U] [𝐑₀ ≼ U] : (T.standardDP U).GoedelSound

Equations

• ⋯ = ⋯