Documentation

Foundation.FirstOrder.TrueArithmetic.Basic

source
@[reducible, inline]
abbrev LO.FirstOrderTrueArith :
FirstOrder.Theory β„’β‚’α΅£
Equations
Instances For
source
def LO.Β«term𝐓𝐀» :
Lean.ParserDescr
Equations
source
instance LO.FirstOrderTrueArith.instModelsTheoryNat :
β„• βŠ§β‚˜* 𝐓𝐀
source
theorem LO.FirstOrderTrueArith.provable_iff {Ο† : FirstOrder.SyntacticFormula β„’β‚’α΅£} :
𝐓𝐀 ⊒! Ο† ↔ β„• βŠ§β‚˜ Ο†
source
instance LO.FirstOrderTrueArith.instWeakerThanSyntacticFormulaORingTheoryOfModelsTheoryNat (T : FirstOrder.Theory β„’β‚’α΅£) [β„• βŠ§β‚˜* T] :
T βͺ― 𝐓𝐀