- The combinations page gives an example of programming in Logiweb by defining the binomial coefficient. You will learn how to produce a similar page in Tutorial T02.
- The proof page gives an example of proving in Logiweb by proving 0*x=0 in Peano arithmetic. You will learn how to produce a similar page in Tutorial T03.
- The base page contains elementary proclamations, definitions, and introductions. Proclamations connect syntax with predefined Logiweb concepts. Definitions connect syntax with user defined concepts. Introductions connect syntax with optimization features. Among other, the base page defines a macro expansion facility.
- The check page implements a proof checker which is based on the 'Logiweb sequent calculus'. The proof checker allows users to define axioms, inference rules, and theories, and to state lemmas and proofs. The proof checker checks each proof against the theory in which the associated lemma is stated. The check page references the base page such that e.g. the macro facilities defined on the base page are available on the check page.
- The Peano page defines propositional calculus (Prop), first order logic (FOL), and Peano arithmetic (PA). Furthermore, the Peano page defines a tactic which allows users to use deduction in their proofs. The Peano page contains a proof of x+y=y+x which illustrates how to use the facilities. If you want to write Logiweb pages, do not miss reading the sources of the proofs (available by clicking 'Source' on the Peano page. Reading the sources is like learning html by reading html sources. The Peano page references both the base and the check page to get access to macro facilities as well as the proof checker. Users who want to define other theories like ZFC may benefit from referencing the base, check, and Peano pages to get access to macros, proof checker, and FOL. Make sure you reference the check page as first reference: that ensures that your page is checked using the proof checker.