[FOM] Formalization Thesis

[rgheck]

Timothy Y. Chow wrote:
> Formalization Thesis, "Mizar version": The correctness of anybody's claim 
> to have proven such-and-such a theorem of ordinary mathematics can be 
> checked by Mizar.
>
> I haven't actually gotten my hands dirty working with Mizar myself, but as 
> I understand it, it's based on ZFC.  Even if I'm mistaken on this point, 
> let's assume it for the sake of argument.
>
> So how do I defend the Mizar version against the counterexamples involving 
> theorems that go beyond ZFC?  My response is that if there's some theorem 
> T that requires an additional axiom A beyond ZFC, then it's true that 
> Mizar can't check it "directly," but Mizar *can* check "if A then T."  So 
> for example Mizar can't check that the continuum hypothesis is independent 
> of ZFC, but it *can* check that if ZFC is consistent then CH is 
> independent. 
If one weakens the thesis in this way, then it appears that a much
weaker system than ZFC is required, since what seems to be at issue is
the correctness of the argument, not the correctness of the axioms used
in the argument. But if that is so, then something implementing Q (or
better, some simple theory of syntax) could check whether e.g. "if
[conjunction of some axioms], then [theorem]". Or, to put the point
another way, this version of the thesis looks like it's equivalent to
something like: all correct mathematical reasoning is formalizable in
first-order logic, this being what Boolos, Burgess, and Jeffrey call
"Hilbert's Thesis" (p. 185).

One might worry about the "conjunction of axioms" part, but there are
ways around that.

Richard