New Classical Logical Systems

Background

The work described here was begun at a time when I was a member of a committee attempting to standardise a formal specification language (VDM-SL) for the "formal method" VDM (Vienna Development Method). The extraction from the problem of standardising VDM-SL of a problem in the foundations of mathematics, and most of the work which I have so far done in solving this problem, were undertaken in 1987 and 1988. None of the work has ever been published, no part of it is sufficiently complete to warrant publication in traditional media. A presentation on the work was given in a evening session on the VDM standardisation process at the VDM-88 conference in Dublin in September 1988. At about this time reorganisation within ICL resulted in my participation in the standardisation process coming to an end, and further work on these ideas was halted. (though in fact all of this foundational work had been done in my own time rather than company time)

The systems described here have been motivated by the desire to improve on classical first order set theory as an underlying logical system for use in applications in Computer Science, particularly in formal specfications.

What's wrong with first order set theory?

Ideas on possible improvements

We propose to consider the construction of a new logical foundation system with the following characteristics:
  1. The system will be essentially classical, and easily shown to be equivalent in proof theoretic strength to ZFC.
  2. The system will have a minimal set of operators which are not in the domain of discourse, and will not require extension of this set of operators to suit applications.
  3. The system will be type-free, and will be suitable for semantic foundations for typed systems.
  4. The system will support structuring mechanisms which at a minimum will permit the use of local names without disadvantage relative to the use of global names.
  5. The system will provide a satisfactory notion of polymorphism.

Methods for developing new classical foundation system

The methods to be adopted are semantically based and are also based on the use of mechanical proof support. A suitable logical framework will be adopted, in fact an axiomatisation of ZFC in HOL (which system is strictly stronger than ZFC). The framework will admit the construction of models for logical systems, and enables reasoning about these models an appropriate operators over these models, effectively establishing the consistency of proposed foundation systems in the course of establishing the systems. In fact a series of structures of increasing complexity are studied as follows:
  1. The Theory of Pure Functions
  2. The Theory of Pure Polymorphic Functions
  3. The Theory of Structured Polymorphic Functions
Use of the term "pure" here is intended in the same sense as that in the term "pure set theory", which means a set theory in which all things which exist are sets.

Putting the ideas into practice

The key elements of the development of these theories are: The key properties are properties which will give rise to axioms in the logic based on these semantic domains. The relevant theorems are analogous to the statement of these axioms in the syntax of the metalanguage rather than the proposed object language. We do not give any consideration to the concrete syntax of the object language.