This is an appreciation of Gödel’s Incompleteness Theorem of 1931. I am provoked by a depreciation of the theorem.
I shall review the mathematics of the theorem, first in outline, later in more detail. The mathematics is difficult. I have trouble reproducing it at will and even just confirming what I have already written about it below (for I am adding these words a year after the original publication of this essay).
The difficulty of Gödel’s mathematics is part of the point of this essay. A person who thinks Gödel’s Theorem is unsurprising is probably a person who does not understand it.
In the “Gödel for Dummies” version of the Theorem, there are mathematical sentences that are both true and unprovable. This requires two points of clarification.

Gödel shows not only

that true unprovable sentences exist, but also

how to write down an example.
The example will be the sentence written symbolically as
∀x Q(x, p),
read out as
“For all numbers x, Q is true of x and p,”
for a certain binary predicate Q and a certain number p.


A sentence known to be true must have a proof of some kind. The proof that the sentence ∀x Q(x, p) is true will be of a new kind, not under consideration when the sentence is constructed. From a system for proving theorems that meets a certain standard, the sentence ∀x Q(x, p) is obtained, and this sentence is not a theorem of that system.
The sentence ∀x Q(x, p) will be true, because its very meaning is that the sentence ∀x Q(x, p) has no proof in the given system. In the “Gödel for Dummies” version, the sentence means, “I have no proof.” If this were false, then the sentence would have a proof and would therefore be true; thus it is true, but has no proof.
The sentence ∀x Q(x, p) does not refer to itself as such. The reader may skip the details, which we shall take up again only later; but

p is the “Gödel number” of the formula ∀x Q(x, y), and

Q is so defined that, for all numbers a and b,

if the sentence Q(a, b) is not true,

then, and only then,

b is the Gödel number of some formula φ(y), and

a is the Gödel number of a proof of the sentence φ(b) within our specified system.


Thus the meaning of ∀x Q(x, p) is that no x is ever the Gödel number of a proof of the sentence φ(p), when φ(y) is the formula of which p is the Gödel number. In short, φ(p) is unprovable. We now observe that φ(p) is precisely the sentence ∀x Q(x, p).
That was a simplified version of Gödel’s Theorem. Such a version can be found, for example, in the twopage article “Gödel’s Theorem” by Peter J. Cameron in the Princeton Companion to Mathematics (2008). There is additional interest in the full version of the Theorem, which is reviewed by C. Smorynski in a 46page article, “The incompleteness theorems,” in the Handbook of Mathematical Logic (1977). For the present article, my main source is Gödel’s own article, translated as “On Formally Undecidable Propositions of Principia Mathematica and Related Systems I” in From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, edited by Jean van Heijenoort (third edition, 1976).
Even in the simplified version, is Gödel’s result surprising? At least one person thinks not. In an interview by John Horgan called “Philosophy Has Made Plenty of Progress” (Scientific American, November 1, 2018), Tim Maudlin says,
Absolutely no one should have ever been surprised that mathematical truth cannot be equated with theoremhood in some finite axiomatic system. An infinitude of mathematical truths are uninteresting trivia, with no obvious route to being proved. Example: [to be considered later].
… All Gödel did was find a clever way to construct a provably unprovable mathematical fact, given any consistent and finite set of axioms to work with. The work is clever but in no way profound. It should have come as no surprise at all.
Gödel’s “clever way to construct a provably unprovable mathematical fact” laid the foundations of computer science, proof theory, recursion theory, and even, in a different sense, my own field, model theory. Perhaps I should say Gödel helped lay the foundations; but the several fields that I named would have been completely different, if they had developed at all, without the failure of Hilbert’s program constituted by Gödel’s results.
I see two important technical errors in what Maudlin says.

Having “no obvious route to being proved” is not the same as being unprovable.

Gödel’s Theorem holds, not for “any consistent and finite set of axioms,” but for a set of axioms that meets a more precise criterion, except that finiteness is not part of it.
Several more points should be clarified.

As noted, the set of axioms covered by the Theorem need not be finite; it can be infinite, as long as it is recursive, in the sense that there is a method for telling whether a given expression is one of the axioms.

The Theorem involves not just axioms, but rules of inference for deriving theorems from the axioms. Axioms and rules of inference together compose the kind of system, a proofsystem, referred to earlier.

