[FOM] Formalization Thesis

[Andrew Boucher]

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".