** Next:** An Example
**Up:** Computation
** Previous:** Properties of the

Not all theorems are interesting computationally, of course.
Recall the ` rootf` function defined in the preceding chapter;
` rootf(`**n**) returns the unique integer **i** such that if **n<0**
then **i=0** and otherwise .
Now consider the following two theorems, where ` square(x)`
is defined as ` rootf(x)*rootf(x)=x in int`.

Thm1 >>all x:int. square(x) | ~ square(x).
Thm2 >>all x:int. square(x) vel ~ square(x).

The first theorem can be proved by introducing **x** and applying the
` rootf` function to **x**.
We can prove that either ` rootf(x)*rootf(x)=x in int` or not
by using the arithmetic rule, ` arith`; the proof yields a
decision procedure identifying which case holds.
From a proof of ` Thm1`, then, we can extract a function which will decide
whether an integer is a square , namely
`
x.decide(term_of(Thm1)(x);
u.0;v.1)`. This function gives **0** if **x** is a square and **1** otherwise.
The second theorem has a trivial proof. We simply use the fact that
` `**P** vel ~ **P** holds for any proposition **P** and take ` rootf(x)*rootf(x)=x in int`
as **P**. However, there is no interesting computational content to this
result; we do not obtain from it a procedure to decide whether **x** is a
square. (The interested reader should prove this theorem and display
its computational content.)

*Richard Eaton *

Thu Sep 14 08:45:18 EDT 1995