The Problem

To produce a Foundation System satisfying the following requirements:

  1. Consistent
  2. Permitting unrestricted abstraction
  3. Of open-ended proof theoretic strength

Motivation

The foundation system is to be used in software engineering as the logical basis for a software tool which is mathematically literate. Users of this tool will need to have settled in principle issues of consistency, i.e. the tool will be able to act for them as a final arbiter of consistency. Hence a high level of proof theoretic strength is required.

Of the required characteristics:

  1. Needs no justification
  2. Is the primary requirement justifying foundational work.
  3. See previous paragraph.

Background

Frege began with unconstrained abstraction, however his system was found to be inconsistent.

The solutions to the paradoxes \cite{Russell08,Zermelo08} both involved restrictions on abstraction.

Though the main stream of mathematical logic abandoned practical application of formal systems to the construction of mathematical proofs, and was content with systems not admitting full abstraction, work on reflexive foundations has continued through to the present day.

Among the work conducted in this tradition is that of Schonfinkel, Curry, Seldin and Bunder of a proof theoretic nature, and Finch, Scott and Aczel of a more model theoretic kind. The problem which has dogged the field has been that of obtaining consistent systems with adequate expressiveness to provide a foundation for classical mathematics. In combinatory logic the extra condition has generally been added that the number of forms of judgement is limited and that all other constructions are conducted by means of application of terms in the object language, which requires that the logical operators are values in the domain of discourse.

Aczel's work on Frege structures provide negative results about such systems. Aczel's work showed that in the general context of Lambda structures important logical operations could not be `internally defined', by which we may understand that the relevant logical operators are not to be found in the domain of discourse of the relevant models. Scott and Aczel both published details of similar logical systems in which unrestrained abstraction is permitted but the logical operators are not values in the domain of quantification. The proof theoretic strength of these systems is not known.

It is the purpose of this paper to show that notwithstanding Aczel's negative results reflexive foundations supporting unrestrained abstraction and whose logical operations are represented in the domain of discourse can be constructed with arbitrarily high proof theoretic strength and shown to be consistent by model theoretic methods. This is possible by the use of essentially incomplete models. Each such model fails to capture fully the intended semantics of some to the logical operators, but represents an approximation good enough to show the consistency of formal systems up to a certain level of proof theoretic strength. Formal systems of arbitrarily high proof theoretic strength can be shown to be consistent by arguing that a model providing a sufficiently good approximation to the intended meaning of the logical operators exists.