[FOM] proof assistants and foundations of mathematics

[katzmik at macs.biu.ac.il]

I detect two rather distinct concerns in Jose's comments:

(1) What did Voevodsky mean when he criticized CIC as allegedly inadequate as
far as foundations are concerned because CIC assumes the integers whereas
apparently it shouldn't in Voevodsky's scheme of things;

(2) the more concrete issue of a mathematician being allegedly able to program
a routine within CIC that would prove that 0=1 and therefore many, many other
theorems.

Can people comment on how direct the relation between (1) and (2) is?  It
doesn't seem so direct to me.  I think finding an answer to (1) may be pretty
hopeless.  As far as (2) is concerned, it was pointed out by one of the
participants in this discussion that the responsibility for avoiding such
malignant routines is the programmer's, not CIC's.  I believe this rebuttal
misses the point, though.  If such routines can in principle be programmed,
this may occur even without the conscious knowledge of the programmer. 
Therefore proofs in such a logical framework are not "absolutely reliable",
which sort of defeats the whole purpose, or does it?

MK

On Tue, August 14, 2018 11:36, Till Mossakowski wrote:
> Am 11.08.2018 um 21:39 schrieb Timothy Y. Chow:
>>
>> 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.