|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:
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|