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