The occasional commenter who goes by the name Coupon Clipper has emailed me some interesting questions about Godel’s Theorem. I think I’ll answer them here.
The first question is about first-order versus second-order logic, so let me explain the distinction. When we reason formally about arithmetic, we need to clearly specify the ground rules. This means, among other things, specifying the language and grammar we’re allowed to use. A very simple language might allow us to say things like “2 + 3 = 5” or “8 is an even number”. With a language like that, you could talk about a lot of sixth grade arithmetic, but you wouldn’t be able to say anything very interesting beyond that. To talk about the questions mathematicians care about, you need a language that contains words like “every”, as in Every number can be factored into primes or Every number can be written as a sum of four squares or Every choice of positiive numbers x, y, and z will yield a non-solution to the equation x3+y3=z3 . That language is called first-order logic.
With first order logic we can specify a set of axioms, and then follow a prescribed set of rules to deduce consequences. For example, if you’ve already established that every number is a sum of four squares, then you’re allowed to conclude that 1,245,783 is a sum of four squares. (The general rule is that if you’ve proved that every number has some particular property, then you’re allowed to conclude that any particular number has that property.)
Second order logic expands the language we’re allowed to use, by allowing us to apply words like “Every” not just to numbers, but to sets of numbers. So in second order logic, we can say things like “Every set of numbers has a smallest element”. In first-order logic, that sentence would be ungrammatical and hence meaningless.
Now: Godel’s Theorem, as it’s sometimes stated, says that no first order logical system can prove all the truths of arithmetic. Start with any true axioms you want, and there will always be other true things you can’t prove—not just because you’re not smart enough but because there really are no proofs within your system.
Coupon Clipper’s first question is (I am paraphrasing, accurately I hope): So what? Why not just use second order logic instead? He also guesses accurately at the answer, which is that Godel’s Theorem applies just as well to second order logic as it does to first order logic. There will still be some true statements in arithmetic that your system can’t prove.
That answers the question, but it raises another question: Why do mathematicians prefer to avoid second order logic?
Second order logic certainly has its advantages, and here’s the big one: It let’s us nail down what we’re talking about. What we’re talking about, of course, are the natural numbers: 0,1,2,3, and the rest. And nothing more! We don’t want our system to contain numbers that are infinitely big or infinitely small or exotic in other ways. First order logic can’t rule that stuff out. Second order logic can.
In other words, in any system of first order logic, all the theorems you can prove are true statements about the natural numbers, but there will always be other more exotic systems of “numbers” of which your theorems are also true. That means there is no way, within the language, to distinguish between the honest-to-god natural numbers and some of these other systems. There is no grammatical way to say “No, no, I mean the *true* natural numbers, not those impostors!”
With second order logic, that problem goes away. The theorems you can prove are true statements about the natural numbers, and they’re not true statements about anything else. There’s no ambiguity about what you’re describing.
But the offsetting disadvantage is huge: In first order logic, I can tell you what all the rules are. (Remember, for example, the rule that says that if you’ve established that every number has some property, you’re allowed to conclude that any particular number has that property.) In second order logic, I can’t. Neither can anybody. Neither can any computer. It is a theorem that no computer program can generate all the valid rules of inference in second order logic. That’s in some sense a much bigger deal than Godel’s theorem. Godel’s theorem says that (in either first or second order logic) no computer can follow the rules and discover all the true statements of arithmetic. But now I’m telling you that in second order logic, no computer can even figure out what the rules are!
Hence the oft-repeated slogan that “second order logic is not logic”, and hence our reluctance to rely on it.
Coupon Clipper’s second question is “Does any of this matter for the actual practice of mathematics?”. That’s a much easier question with a much shorter answer, but I think I’ll save it for tomorrow.
Yikes! Can I at least use a computer program to *check* my proofs that use SOL? It’s a pretty big deal if I can’t trust any theorem about connected graphs! (You can’t even say that a graph is connected in FOL.)
I suspect I am one of the few commentators here who actually studied mathematical logic as a grad student. Steven’s summary here is very good.
There is a very nice application of these ideas in non-standard analysis. This is doing calculus with infinitesimals rahter than limits. This is what engineers often do informally. The ‘normal’ use of them producers contradictions but you can construct a language in which you can use infinitesimals but are physically unable to express the statements that lead to contradictions. This, with a bit of talk of isomorphisms and the usual mathematical jargon/trickery makes it possible to do calculus with ‘infinitely small’ numbers. It makes most proofs easier. ANd here is the definition of a continuous function (for those who know epsilon-delta): a function is continuous if two numbers that start infinitely close together end up infinitiely close together — much simpler.
Great post, if possible could you talk about the significance of the statement in first order logic that translates to, for any x, Px or ~Px. From what I remember it is derivable from zero premises.
Coupon Clipper: Any formal proof is checkable by a computer; this is (essentially) part of the definition of formal proof.
Aha, thank you. I can check a SOL proof, so there’s a finite procedure for determining if a rule is correct, but I can’t tell you in advance every rule. Is that right? If so, I’m really not bothered by SOL. :)
Great post and great blog in general. One question: does Godel’s Theorem apply only to the impossibility of discovering all the true statements of arithmetic, or does it apply more broadly, i.e., to discovering all the true statements that can be expressed in a consistent axiomatic system (not just ones about arithmetic)?
I vaguely (and likely incorrectly) remember that a necessary condition for Godel’s Theorem to apply is that such a system contain certain (first order?) rules of arithmetic, but that as long as this condition is met, Godel’s Theorem applies more broadly to any true statements expressible in that system, not just ones that are related to arithmetic.
Coupon Clipper:
Is that right?
Yes.
Bah, Bob laugh at your puny proofs! Paul Krugman eat seventeenth-order logic for breakfast, and crap nobel prizes!
You clearly have a diverse level of intelligence in your audience.
I don’t get this.
Please post some more videos of you waving colourful balls around.
I spent most of the last thread avoiding the obvious risque humor, and I won’t let Dave tempt me into it with his last sentence.
All hail my self-control!
Sigh. Feel free not to hail my mad HTML coding skills.
Ken B: did you know that there are applications of non-standard analysis to economics?
Manfred: Wanna tell us about it? I’ve heard of non-standard analysis being used for teaching calculus, but never for econ. I’m curious.
Coupon Clipper: I’ve added this to my list of things to blog about soon.
Suppose you have a set of axioms defined, and you encounter a “truth” that you cannot proove with these axioms.
Would it make sense to change your axioms, so that your “truth” can be proven with those new axioms ?
I wonder if :
1. Is it possible to have a same “thruth” that can be encountered with different sets of axioms ?
2. If so, and if you can proove it with one set of axioms, does this also imply that this “truth” will also be true in the space whith the first set of axioms , although you cannot prove that truth with the axioms of your first space ?
in other words : Could you get around Godels law by changing the axioms in order to proove a “truth” ?
Blue-Coat: You can add any true statement you like to your set of axioms, but there will still be (other) true statements that cannot be derived from your axioms.
Coupon_Clipper: I am not sure you will see this reply, but I will try anyway.
There are applications of Non-Standard Analysis to Economics, especially dealing with economies with an infinite number of agents. Robert Aumann has a classic paper on a proof of equilibrium with a continuum of agents (Econometrica 1963 or so). Now, this paper uses “usual” techniques. There are people who translated this paper into “non-standard” techniques. For example, there is a book by Salim Rashid [http://www.amazon.com/Economies-Many-Agents-Approach-Non-Standard/dp/0801833795/ref=sr_1_4?s=books&ie=UTF8&qid=1280330664&sr=1-4 ] on how to apply non-standard techniques to economics. Another author is Robert Anderson at UC Berkeley; he has championed non-standard analysis in Economics, and he has a draft on his webpage for an intro on the subject [http://www.econ.berkeley.edu/~anderson/Book.pdf].
Hope this helps.
Manfred
Coupon_Clipper: one more thing, there is a paper by Salim Rashid in the Journal of Mathematical Economics 1979:
Rashid, Salim (1979), “The Relationship Between
Measure-Theoretic and Non-standard Exchange
Economies”, Journal of Mathematical Economics 6:195-
202.