Early formal systems like Frege's Begriffsschrift or Peano's work on the axiomatization of the natural numbers used axiom systems with an underlying second-order predicate logic (from today's point of view). Why were these second-order logic systems given up in favor of first-order predicate logic? After all, second-order logic is powerful enough to characterize the natural numbers up to isomorphism, while first-order logic cannot characterize infinite structures up to isomorphism (as follows from the Löwenheim Skolem theorem).

Edit The following speculations from the initial question are incorrect (see accepted answer):

One thing I could imagine is that the realization that there cannot be a complete (sequential) deduction system for second-order logic raised suspicions against it. But the completeness of first-order logic was only proved by Kurt Gödel at a time when first-order logic had already displaced second-order logic. What I do realize is that first-order logic was adopted at a time before its own deficiencies were fully understood.

Nevertheless, I still wonder why second-order logic was actually abandoned, and why the inability of first-order logic to characterize infinite structure is not considered a problem.

  • 1
    +1 Do you have any references for your claim that around 1930 "first-order logic had already displaced second-order logic" or, more generally, a timeline of this "decline" and how would that be measured? (I have doubts that your historical assessment is correct, but maybe you have evidence that could convince me of the contrary.)
    – DBK
    Commented Apr 18, 2012 at 0:48
  • 1
    @DBK You are probably right that my historical assessment is incorrect. I identified Hilbert and Russell too much with the dates 1900 (Hilbert's second problem) and 1903 (Principles of Mathematics), even so their main formally worked out contributions to logic appeared much later (which I realized only after you mentioned that my timeline is incorrect). However, even if working out first order logic in full detail took some time, distinguishing first and second order logic must have been possible in 1915, when Löwenheim published his result on first order logic. Commented Apr 18, 2012 at 8:16
  • 1
    @DBK Wow! I especially like the reference section. After reading some of the references, I get the impression that your answer/summary is correct. Especially, you are right that the statement "the completeness of first-order logic was only proved by Kurt Gödel at a time when first-order logic had already displaced second-order logic" is incorrect. And I really learned a lot now, not only about history, but also about logic itself. Commented Apr 22, 2012 at 14:15
  • Thanks! I find the two paper listed on top particularly helpful. I'll try to clear up the brief overview on Skolem's attitude with respect to FOL and FO set theory, as there where some qualms over it. Still, you might want to follow @Mitch's suggestion and ask your question on math.SE and/or mathoverflow as well. There are a lot of logicians knowledgeable in the history of their discipline over there. (Please link to them here, in case you do.)
    – DBK
    Commented Apr 22, 2012 at 15:12
  • I added a paragraph specifically dealing with the problem of characterizing infinite structures in FOL (§4) - it's probably not a satisfying answer, but that's as good as it get's, I think.
    – DBK
    Commented Apr 22, 2012 at 16:31

3 Answers 3


The short answer (tl;dr)

The relevant historical context to answer your question is the long quest of logic to provide foundations for all mathematics. Zermelo's axiomatic set theory displaced contenders like type theory and won the race early on, because logicians in this tradition developed metalogical tools (model theory, proof theory) to investigate axiom systems. Zermelo's contribution came around 1908 and, through the work of Fraenkel, Skolem and others in the mid 20s (before Gödel's completeness result), it quickly became the standard set theory we know today, Zermelo–Fraenkel set theory + Choice (ZFC)

That ZFC became a pure first-order theory is due to David Hilbert's early work on a subsystem of logic which he called restricted functional calculus (effectively today's first-order logic) and Thoralf Skolem, who in 1923 gave the original first-order axiomatization of Zermelo set theory. Axiomatic set theory effectively became a dominant first-order theory in the mid 30s and is first-order up to this day. The majority of set theorists like the properties of first-order logic (completeness, compactness, etc.) a lot. The fact that first-order set theory deviates from mathematical practice is actually seen as a feature, not as a bug.

The long answer

It seems trivial today, but in order to adopt first-order logic (FOL), one has to be able to isolate it from second-order logic (SOL) or higher-order logics. And this possibility was itself an important conquest. Up to Principia Mathematica, several versions of second-order logic (including infinitary logic) were commonly employed by logicians without much care. FOL and SOL were not really distinguished (distinguishable?) until the relative merits and vices of each one were investigated. Or, to state it the other way around: It was the foundationalist quest which lead to study not only the expressibility, but also the properties of various fragments and it was through this venue that FOL and SOL were discerned.

1. Two traditions in logic

It seems to me that it was Russell's discovery of the famous paradox in 1901 in Cantor's naive set theory (discovered independently by Zermelo, who communicated it to Hilbert) that started it all. Since the paradox also appeared in Frege's formalized version of naive set theory, logicians started to devise various ways of avoiding the problem and built new set theoretic approaches. The two most important proposals which fixed these (and other) paradoxes were Russell's type theoretic set theory and Zermelo's set theory.

These two solutions are commonly regarded as expressions of two different "strains" within logic, the Peano-Frege-Whitehead-Russell tradition and the (Peirce)-Schröder-Hilbert-Zermelo tradition.

2. Metalogical research

The important point is that these two traditions scored unevenly in the above mentioned task of investigating logical fragments and their properties. Of the two, the latter was in Lakatosian terms the progressive research program because it was interested from the start in metalogical questions, while the former was not.

To understand why this is the case, it helps to remember that the first tradition is commonly identified with logicism, a conception which defines the raison d'être of logic as the task of giving foundation for all of mathematics. For most logicists this implied that it was impossible to "stand outside" of logic and thereby to study it as a system (in the way that one might, for example, study the real numbers). This had severe consequences: Russell and Whitehead

  • lacked any conception of a metalanguage
  • explicitly denied the possibility of independence proofs for their axioms
  • believed it impossible to prove that substitution is generally applicable in type theory
  • insisted that the Principle of mathematical induction cannot be used to prove theorems about their system of logic

It is hard nowadays to understand what doing logic means without a language-metalanguage distinction and a syntax-semantics distinction!

3. The emergence of FOL

It is not a coincidence, I think, that it was in this metatheoretical setting, and in the Schröder-Hilbert-Zermelo tradition, that logic was put on the operating table to be dissected, so to speak. It was a direct consequence of the need to investigate metalogically the properties (soundness, completeness, compactness, consistency, categoricity etc.) of various logical fragments: In 1918 Bernays gave the first rigorous proof of completeness of such a subsystem of logic, i.e. propositional logic. Another fragment turned out to be what we now call FOL. Specifically, it was first developed in 1917 under the name restricted functional calculus by Hilbert as a subsystem of his functional calculus (effectively a ramified type theory), but was only published in the classic textbook coauthored with Ackermann Grundzüge der theoretischen Logik in 1928, where it was still treated as a subsystem.

In fact, the case was far from settled. While the original Zermelo set theory can be interpreted as being a FO theory (with the separation axiom replaced by an axiom scheme with an axiom for each FO formula), according to Zermelo's own conception it was a second-order theory (with the separation axiom as a single axiom). Zermelo remained a strong proponent of a second-order set theory. Indeed, most logicians did use different fragments of logic for different task and they did not shy to employ second-order theories or anomalous FO theories (i.e. including infinitary operations).

The fact that set theory is today a FO theory is probably due to Thoralf Skolem. In 1923 Skolem presented the original FO axiomatization of Zermelo set theory. Now, there is a standard view that sees a Skolem-Gödel "axis" as urging to adopt a FO set theory and being responsible for the ultimate establishment of FO set theory. It is, however, not clear at all that this was the case, i.e. that Skolem (and Gödel) were pushing an FO object language in set theory. While Skolem was critical of second-order set theory as a foundation of mathematics, he proved his (downward) theorem to hold in FOL. The result - in a countable model it is true that there is a uncountable set - he called a philosophical (albeit not formal) paradox in order to argue that also FOL could not serve as a foundation of mathematics:

I believed that it was so clear that axiomatization in terms of sets was not a satisfactory ultimate foundation of mathematics that mathematicians would, for the most part, not be very much concerned with it. But in recent times I have seen to my surprise that so many mathematicians think that these axioms of set theory provide the ideal foundation for mathematics; therefore it seemed to me that the time had come for a critique. (Skolem 1922)

(There is even the suspicion that Skolem's axiomatization was FO by chance…! There is some good evidence that a lot of the finest minds of their times - like Fraenkel and von Neumann - had trouble developing a real understanding of the difference between FOL and SOL in the mid 20s!).

And Gödel, although he argued for a FO *meta*language, used a variant of type theory in his famous paper in 1931!

To be sure, it is undeniable that both Skolem and Gödel contributed important theorems to help establish FOL, but they did not actually argue for it. The truth seems that there is no simple, success story with heroes to be told here. A more correct account would probably involve multiple causal factors.

The OP's statement that

the completeness of first-order logic was only proved by Kurt Gödel at a time when first-order logic had already displaced second-order logic

is however incorrect. FO axiomatizations of set theory became only dominant starting in the mid 30s. There is an hypothesis to the effect that this timeline should be correlated with Tarski's important contribution to model theory (truth, logical consequence). On this view, FOL became standard not (only) because of its intrinsic qualities, but because it was shown to have a particularly nice model theory.

4. Why (not) first-order set theory?

Nevertheless, I still wonder why […] why the inability of first-order logic to characterize infinite structure is not considered a problem.

Well, a pragmatic answer is that it is not considered a problem because of FOL's inability ;)

As it is not possible to characterize (i.e. axiomatize categorically) infinite structures in FOL, as you say, set theorists simply work with the intended model and they care about non-standard models only when they're needed. That's as good as it gets, I worry.

The more general dispute is about pondering the merits and vices of FOL and SOL. At first glance it seems that

  • FOL

     + complete, compact, nice model theory 
     - deviating from mathematical practice
  • SOL

     + adherent to mathematical practice
     - completeness does not hold

Since nobody would dispute the merits of FOL, it comes down to the question in which way adherence to mathematical practice is really a good thing and how the loss of the merits of FOL is evaluated. From my experience with logicians

  • the supporters of FOL would deem a language without FOL's merits as too much of a loss. In addition, the don't see the deviation from mathematical practice as a vice, but as a feature. This might be a remaining of the finitary tradition in logic: Logic is required to be more strict than mathematics (and its practice) in order to serve as a foundation for it.

  • the supporters of SOL wouldn't deem the loss of completeness etc. as fatal. They see set theory not so much as a foundation of mathematics. Instead, set theory should be more a description of mathematics, i.e. the more adherent to mathematical practice, the better (=more precise) the description becomes.

  • some see a middle-way between the two by adopting another FO set theory like Morse–Kelley set theory. MK, which allows proper classes along withs sets, is syntactically almost identical to second-order ZFC, but differs quite in its semantics.

Pick your choice :)

Sources and further readings:

  • 2
    @RonMaimon By "mathematics is second-order" I simply meant that mathematicians often do use second-order informal reasoning (e.g. they quantify over all functions with a certain property). Even in set theory you find that, e.g. A cardinal κ is measurable if and only if it is the critical point of an elementary embedding j:V → M in V. That these formulations are reducible or translatable to first-order formulations is the whole point of ZFC.
    – DBK
    Commented Apr 20, 2012 at 10:33
  • 2
    This answer has a number of historical errors: first, you are misinterpreting your own Skolem quote! Skolem is not criticizing first or second order, he is criticizing the notion of uncountable infinity, which he believed had no place in mathematics. Your characterization of the history as a series of accidents that left FOL dominant is a gross abuse of the principal actors--- they, especially Hilbert, were trying to make the concept of "effective algorithm" precise, and give an effective algorithm for logical deduction. This led inexorably to the modern computer.
    – Ron Maimon
    Commented Apr 21, 2012 at 1:59
  • 7
    @RonMaimon "Given that we now know computation, the previous literature can be clarified immensely…" Sorry, I don't have neither time nor patience for this kind of Hegelian accounts of history of science. Teleological explanations in history have been left behind a long time ago. As this is not a misunderstanding between us, but two different understandings on how to do history clashing together, I won't spend any more time discussing this point. If that means getting a downvote from you, I'll live with it.
    – DBK
    Commented Apr 21, 2012 at 13:14
  • 3
    @RonMaimon Regarding the interpretation of the quote by Skolem: Your view that Skolem is here criticizing the concept of uncountable sets (as given by Cantor's theorem) is a minority interpretation put forward by Ignacio Janés (2001). I followed the orthodox interpretation (which also reflects how his contemporaries understood Skolem): He had a problem with the fact that we can find a countable model in the first place! …
    – DBK
    Commented Apr 21, 2012 at 13:14
  • 2
    @ChrisS: I haven't read much of anything, I don't read too much. Reading is not the source of knowledge, thinking is.
    – Ron Maimon
    Commented Sep 12, 2012 at 17:46

First order logic is not arbitrary or generalizable, despite the propaganda people give about it. It is a system which is unique up to equivalent reformulations, and it is not a mistake to call it simply "logic". First order logic is the only system one needs for mathematics or philosophy, everything else is a luxury, nice to think about, but not essential. It is best to treat generalizations of first order logic as interesting mathematical exercises.

Before the early 20th century, logic did not exist in any precise enough formulation to allow a machine to deduce consequences from axioms. This means that all the philosophical work on logic from the time of Aristotle to the time of Boole and Frege was of negative value--- it created the illusion that logic was somehow understood, when people didn't have a clue. None of that work is of anything but historical value.

The point of the deduction schemes of the early 20th century was to allow mathematical reasoning to be done mechanically, without any human insight. The goal was to make a set-theory free of contradiction, by treating mathematics as a formal textual manipulation, what we would call nowadays a computation on strings. The development of Hilbert deduction, and Godel's completeness theorem, along with reasonable set-theoretic axioms, completed this program, and it showed that the first-order logic was the correct logic for this purpose. Given any collection of axioms, the first order logic will deduce any consequence, and it will produce a model of these axioms.

First order logic can be done on a computer (in fact, the computer was defined historically as the abstraction of a minimal machine which can do first order logic). Second order logic talks about too-large collections (like the set of subsets of integers, the real numbers) and you cannot reason about these collections in an absolute way on a computer. The only way to know exactly what you mean by the "set of all real numbers" is to make axioms that reflect your metaphysical beliefs about how infinite collections behave, and you get endless debates about the correctness of these axioms, debates which cannot be resolved because they are positivistically meaningless.

Because second order theories talk about collections whose properties are not absolute, it is best to view them as imprecisely defined until they are embedded inside a set theory, and this bigger theory is only made precise when it is a first order theory, so that you can reason about it on a computer. One should not admit anything that cannot be decided by this kind of reasoning as absolutely meaningful.

Because first order logic can model any system that we can work with, its limitations are our limitations, they are true limitations of knowledge not limitations of the system, and it is a mistake to imagine that second order logic extends it in a meaningful way. It is not meaningful to imagine second order creatures reasoning in second order logic "for real", because there is no reasoning in our universe which exceeds first-order reasoning.

  • 1
    I still have too many open questions in my understanding of FOL and SOL. For example, it's unclear to me whether meaningless theorems like us.metamath.org/mpegif/avril1.html which are caused by "emulated second order" definitions like us.metamath.org/mpegif/df-opr.html could have been avoided (and are just accepted for convenience reasons), or whether these are unavoidable artifacts of using FOL as the foundation for the Metamath Proof Explorer. I could ask this question at mathematics.SE, but it's just one of my more concrete open questions regarding SOL. Commented Apr 18, 2012 at 23:59

First-order logic came to be the dominant formal logic because it is fundamental to all logic. Any departure from FOL creates ambiguities which must be resolved. For example, the second-order sentence "a man walked into a room with flowers" is ambiguous. It could mean that a man carried flowers into a room, or that a man walked into a room where flowers were already present.

John Sowa wrote the following about FOL:

"Among all the varieties of logic, classical first-order logic has a privileged status. It has enough expressive power to define all of mathematics, every digital computer that has ever been built, and the semantics of every version of logic including itself. Fuzzy logic, modal logic, neural networks, and even higher-order logic can be defined in [first-order logic]….Besides expressive power, first-order logic has the best-defined, least problematic model theory and proof theory, and it can be defined in terms of a bare minimum of primitives…. Since first-order logic has such great power, many philosophers and logicians such as Quine have argued strongly that classical [first-order logic] is in some sense the ‘‘one true logic’’ and that the other versions are redundant, unnecessary, or ill-conceived."


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .