@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.FirstOrderTrueArith : ArithmeticTheory

Equations

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

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

Equations

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

instance LO.FirstOrder.Arithmetic.TA.instModelsSetStrucORingSentenceStrNatFirstOrderTrueArith : ℕ↓[ℒₒᵣ] ⊧* 𝗧𝗔

theorem LO.FirstOrder.Arithmetic.TA.provable_iff {φ : ArithmeticSentence} : 𝗧𝗔 ⊢ φ ↔ ℕ↓[ℒₒᵣ] ⊧ φ

instance LO.FirstOrder.Arithmetic.TA.instWeakerThanSentenceORingArithmeticTheoryFirstOrderTrueArithOfModelsSetStrucStrNat (T : ArithmeticTheory) [ℕ↓[ℒₒᵣ] ⊧* T] : T ⪯ 𝗧𝗔