greatly enjoyed the talk and the jokes. BTW, 1 is not a prime number (….. okay, now you can stop banging your head against the wall :D) ]]>

Lots of you will enjoy this: http://blogs.msdn.com/b/ericlippert/archive/2011/02/14/what-would-feynman-do.aspx

]]>*But the fact that Â¬Con(ZF) is false only means that the theory is lying, not that it is inconsistent.*

Exactly. Consistency doesn’t imply *soundness*, which is a stronger property.

*But Iâ€™m still uncomfortable with your statement. Wasnâ€™t that a Holy Grail of mathematical logic? A finitary (albeit very large) statement that is actually independent of ZF(C)?*

Well, the Gödel sentences have always provided examples of “finitary statements” that are independent of ZFC. But many mathematicians consider those “unnatural,” since in “everyday” math we don’t typically ask metaquestions about the consistency of the theory we’re working in. So it’s an interesting challenge to find a finitary statement that *arose independently from* logic, computability theory, etc., which can nevertheless be proven independent of ZFC.

(We do have such examples for Peano Arithmetic, and we also have *nonfinitary* statements like the Continuum Hypothesis that are independent of ZFC.)

Now, I do *not* regard the values of BB(n) for large n as answering this challenge, for two reasons:

(1) The values of BB(n) in question can’t even be written down inside the observable universe! So evaluating them isn’t a “math problem” in the ordinary sense of something that a human (or at least computer) could feasibly check the answer to.

(2) The values of BB(n) are *not* something that mathematicians would think to study outside of logic / computability theory — which might be related to the facts that BB is uncomputable, and that BB(n) for large enough n encodes Con(ZFC)! ðŸ™‚

Specifically, when you said that Con(ZF) implies Con(ZF + Â¬Con(ZF)), and thus that ZF+Â¬Con(ZF) can not be trapped in an inconsistency, I thought that you had produced an example of an inconsistent theory without a finite proof of it.

But the fact that Â¬Con(ZF) is false only means that the theory is lying, not that it is inconsistent. Is this it?

(Luke: at first I did not have in mind consistent but untrue, but now I think that’s the case)

But I’m still uncomfortable with your statement. Wasn’t that a Holy Grail of mathematical logic? A finitary (albeit very large) statement that is actually independent of ZF(C)? After all, until now there were only examples of problems that involved silly infinities, and those can be regarded as a curiosity at best.

Or that would just mean that the provability of BB(137) is equivalent to consistency, and thus not being bona fide independence?

]]>I think your conception of what’s “elegant” and “simple” is being obscured by the ineffective usage of language in the theorems and definitions. I note that you have no problem with the “positive” requirement in Theorem 1 of Hardy & Wright, but find “except 1” ugly. But if you consider that “positive” is the same as “natural, except 0”, then adding an “except 1” doesn’t seem too ugly anymore.

Following that line of reasoning, one could create a name for “natural, except 0 or 1”, say, “nezo” (Natural Except Zero or One). Then the definition of prime would not be seem too ugly anymore: “A number is prime if it has exactly one nezo divisor (itself)”. Theorem 1 of Hardy & Wright would be similarly simplified: “Every nezo is a product of one or more primes”.

If the idea of creating a new name for “natural, except 0 or 1” seems contrived, consider this: 0 and 1 they aren’t interesting when thinking about divisibility, because you can’t divide any number by 0, and you can divide _any_ number by 1. So, it seems likely that people have this “nezo” concept while thinking about divisibility and primes, even if they don’t explicitly name it. Maybe the failure to name it explicitly is what makes the definitions and theorems seem ugly, even though they contain beautiful and simple concepts.

]]>“An integer is prime iff it has exactly two positive divisors”

and Theorem 1 of Hardy & Wright stated as

“Every positive integer is a product of zero or more primes” ? ]]>

Scott, you may want to be specific about what you mean by “proof” of a TM whose non-halting is equivalent to Con(ZFC). In systems stronger than ZFC, we know ZFC is consistent, so any TM that doesn’t terminate satisfies your challenge! I assume you probably want to work over Peano Arithmetic or a even weaker system ðŸ™‚

Maxwell Daemon, as Scott says, if a system is inconsistent than there is a finite proof demonstrating this. I think what you’re thinking is that it’s possible for a system to be consistent but *untrue*. (By which I mean technically, omega-inconsistent or arithmetically unsound.) For example, it’s possible to have a consistent system that for all X proves “P(X)”, but also proves “there exists X such that not(P(X))” (note the quotes separating the meta-math from the statement in the system).

]]>Thanks for the direct pointer!

]]>