Countable strict reverse mathematics

We prove (i) by external induction on t.

If t is 0 or a variable other than m,n,r, then we use ternary constant functions obtained from initial functions axioms (i) and composition axiom (ii). If t is among m,n,r, then use projection functions from initial functions axioms (ii)-(iv).

The induction step. If t is g(s_1,s_2,s_3), then by induction hypothesis, let h_1(m,n,r)=s_1, h_2(m,n,r)=s_2, h_3(m,n,r)=s_3 hold for all m,n,r, so by composition axiom (v) we have (\exists f)(\forall m,n,r) (f(m,n,r)=g(h_1(m,n,r), h_2(m,n,r), h_3(m,n,r))). If t is g(s_1,s_2), then we convert it to a ternary function g' by composition axiom (i) and apply composition axiom (v). If t is g(s_1), then we convert it to a ternary function g' by composition axiom (ii) and apply composition axiom (v). If t is S(s_1), we convert function symbol S to a unary function g by initial functions axiom (v) and apply composition axioms (ii) and (v).

We can derive (ii) and (iii) from (i) and composition axioms (iii) and (iv) respectively.

Each equivalence is proved in the same way. For example, here is the proof (ii)\Rightarrow(vi). Let we have f(0,m,n)=g(0,m,n)\&(\forall k)(f(k,m,n)=g(k,m,n)\rightarrow f(S(k),m,n)=g(S(k),m,n)). By Lemma 1.(ii) for any n there are h_1 and h_2 such that for all m,k we have h_1(m,k)=f(k,m,n), h_2(m,k)=g(k,m,n). This means that h_1(m,0)=h_2(m,0)\&(\forall k)(h_1(m,k)=h_2(m,k)\rightarrow h_1(m,S(k))=h_2(m,S(k))). By (ii) we have h_1(m,k)=h_2(m,k), i.e. for any n we have f(k,m,n)=g(k,m,n).

By Lemma 1 let f(n)=s and g(n)=t, where f and g depend internally on the functions in s,t and the variables over \omega in s,t other than n. Then apply rudimentary induction axiom to f(n)=g(n).

Let r and h(n) be given. By Lemma 1 set h'(m,r,n)=h(n) and apply WPRA to h' and the constant function g(n)=r, thus obtaining function f'(m,0)=r\wedge(\forall n)(f'(m,S(n))=h'(m,S(n),f'(m,n))). Then by Lemma 1 set f(n)=f'(m,n). We have f(0)=r\wedge(\forall n)(f(S(n))=f'(m,S(n))=h'(m,S(n),f'(m,n))=h(f'(m,n))=h(f(n))).

Each of functions is defined using WPRA, ITER and composition axioms with previously defined functions.

(i) n+1=n+S(0)=S(n+0)=S(n) by Lemma 5.(i).

(ii) Use Equational Induction from Lemma 2 on n. If n=0 then 0+0=0 by Lemma 5.(i). Suppose 0+n=n, then 0+S(n)=S(0+n)=S(n).

(iii) Use Equational Induction on m. If m=0 then S(n)+0=S(n)=S(n+0)=n+S(0) by Lemma 5.(i). Suppose, S(n)+m=n+S(m), then S(n)+S(m)=S(S(n)+m)=S(n+S(m))=n+S(S(m)) by Lemma 5.(i).

(iv) Use Equational Induction on m. If m=0 then n+0=n=0+n by (ii) and Lemma 5.(i). Suppose n+m=m+n, then n+S(m)=S(n+m)=S(m+n)=m+S(n)=S(m)+n by (iii) and Lemma 5.(i).

(v) Use Equational Induction on r. If r=0 then (n+m)+0=n+m=n+(m+0) by Lemma 5.(i). Suppose (n+m)+r=n+(m+r), then (n+m)+S(r)=S((n+m)+r)=S(n+(m+r))=n+S(m+r)=n+(m+S(r)) by Lemma 5.(i).

(vi) If n=0\wedge m=0, then n+m=0 by Lemma 5.(i). Let n+m=0 and suppose that m\not=0. Then by successor axiom (iii), (\exists r)(S(r)=m) and n+m=n+S(r)=S(n+r)\not=0 by successor axiom (i), contradiction. If n\not=0, then by successor axiom (iii), (\exists t)(S(t)=m) and n+m=m+n=m+S(t)=S(m+t) by (iv) and successor axiom (i), contradiction.

(vii) Use Equational Induction on n. If n=0, then 0\cdot0=0 by Lemma 5.(ii). Suppose 0\cdot n=0, then 0\cdot S(n)=0\cdot n+0=0+0=0 by Lemma 5.(ii) and Lemma 5.(i).

(viii) Use Equational Induction on m. If m=0 then S(n)\cdot 0=0=0+0=n\cdot 0+0 by Lemma 5.(i) and Lemma 5.(ii). Suppose S(n)\cdot m=n\cdot m+m, then S(n)\cdot S(m)=S(n)\cdot m+S(n)=n\cdot m+m+S(n)=n\cdot m+S(n)+m=n\cdot m+n+1+m=n\cdot S(m)+m+1=n\cdot S(m)+S(m) by (i), (iv) and Lemma 5.(ii).

(ix) Use Equational Induction on n. If n=0, then m\cdot0=0=0\cdot m by (vii) and Lemma 5.(ii). Suppose m\cdot n=n\cdot m, then m\cdot S(n)=m\cdot n+m=n\cdot m+m=S(n)\cdot m by (viii) and Lemma 5.(ii).

(x) Use Equational Induction on n. If n=0, then 1\cdot0=0 by Lemma 5.(ii). Suppose 1\cdot n=n, then 1\cdot S(n)=1\cdot n+1=n+1=S(n) by (i), Lemma 5.(ii) and Lemma 5.(i).

(xi) If n=0\vee m=0, then m\cdot n=0 by (vii) and Lemma 5.(ii). Let m\cdot n=0 and suppose that m\not=0\wedge n\not=0. Then by successor axiom (iii), (\exists r)(S(r)=m) and (\exists t)(S(t)=n), thus by Lemma 5.(i) and Lemma 5.(ii), m\cdot n=S(r)\cdot S(t)=S(r)\cdot t+S(r)=S(S(r)\cdot t+r)\not=0 by successor axiom (i), contradiction.

(xii) Use Equational Induction on n. If n=0 then 0+0=0=2\cdot 0 by Lemma 5.(i) and Lemma 5.(ii). Suppose n+n=2\cdot n, then S(n)+S(n)=S(S(n)+n)=S(n+S(n))=S(S(n+n))=S(S(2\cdot n))=S(S(2\cdot n)+0)=S(2\cdot n+S(0))=2\cdot n+S(S(0))=2\cdot n+2=2\cdot S(n) by (iv), Lemma 5.(i) and Lemma 5.(ii).

(xiii) If n=0 then sg(n)=0 by Lemma 5.(iii). If n\not=0, then by successor axiom (iii), (\exists m)(S(m)=n) and sg(n)=sg(S(m))=1 by Lemma 5.(iii).

(xiv) If n=0 then \overline{sg}(0)=1 by Lemma 5.(iv). If n\not=0, then by successor axiom (iii), (\exists m)(S(m)=n), and \overline{sg}(n)=\overline{sg}(S(m))=0 by Lemma 5.(iv).

(xv) Use Equational Induction on n. If n=0 then by (vii), \overline{sg}(0\cdot S(0))=\overline{sg}(0). The induction step. Since S(n)\not=0 and S(S(n))\not=0, we have S(n)\cdot S(S(n))\not=0 by (xi), thus by (xiv), \overline{sg}(S(n)\cdot S(S(n))))=0=\overline{sg}(S(n)).

