Theory $\mathsf{ACA_0}$

The fragment of second-order arithmetic with arithmetic comprehension.

def FFL.SecondOrder.TheoryRestrictedComprehension.ArithmeticalComprehensionAxiom : TheoryRestrictedComprehension ℒₒᵣ

Equations

• 𝗔𝗖𝗔₀ = { theory := 𝗭₂, comprehension := FFL.SecondOrder.Semiformula.IsElementary }

def FFL.SecondOrder.TheoryRestrictedComprehension.«term𝗔𝗖𝗔₀» : Lean.ParserDescr

Equations

• FFL.SecondOrder.TheoryRestrictedComprehension.«term𝗔𝗖𝗔₀» = Lean.ParserDescr.node `FFL.SecondOrder.TheoryRestrictedComprehension.«term𝗔𝗖𝗔₀» 1024 (Lean.ParserDescr.symbol "𝗔𝗖𝗔₀")