逆数学
ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} は、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} に算術的内包公理を付け加えた体系である。 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} は、任意の算術的論理式を満たす自然数の集合の存在を示す。実際、算術的内包公理を得るために、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} にΣ1論理式の内包公理を追加したものである。
ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} の1階部分はペアノ算術と同じである。つまり ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} は算術的な定理についてはにペアノ算術と証明能力は同じである。また、両者は無矛盾性については等価である。
ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} は、可述的数学のほとんどを展開することができ、古典的数学の基本的な定理の多くを証明することができる。