The entire work of the understanding must be begun afresh and the mind, from the start, not left to take its own course but guided step by step and the business done as if by machinery.
Francis Bacon (circa 1600)
This is an essay about how I came to think that formal logic technologies can be useful in mathematics and computer science.
It is shaped as a tree for I have not yet found a simple and logical ordering of the contents.
I examine and explain some of my beliefs about formal logic systems.
First here is how and some of what I learned about them.
I highly recommend this book which is largely about why and how others care.
In summary however, I have become convinced that:
- Formal systems commonly in use today in the math community are faithful enough to my own modes of reasoning that I believe what they formally prove.
- Proofs in such systems are suitable for being checked by fast simple programs.
- Some of the proofs are so long that I may overlook errors and fool myself.
The computer can verify that such a proof indeed follows the rules and I have learned that computers find things like errors in programs and proofs far better than I.
- Formal proof systems in the computer science community may ultimately be simple but little work has been done to make them appear simple.
I looked in vain for the semantics of the formal system used by Mizar.
Maybe this is good.
The statements of formal systems that I dealt with were all short and certainly finite.
The programs whose correctness I worry about all not only terminate but in times that I can afford to wait for.
They run in a finite amount of memory using finite integers.
I very seldom attempt to prove things about floating point as the semantics are obscure.
(exception)
The programs whose correctness I care most about use non-negative integers less than 264.
I suspect that I do not need a system that has a name for the set of integers, but perhaps I am wrong here.
I think that any proof that I need to verify is a sequence of fairly short propositions, but perhaps a very long sequence.
Of course I agree with the widely quoted caveat that the problem with formal proofs is understanding what you have proven.
A course by Benson Mates
Category digression