2.2 Logiweb for verification

Prev Up Next Page 5 of 800 Search internet

For a proof which Logiweb has verified, see the multzero page. Following the multzero link brings you to a pdf rendering of the multzero page. At the multzero page you will find a formal proof of

PA lemma 3.2l : all x : 0 * x = 0 end lemma

The lemma (lemma 3.2l of Mendelson, Introduction to Mathematical Logic) is stated within Peano Arithmetic (PA) as defined on the Peano page. The proof is verified by the proof checker defined on the check page.

When the multzero page was translated by the Logiweb compiler, the compiler verified the proof. The result of the verification is here.

If you like the definition of Peano Arithmetic on the Peano page, you can use it on your own Logiweb pages just by referencing the Peano page from your pages. Logiweb will then use that definition of Peano Arithmetic when verifying your proofs. If you want to define Peano Arithmetic otherwise, write your own definition and let Logiweb use that. If you want to share your definition, publish it on Logiweb.

If you like the proof checker on the check page, you can use it on your own Logiweb pages just by referencing the check page from your pages. If not, write your own. If you want to share your proof checker, publish it on Logiweb.

The proof checker on the check page allows you to define arbitrary, formal theories. That includes traditional theories like Peano Arithmetic and ZFC. If you want classical versions, include the axioms of classical propositional calculus as is done on the Peano page. If you want intuitionistic versions, omit the law of excluded middle. You may even omit propositional calculus if you work with exotic theories like Map Theory.

Logiweb provides notational freedom. If you like the definitions on the Peano page but not the notation you can reference the Peano page but still define your own notation.

Prev Up Next Page 5 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05