Consistency has two meanings a priori:

A set of axioms is consistent if it has a model;

a proofsystem is consistent if it cannot prove a contradiction.
Before the Incompleteness Theorem could be stated and proved, somebody needed to clarify the relation between these two notions of consistency. Gödel did this too, with his Completeness Theorem, to be discussed a bit later.

For examples of rules of inference, I look now to Euclid.

The fifth proposition of the first book of Euclid’s Elements is that the base angles of every isosceles triangle are equal to one another.

From that proposition, we can conclude, by the rule of inference called instantiation, that

if, in a particular triangle ABC, the sides AB and AC are equal,

then so are the angles ABC and ACB.


If we can prove that triangle ABC is indeed isosceles as described, then, by the rule of inference called modus ponens, the base angles of ABC must be equal.
Those rules of inference are nothing surprising, and Euclid does not spell them out. However, Euclid’s “common notions”—rules such as “Equals to the same are equal to one another”—can be understood as the axioms of his proofsystem.
We can apply a proofsystem to additional axioms—or we may call them postulates—, so as to derive theorems from these. Thus we can understand the Elements as an application of a certain proofsystem to Euclid’s explicit postulates, such as the Parallel Postulate (“If a straight line cross two others and make the interior angles on the same side less than two right angles, then the two straight lines, extended, will meet on that side”).
For the Incompleteness Theorem, Gödel derives a proofsystem from the Principia Mathematica (1910–3) of Whitehead and Russell, and he applies it to the Peano Axioms for the counting numbers.
Actually Gödel works with the natural numbers, starting with zero. We shall start with unity instead, which is what Peano himself did, although there are technical reasons why having zero can be nice.
Unity is a counting number, and every counting number has a successor. Concerning these two conditions, we have the following postulates.

Unity is not the successor of any counting number.

Counting numbers having the same successor are the same.

A set contains all counting numbers, provided it contains

the successor of its every element, and

unity.

Those are the Peano Axioms, which Peano published in 1889, using notation that Russell and Whitehead would adopt for the Principia Mathematica. Dedekind published equivalent postulates earlier, in 1888, but without notation that caught on.
Dedekind understood the postulates better than Peano, as I have discussed in an article called “Induction and Recursion” (The De Morgan Journal 2, no. 1 [2012], 99–125). The third of the Peano Axioms above is the Induction Axiom.
The three Peano Axioms together (but no two of them alone) entail the Recursion Theorem. The words induction and recursion are sometimes used interchangeably, but it seems better to distinguish them as follows.

Induction is a method of proving theorems that are true about all counting numbers.

Recursion is a method of defining functions of counting numbers.
For example:

It is a theorem that every counting number is either unity or the successor of a counting number. The proof is that

unity meets the condition of being either unity or a successor, and

the successor of every natural number that meets that condition also meets the condition.
Perhaps that is the simplest nontrivial proof by induction. (Each of the two steps may be trivial, but the proof as a whole is not, if only because it does need those two steps.)


Denoting unity by 1 and the successor of m by Sm, and letting n be an arbitrary counting number, we recursively define addition of counting numbers to n by requiring
n + 1 = Sn
and, for all counting numbers k,
n + Sk = S(n + k).
There is a similar recursive definition of multiplication:
n ⋅ 1 = n & n ⋅ Sk = n ⋅ k + n.
We can write out the Induction Axiom formally as
∀X (1 ∈ X & ∀y (y ∈ X ⇒ Sy ∈ X) ⇒ ∀y y ∈ X),
to be read as,
For all X,

if

1 is in X, and

for all y,

if y is in X,

then the successor of y is in X,



then for all y, y is in X.
The postulate is secondorder, because it uses a variable, namely X, that stands for sets of numbers. The variable y stands for individual numbers; a formula using only such variables is firstorder. Peano introduced the symbol ∈, which we can read as “is in”; the symbol is based on the Greek epsilon, the initial letter of ἐστί, meaning “is.” For the arrow ⇒ of implication, Peano used a different symbol (a reversed letter C, thus Ɔ, later stylized as ⊃).
The Recursion Theorem is also secondorder, since it uses variables for functions of numbers. Using Greek letters η and ζ (eta and zeta) for such variables, we can write the Recursion Theorem as
∀x ∀η ∃ζ (ζ(1) = x & ∀y ζ(Sy) = η(ζ(y))).
In words, for every counting number x, for every function η of a counting number, there is a function ζ of a counting number such that

