15

Metalogic

Metalogic studies logical systems. It focuses on proving things about the systems themselves, not on testing concrete arguments. This chapter gives a brief introduction to metalogic.

15.1 Metalogical questions

Metalogic is the study of logical systems and tries to prove things about them. Recall our first two rules in §6.1 for forming propositional wffs:

1. Any capital letter is a wff.

2. The result of prefixing any wff with “∼” is a wff.

It follows from these that there’s no longest wff – since, if there were a longest wff, then we could make a longer one by adding another “∼.” This simple proof is about a logical system, so it’s part of metalogic.

Consider our system of propositional logic. Metalogic asks questions like: Do we need all five symbols (“∼,” “•,” “∨,” “⊃,” and “≡”)? Could we define some symbols in terms of others? Did we set up our proof system right? Are any of the inference rules defective? Can we prove self-contradictions or invalid arguments? Do we have enough inference rules to prove all valid propositional arguments? What other approaches could systematize propositional logic?

15.2 Symbols

We don’t need all five propositional symbols (“∼,” “•,” “∨,” “⊃,” and “≡”). We could symbolize and test the same arguments if we had just “∼” and “•”; then, instead of writing “(P ∨ Q),” we could write “∼(∼P • ∼Q)”:

· (P ∨ Q) = ∼(∼P • ∼Q)

· At least one is true = Not both are false

These are equivalent (true or false under the same conditions); truth tables can 0335 show this. Similarly, we can express “⊃” and “≡” using “∼” and “•”:

· (P ⊃ Q) = ∼(P • ∼Q)

· If P then Q = We don’t have P true and Q false

· (P ≡ Q) = (∼(P • ∼Q) • ∼(Q • ∼P))

· P if and only if Q = We don’t have P true and Q false, and we don’t have Q true and P false

Or we might translate the other symbols into “∼” and “∨”:

· (P • Q) = ∼(∼P ∨ ∼Q)

· (P ⊃ Q) = (∼P ∨ Q)

· (P ≡ Q) = (∼(P ∨ Q) ∨ ∼(∼P ∨ ∼Q))

Or we might use just “∼” and “⊃”:

· (P • Q) = ∼(P ⊃ ∼Q)

· (P ∨ Q) = (∼P ⊃ Q)

· (P ≡ Q) = ∼((P ⊃ Q) ⊃ ∼(Q ⊃ P))

It’s possible to get by using just “|” for NAND; “(P | Q)” means “not both P and Q.” We can define “∼P” as “(P | P)” and “(P • Q)” as “((P | Q) | (P | Q)).”

Systems with only one or two symbols are more elegantly simple but harder to use. But logicians are sometimes more interested in proving results about a system than in using it to test arguments; and it may be easier to prove these results if we use fewer symbols.

Another approach uses all five symbols but divides them into undefined (primitive) symbols and defined ones. We could take “∼” and either “•” or “∨” or “⊃” as undefined, and then define the others using these. We’d then view the defined symbols as abbreviations; whenever we liked, we could eliminate them and use only undefined symbols.

How do we know that our five symbols suffice to formulate wffs for every possible truth table? Suppose we have a truth table for two letters that comes out as below and we want to replace “??” with a wff that gives this table:

AB	??
0 0	0
0 1	1
1 0	1
1 1	0

How do we know that some wff gives this truth table? To construct a wff with this truth table, we can put an OR between the true cases (rows 2 and 3): A-is-false-and-B-is-true (row 2) OR A-is-true-and-B-is-false (row 3):

· ((∼A • B) ∨ (A • ∼B)) 0336

So we can, using just NOT, AND, and OR, mechanically construct a wff that expresses any specific truth table. (If the formula is always false, use a wff like “(A • ∼A),” which is always false.)

