Is first-order logic 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 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 at least by one 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.

Answer 1

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

Short Answer

No. It's just the most popular logic among mathematicians and philosophers for primarily historical and cultural reasons.

Long Answer

Since you wrote a long question, here's a long answer :-)

Originally, Frege proposed a form of second order logic as a foundation for mathematics in his Grundlagen der Arithmetik (1884). This foundation fell out of fashion after Russell famously found a contradiction in this system (you can read all about it on SEP).

Since then, very few philosophers and mathematicians have argued the revival of second order logic as a foundation for mathematics. The only know of three: Jouko Väänänen, Stewart Shapiro, and George Boolos. Stewart Shapiro has a book about it: Foundations without Foundationalism: A Case for Second-order Logic (2000).

SOL is ugly, though. It has no complete axiom system for its standard semantics; the only complete calculi are for non-standard models (see Henkin (1950)). Also, the compactness theorems fails for SOL's usual semantics; model theory for FOL can generally be regarded as more well behaved. Väänänen (2001) has a nice summary of the properties of second order logic. Also, while the Löwenheim-Skolem theorem fails for SOL's standard semantics, it holds for Henkin's non-standard semantics. Väänänen argues "If second-order logic is construed as our primitive logic, one cannot say whether it has full semantics or Henkin semantics, nor can we meaningfully say whether it axiomatizes categorically ℕ and ℝ."

Abraham Robinson probably agreed with Väänänen on this point. In his opus Nonstandard Analysis (1960), Chapter 2, he presents Henkin's semantics for higher order logic. He goes on to prove compactness, Löwenheim-Skolem, and Łoś's Theorem. Robinson hardly pays any attention at all to the class of standard higher order models, (which he refers to as "full models"). That Robinson would embrace Henkin's non-standard semantics makes sense, of course. All of nonstandard analysis' bite comes from the fact that ℝ isn't categorical and Łoś's Theorem works.

Apart from Robinson (and maybe Väänänen) nobody really considers Henkin's semantics as a foundation. Neither is anybody working on foundations all that interested in systems which are not axiomatizable. The whole point of Harvey Friedman's reverse mathematics research program is that we have various axiomatic systems and we can reason about their provability power.

Of course, the idea that it's FOL vs. SOL for the foundations of mathematics is a false dichotomy anyway.

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?

It's not invariably chosen. It's primacy in mathematics and philosophy is due to it's early success and rapid development compared to its competition.

---

Research by mathematicians and philosophers into the foundations of mathematics schismed in several directions after the dismissal of Frege's Grundlagen. You can read about them in Heijenoort's anthology From Frege to Gödel: A Source Book in Mathematical Logic (1999):

• The First Order Logicians: the early, vast majority. These include Guisseppe Peano, C.S. Pierce, David Hilbert, George Cantor, Richard Dedekind, Skolem, Löwenheim, Zermelo, Fraenkel, Herbrand, the Bourbaki guys, Quine, Tarski, (early) Wittgenstein, etc.
• The Many Sorted Logicians: Russell, Whitehead, and (sometimes) Gödel.
• The Fathers of Computation: Moses Schoenfinkle, Alonzo Church and his students.
• The Constructivists: Kronecker, Kolmogorov, and Brouwer and his students.

It should be pointed out that Peano, Pierce, and Hilbert all developed First Order Logic roughly independently; this lends credence to the idea that FOL is a natural foundation for mathematics.

While the other approaches are not gone, they all faced early difficulties.

Type theory was poorly developed: Everyone knows how Russell and Whitehead's Principia Mathematica is legendarily opaque. Russell struggled for a long time before developing ramified types, which were challenging and hard to work with. Ultimately Leon Chwistek and Frank Ramsey demonstrated that the system could be simplified, resulting in the theory of simple types in the 1920s. Tragically, Ramsey died very young, so any contributions he might have made were cut short. On top of that Russell abandoned logic after writing the Principia, and his student Wittgenstein made no effort to develop it.

The "fathers of computation" also met challenges, although it also came later than FOL and ZF set theory. After publishing On The Building Blocks of Mathematical Logic in 1924, Moses Schönfinkel found himself trapped behind the iron curtain and never published again. His work was later picked up by Church who connected it to his λ-calculus. The λ-calculus, while more expressive than FOL, was never really suitable as a foundation for mathematics. A number of foundational systems built on the λ-calculus were proposed in the 30s by Church and others. The most popular of these systems were shown to be contradictory by what is now known as the Curry Paradox (see Curry (1941)).

Finally, constructivism and intuitionism had its own issues. The obvious defect with constructivism is too restrictive. A mathematician will always accept a constructive proof, but finding a non-constructive proof is easier also generally acceptable. Another issue is logic: intuitionistic logic and arithmetic were not axiomatized until Heyting in the late 1920s. Adequate semantics for intuitionistic predicate logic (IPC) also remained an open problem for a long time. A weak completeness proof was provided by Kreisel in the 1950s, using Brouwer's intended semantics (i.e., choice sequences). Kripke later gave a strong completeness proof for IPC in the 1960s, using Kripke structures. The "hayday" of intuitionistic model theory in the 50s and 60s was 30 years too late to have any impact on the foundations of mathematics.

---

