The proof rules for natural deduction are summarised in Figure 1.2. The
explanation of the rules we have given so far in this chapter is declarative;
we have presented each rule and justified it in terms of our intuition about
the logical connectives. However, when you try to use the rules yourself,
you’ll find yourself looking for a more procedural interpretation; what does
a rule do and how do you use it? For example,
∧i says: to prove φ ∧ ψ, you must first prove φ and ψ separately and then use
the rule ∧i.
∧e1 says: to prove φ, try proving φ ∧ ψ and then use the rule ∧e1. Actually,
this doesn’t sound like very good advice because probably proving φ ∧ ψ will
be harder than proving φ alone. However, you might find that you already have
φ ∧ ψ lying around, so that’s when this rule is useful. Compare this with the
example sequent in Example 1.15.
∨i1 says: to prove φ ∨ ψ, try proving φ. Again, in general it is harder to prove
φ than it is to prove φ ∨ ψ, so this will usually be useful only if you’ve already
managed to prove φ. For example, if you want to prove q |− p ∨ q, you certainly
won’t be able simply to use the rule ∨i1, but ∨i2 will work.
∨e has an excellent procedural interpretation. It says: if you have φ ∨ ψ, and you
want to prove some χ, then try to prove χ from φ and from ψ in turn. (In those
subproofs, of course you can use the other prevailing premises as well.)
Similarly, →i says, if you want to prove φ → ψ, try proving ψ from φ (and the
other prevailing premises).
¬i says: to prove ¬φ, prove ⊥ from φ (and the other prevailing premises).
Aucun commentaire:
Enregistrer un commentaire