There are further options about notation. While we use capital letters for statements, some logicians use small letters (often just “p,” “q,” “r,” and “s”) or Greek letters. Some use “-” or “¬” for negation, “&” or “∧” for conjunction, “→” for conditional, or “↔” for equivalence. Various conventions are used for dropping parentheses. It’s easy to adapt to these differences.

Polish notation avoids parentheses and has shorter formulas. “K,” “A,” “C,” and “E” go in place of the left-hand parentheses for “•,” “∨,” “⊃,” and “≡”; and “N” is used for “∼.” Here are four examples:

· ∼(P • Q) = NKpq

· (∼P • Q) = KNpq

· ((P • Q) ⊃ R) = CKpqr

· (P • (Q ⊃ R)) = KpCqr

Some people can actually understand these formulas.

15.3 Soundness

The most important metalogical questions are about whether a proof system is sound (won’t prove bad things – so every argument provable in the system is valid) and complete (can prove every good thing – so every valid argument expressible in the system is provable in the system).

Could the following happen? A student named Logicus found a flaw in our proof system. Logicus did a formal proof of a propositional argument and then showed by a truth table that the argument was invalid; so some arguments provable using our proof system are invalid. People have found such flaws in proof systems. How do we know that our system is free from such flaws? How can we prove soundness?

Soundness: Any propositional argument for which we can give a formal proof is valid (on the truth-table test).

To show this, we could first show that all the propositional inference rules are truth preserving (when applied to true wffs, they yield only further true wffs). We have 13 inference rules: 6 S-rules, 6 I-rules, and RAA. It’s easy (but tedious) to use the truth-table method of §6.6 to show that S- and I-rules are truth preserving. All these rules pass the test (as you could check for yourself); when applied to true wffs, they yield only further true wffs.

RAA is more difficult to check. First we show that the first use of RAA in a proof is truth preserving. Suppose all previous not-blocked-off lines in a proof are true, and we use RAA to derive a further line; we have to show that this further line is true: 0337

From previous true lines plus assumption “∼A,” we derive contradictory wffs “B” and “∼B” using S- and I-rules. We just saw that S- and I-rules are truth preserving. So if the lines used to derive “B” and “∼B” were all true, then both “B” and “∼B” would have to be true, which is impossible. Hence the lines used to derive them can’t all be true. So if the lines before the assumption are all true, then assumption “∼A” has to be false. So its opposite (“A”) has to be true. So the first use of RAA in a proof is truth preserving.

We can similarly show that if the first use of RAA in a proof is truth preserving, then the second is too. And we can show that if the first n uses of RAA are truth preserving, then the n + 1 use is too. Then we can apply the principle of mathematical induction: “Suppose that something holds in the first case, and that, if it holds in the first n cases, then it holds in the n + 1 case; then it holds in all cases.” From this, it follows that all uses of RAA are truth preserving.

Now suppose an argument is provable in our propositional system. Then there’s some proof that derives the conclusion from the premises using truth-preserving rules. So if the premises are true, then the conclusion also must be true – and so the argument is valid. So if an argument is provable in our propositional system, then it’s valid. This establishes soundness.

Isn’t this reasoning circular? Aren’t we just assuming principles of propositional inference (like modus ponens) as we defend our propositional system? Of course we are. Nothing can be proved without assuming logical rules. We aren’t attempting the impossible task of proving things about a logical system without assuming any logical rules. Instead, we’re doing something more modest. We’re trying to show, relying on ordinary reasoning, that we didn’t make errors in setting up our system.

The consistency of our system is an easy corollary of its soundness. Let’s say that a wff is a theorem if it’s provable from zero premises. “(P ∨ ∼P)” is a theorem; we can prove it by assuming its opposite and deriving a contradiction:

By our soundness result, since “∴ (P ∨ ∼P)” is provable it must be valid on the truth-table test. So then it must be impossible for “(P ∨ ∼P)” to be false. So then “(P ∨ ∼P)” must have an all-1 truth table. And the more general result follows, 0338 that all theorems of our system must have all-1 truth tables.

