[FOM] Project announcement

[Sebastian Reichelt]

Dear Andrej,

thanks for your reply, and please excuse the somewhat lengthy explanation below.

> how is your project related to other projects with similar goals, for
> example Coq, HOL, Isabelle, Mizar, etc?

I would say that there are two main differences, related to the software aspect and the foundational aspect of the project.

Regarding foundations, I guess I should have been more specific. (I just wanted to keep the length of the post down.) The main difference to other similarly strong formal systems is that a consistency proof is possible within classical mathematics. The reason I carried out this proof is the following: While I do not have any doubts in e.g. classical reasoning or the existence of power sets (or rather, the consistency of this assumption), I cannot convince myself that set theories like ZF(C) must be consistent. Of course, I could have confined myself to the natural or real numbers instead, but my goal was to enable the formalization of mathematics in general, not just some parts of it.

So, if I had fully worked out all of the details in the proof, I would simply say "this system is consistent, period." You might argue that since the proof uses classical mathematics, it needs ZF or something equivalent, so if ZF turned out to be inconsistent after all, the proof would become worthless. But I am sure that if an inconsistency in ZF exists, it lies in a specific set construction that is not used in mainstream mathematics. That is, just like the number of primes would still be infinite and the square root of 2 would be irrational, my system would continue to be consistent. The same does not apply to relative consistency proofs.

I have to admit that I have written more of a proof outline than a complete proof. Moreover, even in a completely spelled-out proof, there could be errors, of course. Because of that, there is still a chance that the system in its current state is actually inconsistent. The good news is that it can certainly be fixed if that turns out to be the case. In fact, the proof is much more like a correctness proof for a computer program than a typical mathematical proof. If such a correctness proof reveals a bug in the program when carried out, repairing the program and adapting the proof is usually not a problem. The key is that the system is _constructed_ to be consistent, its consistency is not just some random statement which could be either true or false.

I hope this makes some sense. Anyway, this is not the only difference compared to other systems; I list some in http://hlm.sourceforge.net/semantics.pdf on pages 2 and 3.

The software implementation is a separate issue (though the underlying formalization obviously has a large influence). Please take Freek Wiedijk's comparison of 17 provers (http://www.cs.ru.nl/~freek/comparison/comparison.pdf) and compare it to my formalization of the same proof; starting on page 28 in the current library (http://hlm.sourceforge.net/library.pdf). (At the request of the FOM editors, I'll stop here.)

Regards,
Sebastian Reichelt