[FOM] proof assistants and foundations of mathematics

[Timothy Y. Chow]

Mario Carneiro wrote:

> This is an interesting position. If I read it correctly it is 
> anti-formalization, in the sense that it is better to have a 
> mathematical result not formalized at all, so that it remains 
> foundationally ambiguous (with the presumption that it can fit in a 
> relatively weak logic), rather than to have it formalized in a proof 
> assistant with an unnecessarily strong logic.

I didn't interpret Jose as going so far as this.

If mathematician M is doubtful about axiom system S, then naturally M will 
be somewhat dissatisfied with a proof assistant that takes S for granted. 
But M need not go so far as to say that the proof assistant is worse than 
nothing.

What I think Jose implicitly desires is a proof assistant that has the 
feature that it can verify "T is a theorem of S if your logic is L" where 
S and L are arbitrary and *user-specified*.  Moreover, the verification of 
such statements should assume as little as possible.  So if the next Ed 
Nelson comes along who doesn't even trust PRA, he can still plug in his 
favorite set of axioms and proof calculus and find out if his theorem is 
really a theorem by his own standards.  He won't have to go off and write 
his own home-grown, bug-ridden proof assistant.

I think that most people working in formal proofs can see the value of 
such a feature, but my impression is that it's a tougher engineering job 
than it might seem at first glance.

By the way, Jose's technical question of the relationship between Q0 and 
CIC does sound interesting.  Anyone here know the answer?

Tim