A proof system is consistent provided that no two contradictory formulas are both theorems. We showed that all theorems of our system have all-1 truth tables. But no two contradictory formulas both have all-1 truth tables (since if a formula has all 1’s then its contradictory has all 0’s). So no two contradictory formulas are both theorems. So our propositional system is consistent.

15.4 Completeness

Our soundness proof shows that our propositional system won’t prove invalid arguments. You probably didn’t doubt this. But you may have had doubts about whether our system is strong enough to prove all valid propositional arguments. After all, the single-assumption method of doing proofs wasn’t strong enough; Section 7.3 uncovered valid arguments that require multiple assumptions. How do we know that our expanded method is enough? Maybe Logicus will find a further propositional argument that’s valid but not provable; then we’d have to strengthen our system still further. To calm these doubts, we’ll show that our propositional system is complete:

Completeness: Every valid propositional argument is provable.

Our completeness proof will show that if we correctly apply the proof strategy of §7.3 to a valid propositional argument then we get a proof. Our strategy has five steps: 1-START, 2-S&I, 3-RAA, 4-ASSUME, and 5-REFUTE. Assume that we correctly apply this strategy to a propositional argument. Then:

· We’ll end in the RAA step with all assumptions blocked off, or end in the REFUTE step, or keep going endlessly.

· If we end in the RAA step with all assumptions blocked off, then we’ll get a proof.

· If we end in the REFUTE step, then the argument is invalid.

· We won’t keep going endlessly.

· ∴ If the argument is valid, then we’ll get a proof.

· ((A ∨ F) ∨ E)

· (A ⊃ P)

· (F ⊃ ∼V)

· ∼E

· ∴ (V ⊃ P)

Premise 1 is true because our proof strategy has only two stopping points; so we’ll stop at one or the other or we won’t stop. Premise 2 is true because our proof strategy (especially the S&I and RAA steps) mirrors the §7.1 definition of “proof.” Now we have to argue for premises 3 and 4.

Premise 3 says “If we end in the REFUTE step, then the argument is invalid.” This is true because, when we reach the REFUTE step, all the complex wffs are dissolved into smaller parts and eventually into simple wffs, the larger forms are true if the smaller parts are true, and the simple wffs we end up with are consistent and thus give truth conditions making all the other wffs true – thus 0339 making the premises of the original argument true while its conclusion is false – thus showing that the original argument is invalid.

Here’s a chart (where α and β represent wffs) about how complex wff forms would dissolve into simpler wff forms:

∼∼α dissolves into α [S-rule]

(α • β) dissolves into α and β [S-rule]

∼(α • β) dissolves into ∼α or ∼β [I-rule or assumption]

(α ∨ β) dissolves into α or β [I-rule or assumption]

∼(α ∨ β) dissolves into ∼α and ∼β [S-rule]

(α ⊃ β) dissolves into ∼α or β [I-rule or assumption]

∼(α ⊃ β) dissolves into α and ∼β [S-rule]

(α ≡ β) dissolves into (α ⊃ β) and (β ⊃ α) [S-rule]

∼(α ≡ β) dissolves into (α ∨ β) and ∼(α • β) [S-rule]

The original formula is true if the parts it dissolves into are true.

The chart covers the nine complex wff forms possible in our system and the smaller parts that these complex wff forms will have dissolved into when we reach the REFUTE step. Forms that dissolve using an S-rule always dissolve into the same smaller parts. Other forms can dissolve in two ways. Consider “∼(A • B).” We might be able to use an I-rule on this to derive “∼A” or “∼B.” If not, then we can break “∼(A • B)” by assuming one part or its negation, which will (immediately or after using an I-rule) give us “∼A” or “∼B.” So when we reach the REFUTE step, all not-blocked-off complex wffs will be starred or broken,¹ and thus dissolved into the parts given above.

