[FOM] Formalization Thesis

Freek Wiedijk freek at cs.ru.nl
Mon Jan 7 08:23:19 EST 2008


>> Because most modern proof asistants (Coq, Isabelle) can
>> easily encode ZFC, as well as ZFC + your favorite large cardinals, as
>> well as intuitionistic mathematics, temporal logic, etc.,

Can they also "easily" encode linear logic?  (Not that I
know whether there's anyone out there wanting to do practical
proofs in linear logic.)  Or keep track of whether one used
the impredicativity of the systems?


More information about the FOM mailing list