the value of ζ at 1 is x, and

for every counting number y, the value of ζ at the successor of y is the value of η at the value of ζ at y.
Gödel proves the Incompleteness Theorem using secondorder variables. Then he shows that, by introducing secondorder constants, + and ×, for the recursively defined functions of addition and multiplication, along with appropriate axioms that govern their behavior, we can do everything in firstorder logic.
The firstorder sentences that are true in a particular structure constitute the complete theory of that structure. The structure is then a model of that theory. If we let N be the set of counting numbers, then the complete theory of the structure (N, +, ×) is not recursively axiomatizable. In other words, the indicated complete theory is undecidable: there is no algorithm for deciding whether a proposed firstorder theorem about (N, +, ×) is true. This is Gödel’s 1931 result. Equivalently, any recursively axiomatized theory for which the structure (N, +, ×) is a model must be incomplete.
By contrast, Presburger gave, in 1929, a recursive axiomatization of the complete theory of (N, +); Skolem gave, in 1930, the same for (N, ×). Since then, many decidable complete theories have been found. They are the subject of Abraham Robinson’s 1956 book Complete Theories, and they are a subject of model theory, which again is that branch of mathematical logic that I happen to specialize in.
Tim Maudlin specializes in the philosophy of physics. His belittling of accomplishments in other fields is unbecoming. Mathematics is intimately connected with physics, and the two fields have been indistinguishable for much of their history; but they are different, as follows.

Mathematical proof is deductive, even when it is “proof by induction” as above.

Physical proof is inductive, in the nonmathematical sense.
Maudlin may be satisfied with general inductive proof. Others of us are not.
One might attempt to characterize an inductive proof as having the form, “Suchandsuch has happened in n cases; therefore it will always happen.”
For example, when we draw k points on the circumference of a circle, and connect every pair with a straight line, then these lines divide the circle into 2^{k − 1} regions in at least 5 cases, when k is 1, 2, 3, 4, or 5. Therefore, “by induction,” the same will happen, no matter what number k is.
It doesn’t happen. With 6 points we get 31 regions, not 32. But even if the suggested result always occurred, the proposed proof would be inadequate, even as an inductive proof in the informal sense.
Inductive or not, every proof needs to be backed up with some kind of reason. Different fields of inquiry will allow different kinds of reasons. I can say no more than this, except that, in mathematics, in an inductive proof, the reason will again be a twopart deduction:

The assertion to be proved about k is true when k = 1, and

For every counting number m,

if the assertion is true when k = m,

then the assertion is true when k = m + 1.

