# Some questions about the material conditional and entailment in intuitionist math

In an excellent answer to a question about the history of material implication, @Bumble notes:

Unfortunately, the word ‘implies’ is ambiguous between these meanings. In particular, mathematicians are often taught to call the material conditional material implication and to read A → B as "A implies B". This is potentially misleading, because it leads to confusing the connective with the entailment relation.

I wonder if this mix-up of logical connective (in the object-language) and entailment relation (in the meta-language) is more of a concern for logicians than for mathematicians? I'm not denying that mathematicians may sometimes be pretty sloppy about this (see Bumble's post for references), but I wonder, if for an intuitionist mathematician, -- who might, like Brouwer, even consider logic to be a superfluous and sterile exercise -- and who may see proving a theorem as an essentially non-linguistic, non-formal process that somehow 'precedes' logic, this is an important mix-up? How do the formalisations of intuitionist mathematical logic represent or deal with the distinction between the conditional connective and the entailment relation (assuming they make a distinction)? Are there important differences with non-intuitionist interpretations?

• From the monotonic strict implication standpoint it seems you've also already have an important mix-up regarding your "...who may see proving a theorem as an essentially non-linguistic, non-formal process" and "How do the formalisations of intuitionist mathematical logic represent or deal with..." Commented Jul 22 at 20:52
• I see no real contradiction between developing a logic (after the fact), or formalising intuitionist logic, and claiming that mathematical thinking (constructing proofs - either as the ideal mental construction or as the actual process) is essentially a pre-logical and non-linguistic process. You don't have to be an intuitionist to believe that. Logicians seem to focus always on finished objects (sequences of signs) -- and that is very necessary and good -- but what interests me more are actual (and idealized) processes and actions. Commented Jul 22 at 21:22
• @DoubleKnot - My language was actually pretty deliberate :) Most current intuitionist mathematicians, afaik, are not as hostile to logic as Brouwer was. Commented Jul 22 at 21:25
• The background question is perhaps this that I don't understand what exactly the relation is between a proof as the external, linguistic trace, the witness of a mental construction and a proof as the actual mental (re)construction itself. I may make a separate question out of this at some point. Commented Jul 22 at 21:32
• My intuition tells me since you've resolved your own mix-up by going to the 'pre-', you could perhaps resolve your own questioned mix-up regarding connective and entailment in the exactly same way... Commented Jul 22 at 21:32

## 1 Answer

There are different ways of understanding intuitionism. For Brouwer, it is a theory about mathematical reasoning that is sharply at odds with the logicism of Frege and Russell. Mathematics is not based on logic, and logic is not required for mathematical reasoning. It was Heyting who developed intuitionistic logic, but this was at odds with Brouwer's understanding. Brouwer conceived intuitionism as something that would develop and expand as mathematicians contributed fresh insights into how to prove things. Devising a logic was like setting mathematical reasoning in stone.

According to the SEP article on the development of intuitionistic logic, Brouwer was aware that without a logic, it is problematic to explain how conditionals should be understood. He speaks of hypothetical judgments, and he appears to think of these as conditions on constructions, not as constructive conditional statements. These hypothetical judgments can be chained together in a way that preserves mathematical constructibility. It is not entirely clear how this is supposed to work, but in the absence of a logic maybe a conditional judgment and a conditional proof turn out to be the same.

Heyting's approach seems to have proved more popular. For better or worse, we have intuitionistic logic and on at least one understanding of it, it is a subsystem of classical logic. On the standard BHK intepretation of intuitionistic logic, the concept of proof is taken to be primitive and the conditional A → B is understood to mean I can prove that a proof of A can be transformed into a proof of B. So if we identify entailment with provability, then the conditional is not the same as entailment. In the Gödel-McKinsey-Tarski translation, the intutionistic A → B translates into S4 modal logic as □(□A → □B).

It is also worth noting that unlike classical logic, intuitionistic logic is not structurally complete, so it has rules that are admissible but not derivable. For example, this one:

``````     ¬A → (B ∨ C)
-------------------
(¬A → B) ∨ (¬A → C)
``````

Hence, while this is an admissible rule, the corresponding sentence is not a theorem:

``````  (¬A → (B ∨ C)) → ((¬A → B) ∨ (¬A → C))
``````

This also argues against identifying the conditional with the entailment relation.