Contents

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 $\exists$ 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  $\exists$ in front of $$\mbox{\tt\obeyspaces <All \mbox{$\mu$\{<P x>\}}>} = \left\{ \... ...spaces Z};\;\mbox{\rm no information} \end{array} \right.$$, 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

$$\mbox{\tt\obeyspaces <Exs \mbox{$\mu$\{<P x>\}}>} = \left\{ \... ...\mbox{\rm is stopped; no information} \end{array} \right.$$

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 $\forall y \forall z P(x,y,z)$). 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 $\forall y \forall z P(x,y,z)$).

    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 $\exists x \forall y \forall z P(x,y,z)$. In a similar manner we establish that the logical formula $\forall x\exists y\forall z P(x,y,z)$ 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: $\neg\exists x \forall y Less(y,x)$. 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: $\forall x \exists y Less(x,y)$, (we have used the equivalence $\neg{Less(y,x)}=Less(x,y)$), 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.

Contents  Next