I've heard that first-order logic comes from Peano Arithmetic, yet I can't see how. We don't need numbers to formulate quantifiers, variables, functions, constants, relations or even sets. Insted, it is possible to formulate all Peano's axioms using first-order logic and sets, as one can see here http://de.wikipedia.org/wiki/Peano-Axiome, below the header "Ursprüngliche Formalisierung".

So, how is first-order logic generated from the natural numbers? Does it have anything to do with Primitive Recursive Arithmetic?

  • $\begingroup$ Form one side, we have Peano axioms that are expressed in "mathematical language". They involve a quantification over sets of (natural) numbers; thus, if we want to "formalize" them, we have to use second-order predicate logic. $\endgroup$ – Mauro ALLEGRANZA Mar 20 '15 at 8:52
  • $\begingroup$ Then we have Peano Arithmetic, that is the First-order theory of arithmetic, i.e. a theory based on first-order language with addiotional (specific) axioms. Thus, it makes little sense to say that "first-order logic generated from the natural numbers" ... $\endgroup$ – Mauro ALLEGRANZA Mar 20 '15 at 8:54
  • 1
    $\begingroup$ You ask a lot of reasonable questions, but it seems that you're trying to learn a very delicate and complicated topic, just by asking it online. Are you currently reading some book about it? Have you tried looking at standard material on the topic? All these constructions don't start from nothing. You start by taking some "pre-existing" version of first-order logic, set theory and so on, and you work there, and you show that you can in fact codify everything into the natural numbers in a primitive recursive fashion, and then you can argue about foundations of mathematics being $\sf PRA$. $\endgroup$ – Asaf Karagila Mar 20 '15 at 12:37
  • $\begingroup$ The axioms and rules of logic and set theory must be established before you formally develop number theory or, if you insist, before you formally construct the natural numbers from some other infinite set. $\endgroup$ – Dan Christensen Mar 20 '15 at 14:54
  • $\begingroup$ In an informal way we need to be able to count (to discuss whether two strings are equal, and then to define which of them are valid formulas or statements) to formalize first-order logic. Your Question would be much improved by citing where you "heard" that first-order logic "comes from Peano Arithmetic". It may have been intended as a historical remark rather than as ontological development. $\endgroup$ – hardmath Mar 20 '15 at 15:02

Just in historical terms, "first order logic comes from Peano Arithmetic" is not correct. Really the two ideas, of extending axiomatic reasoning beyond (Euclidean) geometry into algebra and arithmetic, and of formalising logic to express more than Aristotelian syllogisms could, proceeded hand in hand.

Progress in logic beyond the handling of quantifiers in the syllogism was gradual through the 19th century. Important names include Augustus de Morgan and JS Mill. Gottlob Frege essentially nailed the problem in 1879, introducing the first order quantifiers $\forall, \exists$ and hence codifying logic with the syntax still used today.

Meanwhile mathematicians including De Morgan again, Grassmann, and Peirce, had been formalising the theory of arithmetic. Frege's syntax was obviously helpful for putting sentences like Bolzano's $\epsilon$-$\delta$ definition of continuity into a precise form, and equally for the laws of arithmetic. Peirce published a set of axioms in 1881.

But the important part of the project was to get beyond the "deductive" reasoning of syllogisms to all the "inductive" rules which mathematicians use in natural proofs. These require writing down, not just true first-order statements about numbers (etc), but reasoning about collections of numbers together. Frege (and other philosophers, going way back) called such a collection the extension of a concept. The extension of a mathematical predicate $P(x)$ is just $\{x: P(x)\}$, the collection of everything for which $P$ is true. In particular, with Frege's new logical notation, any first-order formula $\phi(x)$ in the notation is a concept, so $\{x: \phi(x)\}$ should be an extension. Frege also introduced the notation $x \in A$, to mean "$x$ satisfies the concept defining $A$".