In mathematics, such a deduction about every number m is possible.
Elsewhere in the interview by John Horgan, Maudlin says he believes—though he has no proof—that
the fundamental physical law—when presented in the right mathematical language—will be so compellingly simple that we would think that any other structure would be unnecessarily complicated.
There seems to be no question of whether there is a fundamental physical law. However, if there were such a thing, it would effectively be an axiom from which every scientific truth could be proved. In that case, with Maudlin’s own interpretation of Gödel in mind, might we not suggest that physicists are wasting their time and our money, trying to find a fundamental physical law, since “absolutely no one” should expect it to exist?
When making such a grand assertion about matters outside one’s own field, one may be missing something.
Physics is mentioned in the 1958 book of Ernest Nagel and James R. Newman called Gödel’s Proof:
… although certain parts of physics were given an axiomatic formulation in antiquity (e.g., by Archimedes), until modern times geometry was the only branch of mathematics that had what most students considered a sound axiomatic basis.
But within the last two centuries the axiomatic method has come to be exploited with increasing power and vigor. New as well as old branches of mathematics, including the familiar arithmetic of cardinal (or “whole”) numbers, were supplied with what appeared to be adequate sets of axioms. A climate of opinion was thus generated in which it was tacitly assumed that each sector of mathematical thought can be supplied with a set of axioms sufficient for developing systematically the endless totality of true propositions about the given area of inquiry.
Gödel’s paper showed that this assumption is untenable …
Should mathematicians really have known all along that “this assumption is untenable”? They would first have had to recognize the assumption as such.
From the discovery of nonEuclidean geometry in the midnineteenthcentury, one may induce, or simply suspect, that Euclidean geometry without the Parallel Postulate is incomplete. This is only a suspicion, until one can actually prove the consistency of Lobachevskian geometry, in which the Parallel Postulate is false.
One can deduce the consistency of Lobachevskian geometry by using Euclidean geometry to construct a model. In one such model, you let an infinite straight line divide the Euclidean plane into two parts. You throw out one part, along with the points on the dividing line itself. In the remaining “halfplane,” semicircles with centers on the boundary line are to be considered as “straight” in Lobachevski’s sense. So are straight lines at right angles to the boundary line; but no other lines, whether straight or curved, are to be considered as “straight” in Lobachevski’s sense. Euclidean full circles in the halfplane are Lobachevskian circles, though their “centers” will not be the usual centers. Right angles stay the same. In this way, as Euclidean geometry is consistent, so is Lobachevskian geometry, though it denies the Parallel Postulate; thus this postulate is not implied by Euclid’s other postulates.
We say Euclidean geometry is consistent, because we think that it has a model, namely the plane that we imagine our geometrical diagrams to lie in. In the seventeenth century, Descartes used this model to establish the consistency of algebra.
The discovery of nonEuclidean geometry casts doubt on whether Euclidean geometry is indeed consistent: on whether the model that we imagine to exist really does exist.
To settle the question, we can turn Descartes around. David Hilbert does this in The Foundations of Geometry (1899). If (Ω, +, ×, <) is an Archimedean ordered field in which Ω contains the square root of each sum a^{2} + b^{2} of squares of elements a and b of Ω, then the set Ω^{2} of ordered pairs of elements of Ω serves as a plane in which Hilbert’s axioms for Euclidean geometry are satisfied.
Evidently Hilbert’s proof requires us to believe that there really are such Archimedean ordered fields Ω.
Hilbert observes the possibility of an Axiom of Completeness, which would ensure that Ω must be the set R of socalled real numbers, the numbers that we imagine to correspond to the points on a geometrical line, once we select points for 0 and 1. Dedekind has shown (on November 24, 1858, he says) that we do not actually need any geometrical assumptions here, but can define the real numbers, with all desired properties, as certain sets of rational numbers. We can understand each rational number as an appropriate set of ordered pairs of counting numbers. Thus if the Peano Axioms are consistent, in the sense of having a model, then so is Euclidean geometry consistent.
The completeness of Hilbert’s Axiom of Completeness is not of a theory; it is completeness of the ordering of the field Ω. An ordered set is complete if every nonempty subset that has an upper bound has a least upper bound. This is a secondorder condition.
As Tarski showed in the 1940s, the firstorder theory of the real ordered field (R, +, ×, <) is decidable; equivalently, the field has a recursive axiomatization. The axioms are those of a real closed field. But there are other real closed fields besides R.
By contrast, the ordered field of real numbers is completely determined by the axioms of a complete ordered field; in a word, these axioms are categorical. So are the Peano Axioms. However, in each of these two cases, one of the axioms is secondorder. The Archimedean Axiom, which Ω above satisfies, is also secondorder; however, the unique complete ordered field R is automatically Archimedean.
There is a third kind of completeness, enjoyed by a consistent proofsystem when, for every sentence σ that is true in every model of a set Γ of axioms, there is a proof of σ from Γ. By the Completeness Theorem, proved by Gödel in his doctoral dissertation of 1930, a complete firstorder proofsystem can be extracted from the Principia Mathematica. Consequently, if this proofsystem cannot derive a contradiction from a given set of axioms, then this set must be consistent in the sense of having a model.
At the beginning of the 1930 paper based on his dissertation, Gödel explains the Completeness Theorem as follows, for the case when Γ above is empty. The bold emphasis is mine:
Whitehead and Russell, as is well known, constructed logic and mathematics by initially taking certain evident propositions as axioms and deriving the theorems of logic and mathematics from these by means of some precisely formulated principles of inference in a purely formal way (that is, without making further use of the meaning of the symbols). Of course, when such a procedure is followed the question at once arises whether the initially postulated system of axioms and principles of inference is complete, that is, whether it actually suffices for the derivation of every logicomathematical proposition, or whether, perhaps, it is conceivable that there are true propositions (which may even be provable by means of other principles) that cannot be derived in the system under consideration.
On the contrary, the question of completeness did not arise at once, at least not for Russell and Whitehead, though it did for Hilbert and Ackermann in 1928. Nonetheless, Gödel continues:
For the formulas of the propositional calculus the question has been settled affirmatively; that is, it has been shown that every correct formula of the propositional calculus does indeed follow from the axioms given in Principia Mathematica. The same will be done here for a wider realm of formulas, namely those of the “restricted functional calculus” …
The restricted functional calculus is a calculus of what we now call firstorder formulas.
In the same paper, Gödel proves also the countable case of what we now call the Compactness Theorem: that if every finite subset of a set Γ of sentences has a model, then Γ itself has a model. Malcev will later establish the general case, where Γ may be uncountable. The general form of the Completeness Theorem follows from the special form, where Γ is empty, and Compactness. Conversely, since proofs are finite, Completeness implies Compactness.
There can be no compactness theorem for secondorder logic, and hence no completeness theorem. For example, to the axioms for a complete ordered field, we can add infinitely many axioms, whereby the ordered field has an element a that is greater than 1, 2, 3, and so on, and is thus infinite. A model of these axioms would be nonArchimedean, and then its ordering would not be complete (since there could be no least upper bound on the set of finite elements). So the enlarged set of axioms has no model, although every finite subset has one, namely R itself with a great enough.
In Hilbert’s Foundations of Geometry, the distinction between first and secondorder logic has yet to be recognized. In the Principia Mathematica, Russell and Whitehead work with variables of arbitrarily high order. For the Incompleteness Theorem, as we said, Gödel works first with the whole system of the Principia Mathematica, before showing that firstorder logic is enough.
Pace Mr Maudlin, a lot of distinctions have to be discovered, before the question can even be raised of whether there are undecidable firstorder theories.
The physicist Richard Feynman had a way of teasing mathematicians about their proofs. Possibly Maudlin imitates Feynman, who told his mathematician friends,
I bet there isn’t a single theorem that you can tell me—what the assumptions are and what the theorem is in terms I can understand—where I can’t tell you right away whether it’s true or false.
Could Feynman cut up an orange and rearrange the pieces into another solid sphere, as large as the sun? He thought not. The mathematicians said he could. However, this result, the Banach–Tarski Paradox, requires infinite divisibility of matter (also the Axiom of Choice). Feynman was correct, if his friends were talking about real oranges, made up of atoms. “So I always won,” he said:
If I guessed it right, great. If I guessed it wrong, there was always something I could find in their simplification that they left out.
This is from “Surely You’re Joking, Mr. Feynman!” (1985; page 85).
By way of showing that the Incompleteness Theorem should have been obvious, Maudlin proposes the question of whether, in the decimal expansions of two real numbers, there is a difference in the first digit, and the next two digits, and the next three digits, and so on. Approximately eight times out of nine, all of these differences will occur. In this case, in Maudlin’s terminology, the original numbers fail to “match.” Can we then prove the failure? Maudlin says,
No amount of just grinding out the digits and checking will ever prove it: there are always more digits to check. And I see zero prospect of any other way to prove that they don’t match. So if they don’t match, that is an unprovable mathematical fact.
Maudlin sees no way to come up with a proof; therefore, for him, there is no proof. This is an induction. Mathematics asks for deductions.
I recall a fellow mathematician to have said that a conjecture ought to be more certain than a theorem. You can prove a theorem without having any intuition for the result; but your proof can always contain mistakes that you did not notice. If you make a conjecture, your confidence in it ought to be greater than your confidence in all of the steps of a proof that convinces you of some other assertion. That is one opinion. I believe the person who expressed it had confidence in the Conjecture of Birch and SwinnertonDyer. This did not mean he was going to derive consequences from the conjecture and assert them as new theorems.
As for Gödel’s Completeness Theorem, one might try to argue that there are uncountably many pairs of real numbers that do not “match,” but only countably many proofs; therefore there must be examples of pairs of real numbers that do not “match,” although we cannot prove the failure. As an alternative to Gödel’s proof, such an argument itself fails, because only countably many real numbers can be defined. For example, if you are going to express a real number by its decimal expansion, you need a rule for generating the digits; and there can be only countably many such rules.
There can be only countably many recursively axiomatized complete theories. However, there are uncountably many countable complete theories, since the structure (N, 1, S, P) has a different theory for each choice of P as a subset of N. We can conclude that one of these theories, even uncountably many of them, must be undecidable; but we do not yet know which. Gödel, again, gives us an example, namely (N, +, ×), of a structure with an undecidable theory.
Gödel’s Proof
Let us look at Gödel’s argument in more detail.
If you are reading these words on a computer screen, you know that, behind the scenes, each letter has a certain code, which is a number. We express mathematics using formulas; we can understand these as strings of symbols or characters from a certain list; we can give each of those characters a number. One example of a formula is a sentence expressing Fermat’s Last Theorem, proved by Wiles:
∀x ∀y ∀z ∀w (x^{w} + y^{w} = z^{w} & w ≠ 1 ⇒ w = 2).
Let us call this an arithmetical formula, because the variables range over the counting numbers: arithmoi for the Greeks. Unity was not an arithmos, because it was just one; but we count unity as a number. Gödel counts zero as well, but I prefer to leave this out.
We should understand the typographical raising of an exponent as having its own symbol, such as a circumflex (ˆ). Then the symbols that we used above are on the list
∀, x, y, z, w, (, ˆ, +, =, &, ≠, 1, ⇒, 2, ).
We can understand our formula itself as the list
∀, x, ∀, y, ∀, z, ∀, w, (, x, ˆ, w, +, y, ˆ, w, =, z, ˆ, w, &, w, ≠, 1, ⇒, w, =, 2, ).
We number the list of all symbols that we may want to use. For writing down numbers themselves in arithmetical formulas, the ten usual digits suffice; moreover, since any number can be written as a sum
1 + 1 + … + 1,
the symbols + and 1 suffice. Still our list of symbols may be infinite, since there is no bound on the number of variables that we may want to use. We could however let every variable be x followed by some number of “primes,” as in x′, x′′, x′′′, and so on. In any case, every symbol on our list can be given its own number, even if the list is infinite. Using these numbers, we can convert any formula into a list of numbers. This will always be a finite list.
We can convert such a list into a single number, in a reversible way. Gödel’s method relies on the Fundamental Theorem of Arithmetic, that each number has a unique prime factorization. If we list the prime numbers as p_{1}, p_{2}, p_{3}, and so on, then any finite list
n_{1}, n_{2}, …, n_{k}
of numbers corresponds reversibly to the product
p_{1}^{n1} × p_{2}^{n2} × … × p_{k}^{nk}.
In this way, given an arithmetical formula φ, we convert it into a list of numbers, and then into a single number. Let us denote this last number by
⌜φ⌝,
using socalled Quine corners. We now call this the Gödel number of φ.
Given some true arithmetical sentences, we can derive other true sentences in a formal way, by such rules of inference as were mentioned earlier. For example,

