Since the discovery of inconsistency in Frege's logical foundations for mathematics, no generally acceptable foundation systems have been put forward which admit as Frege's did an unconstrained principle of set comprehension.
One line of research which has sought to recover this facility, albeit in the more general context of unrestricted functional abstraction, has been research in combinatory logic. In these studies a more exacting requirement has also been sought, that the logical operators are themselves values in the domain of discourse and range of quantification.
Work by Aczel has shown that in a quite broad class of mathematical structures (which he calls `Lambda Structures') from which models of illative combinatory logic might be expected to be drawn, there can be no elements which correspond precisely to our intuitions about the required semantics of the logical operators (e.g. quantification). These result are expressed as negative statements about `internal definability' within the model, of the relevant logical concept.
Aczel goes on to define and then shows how to construct `Frege Structures' which are suitable as models for logical systems close to those of Frege. In these models a semantics can be given to formula involving the necessary logical operators even though these do not denote values in the model (this is in fact the norm and the case also in first order logic, combinatory logic is exceptional in attempting to include these notions in the domain of discourse, though no unique, higher order logics also have this characteristic). While Aczel provides ways of constructing sound logical systems supporting full comprehension, these systems nevertheless fall short of the ideals of combinatory logic, and his theoretical conclusions suggest that these ideals are not achievable.
It may be noted however that the impossibility of constructing models which fully satisfy our intuitive requirements has not been felt a fatal flaw in classical set theory. The iterative conception of the universe of sets on which logical systems like ZFC are based is an essentially incompletable construction. This turns out not to be a problem, since we know that no formalisation of set theory can be complete as a consequence of Godel's work. In practice incomplete models of this universe of sets suffice to interpret these theories. We therefore observe that classical set theory is not only formally incomplete, it is based on models which are essentially incompletable. In the following we therefore propose members of families of logical systems which can be seen to be consistent relative to models which are simply approximations to the intended interpretations. The systems may in principle have arbitrary proof theoretic strength, and the stronger the system the better its models approximate the ideal, but there are no complete systems, and no perfect models either.
We offer arguments to support the claim that combinatory logics can be devised which satisfy the following requirements:
Two qualifications should be noted before we proceed to greater detail.
Firstly, though we require and supply unconstrained abstraction and application, we are not committed to the standard semantics. In the systems we consider application is strict, and this appears in the formal systems as a constraint on beta reduction. We do not know whether this constraint is essential, but our arguments are only good in the presence of the constraint.
Secondly, in relation to proof theoretic strength our claims are relative. Results about consistency necessarily become less certain as apparent proof theoretic strength increases, since it is such strength is strongly correlated with how difficult it is to prove the system consistent. Our claim is that, given some system with a certain proof theoretic strength, we can construct a reflexive combinatory system with at least as high a proof theoretic strength. This result is obtained via some very general claims about how one logical system can `steal' proof theoretic strength from another.
Our arguments are presented in three phases.
Firstly we construct a formal system lacking logical quantifiers which is capable of proving definite facts about computation together with some general facts expressed using free variables. The domain of discourse is natural numbers and computable functions over natural numbers as represented by an effective coding of functions into natural numbers. A distinguished natural number denotes the true proposition, and a sequent is provable for any assignment of natural numbers to the variables in the sequent if the assumptions all evaluate to true then so does the conclusion. This system is easily shown to be consistent.
Next we introduce a new constant name for restricted quantification together with some suitable rules. This extension to the system is shown to be conservative.
Finally we argue that the proof theoretic strength can by increased without limit by the addition of any finite number of true claims about the consistency of other formal systems. The conditions under which proof theoretic strength can be transferred from one logical system to another by this method are discussed.