I. On Fri Oct 5 23:35:03 EDT 2007 Finnur Larusson wrote
http://www.cs.nyu.edu/pipermail/fom/2007-October/012009.html
I confirm that Larusson "proof" under corrections can be formalized in ZFC.
II. On Sun Oct 7 14:12:37 EDT 2007 Timothy Y. Chow wrote:
http://www.cs.nyu.edu/pipermail/fom/2007-October/012015.html
"In order to deduce "ZFC is inconsistent" from "ZFC |- ~con(ZFC)" one needs
something more than the consistency of ZFC, e.g., that ZFC has an
omega-model (i.e., a model in which the integers are the standard
integers).
To put it another way, why should we "believe" a statement just because
there's a ZFC-proof of it? It's clear that if ZFC is inconsistent, then
we *won't* "believe" ZFC-proofs. What's slightly more subtle is that the
mere consistency of ZFC isn't quite enough to get us to believe
arithmetical theorems of ZFC; we must also believe that these arithmetical
theorems are asserting something about the standard naturals. It is
"conceivable" that ZFC might be consistent but that the only models it has
are those in which the integers are nonstandard, in which case we might
not "believe" an arithmetical statement such as "ZFC is inconsistent" even
if there is a ZFC-proof of it.
So you need to replace your initial statement that "we assume throughout
that ZFC is consistent" to "we assume throughout that ZFC has an
omega-model"; then you should see that your "paradox" dissipates.".
J.Foukzon.Remark1. Let Mst be an omega-model of ZFC and let ZFC[Mst] be a ZFC with a quantifiers bounded on model Mst. Then easy to see that Larusson "paradox" valid inside ZFC[Mst]
III. On Wed Oct 10 14:12:46 EDT 2007 Richard Heck wrote:
http://www.cs.nyu.edu/pipermail/fom/2007-October/012035.html
Or, more directly, what you need is reflection for ZFC: Bew_{ZFC}(A) -->
A. And that of course is not available in ZFC, by L"ob's theorem.
J.Foukzon.Remark2 However such reflection is .available in ZFC[Mst] by standard interpretation of Bew_{ZFC}(A) in omega-model Mst