Combinatory Logics with Essentially Incomplete Models


  1. Explain and Motivate Problem
  2. Describe Solution
  3. Justify Solution
  4. Relate to other work (possibly distributed throughout above)

Since the publication of Goedel's incompleteness results it has been accepted that formal systems are often incomplete with respect to their intended subject matter, particularly arithmetic. What this means is that we have some intended semantics for the formal notation, and that we can establish that some statements in this notation which are true relative to the intended interpretation are not provable in the formal system. What Godel showed in relation to arithmetic was that the formal systems are essentially incomplete, that there is no way of patching up the formal systems so as to remedy their deficiencies.

It is sometimes also true that the underlying semantic ideas are also essentially incomplete. A case in point here is classical set theory, based upon the iterative conception of sets. In this view of set theory a universe of sets is created subject only to the constraint that these sets are conceived of as being created in some order, such that no set is created until all of its members have been created. The process of constructing the universe proceeds in stages, starting with an empty universe. At each stage a number of new sets are created whose members are all sets which have been formed at previous stages, and all sets which have not previously been formed but can be formed under this constraint will be formed. This process is undertaken by transfinite iteration, aggregating by taking a union the effects of any infinite sequence of steps. It is understood that this process can never be completed, though a model adequate for any finitary axiomatisation of set theory can always be obtained eventually after a number of stages which depends upon the proof theoretic strength of the formal system.

Any particular axiomatisation of classical set theory (or at least any which is intended to address this standard iterative conception) will be sound with respect to the universes formed at any stage subsequent to the first which provides an adequate model for that theory, and may therefore be thought of informally as being an incomplete formalisation of some ideal universe which represents the completion of this iterative process. However it is clear that this process cannot be completed. This is the case by definition, since the whole conception is based on the view that after any completed phase in this process we can aggregate all the sets so far produced and form a new set with these sets as members.

We do not suggest here that it is the incompletability of the iterative universe that is responsible for the incompleteness in the formal system, this is not the case, we simply point out the incompleteness of the semantic model so that the formal systems which we consider in this paper may be understood not to be so exceptional simply because the models with which we support our claim that the systems are consistent are essentially incomplete relative to the intuitive semantics of the notations.

In the field of combinatory logic the kind of incompleteness present in the iterative conception of set may be felt to be problematic. This incompleteness does have impact on the formal systems based on these models. It causes restrictions on the principle of abstraction, which prevent arbitrary abstractions to be considered as determining sets, and this is a significant inconvenience in some important applications of these theories.