[FOM] Formalization Thesis

[Jesse Alama]

"Timothy Y. Chow" <tchow at alum.mit.edu> writes:

> 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.  I believe that this is a reasonable way to understand what 
> it means for Mizar to "check the correctness" of theorems of ordinary 
> mathematics that go beyond ZFC, because typically when people go beyond 
> ZFC, they make it clear what additional axioms they are assuming.

FYI: mizar is based on so-called Tarski-Grothendieck set theory (TG),
which amounts to ZFC plus "there exist infinitely many strongly
inaccessible cardinals".  (In fact, neither choice nor infinity are
axioms of TG, but they are theorems.  To see their formal proofs, visit

 - http://mmlquery.mizar.org/mml/current/wellord2.html#T26 (Choice)

 - http://mmlquery.mizar.org/mml/current/ordinal1.html#K5 (Infinity)

You can click on the keyword "proof" to expand the proof.)  I don't know
of any statements in the Mizar Mathematical Library (MML), the
collection of mathematical knowledge formalized in mizar, of the form
"if A then T", where A is known to be independent of TG.  (This is not
to say that such statements couldn't be proved in mizar.)

Jesse

-- 
Jesse Alama (alama at stanford.edu)