(xvi) By Lemma 5.(iv) and Lemma 5.(v), odd(1)=odd(S(0))=\overline{sg}(odd(0))=\overline{sg}(0)=1.

(xvii) By (vii), Lemma 5.(vi) and Lemma 5.(iv), f'(1)=\overline{sg}(f'(0))+f'(0)\cdot S(f'(0))=\overline{sg}(0)+0\cdot S(0)=1+0=1.

(xviii) By Lemma 5.(v) and Lemma 5.(vi), \overline{sg}(f'(0))=\overline{sg}(0)=1. Use Equational Induction on n to show that \overline{sg}(f'(S(n)))=0 for all n. If n=0 then by (xvii), \overline{sg}(f'(S(0)))=\overline{sg}(1)=0. Suppose \overline{sg}(f'(S(n)))=0, then by (xv) and Lemma 5.(vi), \overline{sg}(f'(S(S(n))))=\overline{sg}(\overline{sg}(f'(S(n)))+f'(S(n))\cdot S(f'(S(n))))=\overline{sg}(0+f'(S(n))\cdot S(f'(S(n))))=\overline{sg}(f'(S(n)))=0.

(xix) Use Equational Induction on n. If n=0 then by Lemma 5.(ii) and Lemma 5.(v), odd(2\cdot 0)=odd(0)=0. Suppose odd(2\cdot n)=0, then odd(2\cdot S(n)))=odd(2\cdot n+2)=odd(2\cdot n+S(S(0)))=odd(S(2\cdot n+S(0)))=odd(S(S(2\cdot n+0)))=\overline{sg}(odd(S(2\cdot n)))=\overline{sg}(\overline{sg}(odd(2\cdot n)))=\overline{sg}(\overline{sg}(0))=\overline{sg}(1)=0 by Lemma 5.(i), 5.(ii), 5.(iv), 5.(v).

(xx) Use Equational Induction on n. If n=0 then odd(S(S(0)))=\overline{sg}(\overline{sg}(odd(0)))=\overline{sg}(\overline{sg}(0))=\overline{sg}(1)=0=odd(0). Suppose odd(S(S(n)))=odd(n), then odd(S(S(S(n))))=\overline{sg}(odd(S(S(n))))=\overline{sg}(odd(n))=odd(S(n)).

(xxi) Use Equational Induction on n. If n=0 then by Lemma 5.(i), Lemma 5.(ii), odd (m+2\cdot 0)=odd(m+0)=odd(m). Suppose odd(m+2\cdot n)=odd(m), then by (i), (iv), (v), (xii), (xx) and Lemma 5.(i), odd(m+2\cdot S(n))=odd(m+S(n)+S(n))=odd(m+n+1+n+1)=odd(m+n+n+S(0)+S(0))=odd(S(m+2\cdot n+S(0)+0))=\overline{sg}(odd(m+2\cdot n+S(0)))=\overline{sg}(odd(S(m+2\cdot n+0)))=\overline{sg}(\overline{sg}(odd(m+2\cdot n)))=\overline{sg}(\overline{sg}(odd(m)))=\overline{sg}(odd(S(m)))=odd(S(S(m)))=odd(m).

