Logical Foundations for Mathematics

Paradigms:

There are many alternative logical foundations for mathematics. They differ in some cases just in detail or strength. In other cases the differences are more fundamental, possibly representing radically divergent views on the nature of mathematics.

Well-founded Sets By far the most widely accepted foundational paradigm is that provided by the iterative conception of set, usually axiomatised in first order logic. This comes in many variations. (see also:What's wrong with ZFC?) Topos Theory Category theory offers better ways of doing abstract mathematics, and from this point of view the usual axiomatisations of set theory are unsatisfactory. Toposes offer an alternative way of thinking about (and axiomatising) a set theoretic universe. Some category theorists beleive that better foundation systems could be based on topos theory. (see :Category Theoretic Perspectives on the Foundations of Mathematics)

Constructive Foundations Undoubtedly the most prominent alternative paradigm to the well-founded sets is that provided by constructive mathematics. A key feature of constructive approaches is the rejection of classical set theory, and the conception of a function as some kind of rule rather than an arbitrary graph. Reflexive Foundations The well-foundedness of set theory brings some problems with it (which are conspicuous in Category Theory) and there has been some work on foundation systems which omit this feature. A small step away from well-foundedness leads to non-well-founded set theories, such as Quine's NF. Combinatory Logic makes a more radical departure, similar to constructive foundations in that functions are more like rules than graphs.

Dimensions:

We consider five different characteristics or dimensions of logical foundation systems, sometimes clearly separated, other times not so. The formal the semantic, the logical, the ontological and the conceptual.

Formal and Semantic It is essential that a logical foundation system be a formal language, and that rules of reasoning are formally codified which permit the derivation of most of mathematics. Gödel's incompleteness results mean that we must settle for most however much we might like all of mathematics. They also mean that we cannot rely wholly upon the formal inference systems to define the meaning of the notation. Any inference system will result in a theory which could be interpreted in ways we do not intend. It is therefore desirable to have an account of the intended meaning of the notation which is independent of the formal inference rules.

Logic and Ontology The purpose of a logical foundation system is to provide a context in which mathematical concepts can be defined and then theories developed involving these concepts. While an ontologically neutral logical system will enable us to derive the consequences of our definitions, there is a difficulty in undertaking the definitions without an ontology. It is essential that definitions are coherent, otherwise fallacious proofs can be obtained. An ontological framework is necessary to test the coherence of definitions.

Mathematical Concepts The conceptual apparatus necessary to provide a foundationally adequate logic and ontology can be very minimal indeed. If such a minimal vocabulary is employed there will be a need for further concepts which, though not required in constructing the logical foundation system will be shared by the various branches of mathematics, and are therefore foundational in a slightly different sense. An adequate set theoretic logical foundation system will not normally involve the definition of the concept of function which will however be part of the further development of set theory which is common to all branches of mathematics within the classical paradigm.

Formal:

The formal aspect concerns the mathematical theorems which can be proven using the foundation system. Foundation systems are partially ordered according to their proof-theoretic strength.

proof A key feature of the methods of mathematics, going back as far as ancient Greece, is the role of proof. Though mathematics results may be discovered by diverse means of varying reliability. They remain conjectures until they have been verified by proof. Though the construction of a proof may be difficult its checking is expected to be routine, so that there remains no doubt in the conjecture once its proof has been checked. The primary purpose of a logical foundation for mathematics is to provide a context in which the checking of mathematical proofs can be conducted. syntax The first formal element required of a logical foundation system is a formal definition of the syntax of the language in which mathematical conjectures are to be expressed.

type-correctness Some foundation systems make use of "type constraints" supplementary to the basic syntactic well-formedness conditions. In some cases these additional conditions are decidable, and seem like an extension to the syntax, in other cases they are not decidable and well-typedness must itself be demonstrated by a proof, making type-correctness rule seem like an aspect of the deductive system. In more extreme cases (adopting the "propositions as types" paradigm) the entire deductive system is absorbed into the type-correctness proof. derivations A key feature of formal logical systems in general (and hence of formal logical foundation systems for mathematics) is that the correctness of proofs is characterised by purely formal syntactic criteria. These criteria are normally expected also to be effective, in which case they will be machine checkable.

axioms The first element of a deductive system is the definition of the axioms from which the derivation begins. These would normally be decidable. (if they were not even semi-decidable then the role of the deductive system in proof checking would be compromised) rules The second element of a deductive system is the definition of the derivation rules which determine how new theorems can be deduced from already established premises. These rules should also be effectively decidable. extensions A final element which distinguishes a formal foundation system from other formal logical systems is the need for formal rules for conservative extension. These are the means by which non-logical concepts may be safely defined. It is possible to derive mathematics from a logic without such rules by the introduction of new axioms whenever new concepts are introduced, however, a logic adequate for such a method (first order logic, for example) would not normally be called a foundation system, which is expected to fill a larger role.

Semantic:

Gödel's first incompleteness theorem guarantees that truth and theoremhood do not coincide in any foundation system adequate for mathematics. It is therefore desirable to have an account of the intended meaning of the language independent of the definition of formal derivability.

limitations of formality At one time it had been hoped that formal definitions would be able to supercede completely the use of informal or intuitive semantics. However, the incompleteness results obtained by Gödel entailed that formal definition would never be as specific as we would like it to be. For example, even a mathematical structure as intuitively simple as that of the natural numbers could not be given an exact formal definition.

foundational neutrality Part of the intended role of a logical foundation system is to provide a general and topic neutral framework in which any subject matter can be investigated once the concepts of that domain are given a suitable definition. This corresponds to a view of mathematical truths as analytic truths which can be established by logical deduction from the definitions of the mathematical concepts.

semantic foundations To support the definition of mathematical concepts it may be thought preferable for the primary definition of a foundational language to be a semantic definition (even though this must be ultimately informal). For example, it may be desirable to specify some set of intended models for set theory (e.g. the well-founded models) which will enable the definitions of mathematical objects to be unique where this is desired. (e.g. which ensures that a definition of the natural numbers is not satisfied by unintended structures).

Logical:

In some cases it is possible to separate out a part of the system which is concerned with logic and independent of matters ontological.

first order logic For reasons which are not entirely clear to me, first order logic has been the vehicle for such a large part of the work of mathematical logic that it is often thought of or asserted to be logic. One might expect that its adoption has been so widespread because it is thought to be without loss of generality, i.e. that in this logic one can do whatever can be done in other logics by chosing suitable axiom sets. However, I am not aware of any precise result which justifies this expectation.

ontological neutrality A key feature which contributes to the apparent generality of first order logic is its ontological neutrality. The logic itself embodies no presumptions about the domain of discourse except the minimal presumption (which is technically convenient) that it is not empty. This means that there appears to be, when working in first order logic, a clean separation between logical and ontological matters.

other logics In general, logical foundation systems which are not first order axiomatic theories do not share this clean separation between the logical and ontological. Typically these other foundation systems are likely to be some kind of type system in which the logic is inextricably bound up with a view about the various kinds or types of entities which exist in its domain of discourse. This raises the question whether there is some fundamental distinction between logical and ontological matters which is conflated by these logical foundation systems or whether this is simply an arbitrary artefact of first order logic.

Ontological:

Ontology is an important part of semantics, and differences both paradigmatic and in detail, are likely to be reflected in or caused by ontology.

conservative extension It is an essential feature of a logical foundation system that it provides ways of introducing new mathematical concepts which are conservative. What this means is that a new definition should make no difference to the results derivable which involve only previously introduced concepts (and in particular, that it will not compromise the soundness of the logic enabling contradictions to be derived). This feature required in a logical foundation system reflects the need for care in the use of definitions which was recognised long before logical foundation systems were devised.

denotations for entities Ideally we might like to have denotations (i.e. entities denoted by) all of the mathematical concepts which we employ. Regrettably there are some difficulties in devising foundation systems with this characteristic. We must have denotations for the mathematical entities that we will need to quantify over, such as numbers. In order to provide for the introduction of natural numbers by definition (or by conservative extension) it is usual to have the universe pre-populated with suitable abstract entities which will serve as models for the structures we want to talk about.

ontology and consistency A definition (or other extension) can then be shown to be conservative by proving that there already exist abstract entities which satisfy the defining properties of the new concepts introduced by the extension. The role of abstract ontology can therefore be seen to relate to the need to preserve the consistency of the logical foundation system when new concepts are introduced. This and other considerations make clear that there is a close relationship between matters of abstract ontology and logical consistency, which contributes to the case for the claim that abstract ontology is properly a part of logic.

Conceptual:

Over and above the logical and ontological features which determine the strength of the system there is likely to be some conceptual apparatus which provides the first stages in developing mathematics.

pure foundations Consideration above of the logical and ontological aspects of logical foundation systems suggests that an onto-logical foundation system which is topic neutral could be devised within which arbitrary application domains can be formalised by defining their concepts and then deriving theorems involving these concepts. Such a foundation (and perhaps a bare first order set theory qualifies) would permit the study of any of the different "paradigms" of mathematics, provided that one could find definitions for the concepts with which it is concerned. It is moot whether this is the case or not, and doubtful that any intuitionist would agree that what distinguished his mathematics from classical mathematics was simply its subject matter.

concepts shortfall Whether or not a pure onto-logical foundation system could be shown to be universal in any sense, it certainly is the case that its core formal systems would not provide the necessary conceptual apparatus for the foundational purposes of any of the mathematical paradigms. As noted, for example, an axiomatisation of set theory will not determine what a function is. It is possible to satisfy the key logical requirements for a foundation system without providing many of the common concepts which would naturally be regarded as foundational in character. This has the advantage that a purely logical/ontological foundation may be resilient to debates about foundational concepts such as that between set theorists and category theorists.

supplementary concepts There are to be counted as part of a logical foundation system a range of concepts which may be go beyond what is required to establish an onto-logical framework sufficent for the development of mathematics by conservative extension. These additional concepts may be regarded as foundational because of their pervasive use through all branches of mathematics. Concepts which are supplementary to one onto-logical foundation (e.g. function in set theory) may be an integral part of others. Exactly what array of "supplementary" concepts should be regarded as foundational is probably controversial.

---

© created 1998/7/28 modified 1998/08/06