¹ A wff is broken if we already have one side or its negation but not what we need to conclude anything new (§7.3).

Each complex wff is true if the parts it dissolves into are true. We can check this by checking the nine cases in the box. So ∼∼α dissolves into α, and is true if α is true. (α • β) dissolves into α and β, and is true if both of these are true. Similarly, ∼(α • β) goes into ∼α or ∼β, and is true if either of these is true.

Our refutation is the set of all the simple not-blocked-off wffs and is consistent (or else we’d have applied RAA). This refutation gives truth conditions making all the other not-blocked-off wffs true too (since these other wffs dissolved into the simple parts that make up the refutation). So our refutation gives truth conditions making all the not-blocked-off lines true. But these lines include the premises and the denial of the conclusion (of the original argument). So our refutation gives truth conditions making the premises and the denial of the conclusion all true. So the argument is invalid. So if we correctly apply our strategy to a propositional argument and end in the REFUTE step, then the argument is invalid. This establishes premise 3.

Now we argue for premise 4: “We won’t keep going endlessly.” This is a concern, since the proof strategy for some systems can go into an endless loop (§9.5). 0340 That won’t happen in propositional logic, since here the complexity of the wffs that are neither starred nor blocked off nor broken keeps decreasing as we go on, and eventually, if we don’t get a proof, goes to zero, at which point we get a refutation. For the tedious details, study the next paragraph.

Let the complexity level of a wff be the number of instances of “•,” “∨,” “⊃,” and “∼∼” (double negation) that the wff would have if every wff in it of the form “(α ≡ β)” were replaced with “((α ⊃ β) • (β ⊃ α)).” So simple wffs “A” and “∼A” have complexity 0, “(P • Q),” “∼(P ∨ Q),” “∼(∼P ⊃ ∼Q),” and “∼∼P” have complexity 1, “((P • Q) ⊃ R)” has complexity 2, and “(P ≡ (Q ∨ R))” has complexity 5. The complexity level of a stage of a proof is the sum of the complexity levels of the lines to that point that aren’t either starred or blocked off or broken. When we START by assuming the conclusion’s opposite, the argument has a certain complexity level; the sample problem at the start of Chapter 7 has complexity 3. Each S&I step (for example, going from “(P ⊃ Q)” and “P” to “Q” – or from “(P ≡ Q)” to “(P ⊃ Q)” and “(Q ⊃ P)”) decreases the complexity level by at least one.² Any further ASSUME will immediately or in the next step (through an application of an I-rule) reduce the complexity level by at least one.¹ RAA is trickier. If we apply RAA on the initial assumption, then the proof is done and there’s no endless loop. If we apply RAA on a non-initial assumption, then the complexity level may temporarily increase (due to our having to erase multiple stars); but the overall effect is to decrease the complexity from what it was before we made the non-initial assumption in question.² So the complexity level keeps decreasing. Since the proof starts with a finite complexity level which keeps going down, then, if we don’t get a proof, then we’ll eventually end with a complexity level of 0 – which (if we can derive nothing further) will move us to the REFUTE step which ends the strategy. So we won’t get an endless loop.

² One rare occasions, an S&I step can reduce the complexity level by more than one. Suppose that we have “(A • B)” and “(B • A)” and simplify one of them into “A” and “B.” The conjunction we simplify is starred and the other one is broken, so the complexity level is reduced by two.

¹ Suppose we need to break “(A ⊃ B)” and so we assume “A”; then we can conclude “B” and star “(A ⊃ B),” which will reduce the complexity by one. Suppose that instead we assume “∼A”; then “(A ⊃ B)” is broken, which immediately reduces the complexity by one.

² Suppose we make an additional assumption to break a complex wff. For example, we assume “A” to break “(A ⊃ B).” If this assumption dies, we conclude “∼A” and then “(A ⊃ B)” is broken (which reduces the complexity level). If instead we assumed “∼A,” then when this assumption dies then we derive “A”; we then can use this with “(A ⊃ B)” to get “B” – and then star “(A ⊃ B)” (which reduces the complexity level). So when an additional assumption dies, then the complexity level is decreased from what it was before we made the assumption.

