next up previous contents index
Next: An Example Up: Computation Previous: Properties of the

Computational Content

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