ロビンソン算術
Qの基盤となる理論は等号付き一階述語論理である。言語は次の構成要素からなる:
定項記号: 0
単項関数記号: 後者 S {\displaystyle S}
二項関数記号: 加法 + {\displaystyle +} と乗法 ⋅ {\displaystyle \cdot }
次に示すQ'の公理(Q1)–(Q7)はBurgess (2005)による。束縛されていない変数記号は暗黙的に全称量化されているものと考える。すなわちQは以下に示す論理式の全称閉包を公理とする:
S x ≠ 0 {\displaystyle Sx\neq 0} 0 はいかなる数の後者でもない。
S x = S y → x = y {\displaystyle Sx=Sy\to x=y} もし x {\displaystyle x} と y {\displaystyle y} の後者が等しいならば x {\displaystyle x} と y {\displaystyle y} も等しい。すなわち S {\displaystyle S} (の解釈)は単射である。
Robinsonによる公理化(Robinson (1950))ではQは公理(Q1)–(Q13)からなる(Mendelson (1997: 201))。最初の6つの公理は基盤となる公理が等号を含まないことから要求されるものである。Machoverによる公理化では前述の公理(Q3)を次のように分割する(Machover (1996))。
通常の狭義の全順序 < {\displaystyle <} は加法を用いて次のように形式的には定義できる(Burgess (2005)) (全順序性が証明できるわけではない):
x < y ↔ ∃ z ( x + S z = y ) {\displaystyle x<y\leftrightarrow \exists z(x+Sz=y)}
上のようにして定義された < {\displaystyle <} について次の基本的な要請を公理として(Q1)–(Q7)の後に加える:
¬ x < 0 {\displaystyle \neg x<0}
0 = x ∨ 0 < x {\displaystyle 0=x\vee 0<x}
x < y ↔ S x < y ∨ S x = y {\displaystyle x<y\leftrightarrow Sx<y\vee Sx=y}
x < S y ↔ x < y ∨ x = y {\displaystyle x<Sy\leftrightarrow x<y\vee x=y}
別の公理化で < {\displaystyle <} を用いたものは Shoenfield (1967: 22) において見られる。