But the way that that proof is written makes it difficult to follow. Can you write it in the usual way without adding a new Skolem function, and with explicit quantifiers instead of free variables?
Carl, as you asked me, I'm writing the proof in Peano arithmetic syntax - with explicit quantifiers.
Here is three axioms, which define Ackerman function:
A) $A(0,n) = n+1$$\forall n ~ A(0,n) = n+1$
B) $A(m+1,0) = A(m,1)$$\forall m ~ A(m+1,0) = A(m,1)$
C) $A(m+1,n+1) = A(m, A(m+1,n))$$\forall m,n ~ A(m+1,n+1) = A(m, A(m+1,n))$
If we define predicate $\varphi_A(m,n)$, which means: $\exists k ~ k=A(m,n)$, then the three base statements are true:
- $\forall n ~ \varphi_A(0,n)$
- $\forall m ~ \varphi_A(m,1) \to \varphi_A(m+1,0)$
- $\forall m ~ [\forall k ~ \varphi_A(m,k)] \to [\forall n ~ \varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$
Hereafter the proof as such:
- $\forall m ~ [\forall k ~ \varphi_A(m,k)] \to \varphi_A(m+1,0)$ - from (2), by substitution $1$ in place of $k$.
- $\forall m ~ [\forall k ~ \varphi_A(m,k)] \to [\varphi_A(m+1,0) \wedge \forall n ~ \varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$ - from (3) and (4)
- $\forall m ~ [\forall k ~ \varphi_A(m,k)] \to [\forall n ~ \varphi_A(m+1,n)]$ - from (5), using the induction axiom:
$\forall m ~ [\varphi_A(m+1,0) \wedge \forall n ~ \varphi_A(m+1,n) \to \varphi_A(m+1,n+1)] \to [\forall n ~ \varphi_A(m+1,n)]$ - $\forall m,n ~ \varphi_A(m,n)$ - from (1) and (6), using the induction axiom:
$\forall n ~ \varphi_A(0,n) \wedge \forall m ~ [\forall n ~ \varphi_A(m,n) \to \forall n ~ \varphi_A(m+1,n)] \to \forall m ~ [\forall n ~ \varphi_A(m,n)]$