Documentation

Foundation.FirstOrder.TrueArithmetic.Basic

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