Ask HN: Teach me something new
The most commonly used and arguably most useful form of logic, First Order Logic (FOL) is not powerful enough to describe even the natural numbers. In whatever ways we may try to describe them, we always end up with potential extra elements that we cannot account for.<p>Let me describe what I mean.<p>When we want to describe a structure, for example the natural numbers with their usual arithmetic (addition, multiplication and so on), we first decide on a language to use. Our language should contain the symbol 0 (so we can identify the first element) and symbols for the functions S (successor function), + and *. We also introduce variables such as x, y, etc.<p>Then we write down a list of axioms for the structure, i.e. logical statements that should characterise that structure. Such statements in first order logic are built out of the symbols we introduced, together with equality (e.g. 2+3=5 is a statement, where 2 is an abbreviation for S(S(0)) etc.), logical connectives such as &quot;not&quot;, &quot;and&quot;, &quot;or&quot;, &quot;implies&quot;, etc. (e.g. not(1 = 2), or &quot;1 = 1 AND 2 = 2&quot;) and importantly quantifiers, &quot;for all elements&quot; and &quot;there exists an element such that&quot; (for example: &quot;for all x, x = 0 OR there exists a y, such that x = S(y)&quot;).<p>A structure for a specific language is nothing more than a set of elements together with an interpretation for all the symbols. So, for our language we may just take the natural numbers with the usual interpretation of +, * etc. But we might just as well have chosen the single-element set {aardvark}, where 0 is interpreted as aardvark and all functions evaluate to aardvard no matter their arguments, i.e. aardvark + aardvark = aardvark. That&#x27;s silly, but allowed. The natural numbers with their usual interpretation of symbols satisfy all the sentences I introduced above; we say that this structure is a <i>model</i> of that set of sentences. Our aardvark-structure is not a model of these sentences, since not(1 = 2) is not true in it (remember that this is just an abbrevation of not(S(0) = S(S(0))) and in this structure, this evaluates to not(aardvark = aardvark), which is false).<p>We can now take the set of <i>all</i> statements which are true in the natural numbers, a.k.a. the theory of natural numbers, Th(N). This set is clearly infinite (for example, it contains the statement &quot;n = n&quot; for all n), but that doesn&#x27;t bother us. Clearly, the natural numbers are a model of Th(N). But are there other models of Th(N)?<p>Well, in a sense trivially. I can just define the structure {aardvark0, aardvark1, ...} where, for example, aardvark2 + aardvark3 = aardvark5, and so on. That&#x27;s also a model for Th(N), but if that feels like cheating it&#x27;s because it is: these structures are exactly the same except for the names of their elements. We therefore call them &quot;isomorphic&quot; and treat them as the same.<p>But are there models of Th(N) not isomorphic to the natural numbers? Yes, there are.<p>Let&#x27;s introduce a new symbol to the language, call it c. Then add to Th(N) the infinitely many statements not(0 = c), not(1 = c), not(2 = c), etc. There is no way we can interpret this symbol c in the natural numbers and make all these statements true: eventually there has to be some natural number which c is equal to.<p>But now comes the kicker: By the compactness theorem of first order logic, <i>whenever we have a set of sentences so that all finite subsets have a model, the original set has a model</i>. Now, for any finite subset of Th(N) plus the infinitely many statements involving c, we have a model, namely the natural numbers (since the subset is finite, there is a biggest n for which not(n = c) is in the set of statements; then interpret c as n+1). But then, by compactness, the original set of sentences has a model.<p>So there must exist a structure that makes all statements true that are true for the natural languages (i.e. that is a model for Th(N)), but that also has some element c that is bigger than anything that can be &quot;reached&quot; by applying the successor function arbitrarily often to 0. What does such a structure look like? Well, it turns out that such an element must live in a so called Z-chain, a set of elements that &quot;looks like the (positive and nonnegative) integers&quot;, but is totally disconnected from the natural numbers (this is because in Th(N) every number that is not zero has a successor and a predecessor); so in essence this structure contains the natural number and, disconnected from it, a copy of the integers. In fact, we may have more than one copy of the integers.<p>Compactness is a really powerful and weird theorem. It can be used to prove that any set of statements that allows for infinite models has infinite models of arbitrary cardinality (i.e. &quot;as big as we want&quot;). It can be used to construct an extension of the real numbers that contains &quot;infinitesimal&quot;, non-zero elements (smaller than any positive real number), which is what motivated so-called nonstandard analysis (and makes Newton&#x27;s and Leibniz&#x27;s original intuition of &quot;infinitesimally small quantities&quot; precise). And so on.<p>If we want to actually describe the natural numbers uniquely, we have to turn to a stronger logic, such as second-order logic. In second-order logic we can&#x27;t only quantify over elements, we can also quantify over sets (or, equivalently, properties). We may for example say &quot;for any set, if it is not empty, it has a least element&quot; (a statement that is true for the natural numbers if we introduce the usual ordering). We can then in second-order logic formulate the principle of induction, which suffices, with some other axioms, to describe the natural numbers uniquely (up to isomorphism, of course).<p>However, second-order logic has significant downsides. In particular, there exists no proof procedure in second-order logic that is both sound (it only proves true statements) and complete (it can prove all true statements). That means that, in practice, it&#x27;s often not all that useful. We do have well-behaved proof procedures for first-order logic and that&#x27;s why we usually stick to it.