[FOM] Formalization Thesis

[Freek Wiedijk]

Andrej:

>> 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?

Freek