Some questions about the material conditional and entailment in intuitionist math

Question

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?

Answer 1

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.