Is First Order Logic (FOL) the only fundamental logic?
Solution 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. 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.
Solution 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.