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

Equations

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

@[reducible, inline]

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

Equations

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

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

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

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

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