Take the 2-minute tour ×
Philosophy Stack Exchange is a question and answer site for those interested in logical reasoning. It's 100% free, no registration required.

Early formal systems like Frege's Begriffsschrift or the Peano's work on the axiomatization of the natural numbers used axiom system 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 number 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.

share|improve this question
+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 Apr 18 '12 at 0:48
You may want to consider asking this same question at mathematics.SE; there are a number of logicians there with historical knowledge. –  Mitch Apr 18 '12 at 2:08
@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. –  Thomas Klimpel Apr 18 '12 at 8:16
I posted my totally refactored answer. –  DBK Apr 19 '12 at 21:46
@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. –  Thomas Klimpel Apr 22 '12 at 14:15
show 2 more comments

2 Answers

up vote 20 down vote accepted

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:

share|improve this answer
This is a little too relativistic. Second order logic must be built on first order logic and a set theory in order to be precise, because the logic itself suffers from incompleteness. The Godel result established the computation exists, and that the limits of computation are the limits of reason itself. It is not reasonable to use a system that presupposes one can exceed these limits, because one can't. –  Ron Maimon Apr 18 '12 at 11:44
Thanks for your answer (both the definite part "... axiomatic set theory is a first-order theory, this sort of answers..." and the caveat). I'm looking forward to the announced second part of your answer... –  Thomas Klimpel Apr 18 '12 at 23:22
@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 Apr 21 '12 at 13:14
@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 Apr 21 '12 at 13:14
That's a wikipedia page answer! Seems a bit of a pointless argument above though, given Ron admits in his profile he hasn't read much philosophy. –  Chris S Apr 24 '12 at 21:30
show 18 more comments

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.

share|improve this answer
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. –  Thomas Klimpel Apr 18 '12 at 23:59
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.