(xxii) Use Equational Induction on n. If n=0 then by (xvi) and Lemma 5.(v), odd(0+S(0))=odd(1)=1. Suppose odd(n+S(n))=1, then odd(S(n)+S(S(n)))=odd(S(S(n)+S(n)))=\overline{sg}(odd(S(n)+S(n)))=\overline{sg}(odd(S(S(n)+n)))=\overline{sg}(\overline{sg}(odd(S(n)+n)))= \overline{sg}(\overline{sg}(odd(n+S(n))))=\overline{sg}(\overline{sg}(1))=\overline{sg}(0)=1 by (iv), Lemma 5.(i) and Lemma 5.(v).

(xxiii) Use Equational Induction on n. If n=0 then by (vii) and Lemma 5.(v) odd(0\cdot S(0))=odd(0)=0. Suppose odd(n\cdot S(n))=0, then odd(S(n)\cdot S(S(n)))=odd(S(n)\cdot S(n)+S(n)))=odd(S(S(n)\cdot S(n)+n))=\overline{sg}(odd(S(n)\cdot S(n)+n))=\overline{sg}(odd(S(n)\cdot n+S(n)+n))=\overline{sg}(odd(S(n)\cdot n+n+S(n)))=\overline{sg}(odd(S(S(n)\cdot n+n+n)))=\overline{sg}(\overline{sg}(odd(S(n)\cdot n+2\cdot n)))=\overline{sg}(\overline{sg}(odd(n\cdot S(n)+2\cdot n)))=\overline{sg}(\overline{sg}(odd(n\cdot S(n))))=\overline{sg}(\overline{sg}(0))=0 by (iv), (ix), (xix), (xxi), Lemma 5.(i), Lemma 5.(ii) and Lemma 5.(v).

(xxiv) By Lemma 5.(v) and Lemma 5.(vi), odd(f'(0))=odd(0)=0. By (xvi), (xvii) and Lemma 5.(vi), odd(f'(1))=odd(1)=1.

Now, use Equational Induction on n to show that odd(f'(S(S(n))))=0 for all n. If n=0 then odd(f'(S(S(0))))=odd(\overline{sg}(f'(S(0)))+f'(S(0))\cdot S(f'(S(0))))=odd(\overline{sg}(1)+1\cdot S(1))=odd(0+S(1))=odd(S(1))=\overline{sg}(odd(1)))=\overline{sg}(1)=0 by (x), (xiv), (xvi), (xvii), Lemma 5.(v) and Lemma 5.(vi).

The induction step. Suppose odd(f'(S(S(n))))=0, then odd(f'(S(S(S(n)))))=odd(\overline{sg}(f'(S(S(n))))+f'(S(S(n)))\cdot S(f'(S(S(n)))))=odd(0+f'(S(S(n))))\cdot S(f'(S(S(n)))))=0 by (xviii) and (xxiii).

(xxv) By Lemma 5.(vii), P(0)=0.

Use Equational Induction on n to show that S(P(S(n)))=S(n) for all n. By (xxiv) and Lemma 5.(vii), P(1)=\overline{sg}(odd(f'(1)))\cdot S(P(0))=\overline{sg}(1)\cdot S(P(0))=0\cdot 1=0, so S(P(S(0)))=S(P(1))=S(0).

Suppose S(P(S(n)))=S(n), then by (xxiv) and Lemma 5.(vii), S(P(S(S(n))))=S(\overline{sg}(odd(f'(S(S(n)))))\cdot S(P(S(n))))=S(\overline{sg}(0)\cdot S(n))=S(1\cdot S(n))=S(S(n)).

(xxvi) Let S(n)=m. By (xxv), S(P(m))=m, so S(n)=m=S(P(m)), hence n=P(m) by successor axiom (ii). So we have P(S(n))=P(m)=n.

Assume PRA. Let g(m) and h(m,n,r) be given. Set h'(m,n,r)=h(m,S(n),r) and apply PRA to get the function f such that (\forall m)(f(m,0)=g(m)\&(\forall n)(f(m,S(n))=h'(m,n,f(m,n))))=h(m,S(n),f(m,n)).

Assume WPRA. Let g(m) and h(m,n,r) be given. Set h'(m,n,r)=h(m,P(n),r) and apply WPRA to get the function f such that (\forall m)(f(m,0)=g(m)\&(\forall n)(f(m,S(n))=h'(m,S(n),f(m,n))))=h(m,P(S(n)),f(m,n))=h(m,n,f(m,n)).

(i) Use Equational Induction on n. If n=0 then by Lemma 5.(viii) and Theorem 1.(xxvi), 1-S(0)=P(1-0)=P(1)=P(S(0))=0. Suppose 1-S(n)=0, then 1-S(S(n))=P(1-S(n))=P(0)=0.

(ii) Use Equational Induction on n. If n=0 then by Lemma 5.(viii) and Theorem 1.(xxvi), 2-S(S(0))=P(2-S(0))=P(P(2-0))=P(P(2))=P(P(S(S(0))))=P(S(0))=0. Suppose 2-S(S(n))=0, then 2-S(S(S(n)))=P(2-S(S(n)))=P(0)=0.

(iii) Let n\not=0 and n\not=1. Since n\not=0, we have (\exists m)(S(m)=n) by successor axiom (iii). Since S(m)=n\not=1=S(0), we have m\not=0 and by successor axiom (iii), (\exists r)(S(r)=m). Then n=S(S(r)), hence 2-n=2-S(S(r))=0 by (ii).

(iv) Let m\not=0 and P(n)=m, then n\not=0 and by successor axiom (iii), (\exists r)(S(r)=n). Then by Theorem 1.(xxvi), m=P(n)=P(S(r))=r and S(m)=S(r)=n. Conversely, if n=S(m) then P(n)=P(S(m))=m by Theorem 1.(xxvi).

(v) Use Equational Induction on n. If n=0 then by Lemma 5.(viii), 0-0=0. Suppose 0-n=0, then 0-S(n)=P(0-n)=P(0)=0.

(vi) Let n-1=0 and suppose that n\not=0 and n\not=1. Then as in (iii) we have n=S(S(r)) for some r, so n-1=P(n)=P(S(S(r)))=S(r)\not=0 by successor axiom (i), contradiction. Conversely, if n=0 then 0-1=0 by (v), if n=1 then 1-1=P(1-0)=P(1)=0.

(vii) If n=0 then 1-0=1\not=0. If n\not=0, then by successor axiom (iii), (\exists m)(S(m)=n). So 1-n=1-S(m)=0 by (i).

(viii) If n=1 then (n-1)+(1-n)=0+0=0 by (vi) and (vii). Suppose (n-1)+(1-n)=0 then by Theorem 1.(vi), n-1=0 and 1-n=0. By (vi), n=0\vee n=1. By (vii), we have n\not=0. Hence n=1.

(ix) If n=1 then (2-1)\cdot1=(S(S(0))-S(0))\cdot 1=P(S(S(0)-0))\cdot1=P(S(S(0)))\cdot1=S(0)\cdot1=1. If n\not=1 then by (iii), n=0\vee2-n=0, hence by Theorem 1.(xi), (2-n)\cdot n=0.

(x) Note that n is a variable of sort \omega and m is an external natural number. If n=m^* then by Definition 5, n=S(...S(0)), where there are m S’s. By Theorem 1.(xxvi), P(...P(n))=S(0)=1, since there are m-1 P’s.

To prove the converse we use external induction on m\geq2. The basis case is P(n)=1\rightarrow n=2 with m=2. To prove this suppose P(n)=1. Then n\not=0 and n\not=1 and as in (iii) we have that n=S(S(r)) for some r. Then P(n)=P(S(S(r)))=S(r), so S(r)=P(n)=1=S(0). By successor axiom (ii), r=0. Then n=S(S(0))=2.

The induction step. Suppose P(...P(n))=1\rightarrow n=m^*, m\geq2 is provable in PRA_{fcn}, where there are m-1 P’s. Then by substituting P(n) for n, P(...P(P(n)))=1\rightarrow P(n)=m^* is provable in PRA_{fcn}. By (iv), P(n)=m^*\leftrightarrow n=S(m^*)=(m+1)^*. Then P(...P(n))=1\rightarrow n=(m+1)^* is provable in PRA_{fcn}, where there are m P’s.

(xi) Let \varphi be a propositional combination of equations t_1=n^*_1, t_2=n_2^*,..., t_k=n_k^* for some k. For all i, 1\leq i\leq k, if n^*_i=0 then by Theorem 1.(xiv), t_i=0 is replaced by \overline{sg}(t_i)=1, if n^*_i=1 then t_i=1 remains unchanged, if n_i^*\geq2 then by (x), t_i=n_i^* is replaced by P(...P(t))=1.

(xii) It is proved by external induction on every propositional combination of equations of the form t=n^*. By (xi) we assume that they are propositional combinations of equations of the form t=1.

The basis case t=1. By (viii), t=1\leftrightarrow(n-1)+(1-n)=0.

Suppose \varphi\leftrightarrow t=0 is provable, then \neg\varphi\leftrightarrow t\not=0\leftrightarrow\overline{sg}(t)=0.

Suppose \varphi\leftrightarrow s=0 and \psi\leftrightarrow t=0 are provable, then \varphi\wedge\psi\leftrightarrow s+t=0 is provable by Theorem 1.(vi).

(xiii) Let \varphi be a singular open formula. By (xii), \varphi is equivalent to an equation t=0. By Lemma 3 PRA_{fcn} proves induction for the equation t=0, i.e. induction for \varphi.

(xiv) P(0)=0, P(1)=P(S(0))=0. Suppose that n\not=0 and n\not=1. Then as in (iii) we have that n=S(S(m)) for some m. Then P(n)=P(S(S(m)))=S(m)\not=0 by successor axiom (i).

(xv) Use Equational induction on m. If m=0 then S(n)-S(0)=P(S(n)-0)=P(S(n))=n=n-0. Suppose S(n)-S(m)=n-m, then S(n)-S(S(m))=P(S(n)-S(m))=P(n-m)=n-S(m).

(xvi) Use Equational induction on m. If m=0 then (n+0)-0=n. Suppose (n+m)-m=n, we want to prove (n+S(m))-S(m)=n. If m=0, then (n+S(0))-S(0)=P((n+S(0))-0)=P(n+S(0))=P(S(n+0))=P(S(n))=n. If m\not=0, then by by successor axiom (iii), (\exists m')(m=S(m')). We have (n+m)-m=n, i.e. (n+S(m'))-S(m')=n, then S(n+m')-S(m')=n. Hence by (xv), S(S(n+m'))-S(S(m'))=n. Hence (n+S(S(m')))-S(S(m'))=n, i.e. (n+S(m))-S(m)=n.

(xvii) n+r=m+r\rightarrow(n+r)-r=(m+r)-r\rightarrow n=m by (xvi).

(xviii) We use Theorem 1.(xiii). If r=0 then sg(r)=0, then n\cdot sg(r)=n\cdot0=0=m\cdot0=m\cdot sg(r). If r\not=0 and n=m then sg(r)=1 and n\cdot sg(r)=n=m=m\cdot sg(r). Conversely, assume n\cdot sg(r)=m\cdot sg(r). If r=0, then we are done, if r\not=0, then sg(r)=1 and so n=m.

(xix) Use Equational induction on n. If n=0, then 0-0=0 by Lemma 5.(viii). Suppose n-n=0, then by (xv), S(n)-S(n)=n-n=0.

(xx) Use Equational induction on n. If n=0, then S(0)-0=S(0)=1. Suppose S(n)-n=1, then by (xv), S(S(n))-S(n)=S(n)-n=1.

(xxi) Let n\not=0. Then by successor axiom (iii), (\exists r)(S(r)=n). Then P(n)+S(m)=P(S(r))+S(m)=r+S(m)=r+(m+1)=r+(1+m)=(r+1)+m=S(r)+m=n+m by Theorem 1.(i), Theorem 1.(iv), Theorem 1.(v).

(xxii) By (xviii) this statement is equivalent to an equation in m and n. So we can use Equational Induction on m to prove the statement. If m=0 then (n-0)+0=n. Suppose n-m=0\vee(n-m)+m=n. We need to prove that n-S(m)=0\vee(n-S(m))+S(m)=n. If n-m=0 then P(n-m)=0, then n-S(m)=P(n-m)=0 by Lemma 5.(viii). If n-m\not=0 and (n-m)+m=n, then by (xxi), (n-S(m))+S(m)=P(n-m)+S(m)=(n-m)+m=n.

(xxiii) The formula can be put into the form n-m\not=0\vee m-n\not=0\vee n=m, where n-m\not=0\vee m-n\not=0 is a singular open formula. Hence by (xii) we can put the formula into the form t=0\vee n=m and then by (xviii) into a single equation, and after that use Equational Induction on m.

The basis case m=0. If n-0=0-n=0 then n=0 and n=m holds.

Suppose n-m=m-n=0\rightarrow n=m and assume n-S(m)=S(m)-n=0. Clearly, n\not=0 (otherwise S(m)-0=0, contradiction to successor axiom (i)). By successor axiom (iii), n=S(r) for some r, hence S(m)-n=S(m)-S(r)=0. By (xv), S(m)-S(r)=m-r=0. By Lemma 5.(viii), m-n=m-S(r)=P(m-r)=P(0)=0. If n-m=0 then by induction hypothesis n=m, then by (xx), 1=S(m)-m=S(m)-n=0, contradiction. Hence n-m\not=0. Since n-S(m)=0, we have P(n-m)=n-S(m)=0, then by (xiv), n-m=0\vee n-m=1. Since n-m\not=0, we have n-m=1. Also by (xxii), (n-m)+m=n. Then 1+m=n and by Theorem 1.(i) we have n=S(m).

(xxiv) Follows from (xxiii) and (xix).

(xxv) Suppose n-m\not=0 and m-n\not=0. By (xxii), (n-m)+m=n and (m-n)+n=m. Hence (n-m)+m+(m-n)+n=n+m. By Theorem 1.(iv) and Theorem 1.(v), (n-m)+(m-n)+m+n=0+m+n. By (xvii), (n-m)+(m-n)=0. By Theorem 1.(vi), n-m=0 and m-n=0.

(xxvi) Suppose n-m=0. If m-n=0 then by (xxiii), n=m and we can take r=0. Assume m-n\not=0. By (xxii), (m-n)+n=m and we can take r=m-n.

(xxvii) Let \varphi be a propositional combination of equations s_1=t_1,...s_k=t_k for some k. By (xxiv), \varphi is provably equivalent to a propositional combination of equations r_i=0, i.e. to a singular open formula. By (xii), \varphi is provably equivalent to an equation t=0.

(xxviii) By (xxvii) and (xiii).

By definition of terms in L_{fcn} and composition axioms, the term s can be rewritten as g(n,m,r) and the term t can rewritten as h(n,m,r) for some ternary functions g and h. By Theorem 6.(xxvii), \varphi is equivalent to an equation f_1(n,m,r)=0.

Define the auxiliary function f_2(n,m,r)=n\cdot\overline{sg}(m)+r\cdot sg(m). By Theorem 1.(xiii) and Theorem.1.(xiv), f_2(n,m,r)=n if m=0 and f_2(n,m,r)=r otherwise.

By composition axioms define f(n,m,r)=f_2(g(n,m,r),f_1(n,m,r),h(n,m,r)).

Extensional uniqueness follows from the Theorem 6.(xxviii).

By Lemma 7 define the auxiliary function h:

By PRA, (\exists f)(\forall m)(f(m,0)=0)\wedge(\forall m,n)(f(m,S(n))=h(m,n,f(m,n)).

The extensional uniqueness is by open induction.

(i) By Definition 7, m<0 if and only if f(m,0)=S(0), but by Lemma 8, f(m,0)=0 for all m.

(ii) By Definition 7 and Lemma 8, m<S(n)\leftrightarrow f(m,S(n))=S(0)\leftrightarrow f(m,n)=S(0)\vee m=n\leftrightarrow m<n\vee m=n\leftrightarrow m\leq n.

(iii) By Definition 7 and Theorem 6.(xii), m<n\leftrightarrow f(m,n)=S(0)\leftrightarrow t=0 for some t. Hence by Theorem 6.(xii) every propositional combination of inequalities \leq,<,= is equivalent to an equation t=0.

(iv) This follows from (iii) and open induction.

(v) Use induction on n. If n=0 then we have 0=0 and by Definition 7, 0\leq0. Suppose 0\leq n, then by (ii), 0<S(n), hence by Definition 7, 0\leq S(n).

(vi) We show m\leq n\rightarrow m-n=0\rightarrow (n-m)+m=n\rightarrow(\exists r)(m+r=n)\rightarrow m\leq n.

First, prove m\leq n\rightarrow m-n=0 by induction on n. Let n=0 and assume m\leq0, then by (i), m=0 and m-n=0-0=0, so m\leq0\rightarrow m-0=0. Suppose m\leq n\rightarrow m-n=0 and assume m\leq S(n). If m=S(n) then by Theorem 6.(xix), m-S(n)=S(n)-S(n)=0, i.e. m\leq S(n)\rightarrow m-S(n)=0. If m<S(n) then by (ii), m\leq n and hence m-n=0. Then m-S(n)=P(m-n)=P(0)=0, i.e. m=S(n)\rightarrow m-S(n)=0.

Prove m-n=0\rightarrow (n-m)+m=n. Suppose m-n=0. By Theorem 6.(xxii), n-m=0\vee(n-m)+m=n. If n-m=0 then by Theorem 6.(xxiii), m=n and (n-m)+m=(n-n)+n=0+n=n. If (n-m)+m=n then we are done.

To prove (n-m)+m=n\rightarrow(\exists r)(m+r=n) set r=n-m and use Theorem 1.(iv).

Now prove (\exists r)(m+r=n)\rightarrow m\leq n. Assume (\exists r)(m+r=n). By Theorem 6.(xxvi), m-n=0. We prove m-n=0\rightarrow m\leq n by induction on n. If n=0 then assume m-0=0, and we have m=0, 0\leq 0. Suppose m-n=0\rightarrow m\leq n and assume m-S(n)=0. Then P(m-n)=0 and by Theorem 6.(xiv), m-n=0\vee m-n=1. If m-n=0 then m\leq n and by (ii), m<S(n), i.e. m\leq S(n). If m-n=1 then by Theorem 6.(xxii), m=(m-n)+n=1+n=S(n), i.e. m\leq S(n).

(vii) We show m<n\rightarrow S(m)<S(n)\rightarrow S(m)\leq n\rightarrow m<n.

Suppose m<n, then m\leq n and by (vi), let m+r=n with r\not=0. Then by successor axiom (iii), (\exists t)(r=S(t)) for some t and n=m+r=m+S(t)=m+t+1=m+1+t=S(m)+t. Hence S(m)\leq n by (vi) and S(m)<S(n) by (ii).

Suppose S(m)<S(n) then S(m)\leq n by (ii).

Suppose S(m)\leq n. Then S(m)+r=n for some r by (vi). We have n=S(m)+r=m+1+r=m+r+1=m+S(r). Then m\leq n by (vi). If m=n then m=S(m)+r=r+S(m), then by Theorem 6.(xix) and Theorem 6.(xx), 0=m-m=r+S(m)-m=r+1=S(r), contradiction to successor axiom (i). Hence m<n.

(viii) By Theorem 6.(xix), n-n=0. Then by (vi), n\leq n.

By Theorem 6.(xxv), m-n=0\vee n-m=0. Then by (vi), m\leq\vee n\leq m, i.e. \leq is connected.

Let n\leq m\wedge m\leq r, then by (vi), n+s=m\wedge m+t=r, then n+s+t=r, then by (vi), n\leq r, i.e. \leq is transitive.

Let m\leq n\wedge n\leq m, then by (vi), n+r=m and m+s=n. Then n+r+s=n, and hence r+s=0, and by Theorem 1.(vi), r=s=0 and m=n, i.e. \leq is antisymmetric.

0 is the least element by (v).

(ix) To show that < is irreflexive, suppose n<n. Then by (vii), S(n)\leq n, and so by (vi), let n=S(n)+r=n+1+r=r+1+n. Then 0=n-n=r+1+n-n=r+1=S(r), contradiction to successor axiom (i). So < is irreflexive and from (viii) it is transitive and has trichotomy, with least element 0.

By (ii), n<S(n). Suppose n<m<S(n) for some m, then by (ii), n<m\wedge(m=n\vee m<n) which contradicts the linearity of <. Hence each S(n) is the immediate successor of n in <.

Let n\not=0, then by Theorem 1.(xxv), S(P(n))=n is the immediate successor of P(n) in <.

(x) Suppose n+m\leq n+r, then by (vi), (\exists t)(n+m+t=n+r). Then m+t=r, and by (vi), m\leq r.

Suppose m\leq r, then by (vi), (\exists t)(m+t=r). Then n+m+t=n+r, and so n+m\leq n+r by (vi).

(xi) Suppose n+m<n+r, then n+m\leq n+r and by (x), we have m\leq r. Now m=r is impossible by irreflexivity of <, so m<r.

Suppose m<r, then m\leq r and by (x), we have n+m\leq n+r. If n+m=n+r then m=r violating irreflexivity.

(i) By Lemma 7 and Definition 7.

(ii) By PRA, (i) and Lemma 7, define f_{max}(m,0)=0 and

f_{max}(m,S(n))=\left\{ \begin{array} [c]{ll} max(f_{max}(m,n),f(S(n))), \mbox{ if } g(m,S(n),S(n))=0 \\ f_{max}(m,n), \mbox{ otherwise} \end{array} \right.

Clearly, f_{max}(m,n)\leq f_{max}(m,S(n)). Also r\leq n\rightarrow f_{max}(m,r)\leq f_{max}(m,n) by open induction on n.

Now let g(m,n,r)=0\wedge r\leq m, then f(r)\leq f_{max}(m,r)\leq f_{max}(m,n), i.e. f_{max}(m,n)=\max \{f(r)|r\leq n\wedge g(m,n,r)=0\}.

(iii) By PRA and Lemma 7, define h(m,0)=0 and

h(m,S(n))=\left\{ \begin{array} [c]{ll} S(n), \mbox{ if } f(S(n))=f_{max}(m,n) \\ h(m,n), \mbox{ otherwise.} \end{array} \right.

(i) The function t exists by PRA and is extensionally unique by Equational Induction.

(ii) Note, that since 0<n+1, we have t(n)+0<t(n)+n+1=t(S(n)) by Lemma 9.(xi).

We prove m<n\rightarrow t(m)<t(n) by open induction on n. Suppose m<n\rightarrow t(m)<t(n) and assume m<S(n). By Lemma 9.(ii), m\leq n. If m<n then t(m)<t(n)<t(S(n)). If m=n then t(m)=t(n)<t(S(n)).

(iii) Let n=m+2. Since t(m+1)>0, we have t(n)=t(m+2)=t(m+1)+m+2=t(m+1)+n>n.

(iv) Define by Lemma 7

g(m,n,r)=\left\{ \begin{array} [c]{ll} 0, \mbox{ if } t(r)\leq n \\ 1, \mbox{ otherwise}. \end{array} \right.

Then apply Lemma 10.(ii) to get t_{max}(n)=\max \{t(r):r\leq n\wedge t(r)\leq n\}. Then by Lemma 10.(iii), set t'(n)=\max \{r\leq n:t(r)=t_{max}(n)\}.

(v) Let n be given and let by (iv), m be greatest such that t(m)\leq n. Set r=n-t(m). Since t(m+1)\leq n is false, then n<t(m+1)=t(m)+m+1. So r=n-t(m)<t(m)+m+1-t(m)=m+1=S(m), hence by Lemma 9.(ii), r\leq m.

For uniqueness, let t(m)+r=t(m')+r'\wedge r\leq m\wedge r'\leq m'. Assume m<m'. Then S(m)\leq m', and by (ii), t(S(m))\leq t(m'). Then by Lemma 9.(x), t(S(m))+r'\leq t(m')+r'=t(m)+r, and so t(m)+m+1+r'\leq t(m)+r. Hence m+1+r'\leq r\leq m, contradiction. By symmetry, m'<m is impossible. Therefore m=m' and r=r'.

(vi) Note, that \langle,\rangle is defined by composition of functions T and +. Let n be given, then by (v), (\exists!m,r)(n=t(m)+r\wedge r\leq m). By Lemma 9.(vi) \exists k(r+k=m), then \langle k,r\rangle=t(k+r)+r=t(m)+r=n, so n=\langle k,r\rangle and \langle, \rangle is a surjective function.

To define p_2 note that t(n+m)\leq t(n+m)+m and t(n+m+1)=t(n+m)+n+m+1, i.e. \neg t(n+m+1)\leq t(n+m)+m. Hence by (iv), t'(t(n+m)+m)=n+m. Now define p_2(t(n+m)+m)=(t(n+m)+m)-t(t'(t(n+m)+m))=(t(n+m)+m)-t(n+m)=m, so we have p_2(\langle n,m\rangle)=m.

Define p_1(t(n+m)+m)=t'(t(n+m)+m)-p_2(t(n+m)+m)=(n+m)-m=n, so we have p_1(\langle n,m\rangle)=n.

Let n be given, then n=\langle m,r\rangle for some m,r, hence p_1(n)=m, p_2(n)=r. So n=\langle p_1(n),p_2(n)\rangle.

Suppose \langle n,m\rangle=\langle n',m'\rangle then n=p_1(\langle n,m\rangle)=p_1(\langle n',m'\rangle)=n' and m=p_2(\langle n,m\rangle)=p_2(\langle n',m'\rangle)=m', so \langle,\rangle is a bijection.

(i) Since the characteristic function \chi of A\subseteq2\omega+1 exists, i.e. the condition n\in A could be expressed as \chi_A(n)=1, we define by Lemma 7 the following function:

g'(n)=\left\{ \begin{array} [c]{ll} n+1, \mbox{ if } odd(n)=1, \mbox{ or } n+1\not\in A \\ n+2, \mbox{ otherwise}. \end{array} \right.

Then g'(n) is the least number outside of A and greater than n.

Now define f(0)=0, f(n+1)=g'(f(n)). Clearly (\forall n)(f(n)\not\in A) and it is easy to prove n<m\rightarrow f(n)<f(m) by open induction.

Since f is strictly increasing, it is also easy to prove f(n)\geq n by open induction.

Let n\not\in A. By Lemma 10.(ii) define f_{max}(n)=\max \{f(r):r\leq n\wedge f(r)\leq n\} and denote t=f_{max}(n). Let s be such that t=f(s) and suppose that t<n.

We claim that g'(t)\leq n. If g'(t)=t+1 then g'(t)\leq n by Lemma 9.(vii). Suppose g'(t)=t+2 and n<g'(t)=S(t+1). Then by Lemma 9.(ii), n\leq t+1. By Definition 7, n<t+1\vee n=t+1. If n<t+1 then by Lemma 9.(ii), n\leq t, contradicts to t<n. If n=t+1, then since n\not\in A, by definition, g'(t)=t+1=n, contradiction. So, we have g'(t)\leq n.

By definition, f(s+1)=g'(f(s))=g'(t)\leq n. This contradicts to the choice of t. Hence t=n, i.e. f(s)=t=n and f is surjection.

(ii) Since n<m\rightarrow f(n)<f(m), there is the only s such that f(s)=n. By Lemma 10.(iii) define f'(n)=s. Clearly n\not\in A'\rightarrow f(f'(n))=n.

(iii) Define

g(n)=\left\{ \begin{array} [c]{ll} 2\cdot f'(n), \mbox{ if } n\not\in A \\ h(n), \mbox{ otherwise}. \end{array} \right.

Then g maps \omega-A one-one onto 2\omega, and A one-one onto 2\omega+1. Hence g is a permutation which agrees with h on A.

(i) This function exists by PRA and Lemma 5.

(ii) By Theorem 1.(xix), odd(S(2\cdot n))=\overline{sg}(odd(2\cdot n))=\overline{sg}(0)=1.

(iii) Use Equational Induction on n. If n=0 then q(2\cdot 0)=q(0)=0. Suppose q(2\cdot n)=n, then by (ii), Theorem 1.(xii) and Theorem 1.(xx), q(2\cdot S(n))=q(S(n)+S(n))=q(n+1+n+1)=q(n+n+S(0)+S(0))=q(S(2\cdot n+S(0)+0))=q(S(2\cdot n+S(0)))=q(S(S(2\cdot n+0)))=q(S(S(2\cdot n)))=q(S(2\cdot n))+\overline{sg}(odd(S(S(2\cdot n))))=q(2\cdot n)+\overline{sg}(odd(S(2\cdot n)))+\overline{sg}(odd(2\cdot n))=n+\overline{sg}(1)+\overline{sg}(0)=n+0+1=S(n).

1\rightarrow2. Suppose that (\forall m)(\exists n)(f(m,n)=0), then by Lemma 1 define f'(r,m,n)=f(m,n). We have (\forall r,m)(\exists n)(f'(r,m,n)=0). By MIN^3 there exists g such that (\forall r,m)(g(r,m)=(\mu n)(f'(r,m,n)=0)). By Lemma 1 set g'(m)=g(r,m) for some fixed r, so we have g' such that (\forall m)(g'(m)=(\mu n)(f(m,n)=0)).

2\rightarrow3. Obvious.

3\rightarrow4. Suppose that (\forall n)(\exists!m)(f(m)=n). By Lemma 7 define h as follows:

We have (\forall n)(\exists!m)(h(n,m)=0), hence by MIN^1 there is g such that (\forall m)(h(m,g(m))=0), i.e. (\exists g)(\forall m)(f(g(m))=m).

4\rightarrow3 (Friedman [Fr21]). Let (\forall m)(\exists! n)(f(m,n)=0). Let A=\{2\cdot \langle m,n\rangle+1|f(m,n)=0\}. Then A has a characteristic function that is defined by conditional terms from Lemma 7 using the pairing system \langle,\rangle, p_1,p_2 from Lemma 11. Define h as follows:

Then h maps A one-one onto 2\omega+1. By Lemma 12.(iii), let g be a permutation of \omega which agrees with h on A. Applying PERM, g^{-1} exists and for all m, g^{-1}(2\cdot m+1)=2\cdot \langle m,n\rangle+1 for the unique n with f(m,n)=0. Let q be the quotient function from Lemma 13, define g'(m)=p_2(q(g^{-1}(2\cdot m+1)-1))=p_2(q(2\cdot \langle m,n\rangle+1-1))=p_2(q(2\cdot \langle m,n\rangle))=p_2(\langle m,n\rangle)=n. Then (\forall m)(f(m,g'(m))=0).

3\rightarrow2 (Friedman [Fr21]). Let (\forall m)(\exists n)(f(m,n)=0). Define h as follows by Lemma 7:

Clearly, (\forall m)(\exists!n)(h(m,n)=0). By MIN^1 there exists g such that (\forall m)(h(m,g(m))=0), i.e. f(m,g(m))=0. Also (\forall m)(\forall r<g(m))(f(m,g(m))\not=0)), so (\forall m)(g(m)=(\mu n)(f(m,n)=0)).

2\rightarrow1 (Friedman [Fr21]). Let (\forall m,n)(\exists r)(f(m,n,r)=0). Since \langle,\rangle is a bijection, define f'(\langle m,n\rangle,r)=f(p_1(\langle m,n\rangle), p_2(\langle m,n\rangle),r). We have (\forall m,n)(\exists r)(f'(\langle m,n\rangle),r)=0). By MIN^2 there exists g' such that (\forall m)(g'(\langle m,n\rangle)=(\mu r)(f'(\langle m,n\rangle),r)=0). Define g(m,n)=g'(\langle m,n\rangle).