The special status of the implication connective in natural deduction

408 Views Asked by At

In natural deduction, it seems that implication is not 'yet another connective', at least because it is the only one whose introduction rule requires the apparatus of 'assume', then 'discharge':

As a reference http://www.cs.cornell.edu/courses/cs3110/2013sp/lectures/lec15-logic-contd/lec15.html says:

In natural deduction, to prove an implication of the form P ⇒ Q, we assume P, then reason under that assumption to try to derive Q. If we are successful, then we can conclude that P ⇒ Q.

My question is a soft one. Why this design? Could one have designed a system with no apparatus for 'assume then discharge'? Making the process of creating inferences more 'canonical'? Is the reason for taking this path in natural deduction simply the fact that reasoning by 'assume and discharge' is more 'natural', closer to the way informal inference works? Are there other reasons?

1

There are 1 best solutions below

5
On BEST ANSWER

It is indeed a rather 'natural' thing to conclude $P \rightarrow Q$ when the assumption of $P$ leads to $Q$. However, many formal proof systems use the 'assume and discharge' for fairly natural proof techniques other than this kind of conditional proof.

The proof by contradiction is a very common one in fact: Assume $P$, and if that leads to a contradiction, then infer $\neg P$. This is often formalized in formal proof systems as $\neg$ introduction.

Proof by cases is another common one: when you have a disjunction $P \lor Q$, and if the assumption $P$ leads to $R$, and the assumption of $Q$ (in a second, parallel, subproof) leads to $R$ as well, then we can infer $R$. This rule is often formalized as $\lor$ Elimination.

Also, some formal proof systems have no 'assume and discharge' mechanism at all. Axiom systems are like that. The Hilbert system is a well known axiom system.

Still, the conditional does seem to have some kind of 'special' or 'central' status in all of this. As Henning points in the Comments, even when we use 'assume and discharge' for connectives other than the $\rightarrow$, we can still make a close link to the $\rightarrow$. Proof by cases, for example, is sometimes formalized as $P \lor Q, P \rightarrow R, Q \rightarrow R \vdash R$, and to get the two conditionals, one often ends up doing a conditional proof. And, as Luca points out, even the proof by contradiction can be seen as a kind of conditional proof: some systems define $\neg P$ as $P \rightarrow \bot$, and some systems define the rule as $P \rightarrow Q, P \rightarrow \neg Q \vdash \neg P$, and so yet again to get the relevant conditionals one effectively ends up doing a conditional proofs yet again.

And finally, even in axiomatic systems, where there are no 'assume and discharge' rules at all, it is often the case that they have a single inference rule, Modus Ponens, which is, yet again, a conditional rule.

So this is rather interesting: as dozens of questions to this site can attest, the conditional (material implication) is rather controversial as a truth-functional connective (see: Paraodxes of Material Implication), and yet it in many ways does seem to have this central status in logic ... though this can probably be explained by its close connection to the logical implication, which clearly is central in logic.