[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Thu Jan 10 21:51:33 EST 2008
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.
More information about the FOM