Logiweb(TM)

8.2.4 Axioms, rules, theories, and lemmas

Prev Up Next Page 307 of 800 Search internet


If you want some construct to denote some statement, define the 'statement/kg' aspect of the construct to be that statement. As an example, if you want A1 to denote All #x ,, #y : #x imply #y imply #x you can define it thus:

statement define A1 as All #x ,, #y : #x imply #y imply #x end define

The stmt definition construct is define thus:

macro define statement define x as y end define as define statement of x as y end define end define

And the stmt aspect is defined thus:

eager message define statement as "statement/kg" end define

You may also formulate the definition of A1 thus:

axiom A1 : All #x ,, #y : #x imply #y imply #x end axiom

That not only tells the Logiweb sequent calculus how you define A1. It also tells your readers that you think of A1 as an axiom.

Actually, there is a bit more to an axiom than the 'statement/kg' definition. This is how the axiom construct is defined:

macro define axiom x : y end axiom as ensure math define statement of x as y end define,unitac define x as \ u . unitac-rule ( u ) end define end math end define

Thus, stating something as an axiom not only defines the 'statement/kg' aspect. It also states a unitac aspect which says something about how the axiom behaves in proofs during tactic expansion.

A rule x : y end rule is exactly like an axiom x : y end axiom. A lemma x : y end lemma is similar except that the unitac rule is one suited for lemmas. A theory x : y end theory just expands into a 'statement/kg' definition with not unitac.

You are allowed to state all the axioms, inference rules, theories, theorems, lemmas, conjectures, and so you like without any sort of justification. That may seem reasonable for axioms, inference rules, theories, and conjectures, but it may be a surprise that you can also state theorems and lemmas without proof. However, if you state a lemma without proof and you use the lemma anyway in the proof of some other lemma then you will get an error message from the sequent calculus.

For examples of use see Prop, FOL and Peano.

Prev Up Next Page 307 of 800 Search logiweb.eu

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