Page 102 of 800
| Page 102 of 800 | Search internet |
The Peano page defines 
thus:
For the sake of efficiency, the Peano page includes an axiom 
of parallel instantiation which allows to do multiple variable instantiations in parallel. 
and can substitute each other. If one omits then proofs may become longer and more complicated. can directly replace . On the other hand, if one adds axioms for meta-reasoning about side conditions, the side condition of may be easier to reason about than the side condition of . In , both and are included.
In the definition of note that 
is included as an axiom. That makes all axioms of available because of the way the rule tactic 
works. It is the tactic which defines how to prove an axiom: Look it up in all presently assumed theories and see it is there. If yes, generate a sequent term which extracts the axiom from the theory in which it is found.
If the rule tactic is asked to prove e.g. 
in it will look up the definition of in the cache. The tactic sees that is a meta-conjunction. Then it looks into each conjunct. First conjunct of is , then the tactic looks up the definition of and sees it is a meta-conjunction. Then it looks into each conjunction and finds as first conjunct. Then the tactic generates a sequent term which says is true because it is assumed, then dereferences into the definition of , then takes the head of that to get , then dereferences into the definition of , then takes the head of that to get , and finally dereferences into the definition of .
| Page 102 of 800 | Search logiweb.eu |