形式的体系 H

論理式F1 ：xが変数ならば、xは論理式である。
論理式F2 ：xが論理式ならば、¬(x)も論理式である。
論理式F3 ：xとyが論理式ならば、(x)∨(y)も論理式である。
論理式F4 ：F1〜F3で定められるものだけが論理式である。

記号IMPLY (x)→(y)を、(¬(x))∨(y)として定義する。

公理P1：((x)∨(x))→(x)
公理P2：(x)→((x)∨(y))
公理P3：((x)∨(y))→((y)∨(x))
公理P4：((x)∨(y))→((y)∨(z))→((z)∨(x))

推論規則
xと((x)→(y))で、yを推論できる。