Arithmetic

When we display proofs of arithmetical propositions, we will assume that there is an automatic proof procedure which will prove any true quantifier free conclusion in a sequent involving 0, suc(n), +, -, *, = and <. So for example, here are some arithmetic facts in this category

$$0<x, y<suc(z) \vdash y*x < suc(z*x).$$

Although there is no proof procedure with this power (the problem is undecidable), there are good arithmetical proof procedures for restricted arithmetic restricted arithmetic (Arith) (Arith, see [18,27]) and linear arithmeticlinear arithmetic (SupInf) (SupInf, see [22,107,14]). We refer the interested reader to the citations for details. The use of Arith allows us to present proofs in a form close to that of Nuprl ([28,66]). Here are two proofs of the same trivial theorem, one inductive, one not. We write Arith $(l_1, \ldots, l_n)$ to show which labeled hypotheses are used by the proof procedure. For readability we intentionally elided parts of the justification, using --.

	$\vdash \forall x\!:\!{{\mathbb{N} }}.\: \exists y\!:\!{{\mathbb{N} }}.\: (x<y)$	by $\forall R(x, \_\_\_)$
	$x\!:\!{{\mathbb{N} }} \vdash \exists y\!:\!{{\mathbb{N} }}.\: (x<y)$	by $\exists R(s(x); \_\_\_)$
	$\vdash x <suc(x)$	by Arith

The complete proof expression is $\forall R(x.\: \exists R(suc(x); \mbox{Arith}))$.

$\vdash \forall x\!:\!{{\mathbb{N} }}.\: \exists y\!:\!{{\mathbb{N} }}.\: (x<y)$ by $\forall R(x.\: ---)$

$x\!:\!{{\mathbb{N} }} \vdash \exists y\!:\!{{\mathbb{N} }}.\: (x<y)$ by $ind(x; ---;\ \ \ )$

$\vdash \exists y\!:\!{{\mathbb{N} }}(0<y)$ by $\exists R(suc(0); \mbox{Arith})$

$x\!:\!{{\mathbb{N} }}, u\!:\!{{\mathbb{N} }}, i\!: \exists y\!:\!{{\mathbb{N} }}.\: (u<y) \vdash \exists y\!:\!{{\mathbb{N} }}.\: (suc(u)<y)$ by $\exists L(i; y_o,---)$

$x\!:\!{{\mathbb{N} }}, u\!:\!{{\mathbb{N} }}, y_o\!:\!{{\mathbb{N} }}, l\!:\!(u<y_o) \vdash \exists y\!:\!{{\mathbb{N} }}(suc(u)<y)$ by $\exists R(suc(y_o); ---)$

$\hspace*{1.8in} \vdash (suc(u)<suc(y_o))$ by Arith(l)

The complete proof expression is

$$\forall R(x.\: ind(x; \exists R(suc(0);\ \mbox{Arith}); u, i.... ...xists L(i; y_0, l.\: \exists R(suc(y_0);\ \mbox{Arith}(l))))).$$

The following example will provide another compact proof expression. It shows that integer square roots exist without using Magic ([90]). First we specify these roots. Let $Root(r, n) == r^2 \leq n < (r+1)^2.$

Theorem 4   $\vdash \forall n\!:\!{{\mathbb{N} }}.\ \exists r\!:\!{{\mathbb{N} }}.\ Root(r, n).$

by $\forall R\ \mbox{\textsc{then}}\ ind\ new\ u$
base case

1.

$n\!:\!{{\mathbb{N} }}$
$\vdash \exists r\!:\!{{\mathbb{N} }}.\ Root(r, 0)$
by $\exists R\: 0$ THEN Arith

induction case

1.

$n\!:\!{{\mathbb{N} }}$

2.

$u\!:\!\exists r\!:\!{{\mathbb{N} }}.\ Root(r, n)$
$\vdash \exists r\!:\!{{\mathbb{N} }}.\ Root(r, suc(n))$
by $\exists L\ on\ u\ new\ r_o, v$

3.

$r_o\!:\!{{\mathbb{N} }}$

4.

$v\!:\!Root(r_o, n)$
$\vdash \exists r\!:\!{{\mathbb{N} }}.\ Root(r, suc(n))$
by $cut\ (r_o +1)^2 \leq suc(n)\ \vee \ suc(n) < (r_o +1)^2$ with label d THENA Arith.
(This rule generates two subgoals. The ``auxiliary one'' is to prove the cut formula. That subgoal can be proved by Arith, so we say THENA Arith to indicate this.)

(The ``main'' subgoal is this one.)

5.

$d\!:\!(r_o+1)^2 \leq suc(n)\ \vee\ suc(n) < (r_o +1)^2$
$\vdash \exists r\!:\!{{\mathbb{N} }}.\ Root(r, n)$
by $VL\ on\ d$
(This is case analysis on the cases in hypothesis 5.)

6.

$(r_o+1)^2 \leq suc(n)$
$\vdash \exists r\!:\!{{\mathbb{N} }}.\ Root(r, n)$
by $\exists R (r_o+1)\ \mbox{\textsc{then}}\ SupInf$
(Since $r_o^2 \leq n < (r_o +1)^2$, from $(r_o+1)^2 \leq suc(n)$ we know $(r_o+1)^2 \leq suc(n) < ((r_o+1) +1)^2$ since n+1 < (r_o +1)² + 1. The SupInf procedure can find this proof.)

6.

suc(n) < (r_o +1)²
$\vdash \exists r\!:\!{{\mathbb{N} }}.\ Root(r, n)$
by $\exists R r_o$ THEN Arith
(Since $r_o^2 \leq n$ we know immediately that $r_o^2 \leq suc(n)$.)

The proof expression corresponding to this is

$\forall R(n.\ ind(n; \exists R(0; Arith);$
$n, u.\ \exists L(u; r_o, v.\ cut(d.\ VL(d; \exists R(r_o +1; SupIn\!f);$
$\exists R(r_o; Arith)); Arith)))).$
In the appendix, section 6.2, we consider another simple arithmetic example and show a complete Nuprl proof.