[FOM] Formalization Thesis

[Timothy Y. Chow]

Andrew Boucher wrote, in response to Shipman's request for an explicit 
counterexample to the Formalization Thesis:

> "2+2 = 4"
> 
> I'd prefer to have left my answer at that, but a bit of explanation.   
> The challenge seems to me:  provide a sentence and let's see what  
> people belonging to the FOM discussion forum say, with the majority  
> deciding the "winner".

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.

Tim