1.
(k1)(A→(B→A))
(k2)(A→(B→C))→((A→B)→(A→C))(k3)(~A→~B)→(B→A)2.
(k4)(( xi)A→A),xi
A
(k5)(( xi)A(xi)→A(t)),
A(xi)
L
t
L
xi
(k6)( xi)(A→B)→(A→( xi)B),Axi
3.
(E7)(x1=x1)
(E8)(tk=u→(fin(t1,...,tk,...,tn)=fin(t1,...,u,...,tn))),
fin
L(E9)(tk=u→(Ani(t1,...,tk,...,tn)→Ani(t1,...,u,...,tn))),
Ani
L
4.
(N1)( x
1)~(x1=0)
(N2)( x
1)( x2)(x1=x2→x1=x2)(N3)( x1)(x1+0=x1)
(N4)( x
1)( x2)(x1+x2=(x1+x2))(N5)( x1)(x1×0=0)
(N6)( x1)( x2)(x1×x
2=(x1×x2)+x1)
(N7)A(0)→(( x1)(A(x1)→A(x
1))→( x1)A(x1)),x1
A(x1)
4
A(xi)
t1,...,tn,ut1,...,tn,u