@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.FirstOrderTrueArith : ArithmeticTheory

Equations

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

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

Equations

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

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

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

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