Apollo is correct. A slightly more technical way of putting it is that "discharging" is an application of a theorem of metalogic called the deduction theorem:
T,P|-Q iff T|-P->Q
The single turnstile symbol "|-" stands for the syntactic consequences relation. The deduction theorem basically says "Q is derivable from T and P iff if P then Q is derivable from T alone". T may, of course, be an empty class of statements, in which case P->Q is tautologous.
Many systems of natural deduction introduce conditional proof as a primitive rule, but there are simpler systems that are just as powerful in which the deduction theorem is proved and conditional proof is a derived rule supported by the deduction theorem. The deduction theorem is important because it shows you don't need conditional proof as a primitive rule, and this makes the proof of other theorems in metalogic a whole lot simpler. Basically, if you have as few rules as possible it gives you fewer cases to check. For practical purposes, however, it's a whole lot easier to teach and use a system that introduces lots and lots of primitive rules as opposed to one that uses as few rules as possible.
Mathematicians use conditional proof all the time, by the way. For example, in a proof of Q by cases you get conditionals P1->Q, P2->Q, etc. by for each case supposing the antecedents, deriving Q from the supposition, then "discharging" the supposition. Then you show the disjunction of the antecedents is exhaustive.
No comments:
Post a Comment