How is the material conditional treated in Natural Deduction?

Question

I'm confused by the definition of the material conditional.

In my implementation of propositional-logic I have the following definition of the material conditional:

$$\frac{P\to{Q}}{\neg(P\land\neg{Q})}\quad\small\text{[MaterialConditionalElimination]}$$

$$\frac{\neg(P\land\neg{Q})}{P\to{Q}}\quad\small\text{[MaterialConditionalIntroduction]}$$

I should that this is a definition because there is (effectively) a bi-directional inference rule. That is to say, whenever you encounter $\neg(P\land\neg{Q})$ you can replace it by $P\to{Q}$ and vice-versa.

However, according to Wikipedia, only the first of these rules is found in minimal logic. But I cannot see how you can derive the second from the first with the addition of the principle of explosion. Also, it is the second that serves, if one rule only can be taken, as a definition, because that is the rule that introduces the new $\to$ connective.

Update: It seems that the material conditional does not find its way into propositional logic when defined in this natural deductive style. I have therefore taken it out of the aforementioned implementation.

Further update: Well, it appears that it does, but only at the classical level. At this level, however, it is equivalent to logical consequence $\Rightarrow$ and therefore I am opting to leave it out still.

Answer 1

The implication sign does not denote material implication in intuitionistic logic. The Wikipedia page does not say what you think it does. It says that $\lnot P \lor Q$ (not $\lnot (P \land \lnot Q)$) entails $P \to Q$ in intuitionistic logic, but not in minimal logic (which is true but the reverse entailment is not provable in intuitionistic logic). In intuitionistic logic (and hence also in minimal logic) $\lnot P \lor Q$ is not equivalent to $\lnot(P \land \lnot Q)$ and neither of those is equivalent to $P \to Q$.

To see that $\lnot P \lor Q$ is strictly stronger than $P \to Q$ in intuitionistic logic, take $P \equiv Q$ for $P$ a variable, then $P \to P$ is provable, but $\lnot P \lor P$ expresses the intuitionistically unacceptable law of the excluded middle. To see that $P \to Q$ is strictly stronger than $\lnot(P \land \lnot Q)$, take $Q$ to be a variable and take $P = \lnot\lnot Q$, then $\lnot(\lnot\lnot Q \land \lnot Q)$ is provable, but $\lnot\lnot Q \to Q$ is the intuitionistically unacceptable principle of double-negation elimination.

Answer 2

Let me try to answer my own question, although I am far from sure that I have it right. Perhaps this is just another way of asking it.

The first rule, the introduction rule...

$$ \frac{\neg(P\land\neg{Q})}{P\to{Q}} $$

...it looks like should be taken as a given in minimal logic. This is debatable, however, if you consider $\to$ to be a primitive of the logic, and therefore not requiring a rule for its definition at all.

What Wikipedia says is that, additionally, in minimal logic $P\to Q$ logically entails $\neg(P\land\neg{Q})$. I believe that one way of stating this is in the form of the second inference rule, the elimination rule:

$$ \frac{P\to{Q}}{\neg(P\land\neg{Q})} $$

Therefore the statements $P\to Q$ and $\neg(P\land\neg{Q})$ can be seen as being entirely equivalent, since we effectively have a bi-directional inference rule.

If drawing attention to this equivalence seems churlish, consider that introduction and elimination rules are not generally symmetric in this manner. Consider, for example, the introduction rule for logical consequence:

$$ \frac{[P]\;...\;Q}{P\Rightarrow{Q}} $$

Turning this rule on its head is non-sensical, although many (including me) might carelessly view the antecendant and consequent as being equivalent in day to day usage. However, of course the corresponding rule is not the introduction rule just turned on its head, it is Modus Ponens:

$$ \frac{P\Rightarrow{Q}\;\;P}{Q} $$

So the rules concerned with the material conditional seem to stand out to me against all the other standard (whatever quite that means) rules in propositional logic in that they seem to define nothing more than a syntactic equivalence.

Put another way, it seems to me that $P\to Q$ can be viewed as nothing more than a convenient shorthand for $\neg(P\land\neg Q)$ and it is this usage for which I am seeking clarification.

Answer 3

Let me have another go at answering the question...

If the formalism is natural deduction, there appears to be no place for the material conditional. The following rule is not a given rule of minimal logic in natural deduction:

$$ \frac{\neg{(P\land\neg Q)}}{P\to Q} $$

For example, there is no place for the material conditional here:

https://www.cs.cornell.edu/courses/cs3110/2013sp/lectures/lec15-logic-contd/lec15.html

Whilst it might not seem like such a bad idea to define $P\to Q$ as a shorthand for $\neg{(P\land\neg Q)}$ in such systems, this appears never to be done.

On the other hand, away from natural deduction, we should consider $\to$ as a primitive that cannot be defined in terms of other connectives. For example, one form of the principle of explosion is implemented thus...

$$ \neg P\to(P\to Q) $$

...here:

https://en.wikipedia.org/wiki/Minimal_logic

Compare this with the same in natural deductive form:

$$ \frac{\neg P}{P\Rightarrow Q} $$

To compare these two directly, however, and therefore to conclude that $\to$ is in some sense the same as both logical consequence and inference, would seem to be wrong.

If we say that the first and last rules given here are in natural deductive style and the second rule is in the Hilbert style (I am not entirely sure that it is but the definition will have to suffice for now), the lesson seems to be that such comparisons between styles can lead to mis-comprehensions. It appears that it is not quite right to believe that it is the same logic underneath, to put it one way.

In Hilbert style logics we have the concept of the material conditional, the single arrow, if that is what we choose to adopt (and many logicians would disagree rightly on this point and insist that it should simply be referred to as implication and is not the same as the material conditional) and it is a primitive of the logic and not defined by any axiom. In natural deduction style logic, on the other hand, we have the primitive notion of inference and, along with that, a definition of logical consequence, the double arrow, that is not a primitive of the logic and that we define with the standard introduction and elimination rules.

So it is not the case that the natural deduction and Hilbert styles are simply two views of the same underlying logic, and it was my mistake to believe that they were.

Much confusion arises because when logicians commonly speak of minimal and intuitionistic logic, they are referring to the Hilbert style, and do not make this clear, even though it is perfectly possible to define variants of minimal and intuitionistic logic in the natural deductive style.

Further confusion arises because it is permissible to define the material conditional in the natural deductive style, but only for classical logic. So, again, it was my mistake to add the introduction and elimination rules for the material conditional to minimal logic given in the natural deductive style. I hadn't pulled the introduction rule out of thin air, my mistake was simply to add it at the minimal level, not the classical one. And at the classical level of course, it is equivalent to logical consequence, the double arrow, anyway, which I why I have omitted it still.

I hope this clarifies.