Meanwhile, as rival foundations struggled, FOL/ZF ultimately won the hearts of mainstream mathematicians and philosophers. Modern foundational mathematicians mostly explore fine tuning the existing foundation. After Paul Cohen demonstrated the independence of the continuum hypothesis (1963), mathematicians began exploring independence of various propositions in ZF and certain extensions. One important axiomatic extension is Grothendieck's Universe Axiom, which is equivalent to the existence of a strongly inaccessible cardinal. This axiom is widely popular in algebraic geometry, and was used by Wiles' in his proof of Fermat's Last Theorem (although here Harvey Friedman argues the use of the axiom is not really essential). Speaking of Harvey Friedman, another important foundational research program is reverse mathematics, which studies the proof power of systems extending Peano Arithmetic but weaker than ZF.

First order model theory has also developed. An old triumph of model theory is Hrushovski's model theoretic proof of the Lang conjecture (1998). Despite the categoricity of ℕ and ℝ in SOL, few mathematicians have studied second order model theory since the 50s. There's categoricity results in FOL, too: for instance (ℚ,<) is ω-categorical in FOL.

And in philosophy, no philosopher has evangelized FOL more than Quine. I'd say Quine's preeminence is probably why philosophers only know FOL and ZF and don't know about anything else.

---

While mainstream mathematicians and philosophers were ignoring them, the other foundational research programs consolidated, and ultimately flourished.

After the failure of using the λ-calculus as a foundation, Church and many of his students turned to using simple-types. What emerged combined Russell's research program into Church's program.

A further development was an unexpected, non-Dutch interpretation of intuitionistic logic: the constructable types in the simply typed λ-calculus exactly correspond to propositional intuitionistic logic. This is the so-called Curry-Howard Correspondence.

The Curry-Howard Correspondence ultimately inspired Per Martin-Löf to invent Intuitionistic Type Theory in the early 70s, as a novel alternative foundation for mathematics. The original formulation suffered a defect known as Girard's paradox, although the system was salvageable and Martin-Löf didn't abandon it.

It is generally well known by students of computer science that the λ-calculus inspired John McCarthy and Steve Russell to invent LISP. A similar thing happened to the simply-typed λ-calculus in the early 70s. Dana Scott, a former student of Alonzo church invented The Logic for Computable Functions for reasoning about the denotation semantics of typed functional programs in the late 60s. In 1973 Robin Milner and company implemented LCF as the first computer proof assistant. This was done after developing the first simply-typed functional programming language ML ("MetaLanguage") that it was written in.

Ever since, non-FOL/ZF foundational research has largely worked with the computer science community.

One example is HOL, or "Higher Order Logic", roughly modeled after Church's simply-typed lambda calculus (1940). After a number of revisions, Mike Gordon released HOL88, intended for hardware verification. As Gordon admits in his short history on the subject that his code hacked parts of LCF when it was convenient, and was rather ad hoc (1996). HOL was later polished by John Harrison and Konrad Slind into HOL-Light; HOL-Light has 9 elementary rules which look vaguely like Equational Logic, and three axioms (the axiom of infinity, the axiom of choice using Hilbert's ε, and Leibniz' Law).

Another extension is Isabelle/HOL, which conservatively extends the type system of HOL with "context". Still another system is Homeier's HOL-Omega, which conservatively extends the type system even further.

Another development is NuPRL from Cornell university, which implements Martin-Löf's intuitionistic type theory. Agda is similar. A related system out of INRIA is Coq, which implements Thierry Coquand's Calculus of Constructions that extends intuitionistic type theory.

Development of new systems has slowed in the last decade or so, but it hasn't stopped. The few FOL/ZF systems (namely, Isabelle/ZF and Mizar) are comparatively inactive.

---

I would summarize my position as thus: saying that FOL invariably chosen as the underlying logic is like saying that Windows is invariably chosen as the underlying platform for PC games.

In both cases, it's a cultural thing.

Answer 2

Someone should point out that the semantics mathematicians actually use on a day-to-day basis is still second-order logic, or the equivalent, despite all the worry over foundations.

We generally allow one layer of reference to sets of sets, and implicitly assume 'Currying' makes this totally sufficient. And we do not weaken the logic to avoid the contradiction, unless we are trapped into a corner by a logician or a paradox.

Even people who reject large pieces of the standard logic of mathematics by requiring some level of 'constructiveness' do not reduce their thinking to first-order manipulations, but instead control access to negation and universality claims that are not grounded in some specific perspective.

The focus on first-order logic as the basis of everything seems to have sidetracked logic away from actual mathematical practice, and basically stopped the search for a usable standard logic within second-order logic, with the assumption that all of them will fall prey to the elevated version of Godel's theorem. This is not a foregone conclusion.

I have seen occasional work on 'well-foundedness' definitions (a la Category Theory as an alternative set theory) and other restraints on self-reference as a basis for a form of logic that works more on the basis of consistency by resolving or converging loops than on a positivistic basis that requires an absolute foundation, but it seems to proceed slowly and does not get taught.

Answer 3

Foundations has goals:

1. To present an approach to mathematics that we can be confident is consistent
2. To present language and methodology with which we can actually do mathematics

These goals are basically diametrically opposed. The simplest method to achieve the first goal is basically to have very minimal set of tools to make it feasible to reason about their correctness. However, the second goal strongly encourages us to throw in lots and lots of different tools for constructing, manipulating, and proving things.

A very nice solution to this problem is to simply split foundations into two layers: the first layer is a very minimal one whose correctness we are confident in, and using that we build the second layer which has all of the practical features we want to use for doing mathematics.

That's what you see today; first-order logic is a common choice for the first layer, and then some form of set theory as the second layer.

Note, incidentally, that higher order logic is itself some form of set theory.

---

Note, incidentally, that once you have the foundations set up, you still want to develop a theory of formal logic upon those foundations; it is that formulation of logic, not whatever appears at the base of your foundations, that is most relevant to actually practicing mathematics.