How is the material conditional treated in Natural Deduction?

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.

• Your implementation is now fine except that the law of the excluded middle should be $P \lor \lnot P$. – Rob Arthan May 6 '18 at 20:14
• The above "definition" can be easily derived from elementary properties of various logical connectives in natural deduction. See dcproof.com/DeriveImplies.html – Dan Christensen May 6 '18 at 21:19
• I think that a deeper issue in the question is that, to me, the term "material conditional" refers to a very specific Boolean truth-functional connective, but in intuitionistic logic the implication $\to$ is not intended to represent a Boolean truth-functional connective. It is a quirk of classical logic that the implication operator can be interpreted as simply the material conditional operation. – Carl Mummert May 6 '18 at 21:21
• @CarlMummert A "quirk" of classical logic? More like a theorem of classical logic (natural deduction). See the above link. – Dan Christensen May 6 '18 at 23:43
• The conditional in Natural Deduction is treated with its couple of intro- and elim- rules. IF we adopt classical logic, i.e. if we have some of the equivalent rules for it, like DN, LEM, etc. we can prove the interderivability of $P \to Q$ and $\lnot P \lor Q$ as well as $\lnot (P \land \lnot Q)$. – Mauro ALLEGRANZA May 7 '18 at 6:16

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.

• You haven't mentioned $\lnot P \lor Q$: I am quoting accurately the statement that I believe you have misread. Please check the Wikipedia page again. – Rob Arthan May 6 '18 at 15:10
• I am talking about the implication in the object language (as is the Wikipedia page). I am not talking about the metalanguage symbol for entailment. Although by the deduction theorem which holds for both minimal and intuitonistic logic, $A$ entails $B$ iff $A \to B$ is provable. – Rob Arthan May 6 '18 at 15:23
• "Entailment" means "logical consequence", which is what you are talking about when you define $P \Rightarrow Q$ apparently to mean that $Q$ is a logical consequence of (i.e., is entailed by) $P$. This is a metalanguage notation and the deduction theorem is very relevant to it. – Rob Arthan May 6 '18 at 15:35
• Please don't be abusive. I think now that you probably intended some kind of natural deduction rule in your definition of $\Rightarrow$, but it makes no difference to the facts I state in my answer. The Wikipedia page is making correct statements about the standard intuitionistic implication. – Rob Arthan May 6 '18 at 15:51
• I have told you that they are not equivalent in intuitionistic logic, from which you can conclude that they are certainly not equivalent in minimal logic. I assumed you would know that minimal logic is weaker than intuitionistic logic and hence would have been able to draw that conclusion. – Rob Arthan May 6 '18 at 16:38

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.

• It is not at all the case that $\lnot (P \land \lnot Q)$ entails $P \to Q$ in minimal logic. Implication cannot be defined from the remaining connectives in that setting. Recall that, in minimal logic, $\lnot (P \land \lnot Q)$ is an abbrevation for $(P \land (Q \to \bot)) \to \bot$, and there are no special axioms at all about $\bot$ in minimal logic. Cf. en.wikipedia.org/wiki/Minimal_logic – Carl Mummert May 6 '18 at 16:58
• Actually, I've just added to the answer something vaguely to that effect as far as my limited understanding goes (although I'm not claiming for a moment that I've prestaged your comment). – James Smith May 6 '18 at 17:04
• So how do I rescue my implementation? It seems that I have to throw away the notion of material implication altogether. – James Smith May 6 '18 at 17:06
• I am not familiar with your implementation, but if you are trying to treat $\to$ as something that can be rewritten in terms of $\lnot$, $\land$, and $\lor$, then you will need to stick to classical logic, because $\to$ cannot be expressed in terms of those connectives in intuitionistic logic. The operator $\to$ is a basic symbol in intuitionistic logic, not something introduced later by definition; the $\to$ will have its own introduction and elimination rules. I'm not sure what "prestaged means". – Carl Mummert May 6 '18 at 17:08
• I think the thing to do is just to leave it out. To me, in an intuitionistic setting it seems indistinguishable from what I would term inference. For example here the principle of explosion is given as a tautology rather than an inference rule. The fact that here effectively says that it should be considered synonymous with a causal relationship I will just have to ignore. – James Smith May 6 '18 at 17:20

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.

• Your answer is very unclear. Whether you use a Hilbert-style logic, natural deduction or a Gentzen-style sequent calculus is irrelevant: in all cases you get a form of the deduction theorem that tells you that $A \to B$ is intuitionistically provable iff $B$ can be proved taking $A$ as an assumption. Your last statement is incomprehensible. – Rob Arthan May 6 '18 at 18:36
• Answer me one thing. I would say the first and last rules are inference rules in the natural deduction style. Am I right? What is the second formalism? I would say Hilbert style. – James Smith May 6 '18 at 18:44
• Neither of the two rules you propose as natural deduction rules seem like natural deduction rules to me: natural deduction rules are about introducing or eliminating a single connective. $\lnot P \to P \to Q$ is a provable formula in any presentation of intuitionistic logic. – Rob Arthan May 6 '18 at 20:07
• Well, if you don't mind me saying I think you're being deliberately obtuse again. The aforementioned formula is given as an axiom on the Wikipedia page I link to, not a provable formula. There are at least two versions of the principle of explosion that I know of. Each is derivable from the other, depending on which you choose to state as an axiom. I assume you know this or, well, maybe you don't. Again I'd suggest that we leave off this discussion. I think I have what I need and I am tired of these attritional exchanges. – James Smith May 6 '18 at 20:14
• I think you are being obtuse: axioms are provable formulas. If you want help on MSE, I suggest you moderate your offensive attitude. – Rob Arthan May 7 '18 at 0:01