Page 307 of 800
| 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 
to denote 
you can define it thus:
The stmt definition construct is define thus:
And the stmt aspect is defined thus:
You may also formulate the definition of thus:
That not only tells the Logiweb sequent calculus how you define . It also tells your readers that you think of 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:
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 
is exactly like an 
. A 
is similar except that the unitac rule is one suited for lemmas. A 
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.
| Page 307 of 800 | Search logiweb.eu |