if ∀x φ(x) is true, then so is φ(3), that is, φ(1 + 1 + 1); and

if φ and φ ⇒ ψ are true, then so is ψ.
If we choose a specific list Σ of true arithmetical sentences, called axioms, then a proof from Σ is a finite list of sentences, each one being either an axiom or a sentence derived from previous sentences on the list by a rule of inference. The last sentence on the list is what the proof proves. If a proof Σ is the list
σ_{1}, …, σ_{k},
so that Σ proves σ_{k}, then we define
⌜Σ⌝ = p_{1}^{⌜σ1⌝} × p_{2}^{⌜σ2⌝} × … × p_{k}^{⌜σk⌝}.
Our list of axioms may be infinite. Still we shall require the list to be recursive; again, this means there will be some clear rule for determining whether a given sentence is on the list. Equivalently, the set of Gödel numbers ⌜σ⌝ of sentences σ on the list should be recursive.
The notions of recursive set, formula, and proof are so bound up together that, for any counting number m, a recursive set of mtuples of counting numbers is precisely a subset R of N^{m} such that, for some formula φ(x_{1}, …, x_{m}), for all mtuples (a_{1}, …, a_{m}) in N^{m}, the following two conditions hold.

(a_{1}, …, a_{m}) belongs to R if and only if the sentence φ(a_{1}, …, a_{m}) is true.