So if we correctly apply our strategy to a propositional argument and the argument is valid, then we’ll get a proof. This establishes completeness. So we’ve proved both soundness (every provable propositional argument is valid) and completeness (every valid propositional argument is provable) for our system. 0341

15.5 An axiomatic system

Our propositional system is an inferential system, since it uses mostly inference rules (these let us derive formulas from earlier formulas). It’s also possible to systematize propositional logic as an axiomatic system, which uses mostly axioms (formulas that can be put on any line, regardless of earlier lines). Both approaches can be equally powerful: anything provable with one is provable with the other. Axiomatic systems have a simpler structure while inferential systems are easier to use. Symbolic logic’s pioneers used axiomatic systems.

I’ll now sketch a version of an axiomatic system from Principia Mathematica.³ We’ll use our earlier definitions of “wff,” “premise,” and “derived line.” But now a proof is a vertical sequence of zero or more premises followed by one or more derived lines, where each derived line is an axiom or follows from earlier lines by the inference rule or the substitution of definitional equivalents. There are four axioms; these axioms, and the inference rule and definitions, hold regardless of which wffs uniformly replace “A,” “B,” and “C”:

³ Bertrand Russell and Alfred North Whitehead (Cambridge: Cambridge University Press, 1910).

· Axiom 1. ((A ∨ A) ⊃ A)

· Axiom 2. (A ⊃ (A ∨ B))

· Axiom 3. ((A ∨ B) ⊃ (B ∨ A))

· Axiom 4. ((A ⊃ B) ⊃ ((C ∨ A) ⊃ (C ∨ B)))

The system has one inference rule (modus ponens): “(A ⊃ B), A → B.” It takes “∨” and “∼” as undefined; it defines “⊃,” “•,” and “≡” as follows:

· Definition 1. (A ⊃ B) = (∼A ∨ B)

· Definition 2. (A • B) = ∼(∼A ∨ ∼B)

· Definition 3. (A ≡ B) = ((A ⊃ B) • (B ⊃ A))

The inferential proof of “(P ∨ ∼P)” in our system is trivially simple (§15.3). The axiomatic proof is difficult:

· 1 ∴ (((P ∨ P) ⊃ P) ⊃ ((∼P ∨ (P ∨ P)) ⊃ (∼P ∨ P))) {from axiom 4, substituting “(P ∨ P)” for “A,” “P” for “B,” and “∼P” for “C”}

· 2 ∴ ((P ∨ P) ⊃ P) {from axiom 1, substituting “P” for “A”}

· 3 ∴ ((∼P ∨ (P ∨ P)) ⊃ (∼P ∨ P)) {from 1 and 2}

· 4 ∴ (P ⊃ (P ∨ P)) {from axiom 2, substituting “P” for “A” and “P” for “B”}

· 5 ∴ (∼P ∨ (P ∨ P)) {from 4, substituting things equivalent by definition 1}

· 6 ∴ (∼P ∨ P) {from 3 and 5}

· 7 ∴ ((∼P ∨ P) ⊃ (P ∨ ∼P)) {from axiom 3, substituting “∼P” for “A” and “P” for “B”}

· 8 ∴ (P ∨ ∼P) {from 6 and 7} 0342

Since there’s no automatic strategy, creating such proofs requires guesswork and intuition. And we might work for hours trying to prove an argument that’s actually invalid. Axiomatic systems tend to be painful to use.

15.6 Gödel’s theorem

Now we’ll consider metalogic’s most surprising discovery: Gödel’s theorem.

Let’s define a formal system (or calculus) to be an artificial language with notational grammar rules and notational rules for determining validity, where these rules can be applied in a mechanical way to give a definite result about wffhood and validity in a finite amount of time. Many formal systems are inferential (our approach) or axiomatic.

