[FOM] Formalization Thesis

[Andrej Bauer]

Freek Wiedijk wrote:
> 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.)

Linear logic is a bit different, as is any other "sub-structural" logic.
While it can be encoded, say in Coq,
http://citeseer.ist.psu.edu/576077.html, most effort has gone in the
direction of using linear logic for programming, as opposed to building
general proof search systems for linear logic. For example, see Lolli,
http://www.lix.polytechnique.fr/Labo/Dale.Miller/lolli/

It would be interesting to try to actually develop mathematics in linear
logic, but to my knowledge nobody has tried to do that. Certainly it
would have to look much different from "ordinary" mathematics.

> Or keep track of whether one used the impredicativity of the systems?

Well, yes, that's much easier and is just a matter of "logic
engineering". In general, computers are good at figuring out what
precisely was used in a formal proof.

Aside note: I never meant to disqualify Mizar, which for some reason
Wojtek Moczydlowski seems to think. I am sure Mizar is just fine for
formalizing "ordinary" math, and there are many examples to prove that.
I was rather pointing out that for practical formalization one needs to
think very carefully about organization of knowledge. In fact, figuring
out how to organize large quantities of formalized mathematics is a much
harder engineering problem than writing a proof checker (or even an
asistant) for ZFC, or any other theory.

Andrej Bauer