3.2 MST Schemes for Logical Formulae
The logical formula for commutativity of addition is universally quantified over x and y. Now we want to find out how the computational paradigm tackles the cases of existential quantification and, especially, those where and alternate. As is well known, a sequence of identical quantifiers can be reduced to one by operating on tuples of variables, but there is no similar reduction when quantifiers alternate. We shall see that each placing of in front of , or vice versa, requires, computationally, a metasystem transition.
Let All be a function which uses a supercompiler
to prove universally quantified statements, as in the above examples. If the supercompiler
comes with a graph where no branch ends with F, it outputs T,
otherwise it outputs Z. Thus
To introduce existential quantification we define the function Exs which constructs by driving the potentially infinite tree of configurations using the breadth-first principle. If it finds that some branch ends with T, it outputs T. Otherwise it works infinitely - or, realistically, till it is stopped:
<Exs |
{<P x>}> = | T; is proven |
||
is stopped; no information |
As always in Refal, a variable x may be an n-tuple (x1)...(xn).
If all these variables take part in the driving implied in <All {<P
x>}> or <Exs {<P x>}>, they are
all appropriately quantified, e.g., computing
<All ........... > |
<P x, y, z> |
is proving ). We can fix the value of
one variable, say x, by raising it to the top level (see Sec.2.4):
<All ...x ....... > |
<P , y, z> |
This computation requires some value of x be given, and for this
value it tries to prove ).
We can consider this function as a predicate depending on x and quantify it existentially by submitting it to function Exs:
<Exs ........................ > |
<All ...x ....... > |
<P , y, z> |
This is the metacomputation formula for . In a similar manner we establish that the logical formula is represented by:
<All ........................ > |
<Exs ..... x ........... > |
<All .. | y ..... > |
<P , , z> |
Following these lines it is easy to construct an MST scheme for every logical formula, after it has been reduced to the prenex form.
As an example, consider the theorem: there exists no maximal natural number: . Here the function Less is defined as follows:
<Less x'1',y'1'> = <Less x,y> |
<Less x'1','0'> = F |
<Less '0',y'1'> = T |
<Less '0','0'> = F |
To prove the theorem, we first reduce the proposition to the prenex normal form: , (we have used the equivalence ), then we form the corresponding MST scheme:
<All ................ > |
<Exs ..... x .. > |
<Less , y> |
Supercompilation of this simple configuration can be done manually, and I did it. I wrote a specialized version of Exs which does driving in the expectation that the only function called is Less. Then I did the supercompilation implied in All, and the result was T, which proves the theorem.