In section two of chapter three we proved a representation theorem stating that a domain D is, up to isomorphism, the ideal completion of its compact elements, Dc. An ordered set having the properties derivable for Dc was christened a cusl or conditional upper semilattice with least element. It turns out that a somewhat weaker version of cusl's, namely precusVs, serves just as well as a representation of domains and is better suited for the purposes of the last section of this chapter, which deals with solutions of domain equations to identity. In this chapter we sketch, without detailed proof, the basic results known on the representation of domains in this sense.

We begin with two additional representations of domains, information systems and formal spaces. Both have their origins in the works of D. S. Scott, Scott [1982] and [1982a], where the latter were presented in a less general form as neighbourhood systems. The versions presented here differ at some points from those of Scott for reasons to be explained later. Each of these three representations has its own particular point of departure. Cusl's and precusl's, by virtue of their emphasis on an ordering, give an algebraic representation. Information systems, based upon a relation of entailment, give a logical representation in analogy with the corresponding notion in formal logical systems. Finally, formal spaces, through their emphasis upon a relation of (formal) inclusion between neighbourhoods, provide a topological representation.

A domain is a structure modelling the notion of approximation and of computation. A computation performed using an algorithm proceeds in discrete steps. After each step there is more information available about the result of the computation. In this way the result obtained after each step can be seen as an approximation of the final result. This final result may be reached after finitely many steps as, for example, when computing the greatest common divisor of two positive integers using the Euclidean algorithm. However, it may also be the case that a computation never stops, in which case the final result is the sequence of approximations obtained from each step in the computation. The latter situation occurs by necessity when computing on infinite objects such as real numbers. Thus an appropriate model of approximation can provide a good model of computation.

To be somewhat more technically precise, a domain is a structure having one binary relation ⊑, a partial order, with the intended meaning that x ⊑y just in case x is an approximation of y or y contains at least as much information as x. We also require that a domain should include a least element modelling no information. This is not necessary, but is useful for establishing the existence of fixed points. To model infinite computations we require a domain to be complete in the sense that each increasing sequence of approximations should be represented by an element in the domain, that is, should have a supremum.

The class of partial recursive functions is the mathematical abstraction of the class of partial functions computable by an algorithm. In this chapter we present them in the form of the μ-recursive functions. We then state some basic results, the main motivation being to set the stage for the theory of effective domains. Finally we show that the partial μ-recursive functions can be obtained from some simple initial functions using substitution and the fixed point theorem for computable functional. This illuminates the central role of taking fixed points and supports the claim of Chapter 1 that the function computed by an algorithm or a program is the least fixed point of a computable functional.

Section 9.1 Partial Recursive Functions

An algorithm for a class K of problems is a method or procedure which can be described in a finite way (a finite set of instructions) and which can be followed by someone or something to yield a computation solving each problem in K. The computation should proceed in discrete steps. For a given problem in K the procedure should say exactly how to perform each step in the computation. After performing a step, the procedure should prescribe how to do the next step. This next step must only depend on the problem and on the then existing situation, that is what has been done during previous steps.

Very few mathematical statements can be judged to be true or false solely by means of direct observation. Some statements, the axioms, have to be accepted as true without too much further argument. Other statements, the theorems, are believed because they are seen as logical consequences of the axioms by means of a proof. Proofs constitute the only effective mechanism for revealing truth in mathematics. We would naturally hope that all provable statements are indeed true. Most of us would also optimistically believe that any true statement has a proof, but such is not the case. Gödel showed that for any reasonably powerful formal system of axioms and inference rules, there are statements that can neither be proved nor disproved on the basis of the axioms and inference rules, and are therefore undecidable. Gödel also showed that for such formal systems, there could be no absolute proof that all provable statements were in fact true. In his proof, Gödel described a machine that could check if a given construction constituted a valid proof. It was hoped that one could similarly define a machine to discover the proof itself, but Church and Turing showed that such a machine could not exist. We show in this book that a machine, the Boyer–Moore theorem prover, can be used to check Gödel's proof of the existence of undecidable sentences.

The construction of an undecidable sentence of Z2 will be completed in this chapter. This construction involves

1. Enumerating Z2 proofs using a one-to-one mapping from Z2 proofs to the natural numbers.

2. Defining a Lisp predicate that searches for the first proof or disproof (i.e., proof of the negation) of the given formula in this enumeration of proofs, and returns T or F, accordingly. Let this “theorem checker” be of the form (Theorem X), where X is the given formula.

3. Using the representability of the above predicate to construct a sentence U which can be seen to assert, “(Theorem u) = F,” where u is the Lisp representation of U. It will be shown that if U is either provable or disprovable in Z2, then it is both provable and disprovable.

The Enumeration of Proofs

Proofs in Z2 are Lisp data structures constructed using Lisp constructors such as Cons, Add1, F-Not, F-Or, Forsome. If we can enumerate all such data structures, then we can also enumerate all Z2 proofs. This enumeration is achieved by mapping these data structures (z-expressions) to n-expressions and, in turn, mapping n-expressions to natural numbers. The mapping from z-expressions to n-expressions is performed by the function GCODE discussed in the previous chapter (page 99). The resulting n-expressions are enumerated by the function Numcode below. If X is a number, (Numcode X) returns the odd number 2X+1.

In the previous chapter we defined a proof-checking program to check formal proofs constructed according to the axioms and rules of inference of the formal system Z2. In order to make progress towards the goal of proving the incompleteness of Z2, we need to formally develop a small amount of mathematics within Z2. While it is true that constructing formal proofs is very tedious, we have no intention of abandoning formalized mathematics. We will show in this chapter that formal proofs can be constructed in bigger and more natural steps by using powerful derived inference rules. These are inference rules whose application can always be eliminated in favor of the primitive axioms and inference rules of Z2. In other words, the soundness of these rules can be proven as a metatheorem. These derived rules do not yield any new theorems but they make the process of formal proof construction more natural and less laborious.

We demonstrate how the Boyer–Moore theorem prover can be used to prove and use derived inference rules to construct nontrivial formal proofs. Most of this chapter is an exposition of one powerful derived inference rule which states that all propositional tautologies are theorems of Z2. We also list several other derived inference rules that were similarly proved.

Metamathematical Extensibility

While it is, in principle, possible to use the proof checker Proves to construct and check formal proofs of interesting theorems, it would require an unrealistic amount of labor.