There has been for most of this century a broad (if not unanimous) consensus among mathematicians that mathematics as a whole can and should be regarded as founded in first order set theory.
Among theoretical computer scientists, typically less attached to set theory, there has arisen a pluralistic culture in which any one of many logical systems may be adopted, depending on the purposes in hand. Anti-foundational views are now popular in the Philosophy of Mathematics. |
Mathematics, Science and Engineering require many different notations. To conduct rational arguments involving these notations requires special logics whose inference rules reflect the semantics of the notations and are convenient for use in the domain. Software tools aiming to support the use of logic should therefore be engineered to support a plurality of diverse logics.
Set theoretic foundations for mathematics are based on the premise that all mathematically interesting abstract entities should be coded up as sets. Since these ideas were developed mathematics has become more abstract. These codings are now considered arbitrary and unmathematical in character. Mathematics studies structures up-to-isomorphism and the reductionism involved in the foundation of mathematics on set theory is contrary to the spirit of modern mathematics.
Notational pluralism, fully supported by sympathetic proof systems, is realisable within a single foundational framework using techniques of semantic embedding. These techniques recognise that the key differences between different notations lie in their semantics, they make use of a semantic mapping from domain oriented notations into the concepts of the underlying foundation system, supported by appropriate derived inference rules convenient for the notation concerned. These techniques permit the appearance of logical pluralism within a single foundational framework. |
Mathematicians, despite the wide range of their subject and its applications right across science and engineering, do not find it necessary to give any thought to which logic they should be using, however much they hop from one problem domain to the next. First order logic and set theory are thought to provide a topic neutral framework supporting applicability of results from one subject domain in another.
Just as mathematics has become more abstract, so have logical systems. Support for defining new concepts has been augmented by support for liberal forms of conservative extension, permitting constants to be introduced without selecting a particular encoding from the many possible. Used in this way the use of set theory can be confined to the reduction of the fundamental questions of consistency (does a structure exist satisfying a certain property) and similarity (is there a morphism relating the structure of two entities).
Gödel's incompleteness results tell us (for certain classes of logical systems), that if in logic A we can prove the consistency of logic B then B cannot prove the consistency of A. This induces a partial ordering on these proof systems according to how good they are at proving consistency results, which is related closely to the question whether a semantic embedding of one system in the other is possible (since a semantic embedding provides a relative consistency result). proof theoretic strength is a measure of how high you are up this partial ordering. If semantic embedding is intended, a foundation system should therefore have high proof theoretic strength. |