つぎは，定理シェマである：
| (0) | num＝num1 ⊃ num＋num11＝num1＋num11
| | (1) | num＋num1′＝ num′＋num1
| | (2) | num＋num1 ＝ num1＋num
| | (3) | (num＋num1)＋num11 ＝ num＋(num1＋num11)
| | (4) | num×num1 ＝ num1×num
| | (5) | (num×num1)×num11 ＝ num×(num1×num11)
| | (6) | (num＋num1)×num11 ＝ num×num11＋num1×num11
|
証明の例として，以下，(2) の証明を示す。
-
先ず，1＋1＝1＋1 は定理：
| | ε
| | | ↓(E1)
| | 1＋1＝1＋1 | ←─ | trm＝trm
|
-
演繹定理を用いて
x＋1＝1＋x → x′＋1＝1＋x′
を証明する：
| x＋1＝1＋x | ←─ | num＝num1
| | | ↓(N0)
| | (x＋1)′＝(1＋x)′ | ←─ | num′＝num1′
| | ‖
| | (x＋1)′＝(1＋x)′ | ←─ | (num＋1)′＝trm
| | | ↓(A1)
| | (x′)′＝(1＋x)′ | ←─ | (num′)′＝trm
| | ‖
| | (x′)′＝(1＋x)′ | ←─ | num′＝trm
| | | ↓(A1)
| | x′＋1＝(1＋x)′ | ←─ | num＋1＝trm
| | ‖
| | x′＋1＝(1＋x)′ | ←─ | trm＝(num＋num1)′
| | | ↓(A2)
| | x′＋1＝1＋x′ | ←─ | trm＝num＋num1′
|
-
x＋1＝1＋x の証明：
| 1＋1＝1＋1 | ←─ | sen[nvr↓1]
| | & | | &
| | x＋1＝1＋n⊃x′＋1＝1＋x′ | | sen⊃sen[nvr↓nvr′]
| | | ↓(N3)
| | x＋1＝1＋x | ←─ | sen
|
-
演繹定理を用いて
x＋b＝b＋x ⊃ x＋b′＝b′＋x
を証明する。
| x＋b＝b＋x | ←─ | num＝num1
| | | ↓(N0)
| | (x＋b)′＝(b＋x)′ | ←─ | num′＝num1′
| | ‖
| | (x＋b)′＝(b＋x)′ | ←─ | (num＋num1)′＝trm
| | | ↓(A2)
| | x＋b′＝(b＋x)′ | ←─ | num＋num1′＝trm
| | ‖
| | x＋b′＝(b＋x)′ | ←─ | trm＝(num＋num1)′
| | | ↓(A2)
| | x＋b′＝b＋x′ | ←─ | trm＝num＋num1′
| | | ↓(1)
| | x＋b′＝b＋x′ | ←─ | trm＝trm1
| | & | | &
| | b＋x′＝b′＋x | | trm1＝trm11
| | | ↓(E3)
| | x＋b′＝b′＋x | ←─ | trm＝trm11
|
-
最後に，a＋b＝b＋a がつぎのように証明される：
| a＋1＝1＋a | ←─ | sen[nvr↓1]
| | & | | &
| | a＋x＝x＋a⊃a＋x′＝x′＋a | | sen⊃sen[nvr↓nvr′]
| | | ↓(N3)
| | a＋x＝x＋a | ←─ | sen
| | | ↓(Q0)
| | a＋b＝b＋a | ←─ | sen[tvr↓trm]
|
|