# Is First Order Logic (FOL) the only fundamental logic?

I'm far from being an expert in the field of mathematical logic, but I've been reading about the academic work invested in the foundations of mathematics, both in a historical and objetive sense; and I learned that it all seems to reduce to a proper -axiomatic- formulation of set theory.

It also seems that all set theories (even if those come in ontologically different flavours, such as the ones which pursue the "iterative approach" like ZFC, versus the "stratified approach" -inspired by Russell's and Whitehead's type theory first formulated in their Principia- such as Quine's NFU or Mendelson's ST) are built as collections of axioms expressed in a common language, which invariably involves an underlying first order predicate logic augmented with the set-membership binary relation symbol. From this follows that FOL makes up the (necessary) "formal template" in mathematics, at least from a foundational perspective.

The justification of this very fact, is the reason behind this question. All the stuff I've read about the metalogical virtues of FOL and the properties of its "extensions" could be summarized as the statements below:

• FOL is complete (Gödel, 1929), compact and sound, and all its particular formalizations as deductive systems are equivalent (Lindström, 1969). That means that, given a (consistent) collection of axioms on top of a FOL deductive system, the set of all theorems which are syntactically provable, are semantically satisfied by a model of the axioms. The specification of the axioms absolutely entails all its consequences; and the fact that every first order deductive system is equivalent, suggests that FOL is a context-independent (i.e. objective), formal structure.
• On the other hand, the Löwenheim–Skolem theorem implies that FOL cannot categorically characterize infinite structures, and so every first order theory satisfied by a model of a particular infinite cardinality, is also satisfied by multiple additional models of every other infinite cardinality. This non-categoricity feature is explained to be caused by the lack of expressive power of FOL.
• The categoricity results that FOL-based theories cannot achieve, can be obtained in a Second Order Logic (SOL) framework. Examples abound in ordinary mathematics, such as the Least Upper Bound axiom, which allows the definition of the real number system up to isomorphism. Nevertheless, SOL fails to verify an analog to the completeness results of FOL, and so there is no general match between syntactic provability and semantic satisfiability (in other words, it doesn't admit a complete proof calculus). That means that, even if a chosen collection of axioms is able to categorically characterize an infinite mathematical structure, there is an infinite set of wff's satisfied by the unique model of the axioms which cannot be derived through deduction.
• The syntactic-semantic schism in SOL also implies that there is no such a thing as an equivalent formulation of potential deductive systems, as is the case in FOL and stated by Lindström's theorem. One of the results of this fact is that the domain over which second order variables range must be specified, otherwise being ill-defined. If the domain is allowed to be the full set of subsets of the domain of first order variables, the corresponding standard semantics involve the formal properties stated above (enough expressive power to establish categoricity results, and incompleteness of potential, non-equivalent deductive systems). On the other hand, through an appropiate definition of second order domains for second order variables to range over, the resultant logic exhibits nonstandard semantics (or Henkin semantics) which can be shown to be equivalent to many-sorted FOL; and as single-sorted FOL, it verifies the same metalogical properties stated at the begining (and of course, its lack of expressive power).
• The quantification extension over variables of successive superior orders can be formalized, or even eliminate the distinction between individual (first order) variables and predicates; in each case, is obtained -for every N- an Nth Order Logic (NOL), and Higher Order Logic (HOL), respectively. Nevertheless, it can be shown (Hintikka, 1955) that any sentence in any logic over FOL with standard semantics to be equivalent (in an effective manner) to a sentence in full SOL, using many-sorting.
• All of this points to the fact that the fundamental distinction, in logical terms, lies between FOL (be it single-sorted or many-sorted) and SOL (with standard semantics). Or what seems to be the case, the logical foundations of every mathematical theory must be either non-categorical or lack a complete proof calculus, with nothing in between that trade-off.

Why, so, is FOL invariably chosen as the underlying logic on top of which the set theoretical axioms are established, in any potentially foundational formalization of mathematics?

As I've said, I'm not an expert in this topic, and I just happen to be interested in these themes. What I wrote here is a summary of what I assume I understood of what I read (even though I'm personally inclined against the people who speaks about what they don't fully understand). In this light, I'd be very pleased if any answer to this question involves a rectification of any assertion which happened to be wrong.

P.S. : this is an exact repost of the question I originally asked at Philosophy .SE, because I assumed this to be an overly philosophical matter, and so it wouldn't be well received by the mathematics community. The lack of response there (be it because I wrong, and this actually makes up a question which can only be answered with a technical background on the subject, or because it's of little philosophical interest) is the reason why I decided to ask it here. Feel free to point out if my original criterium was actually correct, and of course, I'll take no offense if any moderator takes actions because of the probable unsuitability of the question in this site.