Whichever of the sentences φ(a_{1}, …, a_{m}) and ¬φ(a_{1}, …, a_{m}) is true, it has a proof.
The first condition is that φ defines R. We need the second condition, because the set that a formula defines is not always recursive: this will be a consequence of Gödel’s Theorem.
In fortyfive steps, Gödel shows that there is a formula B(x, y) defining a recursive set, and for all counting numbers a and c, the sentence B(a, c) is true if and only if, for some proof Γ of some sentence σ, we have
a = ⌜Γ⌝,
c = ⌜σ⌝.
There is then another formula, Q(x, y), also defining a recursive set, and for all counting numbers a and b, the sentence Q(a, b) is true if and only if

b = ⌜φ(y)⌝ for some formula φ(y), and

the negation ¬B(a, ⌜φ(b)⌝) is true, so that a is not ⌜Γ⌝ for any proof Γ—if it even exists—of φ(b).
Now let p be the number ⌜∀x Q(x, y)⌝. Suppose, if possible, that there is a proof Γ of ∀x Q(x, p). Then

B(⌜Γ⌝, ⌜∀x Q(x, p)⌝) is true, by definition of B; therefore

¬Q(⌜Γ⌝, p) is true, by definition of Q and p.
Since Q, and therefore ¬Q, defines a recursive set, the true sentence ¬Q(⌜Γ⌝, p) has a proof. We can extend this to a proof of ¬∀x Q(x, p). Again, this is based on the assumption that there is a proof of ∀x Q(x, p) as well.
Thus, if ∀x Q(x, p) is provable, then so is its negation. Assuming our proofsystem is consistent, we can conclude that ∀x Q(x, p) has no proof. In particular, for each counting number n, ¬B(n, ⌜∀x Q(x, p)⌝) is true. This sentence is equivalent to Q(n, p), which therefore has a proof.
According to Gödel,
We can readily see that the proof just given is constructive; that is, the following has been proved in an intuitionistically unobjectionable manner.
The “following”—what we have proved—is that, if either of ∀x Q(x, p) and ¬∀x Q(x, p) has a proof, then from it we can obtain proofs of

