8.1 Approach

Page 302 of 800

Search internet

The Logiweb proof checker is the proof checker which comes with the Logiweb package. It provides an example of how one can express a proof checker in Logiweb.

The proof checker is not part of Logiweb. If you like it, use it. If you don't, make your own. If you want to share your work with others, publish it on Logiweb.

The Logiweb proof checker is general enough to support any, axiomatic theory I can dream of. At the time of writing, I have been dreaming about peculiar, non-standard theories for more than 30 years: theories whose proofs have peculiar renderings, theories with peculiar metatheories, and non-standard theories like map theory. Providing support for map theory was the main motivation for starting work on Logiweb, but the Logiweb proof checker has no bias towards any, particular theory.

The Logiweb package contains a definition of Peano arithmetic. The definition has been included to give an example of how to use the Logiweb proof checker. Peano arithmetic has been chosen because many people know it. The definition of Peano arithmetic essentially follows E. Mendelson: 'Introduction to mathematical logic'.

If you want to prove something in Peano arithmetic, you may think of the system as comprising the following layers:

Application layer

This is where you build up your own theories on top of Peano arithmetic.

Peano arithmetic

This is the low level language you build on top of. You can take it from the Peano page or make your own.

Logiweb sequent calculus

This is the 'machine language' which the Peano page builds on top of. The Logiweb sequent calculus is hardcoded into the Logiweb proof checker. Stubborn users may use the sequent calculus directly, but the intended use is that proof tactics generate sequent terms as their output and that users never see them. Proof tactics run at verification time and their output is discarded as soon as it is verified, so you cannot see the sequent code unless you include print statements in your tactics. The Logiweb sequent calculus is intuitionistic, but even if you do intuitionistic logic, you should define an intuitionistic theory on top of the calculus rather than using the calculus directly.

The Logiweb proof checker

This is defined on the check page. It implements the Logiweb sequent calculus.

The Logiweb Compiler

Lgc(1) is the program you use to get your proof verified.

The Logiweb Abstract Machine

Lgwam(1) is the actual binary which verifies your proof.

Depending on how much freedom you want, you can build on top of Peano arithmetic, make your own Peano arithmetic, make your own proof checker, make your own compiler, or make your own abstract machine. At each level, however, care has been taken to leave as much freedom as at all possible to the next level above.

Thus, the philosophy at all stages is to give you the freedom not to use the offered systems and make your own, but also to give you systems that are so general that you will never need to make your own.

Page 302 of 800

Search logiweb.eu