@[reducible, inline]

abbrev LO.FirstOrderTrueArith : FirstOrder.Theory ℒₒᵣ

Equations

• 𝗧𝗔 = LO.FirstOrder.Structure.theory ℒₒᵣ ℕ

def LO.«term𝗧𝗔» : Lean.ParserDescr

Equations

• LO.«term𝗧𝗔» = Lean.ParserDescr.node `LO.«term𝗧𝗔» 1024 (Lean.ParserDescr.symbol "𝗧𝗔")

instance LO.FirstOrderTrueArith.instModelsTheoryNat : ℕ ⊧ₘ* 𝗧𝗔

theorem LO.FirstOrderTrueArith.provable_iff {φ : FirstOrder.Sentence ℒₒᵣ} : 𝗧𝗔 ⊢! φ ↔ ℕ ⊧ₘ φ

instance LO.FirstOrderTrueArith.instWeakerThanSentenceORingTheoryOfModelsTheoryNat (T : FirstOrder.Theory ℒₒᵣ) [ℕ ⊧ₘ* T] : T ⪯ 𝗧𝗔