# What exactly is the role of the material conditional in intuitionistic logic?

There seems precious little around about the use of the material conditional in intuitionistic logic aside from the Wikipedia page https://en.wikipedia.org/wiki/Material_conditional and I can't seem to glean what I need from there.

To quote wikipedia:

"Whereas, in minimal logic (and therefore also intuitionistic logic) $p\rightarrow q$ only logically entails $\neg(p\land \neg q)$..."

Right, so this gives me the following rule:

$$\frac{p\rightarrow q}{\neg (p\land \neg q)}$$

However the use of the phrase 'logically entails' suggests that this is a theorem, not an axiom. Wikipedia then goes on:

"...and in intuitionistic logic (but not minimal logic) $\neg p\lor q$ entails $p\rightarrow q$."

From which I get the following rule:

$$\frac{\neg p\lor q}{p\rightarrow q}$$

Here the use of the phrase 'entails' I read as different to rather than synonymous with the phrase 'logically entails', in the sense that this is an axiom rather than a theorem. Put another way, the wording suggests that I am to take this as the rule for the introduction of the material conditional. If so, why the qualification that this only holds in intuitionistic logic and not minimal logic?

[A plea to logicians: please stick to the convention I've adopted here that $\rightarrow$ stands for the material conditional whereas $\Rightarrow$ stands for logical consequence! Admittedly I haven't used the latter but just in case you do. Otherwise things will just get impossible to fathom. Thank you!]

I believe that "logically entails" and "entails" mean the same thing, here.

The point is that in minimal logic, $p\rightarrow q\vdash \neg(p\wedge\neg q)$ is a valid sequent (I'm using "$\vdash$" instead of "$\implies$" here, both for added clarity and to mesh with the standard notation in proof theory). Meanwhile, in intuitionistic logic, $\neg p\vee q\vdash p\rightarrow q$ is a valid sequent; but $\neg p\vee q\vdash p\rightarrow q$ is not a valid sequent in minimal logic.

The "only" in the phrase "only logically entails" doesn't apply to "logically"; the point is that in minimal (and even in intuitionistic) logic, we only have $$p\rightarrow q\vdash \neg(p\wedge\neg q)$$ as a valid sequent, not also $$p\rightarrow q\vdash \neg p\vee q.$$

(Note that talking about valid sequents frees me from having to specify a proof system; in particular, I don't need to distinguish between assumed sequents - that is, logical axioms - and derived sequents.)

• Hi, Noah. Thanks for the answer. I'm not marking it as the accepted answer yet only because of my own still limited understanding. From your answer I guess that my first rule, which I'll write in your notation $p\rightarrow q\vdash \neg(p\wedge\neg q)$, I should take as an axiom in my system? – James Smith Jun 15 '16 at 20:29
• @JamesSmith Well, whether or not you should take that specific sequent as an axiom in your system depends on the rest of your system (and what properties you want your system to have). But it would be a reasonable choice. – Noah Schweber Jun 15 '16 at 20:31
• Okay, I'll accept your answer now and add my own underneath (mainly for the sake of formatting). – James Smith Jun 16 '16 at 19:55

So we have the following rule as a definition of the material conditional, so to speak, at least one way:

$$\frac{p\rightarrow q}{\neg (p\land\neg q)}\quad\text{MaterialConditionalElimation}$$

Now @noah-schweber's comment is that $p\lor\neg q\Rightarrow p\rightarrow q$ rather than $p\lor\neg q\Rightarrow\neg(\neg p\land q)$ which suggests that he considers $\neg(\neg p\land q)$ and $p\rightarrow q$ to be equivalent. Therefore we should also add the rule:

$$\frac{\neg (p\land\neg q)}{p\rightarrow q}\quad\text{MaterialConditionalIntroduction}$$

To summarise, in all logics $p\rightarrow q$ is synonymous with $\neg (p\land\neg q)$ and not $p\lor\neg q$.

Next we show that $p\lor\neg q\Rightarrow\neg(\neg p\land q)$. The proof is intuitionistic:

Rule
Premise
⌐P∨Q
Conclusion
⌐(P∧⌐Q)
Proof
Suppose
P∧⌐Q
Then
⌐⌐P∧⌐Q by DoubleNegationIntroduction
Hence
⌐(⌐P∨Q) by ConjunctionOfNegationsImpliesNegationOfDisjunction
P∧⌐Q=>⌐(⌐P∨Q)
⌐P∨Q
⌐(P∧⌐Q) by ModusTollens


Next we show that $\neg(\neg p\land q)\Rightarrow p\lor\neg q$. The proof is classical:

Rule
Premise
⌐(P∧⌐Q)
Conclusion
⌐P∨Q
Proof
⌐P∨⌐⌐Q by NegationOfConjuctionImpliesDisjunctionOfNegations
⌐P∨Q by DoubleNegationIntroduction


To summarise, the equivalence between $\neg (p\land\neg q)$ and $p\lor\neg q$ only holds classically.

Finally here are the two derivations alluded to above...

This is the proof that the conjunction of two negated propositions implies the negation of their disjunction, which is intuitionistic. Perhaps there is a neater way of doing this:

Rule (ConjunctionOfNegationsImpliesNegationOfDisjunction)
Premise
⌐P∧⌐Q
Conclusion
⌐(P∨Q)
Proof
⌐P, ⌐Q
P=>S, Q=>S by PrincipleOfExplosion
P=>⌐S, Q=>⌐S by PrincipleOfExplosion
P∨Q=>S by DisjunctionImplication
P∨Q=>⌐S by DisjunctionImplication
⌐(P∨Q) by NegationIntroduction


This is the proof that the negation of the conjunction of two propositions implies the disjunction of their negations, which is classical. Again, perhaps there is a neater way of doing this:

Rule (NegationOfConjuctionImpliesDisjunctionOfNegations)
Premise
⌐(P∧Q)
Conclusion
⌐P∨⌐Q
Proof
Suppose
⌐(⌐P∨⌐Q)
Suppose
P
Then
Suppose
Q
Then
P
Hence
P∧Q
Q=>P∧Q
⌐(P∧Q)
⌐Q by ModusTollens
Hence
⌐P∨⌐Q by DisjunctionIntroduction
P=>⌐P∨⌐Q
⌐(⌐P∨⌐Q)
⌐P by ModusTollens
Hence
⌐P∨⌐Q by DisjunctionIntroduction
⌐(⌐P∨⌐Q)=>⌐P∨⌐Q
⌐(⌐P∨⌐Q)=>⌐(⌐P∨⌐Q)
⌐⌐(⌐P∨⌐Q) by NegationIntroduction
⌐P∨⌐Q by DoubleNegationElimination

• Incidentally, I've used a derived rule which I've called 'Disjunction introduction' in the above. It should be clear what it does. In the latest proofs I've done away with this and used the more standard 'Constructive dilema' but the result is the same. – James Smith Jun 18 '16 at 6:18