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

Question

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 objective 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 appropriate 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 beginning (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 criteria 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.

Answer 1

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. Author's website, ASL, JSTOR, DOI: 10.2307/2687794.

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.

Answer 2

I have not an answer, just an additional note about this.

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!

Addendum (very much later)

In The Emergence of First-Order Logic, Gregory H. Moore explains (a bit confusingly, these papers on history need timelines and diagrams) how mathematicians converged on what is today called (untyped) FOL from initially richer logics with Second-Order features. In particular, to formalize Set Theory.

The impression arises that FOL is not only non-fundamental in any particular way but objectively reduced in expressiveness relative to a Second-Order Logic. It has just been studied more.

Thus, Robinson's "FOL as all of logic with anything beyond reducible to FOL" sounds like a grumpy and ill-advised statement (even more so as the reductions, if they even exist, will be exponentially large or worse). Robinson may be referring to Willard Van Orman Quine's works. Quine dismisses anything outside of FOL as "not a logic", which to me is frankly incomprehensible. Quine's attack on Second-Order Logic is criticized by George Boolos in his 1975 paper "On Second-Order Logic" (found in "Logic, Logic and Logic"), which is not available on the Internet, but searching for that paper brings up other hits of interest, like "Second-Order Logic Revisited" by Otávio Bueno. In any case, I don't understand half of the rather fine points made. The fight goes on.

Let me quote liberally from the conclusion of Gregory Moore's fine paper:

As we have seen, the logics considered from 1879 to 1923 — such as those of Frege, Peirce, Schröder, Löwenheim, Skolem, Peano, and Russell — were generally richer than first-order logic. This richness took one of two forms: the use of infinitely long expressions (by Peirce, Schröder, Hilbert, Löwenheim, and Skolem) and the use of a logic at least as rich as second-order logic (by Frege, Peirce, Schröder, Löwenheim, Peano, Russell, and Hilbert). The fact that no system of logic predominated — although the Peirce-Schröder tradition was strong until about 1920 and Principia Mathematica exerted a substantial influence during the 1920s and 1930s — encouraged both variety and richness in logic.

First-order logic emerged as a distinct subsystem of logic in Hilbert's lectures (1917) and, in print, in (Hilbert and Ackermann 1928). Nevertheless, Hilbert did not at any point regard first-order logic as the proper basis for mathematics. From 1917 on, he opted for the theory of types — at first the ramified theory with the Axiom of Reducibility and later a version of the simple theory of types ($\omega$ - order logic). Likewise, it is inaccurate to regard what Löwenheim did in (1915) as first-order logic. Not only did he consider second-order propositions, but even his first-order subsystem included infinitely long expressions.

It was in Skolem's work on set theory (1923) that first-order logic was first proposed as all of logic and that set theory was first formulated within first-order logic. (Beginning in [1928], Herbrand treated the theory of types as merely a mathematical system with an underlying first-order logic.) Over the next four decades Skolem attempted to convince the mathematical community that both of his proposals were correct. The first claim, that first-order logic is all of logic, was taken up (perhaps independently) by Quine, who argued that second-order logic is really set theory in disguise (1941). This claim fared well for a while. After the emergence of a distinct infinitary logic in the 1950s (thanks in good part to Tarski) and after the introduction of generalized quantifiers (thanks to Mostowski [1957]), first-order logic is clearly not all of logic. Skolem's second claim, that set theory should be formulated in first-order logic, was much more successful, and today this is how almost all set theory is done.

When Gödel proved the completeness of first-order logic (1929, 1930) and then the incompleteness of both second-order and co-order logic (1931), he both stimulated first-order logic and inhibited the growth of second-order logic. On the other hand, his incompleteness results encouraged the search for an appropriate infinitary logic—by Carnap (1935) and Zermelo (1935). The acceptance of first-order logic as one basis on which to formulate all of mathematics came about gradually during the 1930s and 1940s, aided by Bernays's and Gödel's first-order formulations of set theory.

Yet Maltsev (1936), through the use of uncountable first-order languages, and Tarski, through the Upward Löwenheim-Skolem Theorem and the definition of truth, rejected the attempt by Skolem to restrict logic to countable first-order languages. In time, uncountable first-order languages and uncountable models became a standard part of the repertoire of first-order logic. Thus set theory entered logic through the back door, both syntactically and semantically, though it failed to enter through the front door of second-order logic.

There sure is space for a few updated books in all of this.