Prove $Q \vdash [\forall x < \overline{n+1}]\phi \leftrightarrow [\phi^x_{\overline{n}}\land(\forall x <\bar{n})\phi]$

Question

Prove that $Q \vdash [\forall x < \overline{n+1}]\phi \leftrightarrow [\phi^x_{\overline{n}}\land(\forall x <\bar{n})\phi]$ where $Q$ is the Robinson Arithmetic, $\phi$ is a formula with single free variable $x$, and $\bar{n}$ denotes $S\cdots S(0)$ ($n$ times $S$).

I can certainly show that $Q \vdash x< \overline{n+1} \leftrightarrow (x<\bar{n} \lor x=\bar{n})$ using one of the axioms of Robinson Arithmetic ($\forall v_1 \forall v_2 (x<Sv_2 \leftrightarrow (v_1<v_2 \lor v_1=v_2))$, but I can't proceed anymore.

Answer 1

Note that $[\forall x < \overline{n+1}]\phi$ is a shorthand for $\forall x (x < \overline{n+1} \to \phi)$, which is equivalent to $\forall x ((x = \overline{n} \lor x < \overline{n}) \to \phi)$, as you correctly remarked.

Now, observe that $\forall x ((x = \overline{n} \lor x < \overline{n}) \to \phi)$ is equivalent to $\forall x ((x = \overline{n} \to \phi) \land (x < \overline{n} \to \phi))$, because in propositional logic $(A \lor B) \to C \equiv (A \to C) \land (B \to C)$.

Since in first-order logic $\forall x (A \land B) \equiv \forall x A \land \forall x B$, then $\forall x ((x = \overline{n} \to \phi) \land (x < \overline{n} \to \phi))$ is equivalent to $\forall x (x = \overline{n} \to \phi) \land \forall x(x < \overline{n} \to \phi)$, which is equivalent to $\phi_\overline{n}^x \land \forall x(x < \overline{n} \to \phi)$.

Answer 2

First part:

1) $\forall x \ ((x < (n+1)) \to \phi)$ --- premise

2) $(x < (n+1)) \to \phi$ --- from 1) by $\forall$-elim

3) $x < n$ --- assumed [a]

4) $x < (n+1)$ --- from 3) by $\lor$-intro and your equivalence

5) $\phi$ --- from 4) and 2)

6) $(x < n) \to \phi$ --- from 3) and 5) by $\to$-intro, discharging [a]

7) $\forall x \ ((x < n) \to \phi)$ --- from 6) by $\forall$-intro

8) $(n < (n+1)) \to \phi^x_n$ --- from 1) by $\forall$-elim

9) $\mathsf Q \vdash n < (n+1)$

10) $\phi^x_n$ --- from 9) and 8) by modus ponens

11) $\phi^x_n \land \forall x \ ((x < n) \to \phi)$ --- from 7) and 10) by $\land$-intro.

---

Second part:

1) $\phi^x_n \land \forall x \ ((x < n) \to \phi)$ --- premise

2) $\phi^x_n$ --- from 1) by $\land$-elim

3) $\forall x \ ((x < n) \to \phi)$ --- from 1) by $\land$-elim

4) $(x < (n+1))$ --- assumed [a]

5) $x < n \lor x=n$ --- from 4)

Now a proof by cases ($\lor$-elim) deriving $\phi$ under both braches: $x=n$ and $x < n$:

6) $\phi$

7) $(x < (n+1)) \to \phi$ --- from 4) and 6), discharging [a]

8) $\forall x \ ((x < (n+1)) \to \phi)$ --- from 7) by $\forall$-intro.