10.1 Introduction

Page 368 of 800

Search internet

Logiweb pages can be used for stating definitions, programs, theories, lemmas, proofs, and other entities which can be processed by computers. Some examples follow:

A definition

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.

A proof

The multzero page proves . The Logiweb compiler automatically verifies proofs like the one on the multzero page whenever it translates a page. You will learn how to produce a similar page in Tutorial T03.

A proof checker

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.

An axiomatic theory

The Peano page defines classical propositional calculus (Prop), classical 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 which illustrates how to use the facilities. If you want to write Logiweb proofs, 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.

A compiler

The lgc page defines the Logiweb compiler.

A testsuite

The test page defines one among the Logiweb regression testsuites.

A base page

The base page defines a lot of elementary constructs.

The base page happens to be a 'Logiweb base page', i.e. a Logiweb page which references no other pages. For that reason, the base page cannot rely on any definitions on any other page. Rather, the base page defines everything bottom up starting from scratch. Here are some examples of what the base page defines:

• The base page proclaims to denote lambda abstraction. Logiweb knows from birth what lambda abstraction is but has no notation for it. The base page tells Logiweb that is one notation for lambda abstraction. Actually, the base page defines more than one notation for lambda abstraction, and you can define even more notations if you like. You can also define your own base page if you like and dare.
• Logiweb knows from birth what a definition is but has no name for it. The base page proclaims several names for various kinds of definitions.
• The base page defines elementary constructs like and . Such constructs are typically hardwired into programming languages, but Logiweb is designed to offer complete notational freedom and, from birth, does not assign any meaning to any notation.
• The base page defines a macro expansion engine. Whenever you reference the base page as first reference from your pages and do not define a macro expansion engine yourself, the base page expansion engine will macro expand your page. The expansion engine is the magic thing which makes macro definitions take effect.
• The base page defines a verification engine. Whenever you define test cases, the verification engine is the magic which executes your test cases. Note that the check page offers the same expansion engine as the base page but extends the verification engine to cover mathematical proofs as well as test cases. Thus, if you want to do math, consider referencing the check page as first reference rather than the base page.

Page 368 of 800

Search logiweb.eu