[FOM] proof assistants and foundations of mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Sat Aug 11 15:39:04 EDT 2018
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
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?
More information about the FOM