the sentence ¬∀x Q(x, p) and,

for each counting number n, the sentence Q(n, p).
Not all of these sentences can be true in N. If the theorems of our proofsystem must be true in N, then neither ∀x Q(x, p) nor its negation is provable in the system.
If we are not worried about being “intuitionistically unobjectionable,” we may just observe that, if the sentence ∀x Q(x, p) is false, this means that the same sentence actually has a proof; thus, if our proofsystem is consistent, the given sentence must be true, while it has no proof.
We saw earlier the Recursion Theorem, whereby, if a is a counting number, and f is a function of counting numbers, then there is another such function, g, given uniquely by the requirements
g(1) = a,
∀x g(Sx) = f(g(x)),
where S is the function converting x to x + 1. Functions built up in this way, from constant functions and S, by repeated application of recursion in the sense above are by definition recursive (now they are called primitive recursive). If f is recursive, then the solution set of the equation f(x) = 1 is by definition recursive. There are clear procedures for

evaluating a recursive function at a particular number;

determining whether a particular number belongs to a recursive set.
We have seen that addition is recursive. We can understand the formula
x + y = z
to be an abbreviation of the formula
∃η (η(1) = Sx & ∀w η(Sw) = S(η(w)) & η(y) = z).
This is how formulas defining recursive sets are obtained. However, the example here is secondorder. We can simplify it to the formula
∃η (η(1) = Sx & ∀w (w < y → η(Sw) = S(η(w))) & η(y) = z).
That x + y = z means there are numbers u_{1}, …, u_{y} such that
u_{1} = Sx,
∀w (w < y → u_{w + 1} = S(u_{w})),
u_{y} = z.
By the Chinese Remainder Theorem, there are numbers b and d such that each u_{k} is the remainder of b after division by 1 + kd. This allows us to express x + y = z in a firstorder way. In return though, we need both addition and multiplication, in order to be able to do this. However, if we allow ourselves symbols for these operations, then we can define all other recursive functions and relations using firstorder formulas.
They will not be arbitrary firstorder formulas either, but their quantified variables will be bounded, as in
∃x (x < z & R(x, y)).
Conversely, the sets defined by such formulas are recursive.
Recursive functions and sets are now called primitive recursive, because as Gödel observed in lectures at the Institute for Advanced Study in Princeton in 1934, there are general recursive functions that are not recursive in the original sense (as Ackermann had shown in 1928).
There is a Second Incompleteness Theorem. The set of all Gödel numbers of sentences being recursive, there is a formula F defining it. Let τ be the sentence
∃y (F(y) & ∀x ¬B(x, y)),
with B as earlier. Then τ expresses the consistency of our proofsystem. Thus we have shown
τ ⇒ ∀x Q(x, p).
Our proof of this can be formalized within our proofsystem (though as Gödel admits, this point needs fleshing out). The proof of ∀x Q(x, p) cannot be formalized. Therefore a proof of τ cannot be formalized, if it is true. If consistent, our system cannot prove this.
Coda
The theory of (N, +, ×) has no recursive axiomatization; but again, the theories of some interesting structures do have. This is what makes interesting the mathematics that I do.
John Horgan’s interview of Tim Maudlin is called, again, “Philosophy Has Made Plenty of Progress.” According to Maudlin,
Overwhelmingly most philosophers are atheists or agnostics, which I take to be convergence to the truth.
According to Christopher Hitchens in God Is Not Great (2007),
Not all can be agreed on matters of aesthetics, but we secular humanists and atheists and agnostics do not wish to deprive humanity of its wonders or consolations. Not in the least. If you will devote a little time to studying the staggering photographs taken by the Hubble telescope, you will be scrutinizing things that are far more awesome and mysterious and beautiful—and more chaotic and overwhelming and forbidding—than any creation or “end of days” story …
Twenty years ago, in 1998, when I was a postdoc in California, a friend sent me prints of a couple of those Hubble photographs. I have them still. They are awesome and mysterious and so on, as Hitchens says; but I leave off the comparative “more.” More awesome to me is the power of the mind, in its ability to create myths; to take and interpret photographs; and especially to discover, prove, and make use of such results as Gödel’s Incompleteness Theorem.
What is now denoted by ⌜φ⌝ was originally ‹φ›, till on October 11, 2020, I learned that there were Quine corners at positions 231C and 231D in Unicode, among the “Miscellaneous Technical” symbols in the range 2300–23FF
One Comment
Great post. I feel like more technical developments in logic/theoretical computer science/set theory cause people forget about some foundational work such as Goedel’s. I wish all my students read this post.
12 Trackbacks
[…] « On Gödel’s Incompleteness Theorem […]
[…] We know from the work of Kurt Gödel in 1931 that the firstorder theory of the natural numbers with addition and multiplication is undecidable. (See “On Gödel’s Incompleteness Theorem.”) […]
[…] between Collingwood’s work and some of the mathematics of his time. A similar analogy with Gödel’s Incompleteness Theorem (1931) is possible as […]
[…] What shall we do? For Collingwood, the archbarbarists are the Ottoman Turks, when they are at the height of their power (45. 93); but even they “are no exception to the rule which elsewhere, to the best of my knowledge, is unbroken: the rule that barbarists in the end have always been beaten; a rule which I state here merely as the conclusion arrived at by the inductive study of cases” (45. 94). Such an induction is not a proof; to draw the universal conclusion that barbarism always fails, one would have to give a reason—as I suggested in the post “On Gödel’s Incompleteness Theorem.” […]
[…] unfitness of her associates and wooers …’ ” (535 C). In writing “On Gödel’s Incompleteness Theorem,” I expressed my dismay over the attitude (and attendant misunderstanding) of one […]
[…] Neither is experiment enough: if something happens n − 1 times, we still need a reason to conclude that it will happen an nth time. (I worked with this idea a bit in an essay “On Gödel’s Incompleteness Theorem.”) […]
[…] fantasy for mathematics, as Kaznatcheev reminds us. Versions of the fantasy have been shown, as by Gödel and Turing, to be not just impractical, but […]
[…] at issue. In any case, we were considering computer verification of a proof from given axioms. From Gödel, there are theorems about the natural numbers that do not follow from a previously identified list […]
[…] “On Gödel’s Incompleteness Theorem,” […]
[…] of proof that Haynes refers to is inductive, in one of the senses that I discussed in the post “On Gödel’s Incompleteness Theorem.” Haynes uses the term “incomplete induction” for such proofs, as when she says of the […]
[…] have already reviewed both of Gödel’s incompleteness theorems. I do it here now, somewhat differently: usually more […]
[…] written two long blog posts on Gödel, in 2018 and a month ago. They are about a lot of related stuff too, as is usual for my […]