[FOM] Formalization Thesis

[Timothy Y. Chow]

On Mon, 31 Dec 2007, rgheck wrote:
> Timothy Y. Chow wrote:
> > 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]".

It's true that *if* one agrees that the formal theorem correctly 
represents the informal theorem, then checking the proof requires only a 
very weak system.  However, part of what's at issue is what is required 
for the formal theorem to represent the informal theorem, and it seems 
to me that some set-theoretical axioms are needed.

For a simple example, does "x = {{x_1}, {x_1, x_2}}" faithfully capture
"x is the ordered pair (x_1, x_2)" if I can't prove that "(x_1, x_2) = 
(y_1, y_2) iff x_1 = y_1 and x_2 = y_2"?  I think not.  But in order to 
prove that, I need some axioms about sets (extensionality, in particular); 
pure logic isn't enough.  Some amount of set-theoretical reasoning is 
tacitly assumed when one translates concepts from other branches of 
mathematics into set theory.

Of course, it's plausible that some other system of axioms for set theory 
that is much weaker than ZFC would suffice, but once we admit that we need 
some set theory, then my inclination is to pick ZFC, for name recognition 
if nothing else.

Tim