Page 101 of 800
| Page 101 of 800 | Search internet |
If you want to define your own theories it may be a good idea to look at the way 
, 
, and 
are defined. We mainly follow E. Mendelson: 'Introduction to mathematical logic' in the formulation of axioms, inference rules, and theories. To define we first define axiom 
:
That statement macro expands into two definitions. The first one says:
That defines what the axiom says. It says that for all object terms 
and 
we have 
. Since implication is post-associative, the axiom says 
.
The second definition reads:
This defines how to prove Axiom : Look it up in all presently assumed theories and see it is there. If yes, generate a sequent term which extracts from the theory in which it is found.
Note that looking up an axiom in all assumed theories can be costly in terms of cpu time. If you need e.g. very often and always need it in a context where you have assumed e.g. , then prove
once and for all and reference that lemma instead of axiom . That will save you a lot of cpu time.
has more rules:
Axioms and rules macro expand in exactly the same way and the Logiweb sequent calculus makes absolutely no distinction between axioms and inference rules.
The understood parentheses in the 
rule are:
Thus, says that if we have a proof of 
then we can conclude 
. And if we also have a proof of then we can in turn conclude
The defined by the Peano page also has a rule of definition:
The rule says: For all object terms and , if the side condition 
evaluates to 
then . The side condition is true if and are identical except for application of definitions.
As an example, the Peano page defines
In other words, the Peano page defines the 'math/kg' aspect of 
to be 
. Because of that, the 
rule allows to replace by and vice versa.
The Peano page defines the side condition thus:
When the side condition is evaluated, it is applied to the cache of the page on which the proof occurs. Among other, that grants access to all definitions on that page and all transitively referenced pages. The 
function then traverses the terms 
and 
in parallel and sees if all differences are in accordance with math definitions in the cache 
.
The Peano page does not follow Mendelson completely. Among other, the Peano page takes implication 
and falsehood 
as primitives and defines negation thus:
The Peano page also defines truth:
and a couple of convenient operators like 
, 
, and 
.
The definition of is a meta-conjunction:
The Peano page also defines the tactic to be used on proofs:
That is the tactic which, among others, knows how to handle hypothetical reasoning and deduction blocks in .
| Page 101 of 800 | Search logiweb.eu |