Supporting results for pointwise provable equality.

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.FirstOrderTrueArith : ArithmeticTheory

The 𝐓𝐀 construction in 𝐓𝐀.

Equations

• 𝐓𝐀 = PointwiseComposition.FFL.FirstOrder.Tarski.Structure.theory ℒₒᵣ ℕ

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐓𝐀» : Lean.ParserDescr

The «term𝐓𝐀» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐓𝐀» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐓𝐀» 1024 (Lean.ParserDescr.symbol "𝐓𝐀")

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.TA.instModelsSetStrucORingSentenceStrNatFirstOrderTrueArith : ℕ↓[ℒₒᵣ] ⊧* 𝐓𝐀

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.TA.instWeakerThanSentenceORingArithmeticTheoryFirstOrderTrueArithOfModelsSetStrucStrNat (T : ArithmeticTheory) [ℕ↓[ℒₒᵣ] ⊧* T] : T ≼ 𝐓𝐀