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.)