Are You Using the Right Axiomatic System?

Estasis have provided an approach to theorem proving, the Falso system, leveraging a very proof-theoretically strong axiomatic system - indeed the strongest possible in the tower of consistency strengths, far stronger than Woodin cardinals - together with elegant economy to provide highly compressed proof techniques. It is evidently much easier to prove theorems in this system than, for example, in Coq.

Past discussions here, such as On the (Alleged) Value of Proof for Assurance, show that the great speed-up in providing correctness proofs offered here is to be valued. I cannot bring myself to recommend this system too highly.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.




Nice to see this here, and I think my friend who did it (I only host the website) will be even more pleased than me!

You may want to have a look to some little ads for Falso, which I made yesterday just before posting this to Hacker News, some of them are pretty fun too.