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