I was surprised and delighted to discover that Robert Solovay, a logician whom I admire, reads my diary. He's picked up an important issue with my post promoting Proofs and Types, namely that consistency as defined by Goedel, the inability to prove 0=1 is too weak a notion; 1-consistency is the right notion. I have more to say about this, which I will post in a future diary entry.
Robert also made an interesting comment on a post from two months ago on Bram's Minefield game. I said then that:
In Bram's 6th August entry Bram introduces a `game' played over ZFC: even in the simplified case of large cardinal axioms (LCAs), there may be no fact of the matter of which is stronger: if you look at the diagram of important LCAs in Kanamori's "The Higher Infinite", they form a partial order, not a linear order (I don't know whether this reflects known independence results or just ignorance). I do think as a kind of thought experiment, your exercise is illuminating; I like to think about how different mathematical pholosophy might be if results came to known in different order, might we regard a much weaker or stronger set theory as the default?
Robert replied that:
I don't have Kanamori's table in front of me. But the general consensus is that LCA's are linearly ordered by consistency strength in the following sense:If A and B are LCA's then either 1) PA proves "Con(ZFC + A) iff Con(ZFC + B)" or 2) ZFC + A proves Con (ZFC + B) or 3) ZFC + B proves Con(ZFC + A).
Some comments:
- There are two "base theories" in Robert's remark. The first is Peano Arithmetic (PA), which can be replaced by any theory that is strong enough to `talk' about consistency. Primitive Recursive Arithmetic (PRA) is a good theory, weaker than PA, interesting especially because it is logic-free: it consists solely of equations between arithmetic expressions. There are weaker theories than PRA, and interesting theories of arithmetic that are too weak, for example Robinson's theory Q, sometimes called Robinson Arithmetic.
- The second is Zermelo-Fraenkel set theory (with choice). We can reasonably omit the axiom of infinity from our base theory, getting a well-studied finitary system. We could instead omit the power set axiom, in which we would get a system rather like Z_2 (second-order arithmetic). In each case we can play Bram's game over the new base theory. Question: for the first alternate base theory, obviously the game is almost the same; is this so for the second (ie. without the power set axiom)>
- If the consensus is true, then one can image that what much of the set-theoretic community is doing is exactly playing Bram's game. My guess is, for what little it is worth, that if we make reasonably restrictions about the form that LCAs can take, then the consensus view is false.
- It seems appropriate to report a recent (two years old) breakthrough in the theory of Goedelian incompleteness. I talked above about base theories that talk about completeness. Most theories fall into one of two categories: either they are too weak to talk about consistency, or they prove that they cannot prove their own consistency. A natural question arises: are there theories strong enough to talk about consistency that are weak enough to prove their own consistency? Most people who understand the question would say no; it turns out that in fact there are such theories, as proven by Dan Willard.
Explanations and mechanical
proofs
There is an interesting discussion on the FOM list regarding
what is an explanatory proof. Harvey Friedman connects this
to proof assistants in a shocked message.
Update
Robert Solovay points out another error in the above...