Page 93 of 800
| Page 93 of 800 | Search internet |
Recall the proof of 
:
Line L03 assumes 
for the duration of the enclosing block. The hypothesis can be used in Line L04-L07. In the example above, the hypothesis is used in Line L07.
The Logiweb sequent calculus also permits hypothetical reasoning. Actually, it permits two kinds of hypothetical reasoning.
In the first kind of hypothetical reasoning, you assume a statement as a 'premise'. As an example, the proof above is one, big hypothetical proof which uses Peano arithmetic 
as premise. In other words, the proof takes as a premise that all rules of Peano arithmetic hold.
In the second kind of hypothetical reasoning, you assume a side condition as a 'condition'. As an example, you may assume that 
does not occur free in 
and then prove something under this condition.
Thus, you can use premisses and conditions at meta level and hypotheses at object theory level. The kind of hypothetical reasoning possible at object theory level depends on the object theory.
| Page 93 of 800 | Search logiweb.eu |