Home Philosophy Advances in Proof-Theoretic Semantics

## Several I-RulesWhere a logical constant (such as ∨) is introduced by several alternative [ . [ .
so an appropriate generalisation for as in [9, 24], has no minor premises ## I-Rule Has Several PremissesNow there are two possibilities following the general idea that the conclusion of a GE-rule is arbitrary. Let us consider the intuitionistic constant ∧ (with its only I-rule having two premisses) as an example. The first possibility is as illustrated earlier: the rule [ .
. The second is to have two GE-rules: [ .
.
and it is routine to show that the ordinary GE-rule for ∧ is derivable in a system including these two rules, and vice-versa. Tradition goes for the first possibility; examples below show however that this doesn't always work and that the second may be required. ## Premiss of I-Rule Discharges Some AssumptionsNatural deduction's main feature is that assumptions can be discharged, as illustrated by the I-rule for ⊃ and the E-rule for ∨. This raises difficulties for the construction of the appropriate GE-rules: Prawitz [26] got it wrong (corrected in [27]), SchroederHeister [30] gave an answer in the form of a system of rules of higher level, allowing discharge not just of assumptions but of rules (which may themselves discharge …)—but, although much cited, use of this system seems to be modest. As already discussed, an alternative was mentioned (disparagingly) in [3] and (independently) adopted more widely by others [13, 36, 39], the “flattened” GE-rule for ⊃ being [ .
Let us now consider the position where two premisses discharge an assumption (just one each is enough): consider the logical constant ≡ with one I-rule, namely [ . [ .
According to our methodology, we have two possibilities for the GE-rule; first, have the minor premiss of the rule with two assumptions above for ∧, and these are clearly [ .
.
by means of which it is clear that, from the assumption of completeness” of this set of rules in a sense explored by Pfenning and Davies [22]:
.
.
We are thus committed in general to the use of the second rather than the first possibility of GE-rules—the use of two such rules rather than one—when there are two premisses in an I-rule. |

< Prev | CONTENTS | Next > |
---|

Related topics |

Academic library - free online college e textbooks - info{at}ebrary.net - © 2014 - 2019