Propositional logic can be put into a sound and complete formal system. Our inferential system does the job – as does the axiomatic system we just considered. In either, an argument is valid if and only if it’s provable.

You might think that arithmetic could similarly be put into a sound and complete system. If we succeeded, we’d have an inferential or axiomatic system that could prove any truth of arithmetic but no falsehood. Then a statement of arithmetic would be true if and only if it’s provable in the system.

But this is impossible. Gödel’s theorem shows that we can’t systematize arithmetic in this way. For any attempted formalization, one of two bad things will happen: some true statements of arithmetic won’t be provable (making the system incomplete), or some false statements of arithmetic will be provable (making the system unsound). Gödel’s theorem shows that any formal system of arithmetic will be incomplete or unsound.

You may find Gödel’s theorem hard to believe. Arithmetic seems to be an area where everything can be proved one way or the other. But Kurt Gödel in 1931 showed that this was wrong. The reasoning behind his theorem is difficult; here I’ll just try to give a glimpse of what it’s about.¹

¹ My little Gödel’s Theorem Simplified (Langham, Md.: University Press of America, 1984) tries to explain the theorem. Refer to this book for further information.

What is this “arithmetic” that we can’t systematize? “Arithmetic” here is roughly like high-school algebra, but limited to positive whole numbers. It includes truths like these three:

· 2 + 2 = 4

· If x + y = z, then y + x = z.

· If xy = 18 and x = 2y, then x = 6 and y = 3.

More precisely, arithmetic is the set of truths and falsehoods that can be expressed using symbols for the vocabulary items in these boxes: 0343

Mathematical vocabulary

positive numbers: 1, 2, …

plus, times, to the power of

parentheses, equals

Logical vocabulary

not, and, or, if-then

variables (x, y, …), all, some

parentheses, equals

Gödel’s theorem claims that no formal system with symbols for all the items in these two boxes can be both sound and complete.

The notions in our mathematical box can be reduced to a sound and complete formal system; we’ll call it the “number calculus.” And the notions in our logical box can be reduced to a sound and complete formal system: our quantificational system. But combining these two systems produces a monster that can’t be put into a sound and complete formal system.

We’ll now construct a number calculus (NC) that uses seven symbols:

· / + • ^ ( ) =

“/” means “one” (“1”). We’ll write 2 as “//” (“one one”), 3 as “///” (“one one one”), and so on. “+” is for “plus,” “•” for “times,” and “^” for “to the power of.” Our seven symbols express all the notions in our mathematical box.

Meaningful sequences of NC symbols are numerals, terms, and wffs:

1. Any string consisting of one or more instances of “/” is a numeral.

2. Every numeral is a term.

3. The result of joining any two terms by “+,” “•,” or “^” and enclosing the result in parentheses is a term.

4. The result of joining any two terms by “=a” is a wff.

Here are examples (with equivalents):

· 2, 4 (numerals): // ////

· 2, 2 • 2, (1 + 1)² (terms): // (// • //) ((/ + /) ^ //)

· 4 = 4, 2 + 2 = 4 (wffs): //// = //// (// + //) = ////

Our NC can prove the true wffs. NC uses one axiom and six inference rules; here’s our axiom (in which any numeral can replace “a”):

Axiom: a = a

Any instance of this (any self-identity using the same numeral on both sides) is an axiom: “/=/,” “//=//,” “///=///,” and so on.

Our inference rules let us substitute one string of symbols for another. We’ll use “↔” to say that we can substitute the symbols on either side for those on the other side. We have two rules for “plus” (where “a” and “b” in our inference 0344 rules stand for any numerals):

· R1. (a+/) ↔ a/

· R2. (a+/b) ↔ (a/+b)

