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.