34

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.

  • 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
    Apr 18, 2012 at 0:48
  • 1
    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, 2012 at 2:08
  • 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. Apr 18, 2012 at 8:16
  • I posted my totally refactored answer.
    –  DBK
    Apr 19, 2012 at 21:46
  • 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. 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
    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
    Apr 22, 2012 at 16:31

3 Answers

31

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:

  • 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, 2012 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... Apr 18, 2012 at 23:22
  • @Ron What do you mean by "relativistic"? Do you mean the circumstance that I do not profess unconditional love and praise for FOL? ;)
    –  DBK
    Apr 18, 2012 at 23:46
  • @DBK: Yeah--- sort of--- not love or praise, but full understanding. I don't have a full understanding of second order logic, because I can't compute it like FOL.
    –  Ron Maimon
    Apr 19, 2012 at 0:09
  • @RonMaimon Well, since mathematics is second-order, then you do not fully understand mathematics ;) BTW, I totally rewrote my answer…
    –  DBK
    Apr 19, 2012 at 22:09
  • @DBK: Matheamtics is first order--- ZF is stronger than second order arithmetic, and it is stronger than all reasonable "second-order" logic, but it is a first order theory. It is precisely because you want the uncountable collections in the theory, not in the logic, that people standardized on first-order logic. This logic is sufficient for all of mathematics as practiced, and it can describe second order theories with a greater precision than the second order theories themselves. To make second order quantification precise, you need a first order framework to define the domain.
    –  Ron Maimon
    Apr 20, 2012 at 0:32
  • @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
    Apr 20, 2012 at 10:33
  • @DBK: Yeah, of course, but that second order sentiment is imprecise unless it is in ZF. It becomes precise in ZF, because ZF has a deduction program to produce all consequences and the result produces a symbol model. This is why first order logic is fundamental and second order is not, and this answers the question.
    –  Ron Maimon
    Apr 20, 2012 at 15:22
  • 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
    Apr 21, 2012 at 1:59
  • Given that we now know computation, the previous literature can be clarified immensely. They are attempts to produce a notion of deduction in an era where it was not clear there was a unique notion of computation that did not rely on any metaphysical assumptions. Skolem's prejudice that countable sets are absolute, while uncountable collections are paradoxical is reflected in the fact that any textual manipulation algorithm can only give countably many distinct names to objects. There is absolutely no way this development could have ended with anything different than what we have today.
    –  Ron Maimon
    Apr 21, 2012 at 2:01
  • -1, sorry, this answer is completely wrong in both general scope and thrust, and in all the details. I'll remove if it gets fixed. The Skolem stuff must be rewritten. Also, the statement that second order quantification is closer to mathematical practice is completely moot in a normal set theory where you quantify over sets, so I don't see the point.
    –  Ron Maimon
    Apr 21, 2012 at 2:04
  • 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
    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
    Apr 21, 2012 at 13:14
  • @RonMaimon … Since this holds precisely for every countable axiomatisation of set theory in FOL, Skolem's paradox expresses his general critique of FO axiomatisations of set theory. Skolem's remark is also motivated by his discovery that first-order theories are not categorical. Löwenheim-Skolem implies that categoricity fails in first-order theories. Since semantic completeness follows from categoricity, the failure was seen by Skolem as an argument against a first-order axiomatization of set theory.
    –  DBK
    Apr 21, 2012 at 13:14
  • @DBK: As for "Hegelian" account--- I don't like Hegel. The account I give is simply the correct one as any mathematician will tell you. People were groping toward a computer all throughout the early 20th century, primitive recursion was defined and redefined, Post gave a computer, finally it was made precise by Godel and Turing in 1936 and it stuck. The action was teleologically motivated, as even they write! They are looking for a precise finitistic formulation of algorithm and logic. There is only one way to do this, and this is what they found. This is not debatable.
    –  Ron Maimon
    Apr 21, 2012 at 17:27
  • @DBK: Your assertion that the "intended model" of set theory is an obvious well defined notion is false. The "intended model" certainly has ordinals aleph-1 aleph-2 aleph-omega, and it has the real numbers P(omega), and P(omega) maps one to one to exactly one aleph. Which one? Perhaps you think the intended model obeys V=L. Perhaps you think it obeys P(omega)=aleph-2. Who can decide? These questions are easily shown to be vague in first order ZFC--- you can force them one way or the other--- and the issues do not ever get resolved, not by higher cardinals, not by anything.
    –  Ron Maimon
    Apr 22, 2012 at 18:02
  • @DBK: All set theorists since 1963 work regularly with countable models of ZF as the main object of study, and which countable model better reflects the "true" structure of the universe has never been settled on. I of course think the question is meaningless, but if I had to choose, I would put the reals at higher than any ordinal, and every subset of R measurable (so no choice on R). This is the most convenient choice for measure theory and integration, but it is not popular among mathematicians who want to believe the reals can be well ordered, although it is proved it can't really be done.
    –  Ron Maimon
    Apr 22, 2012 at 18:13
  • @RonMain: Where did I assert that the "intended model of set theory is an obvious well defined notion"? I didn't. Please stop falsely ascribing claims to others. For generic purposes, the intended model of ZFC is V = the full cumulative hierarchy. But, as you said, one can restrict V by adding V=L or force new models to his or her liking. As for my own view, I am sympathetic to Hamkins' multiverse view.
    –  DBK
    Apr 22, 2012 at 21:57
  • 6
    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, 2012 at 21:30
  • 1
    @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
    Sep 12, 2012 at 17:46
  • @Ron so how do you pass on knowledge to other people? (Please don't say the bible way!)
    –  Chris S
    Sep 12, 2012 at 19:42
  • 1
    @ChrisS: By writing. But you want to be respectful of people's time and write the tersest possible account. This means, Hegel is wasting my time, Heidegger is wasting my time, Kant is wasting my time, and I will not read them, I will skim them quickly, as they do not deserve close reading. Nietzsche doesn't deserve any reading at all. I try to read the densest possible literature, as this packs the most information per word. What the heck is the Bible way? Prayer?
    –  Ron Maimon
    Sep 13, 2012 at 7:57
  • 1
    @ChrisS: This answer is abysmal and should be deleted. It might be a "Wikipedia page" answer, but that's not a complement in this case.
    –  Ron Maimon
    Sep 13, 2012 at 8:16
7

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. Apr 18, 2012 at 23:59
2

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."

Your Answer

  • Links
  • Images
  • Styling/Headers
  • Lists
  • Blockquotes
  • Preformatted
  • HTML
  • Tables
  • Advanced help

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