MHB Ackermann's function is well defined

[mathmari]

Hey!

To show that the Ackermann's function is well defined we have to show that for all $x, y \in \mathbb{N}$, there exists a $z \in \mathbb{N}$ such that $A(x,y)=z$, right?? (Wondering)

To prove we use induction on $x$.

Base case. For $x=0$ we have $A(0,y)=y+1$.
So, for all $y \in \mathbb{N}$ there exists a $z=y+1 \in \mathbb{N}$ such that $A(0,y)=z$.

Inductive hypothesis. We assume that it stands for $x=n$, that means that $
\exists z \in \mathbb{N}: A(n, y)=z$. (IH1)Inductive step. To show that $\exists z' \in \mathbb{N}: A(n+1, y)=z'$ we use induction on $y$.

Base case. For $y=0$ we have $A(n+1,0)=A(n,1)\overset{\text{ (IH1) }}{=}z$.
Inductive hypothesis. We assume that it stands for $y=m$, that means that $\exists z' \in \mathbb{N}: A(n+1, m+1)=z'$. (IH2)
Inductive step. $A(n+1, m+1)=A(n,A(n+1,m))\overset{\text{ (IH2) }}{=}A(n,z')=z$.​

Is this correct?? Or could I improve something?? (Wondering)

 

[Evgeny.Makarov]

It's sort of correct, but to make it fully correct you should re-read my description of different kinds if inductions for statements with two variables in another thread. When you are proving $\forall n,m\,\exists z\;A(n,m)=z$ by (external) induction on $n$, you have a choice to make about $m$. Either you fix $m$ for the duration of the whole proof, or you leave it universally quantified in the induction statement (the property of $n$ that you are proving by induction). You need to decide which one you need, why the other choice does not work, and then write the induction statement explicitly, quantifying every variable that should be quantified. In a proof like this, this is crucial if you want to understand all the details.

Also, you are writing things like $A(n,1)= z$ where the origin of $z$ is unclear.

Finally, IH2 should say $\exists z'\in\Bbb N:A(n+1,m)=z'$, not $A(n+1,m+1)=z'$.

 

[mathmari]

When you are proving $\forall n,m\,\exists z\;A(n,m)=z$ by (external) induction on $n$, you have a choice to make about $m$. Either you fix $m$ for the duration of the whole proof, or you leave it universally quantified in the induction statement (the property of $n$ that you are proving by induction). You need to decide which one you need, why the other choice does not work, and then write the induction statement explicitly, quantifying every variable that should be quantified. In a proof like this, this is crucial if you want to understand all the details.

There are several ways of proving $\forall m,n.\,P(m,n)$ by induction.

(1) Fix an arbitrary $m$ as in a direct proof and prove $\forall n.\,P(m,n)$ by induction on $n$. Then in proving the induction step $P(m,n+1)$ one can only to use the induction hypothesis $P(m,n)$ for the same $m$.

(2) Fix an arbitrary $n$ and prove $\forall m.\,P(m,n)$ by induction on $m$. This is similar to (1).

(3) Prove the statement $\forall n.\,P(m,n)$ by induction on $m$. Compared to (2), in the induction step one has to prove $\forall n.\,P(m+1,n)$ and not just $P(m+1,n)$ for some previously fixed $n$. However, this is irrelevant since $n$ is arbitrary anyway. But in this case one has a stronger induction hypothesis: $\forall n.\,P(m,n)$ versus $P(m,n)$ in (2). This means that in proving $P(m+1,n)$ one can use the hypothesis $P(m,n')$ for any $n'$, not necessarily equal to $n$. In other words, whereas in (2) the parameter $n$ is fixed throughout the proof, in this method one can use the induction hypothesis with a different value of the parameter. For some statements, this type of induction goes through while (2) does not.

(4) Prove the statement $\forall m.\,P(m,n)$ by induction on $n$. This is better than (1) similarly to how (3) is better than (2).

(5) Use nested induction: external on $m$ and internal on $n$. This is what you described in post #2. This is even more powerful than (3): one has the same induction hypothesis $\forall n.\,P(m,n)$, but one proves $\forall n.\,P(m+1,n)$ by induction on $n$ and not using a direct proof (the latter doesn't always work).

(6) Use nested induction: external on $n$ and internal on $m$. This is similar to (5).

I think that we have to use the third way of induction. To use the nested induction $(5)$ we would have to assume at the inductive hypothesis that $A(n,y)=z$ stands for all $y \in \mathbb{N}$ to continue at the inductive step but this is what we want to show. Is this correct?? (Wondering) I tried the following but I got stuck...

For all $x, y \in \mathbb{N}$, there exists a $z \in \mathbb{N}$ such that $A(x,y)=z$.

Induction on $x$.

Base case. For $x=0$ we have $A(0,y)=y+1$.

So, for all $y \in \mathbb{N}$ there exists a $z=y+1 \in \mathbb{N}$ such that $A(0,y)=z$.

Inductive hypothesis. We assume that it stands for $x=n$, that means that $

\exists z \in \mathbb{N}: A(n, y)=z, \forall y \in \mathbb{N}$. (IH)

Inductive step. We want to show that $\exists z \in \mathbb{N}: A(n+1, y)=z, \forall y \in \mathbb{N}$.
$A(n+1, y)=A(n,A(n+1, y-1))$.

Is this correct so far ?? (Wondering)

How can we get rid of the $n+1$ of the first argument of $A$ and get $n$ so that we can use the inductive hypothesis?? (Wondering)

 

[Evgeny.Makarov]

The induction statement of the external induction IH1 is $\forall y\,\exists z.\;A(n,y)=z$. This is proved by induction on $n$.

Inductive hypothesis. We assume that it stands for $x=n$, that means that $\exists z \in \mathbb{N}: A(n, y)=z, \forall y \in \mathbb{N}$. (IH)

All quantifiers should be written up front:
\[
\forall y\,\exists z.\;A(n,y)=z.\qquad\text{(IH1)}
\]

[Inductive step. We want to show that $\exists z \in \mathbb{N}: A(n+1, y)=z, \forall y \in \mathbb{N}$.

Should say \(\forall y\,\exists z.\; A(n+1, y)=z\).

How can we get rid of the $n+1$ of the first argument of $A$ and get $n$ so that we can use the inductive hypothesis?

$\forall y\,\exists z.\; A(n+1, y)=z$ is proved by induction on $y$. The induction statement $P(y)$ is $\exists z.\; A(n+1, y)=z$. For $y=0$ we have $A(n+1,0)=A(n,1)$ and instantiating $y=1$ in the induction hypothesis (IH1) we have $\exists z.\,A(n,1)=z$, as required. Note that we started from $A(n+1,0)$ where $y=0$, but we had to apply IH1 where $y=1$. This is why it is important that IH1 be universally quantified over all $y$. You can't fix $y=0$.

Similarly, in the inductive step we need to prove \(\exists z.\; A(n+1, m+1)=z\). But $A(n+1,m+1)=A(n,A(n+1,m))$. You apply IH2 to get some $z$ such that $A(n+1,m)=z$. Then instantiate $y=z$ in IH1. Again, $y$ changes from $m+1$ to some $z$ that we obtained from IH2. This means that IH1 has to be universally quantified.

 

[mathmari]

I tried it again...

For all $x, y \in \mathbb{N}$, there exists a $z \in \mathbb{N}$ such that $A(x,y)=z$.

Induction on $x$.

Base case. For $x=0$ we have $A(0,y)=y+1$.

So, for all $y \in \mathbb{N}$ there exists a $z=y+1 \in \mathbb{N}$ such that $A(0,y)=z$.

Inductive hypothesis. We assume that it stands for $x=n$, that means that $

\forall y \exists z: A(n, y)=z$. (IH1)

Inductive step. We want to show that $\forall y \exists z: A(n+1, y)=z$.

Induction on $y$.
Base case. For $y=0$ we have $A(n+1, 0)=A(n,1)$. From (IH1) we have that $\exists z: A(n,1)=z$. So, $A(n+1, 0)=z$.
Inductive hypothesis. We assume that it stands for $y=m$ that means that $\exists z: A(n+1, m)=z$ (IH2)
Inductive step. We want to show that $\exists z: A(n+1, m+1)=z$.
$A(n+1,m+1)=A(n,A(n+1,m))$
From (IH2) we have that $\exists z : A(n+1, m)=z$.
So, $A(n+1, m+1)=A(n,z)$.
From (IH1) we have that $A(n,z)=z$.
So, $A(n+1, m+1)=z$.​

Is this correct?? (Wondering) Do we have to use different $z$ in the two induction hypotheses or is it correct to use the same?? (Wondering)

 

[mathmari]

When we prove that $\forall x, y \in \mathbb{N}$ there exists a $z\in \mathbb{N}$ such that $A(x,y)=z$, have we proven that the Ackermann's function is well-defined? (Wondering)

Or do we have to show that there exists a unique $z\in \mathbb{N}$ such that $A(x,y)=z$ ?

 

[Evgeny.Makarov]

Uniqueness has to be shown as well.

In general, if there is a well-ordered set $(S,{<})$, then we can consider a function
\[
f(x)=\begin{cases}c,&x\text{ is the least element}\\g(f(h(x)),x),&\text{otherwise}\\\end{cases}
\]
defined by recursion using two functions $g$ and $h$ such that $h(x)<x$ if $x$ is not the least element. Such $f$ is well-defined w.r.t. both existence and uniqueness.