[FOM] Formalization Thesis
Andrew Boucher
Helene.Boucher at wanadoo.fr
Fri Jan 11 21:55:20 EST 2008
On Jan 11, 2008, at 3:51 AM, Timothy Y. Chow wrote:
> Andrew Boucher wrote, in response to Shipman's request for an explicit
> counterexample to the Formalization Thesis:
>
> O.K., let me see if I understand you correctly. We ask someone who is
> familiar with Mizar to express "2+2 = 4" in a form that Mizar
> understands,
> create a proof of that statement that Mizar verifies, and then poll
> FOM
> readers with the question, "Did Mizar just verify that 2+2 = 4, or
> did it
> instead verify some statement that is different enough from "2+2 =
> 4" that
> we cannot regard Mizar's computation as a formal verification that 2
> +2 =
> 4?" And your prediction is that most FOMers (or mathematicians) would
> vote that Mizar did not, in fact, verify that 2+2 = 4. Is that an
> accurate restatement of your claim?
>
> If so, then this seems to me to be a surprising claim, because it
> seems to
> be a fundamental rejection of the whole concept of Mizar (and
> automated
> proof-checking in general). I would not expect most FOMers (or
> mathematicians) to adopt such a radically skeptical position.
>
Here is your first expression of the Formalization Thesis:
"Every theorem of ordinary mathematics is faithfully expressed by a
formal theorem of ZFC."
Here is Shipman's challenge:
> I repeat my earlier challenge: can anyone who disputes Chow's
> Formalization Thesis respond with a SPECIFIC MATHEMATICAL STATEMENT
> which they are willing to claim is not, despite its expressiblity in
> English text on the FOM discussion forum, "faithfully
> representable" or "adequately expressible" as a sentence in the
formal system ZFC?
Notice in both cases the use of "ZFC."
I proposed "2 + 2 = 4" as a counterexample.
As I said, I distinguished three categories of people: FOMers,
working mathematicians, and the proverbial man-on-the-street. I
made no prediction about FOMers. I would expect to have an even
chance that working mathematicians would agree that it is a
counterexample. I think hands-down the man-on-the-street would
agree it is a counterexample.
Somehow you are now jumping to conclusions about skepticism about
automated proof-checking in general, which I would certainly not hold
concerning "2 + 2 = 4".
In ZFC one method of defining the natural numbers would be: 0 as {},
1 as {{}}, 2 as {{},{{}}}, 3 as {{},{{}},{{},{{}}}}, and 4 as {{},
{{}},{{},{{}}},{{},{{}},{{},{{}}}}}. Abbreviate xx for a definition
in ZFC of addition, and you then have the assertion that "{{},{{}}}
xx {{},{{}}} = {{},{{}},{{},{{}}},{{},{{}},{{},{{}}}}}" is a faithful
expression of "2 + 2 = 4".
Since posting it has occurred to me that an even better example would
be the Pythagorean Theorem, "better" in the sense that I would expect
a better than even chance that working mathematicians would agree
that it is a counterexample.
I should emphasize that I am making a prediction about a poll.
People are asked the question: Is xxx a faithful expression of yyy?
There are answers and one tabulates the results. This, as I
understand it, is the idea behind Shipman's challenge, so that one
does not have to argue about what constitutes a "faithful expression".
More information about the FOM
mailing list