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

Question

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!]

Answer 1

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.)

Answer 2

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