Stratified abstraction

The components of the logic of Watson given so far support the logic of propositional connectives and equality, in conventional terms.

The new component of the logic introduced here is a restricted form of $\lambda$-abstraction, the introduction of functions by abstraction. The new component is adequate to support the logic of quantification, and also a powerful higher-order logic.

The particular higher-order logic used will be unfamiliar to most readers, though (we hope) not difficult to explain. It is a variation on the nonstandard set theory ``New Foundations'' (NF) introduced by W. V. O. Quine in [25] (1937), as revised by R. B. Jensen in [19] (1969). Set theories like NF avoid paradox by allowing the scheme of set comprehension to be applied only to ``stratified'' predicates. We will not discuss the set theories here, but will describe the analogous system of $\lambda$-calculus with ``stratified'' $\lambda$-abstraction, which is the higher-order logic of Watson (references for this system are [13] (based on Holmes's Ph.D. thesis), which describes a system of synthetic combinatory logic rather than a $\lambda$-calculus, [15], which describes the $\lambda$-calculus, and chapter 23 of Holmes's book [17], which introduces further material about the representation of data types, discussed below).

The notation we will use in this subsection for $\lambda$-abstraction is different from the notation used by Watson. Watson uses a scheme of name-free variable binding due to de Bruijn (see [8]; not de Bruijn indices, but a related scheme which we have seen called ``de Bruijn levels''); this will be explained below. In this subsection, the usual $\lambda$-notation will be used. The usual notation f(x) for function application will be used instead of the notation (fx) more usual in $\lambda$-calculus.

We introduce the term constructions of a stratified $\lambda$-calculus. These are defined by mutual recursion with a notion of ``relative type''. We begin with the description of the type constructions and follow it with a description of the notion of ``relative type''.

variables:

We have a countably infinite supply of variables.

primitive constants:

true and false are primitive constants, as are the projection functions $\pi_1$ and $\pi_2$. There is a temptation to identify the projection operators with the truth values which we will resist here.

equations:

If T and U are terms, T = U is a term.

pairs:

If T and U are terms, (T,U) is a term.

case expressions:

If P, T, and U are terms, if P then T else U is a term.

function application:

If T and U are terms, T(U) is a term.

$\lambda$-term:

If T is a term in which the variable x appears free with no type relative to T other than 0 (it need not appear at all) then $(\lambda x.T)$ is a term, in which the variable x is called the binding variable.

As usual, an occurrence of a variable x in a term T is termed bound if it appears as part of some occurrence of a subterm $(\lambda x.U)$ of T with the same binding variable; occurrences of variables which are not bound are said to be free.

We now define the notion of relative type. Each occurrence of a subterm of a term T has a type relative to T, which is an integer.

the whole term:

The type of the term T relative to itself is 0.

equations:

If the type of an occurrence of A = B relative to T is n, the types relative to T of the obvious occurrences of A and B are also n.

pairs:

If the type of an occurrence of (A,B) relative to T is n, the types relative to T of the obvious occurrences of A and B are also n.

case expressions:

If the type of an occurrence of if P then Q else R relative to T is n, the types relative to T of the obvious occurrences of P, Q, and R are also n.

function application:

If the type of an occurrence of A(B) relative to T is n, the types relative to T of the obvious occurrences of A and B are n+1 and n, respectively.

$\lambda$-terms:

If the type of an occurrence of $(\lambda x.U)$ relative to T is n, the type relative to T of the obvious occurrence of U is n-1 (by the condition on well-formedness of $\lambda$-terms, this will be the same as the type of the free occurrences of the variable x in U).

A well-formed $\lambda$-term is said to be stratified, for reasons which will be explained in the next subsection.

The axioms of this theory are the axioms of algebraic and case expression logic from above, plus the following axioms for the new notions of pair, application and $\lambda$-abstraction:

projection functions:

$\pi_1(x,y) = x$; $\pi_2(x,y) = y$.

$\beta$-reduction:

$(\lambda x.T)(A) = T[A/x]$

Unfortunately, things are not as simple as the brief paragraph before the new axioms tries to make them appear. Algebraic logic is extended to allow substitution of equals for equals inside $\lambda$-terms, without regard to the fact that the terms for which substitutions are made may fail to have reference outside the $\lambda$-terms, because of the presence of bound variables. This extension of the notion of substitution is equivalent to a weak form of extensionality for functions. Notice that we do not adopt the full axiom of extensionality, which we exhibit:

extensionality axiom not adopted:

$(\lambda x. f(x)) = f$

If we were to adopt this assumption we would have a system equivalent to Quine's ``New Foundations'', which is not known to be consistent. As it is we have a system equivalent to an extension of the modification NFU + Infinity of NF due to Jensen in [19], which is known to be equivalent to Russell's theory of types (with infinity), which is generally believed to be consistent.

Further, the notion of substitution which appears both here and in the earlier axioms is considerably complicated by the need to avoid collisions of bound variables. We will not give a formal account of substitution here, but we will give a formal description below of the notion of substitution for Watson's own notation (using de Bruijn levels).

We briefly indicate how quantification is supported. We can define the universal quantifier thus:

definition of $\forall$:

$(\forall x.T) = ((\lambda x.T) = (\lambda x.{\bf true}))$

The notation of Watson does not permit the introduction of new binders: the actual notation is more like $\forall(\lambda x.T)$. The existential quantifier $\exists$ may be defined using deMorgan's laws as usual. Reasoning with the existential quantifier may be facilitated by introducing a new primitive function choose and the dreaded

axiom of choice:

$(\exists x.T) = T[$choose $(\lambda x.T)/x]$

The HOL system uses this as the definition of the existential quantifier (and defines the universal quantifier in terms of the existential quantifier); this axiom can be used to facilitate existential reasoning in Watson, though the built-in logic without choice also supports adequate existential reasoning. It is interesting to note that the logic of Watson with full extensionality is inconsistent with the axiom of choice (because NF is inconsistent with choice).