R1 lets us interchange “(///+/)” and “////.” R2 lets us interchange “(//+//)” and “(///+/)” – moving the “+” one “/” to the right. We’ll see R3 to R6 in a moment.

An NC proof is a vertical sequence of wffs, each of which is either an axiom or else follows from earlier members by one of the inference rules R1 to R6. A theorem is any wff of a proof.

Using our axiom and inference rules R1 and R2, we can prove any true wff of NC that doesn’t use “•” or “^.” Here’s a proof of “(//+//)=////” [“2 + 2 = 4”]:

1. ////=//// {from the axiom}

2. (///+/)=//// {from 1 using R1}

3. (//+//)=//// {from 2 using R2}

We start with a self-identity. We get line 2 by substituting “(///+/)” for “////” (as permitted by rule R1). We get line 3 by further substituting “(//+//)” for “(///+/)” (as permitted by rule R2). So “(//+//)=////” is a theorem.

Here are our rules for “times” and “to the power of”:

· R3. (a • /) ↔ a

· R4. (a • /b) ↔ ((a • b) + a)

· R5. (a ^ /) ↔ a

· R6. (a ^ /b) ↔ ((a ^ b) • a)

Our NC is sound and complete; any wff of NC is true if and only if it’s provable in NC. This is easy to show, but we won’t do the proof here.

Suppose we take our number calculus, add the symbols and inference rules of our quantificational logic, add a few more axioms and inference rules, and call the result the “arithmetic calculus” (AC). We could then symbolize any statement of arithmetic in AC. So we could symbolize these:

· If x + y = z, then y + x = z.

· ((x+y)=z ⊃ (y+x)=z)

· If xy = 8 and x = 2y, then x = 4 and y = 2.

· (((x•y)=//////// • x=(//•y)) ⊃ (x=//// • y=//))

· x is even.

· For some number y, x = 2 times y.

· (∃y)x=(// • y)

· x is prime.

· For every number y and z, if x = y times z, then y = 1 or z = 1.

· (y)(z)(x=(y • z) ⊃ (y=/ ∨ z=/)) 0345

Here’s Goldbach’s conjecture (which is still neither proved nor disproved):

· Every even number is the sum of two primes.

· (x)((∃y)x=(2 • y) ⊃ (∃x’)(∃x’’)(x=(x’+x’’) • ((y)(z)(x’=(y • z) ⊃ (y=/ ∨ z=/)) • (y)(z)(x’’=(y • z) ⊃ (y=/ ∨ z=/)))))

Gödel’s theorem shows that any such arithmetic calculus has a fatal flaw: either it can’t prove some arithmetic truths or it can prove some arithmetic falsehoods. This flaw comes not from an accidental defect in our choice of axioms and rules, but from the fact that any such system can encode messages about itself.

To show how this works, it’s helpful to use a version of AC with minimal vocabulary. The version that we’ve sketched so far uses these symbols:

· / + • ^ ( ) = ∼ ∨ ⊃ ∃ x, y, z, x’, …

We’ll now economize. Instead of writing “^” (“to the power of”), we’ll write “••.” We’ll drop “∨” and “⊃,” and express the same ideas using “∼” and “•” (§15.2). We’ll use “n,” “nn,” “nnn,” “nnnn,” … for our variables (instead of “x,” “y,” “z,” “x’,” …). We’ll drop “∃,” and write “∼(n)∼” instead of “(∃n).” Our minimal-vocabulary version of AC uses only eight symbols:

· / + • ( ) = ∼ n

Any statement of arithmetic can be symbolized by combining these symbols.

Our strategy for proving Gödel’s theorem goes as follows. First we give ID numbers to AC formulas. Then we see how AC formulas can encode messages about other AC formulas. Then we construct a special formula, called the Gödel formula G, that encodes this message about itself: “G isn’t provable.” G asserts its own unprovability; this is the key to Gödel’s theorem.

It’s easy to give ID numbers to AC formulas. Let’s assign to each of the eight symbols a digit (an ID number) from 1 to 8:

Thus “/” has ID # 1 and “+” has ID # 2. To get the ID number for a formula, we replace each symbol by its one-digit ID number. So we replace “/” by “1,” “+” by “2,” and so on. Here are two examples:

/=/

161

(//+//)

4112115

The ID numbers follow patterns. For example, each numeral has an ID number consisting of all 1’s: 0346

/	//	///	////
1	11	111	1111

So we can say:

· Formula # n is a numeral if and only if n consists of all 1’s.

We can express the right side as the equation “(nine-times-n plus one) equals some power of ten,” or “(∃x)9n+1=10^x,” which can be symbolized in an AC formula.¹ This AC formula is true of any number n if and only if formula # n is a numeral. This is how system AC encodes messages about itself.

¹ The AC formula for this equation is “∼(nn)∼(((///////// • n) + /) = (////////// •• nn)).” This formula has ID # 748857444111111111385215641111111111338855. It’s important that our right-hand bold formulas can be symbolized in AC formulas with definite ID numbers. It’s not important that we write out the formulas or their ID numbers.

An AC theorem is any formula provable in AC. The ID numbers for theorems follow definite but complex patterns. It’s possible to find an equation that’s true of any number n if and only if formula # n is a theorem. If we let “n is …” represent this equation, we can say:

· Formula # n is a theorem if and only if n is ….

The equation on the right side would be very complicated.

To make things more intuitive, let’s pretend that all and only theorems have odd ID numbers. Then “n is odd” encodes “Formula # n is a theorem”:

· Formula # n is a theorem if and only if n is odd.

For example, “161 is odd” encodes the message that formula # 161 (which is “/=/”) is a theorem:

· Formula # 161 is a theorem if and only if 161 is odd.

Then “n is even” would encode the message that formula # n is a non-theorem:

· Formula # n is a non-theorem if and only if n is even.

Imagine that “485…” is some specific very large number. Let “485… is even” represent the AC formula that says that 485… is even:

· 485… is even.

This formula would encode the following message:

· Formula # 485… is a non-theorem. 0347

So the AC formula is true if and only if formula # 485… is a non-theorem. Now suppose this formula itself happens to have ID number 485…. Then the formula would talk about itself, declaring that it itself is a non-theorem. This is what the Gödel formula G does. G, with a certain ID number, encodes the message that the formula with this ID number is a non-theorem. G in effect says this:

· G G is not a theorem.

So G encodes the message “G is not a theorem.” But this means that G is true if and only if it’s not a theorem.

So G is true if and only if it’s not provable. Now G, as a formula of arithmetic, is either true or false. Is G true? Then it’s not provable – and our system contains unprovable truths. Or maybe G is false? Then it’s provable – and our system contains provable falsehoods. In either case, system AC is flawed.

We can’t remove the flaw by adding further axioms or inference rules. No matter what we add to the arithmetic calculus, we can use Gödel’s technique to find a formula of the system that’s true-but-unprovable or false-but-provable. Hence arithmetic can’t be reduced to any sound and complete formal system.

This completes our sketch of the reasoning behind Gödel’s proof. To fill in the details would require answering two further questions:

· Consider the equation that’s true of any number n if and only if formula # n is a theorem. This equation would have to be much more complicated than “n is odd.” How can we produce this equation?

· If we have this equation, how do we then produce a formula with a given number that says that the formula with that number is a non-theorem?

The answers to these questions are too complicated to go into here. While the details can be worked out, we won’t here worry about how to do this.¹

Most people find the last two chapters surprising. We tend to think that everything can be proved in math, and that nothing can be proved in ethics. But Gödel’s theorem shows that not everything can be proved in math. And our golden-rule formalization shows that some important ideas (like the golden rule) can be proved in ethics. Logic can surprise us.

¹ My Gödel’s Theorem Simplified (Langham, Md.: University Press of America, 1984) has details.