-
You might find illuminating some of the expository introductions in literature on institutions (Goguen, Burstall). – Bill Dubuque Jul 28 '12 at 19:44
You might also find of interest Lindstrom's theorem, that first-order logic may be characterized as the only logic enjoying compactness and Lowenheim-Skolem and closed under $\:\wedge,\ \lnot,\ \exists.\ \$ This is one of the first results in Abstract Model Theory, which investigates such matters. – Bill Dubuque Jul 28 '12 at 19:54

For the history of first-order logic I strongly recommend "The Road to Modern Logic-An Interpretation", José Ferreirós, Bull. Symbolic Logic v.7 n.4, 2001, 441-484. The abstract at least is freely available.

Apart from first order logic and higher order logic there are several less well known logics that I can mention:

• Constructive logics used to formalize intuitionism and related areas of constructive mathematics. One key example is Martin-Löf's intuitionistic type theory, which is also very relevant to theoretical computer science.

• Modal logics used to formalize modalities, primarily "possibility" and "necessity". This is of great interest in philosophy, but somehow has not drawn much interest in ordinary mathematics.

• Paraconsistent logics, which allow for some inconsistencies without the problem of explosion present in most classical and constructive logics. Again, although this is of great philosophical interest, it has not drawn much attention in ordinary math.

• Linear logic, which is more obscure but can be interpreted as a logic where the number of times that an hypothesis is used actually matters, unlike classical logic.

-
Ferreirós' paper is freely downloadable here. However, I don't see any mention of abstract model theory there - only much older history. – Bill Dubuque Jul 28 '12 at 20:28
Regarding modal logics: Temporal logics can be considered variants of modal logics and are widely used in software and hardware verification. – Johannes Kloos Jul 28 '12 at 20:32
Linear logic has also been used and studied in computer science. One of the applications is modeling bounded resource consumption. – bellpeace Aug 30 '14 at 18:41
@bellpeace "Linear logic" seems to be useful in Quantum Mechanics too. In Quantum Picturalism, Bob Coecke writes: "One may wonder whether there is a connection between the logical and the physical no-cloning and no-deleting laws. In particular, the above indicates that maybe this new ‘linear logic’ might be more of a ‘quantum logic’ than the original ‘Birkhoff-von Neumann quantum logic’ which according to most logicians wasn’t even a ‘logic’." – David Tonhofer Nov 17 '14 at 20:14

In 2000, John Alan Robinson (known for joining the "cut" logic inference rule and unification into the Resolution logic inference rule, thus giving logic programming its practical and unifying processing principle) authored an eminently readable overview of the "computational logic" research domain: "Computational Logic: Memories of the Past and Challenges for the Future". On page 2 of that overview, he wrote the following:

First Order Predicate Calculus: All the Logic We Have and All the Logic We Need.

By logic I mean the ideas and notations comprising the classical first order predicate calculus with equality (FOL for short). FOL is all the logic we have and all the logic we need. (...)

Within FOL we are completely free to postulate, by formulating suitably axiomatized first order theories, whatever more exotic constructions we may wish to contemplate in our ontology, or to limit ourselves to more parsimonious means of inference than the full classical repertoire.

The first order theory of combinators, for example, provides the semantics of the lambda abstraction notation, which is thus available as syntactic sugar for a deeper, first-order definable, conceptual device.

Thus FOL can be used to set up, as first order theories, the many “other logics” such as modal logic, higher order logic, temporal logic, dynamic logic, concurrency logic, epistemic logic, nonmonotonic logic, relevance logic, linear logic, fuzzy logic, intuitionistic logic, causal logic, quantum logic; and so on and so on.

The idea that FOL is just one among many "other logics" is an unfortunate source of confusion and apparent complexity. The "other logics" are simply notations reflecting syntactically sugared definitions of notions or limitations which can be formalized within FOL. (...) All those “other logics”, including higher-order logic, are thus theories formulated, like general set theory and indeed all of mathematics, within FOL.

So I wanted to know what he meant by this and whether this statement can be defended. This being Robinson, I would assume that yes. I am sure there would be domains where expressing the mathematical constraints using FOL instead of something more practical would be possible in principle, but utterly impractical in fact.

The question as stated is better than I could have ever have formulated (because I don't know half of what is being mentioned). Thank you!

-