Obviously these extensions are now recognisable as (naive) sets. (I can't recall offhand when this word was introduced). Dedekind in 1888 and then more neatly Peano in 1889 gave axioms for arithmetic including reasoning with these sets. Peano's point is that all the use one needs to make of sets in arithmetic comes in the familiar rule of arithmetic induction, which (as had been obvious for ages) can't be expressed in syllogisms. "If the extension of any predicate includes 0, and includes $x+1$ whenever it includes $x$, then it includes all numbers"---Peano was certainly thinking in terms of full Fregean logic.

Then in 1901 Bertrand Russell demonstrated, in a letter to Frege, his paradox of the set $\{x: x \not \in x\}$. This horrified Frege, Dedekind, and everybody else involved with the project of formalising mathematics---it showed that some of the formulas expressible in Frege's syntax aren't consistent concepts. Or possibly it showed that the whole formalism was wrong; but it was obviously too useful for real mathematics to throw away entirely.

So Russell, Zermelo, and all the rest, put in a lot of effort salvaging Fregean logic from the paradox. The obvious cause of the problem with $\{x: x \not \in x\}$ is that it's self-referential (like the ancient Liar paradox), and the natural way to avoid self-reference is to stratify your reasoning. Philosophically the paradoxical set is failing to distinguish between an object and a predicate. Russell's solution was, from the top down, to impose a Byzantine structure of orders and degrees on the sets and quantifiers, to ensure that objects and predicates never conflicted. From this the language of first-order and second-order logic emerged.

The downside of this is that you can obviously do first-order reasoning about (well-behaved) sets themselves---De Morgan's laws, for example---and so you need to replicate all of first-order logic in the second-order case, and so on for a towering hierarchy of identical proofs with different subscripts. The symbol $\in$ becomes very difficult to work with.

Zermelo introduced a bottom-up construction for well-behaved sets which could be guaranteed not to need Russell's structure, to let $\in$ be an ordinary mathematical relation, and yet still to avoid the paradox.

Fortunately Peano's axioms can be made to work in either context. You don't need the full self-referential behaviour of $\in$ to talk about arithmetic, so "second-order" formulas in Russell's sense are adequate. In Zermelo's set theory you can construct a set satisfying the Peano second-order axiom whenever the predicate for inducting over is expressible as a set, so (relative to the set theory) Peano arithmetic works here as well.

Much of the work on Zermelo sets was done, in the 1920s, by Skolem; he refined the Zermelo axioms, especially distinguishing the Axiom of Choice. In the meanwhile a whole school of "Intuitionistic Logic" had been developed, to try to encapsulate more accurately the reasoning mathematicians really need, rather than trying to row backwards from the excessive and inconsistent Fregean system, in which Peano arithmetic seems to work but only haphazardly. This wasn't successful in its own terms (though it has proved useful in other contexts, category theory and so forth). Primitive recursive arithmetic was Skolem's formulation of an intuitionistically valid part of all arithmetic. It wasn't successful in supplanting full Peano reasoning, but is genuinely interesting in its own right.

Finally in 1931 Gödel published his first Incompleteness Theorem, showing that second-order Peano reasoning, or equally arithmetic in the Zermelo universe, could neither of them be proved consistent. At this point mathematicians heaved a sigh of relief and stopped worrying that they might be proved inconsistent. And that is where the story ends.

(All dates off Wikipedia.)

  • $\begingroup$ Very nice answer, +1. $\endgroup$ – Demosthene Mar 20 '15 at 17:06
  • $\begingroup$ It was Godel's Second Incompleteness Theorem which dealt with consistency proofs. The First Incompleteness Theorem introduced the point that none of these axiomatisations could be complete, a somewhat different result. $\endgroup$ – Roy Simpson Feb 23 '19 at 12:41

To add to HTFB's excellent answer above, I'd only add a few small points:

  • Though Frege was first with the invention of quantifiers, he appears to have been overlooked at the time; it was Peirce's subsequent independent reinvention that spread. Consequently the notation we use is more similar to Peirce's than to Frege's two-dimensional notation (though we owe the "turnstile" notation for entailment to Frege). This random web page claims the $\in$ notation was introduced by Peano in 1889, as an abbreviation of "est".

  • In retrospect, it's perhaps unsurprising that Frege ran into set-comprehension problems; his 1884 (non-rigorous) book The Foundations of Arithmetic is breathtakingly cavalier about such issues. He defines the number 3 as the collection of all collections with three elements - every triple of boots, telephones, planets, emotions, numbers...

  • The formalization of arithmetic induction had been going on for a while before Peano; according to his Wikipedia page De Morgan made great strides here.

  • $\begingroup$ Note that Peano didn't use the modern $\in$ sign, he used a standard $\varepsilon$. I don't know when $\in$ became common but I imagine there was a transition through $\epsilon$ on the way to $\in$. I wrote a few other notes about the history of logical notation here. One thing I didn't mention there is that Principia Mathematica uses $(\exists x)(\Phi x)$ for existential quantification, following Peano, and $(x)(\Phi x)$ for universal quantification, sort-of-following Frege. $\endgroup$ – MJD Jun 5 '15 at 18:03
  • $\begingroup$ (The Frege Begriffsschrift notation for universal quantification is to put the quantified variable into a sort of little cup.) $\endgroup$ – MJD Jun 5 '15 at 18:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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