DC

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arith.instDiagonalization (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] : DerivabilityCondition.Diagonalization T

Equations

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

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Theory.standardDP (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] (U : Theory ℒₒᵣ) [U.Delta1Definable] : DerivabilityCondition.ProvabilityPredicate T U

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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