instance
LO.FirstOrder.Arith.instDiagonalization
(T : LO.FirstOrder.Theory ββα΅£)
[ππΊβ βΌ 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]
:
Equations
- T.standardDP U = { prov := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val U.provableβ, spec := β― }
Instances For
instance
LO.FirstOrder.Arith.instHBL2StandardDP
(T : LO.FirstOrder.Theory ββα΅£)
[ππΊβ βΌ T]
(U : LO.FirstOrder.Theory ββα΅£)
[U.Delta1Definable]
:
(T.standardDP U).HBL2
Equations
- LO.FirstOrder.Arith.instHBL2StandardDP T U = { D2 := β― }
instance
LO.FirstOrder.Arith.instHBL3StandardDP
(T : LO.FirstOrder.Theory ββα΅£)
[ππΊβ βΌ T]
(U : LO.FirstOrder.Theory ββα΅£)
[U.Delta1Definable]
:
(T.standardDP U).HBL3
Equations
- LO.FirstOrder.Arith.instHBL3StandardDP T U = { D3 := β― }
instance
LO.FirstOrder.Arith.instHBLStandardDP
(T : LO.FirstOrder.Theory ββα΅£)
[ππΊβ βΌ T]
(U : LO.FirstOrder.Theory ββα΅£)
[U.Delta1Definable]
:
(T.standardDP U).HBL
Equations
- LO.FirstOrder.Arith.instHBLStandardDP T U = LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL.mk
instance
LO.FirstOrder.Arith.instGoedelSoundStandardDP
(T : LO.FirstOrder.Theory ββα΅£)
[ππΊβ βΌ T]
(U : LO.FirstOrder.Theory ββα΅£)
[U.Delta1Definable]
[β β§β* U]
[πβ βΌ U]
:
(T.standardDP U).GoedelSound
Equations
- LO.FirstOrder.Arith.instGoedelSoundStandardDP T U = { Ξ³_sound := β― }