# Heyting's Intuitionist PC

John Halleck's site gives the axioms for Intuitionistic Propositional Logic using material implication, but lists those for Heyting's version thereof using strict implication where this page defines the notation. To make it more confusing, he cites Hackstaff 1966 which uses 'intuitionistic implication' (which is not clearly defined).

So, which implication should I use to properly encode Heyting's version of IPC? [The underlying exercise here is a formalization of many of the logics on Halleck's site, and so we want to stay true to the historical versions, even if it means we need to also have more versions so as to also encode more recent variants. Our techniques are such that the effort of adding variants is very low.]

-
If you want a historical reference you should be able to find your answer in Heyting's own book "Intuitionism. An introduction." – Kaveh Jun 29 '13 at 5:54

The usual intuitionistic implication, for example in Heyting's predicate calculus, should be considered an intuitionistic analog of classical material implication, not of any modal or relevantist notion.

-
Do you have some citation I can use to back up this response? I am happy to believe you, I just want to leave a proper traceable comment in my sources when the question comes up again a few years hence. – Jacques Carette Jun 28 '13 at 15:18
Being away from home and from libraries, I'll have a hard time finding a citation. Might it suffice to notice that "false implies p" is provable in Heyting's logic but (as far as I know) unacceptable in relevant logic? – Andreas Blass Jun 28 '13 at 15:45
It is indeed somewhat strange that Halleck (or Hackstaff) offers such alternative formulation of Intuitionist PC in terms of strict implication, as axioms such as HA5: q=>(p=>q) and HA10: ~p=>(p=>q) are precisely examples of "paradoxes of material implication" that strict implication is meant to avoid. – J Marcos Jun 29 '13 at 16:31
I don’t think it’s so straightforward. Gödel’s faithful interpretation of intuitionistic logic in S4 translates the intuitionistic implication $A\to B$ as $\Box(A\to B)$, i.e., strict implication. (The “paradoxes” do not arise because variables also become boxed: e.g., if I denote strict implication by $\succ$, the intuitionistic axiom $q\to(p\to q)$ effectively translates to $(\top\succ q)\succ((\top\succ p)\succ(\top\succ q))$.) – Emil Jeřábek Jul 2 '13 at 17:01
@EmilJeřábek I think I was misusing the terminology "strict implication". What I meant was the sort of implication used in relevance logic, where, for example, $\bot\to A$ would not be considered valid. – Andreas Blass Jul 2 '13 at 18:07

Where does Halleck mention either material implication or strict implication? How did you come up with that?

In intuitionism, implication is not reducible to the other logical connectives. The standard intuitionistic interpretation of the logical connectives is the BHK (Brouwer-Heyting-Kolmogorov) or "proof" interpretation: a proof of $A \wedge B$ is something which is both a proof of $A$ and a proof of $B$; a proof of $A \vee B$ is something which is either a proof of $A$ or a proof of $B$; a proof of $A \to B$ is something which enables you to convert any proof of $A$ into a proof of $B$.

-
He mentions it in the explanation of the ASCII symbols here home.utah.edu/~nahaj/logic/structures/axioms/index.html . I haven’t got the slightest idea why is he using different implication symbols in the two equivalent axiom systems for intuitionistic logic, which at any rate has only one implication connective. – Emil Jeřábek Jun 28 '13 at 14:48
Thanks @EmilJeřábek, you beat me to it. – Jacques Carette Jun 28 '13 at 15:16
Okay, first, it would have helped if you had linked to that page, second, this is little more than a typo. In intuitionistic logic the implication is neither material nor strict, it is intuitionistic. – Nik Weaver Jun 28 '13 at 16:50
Yes, I should have done that - edited to include a link. So Halleck should have used 3 different symbols for implication? – Jacques Carette Jun 28 '13 at 16:57
I wouldn't say he had to use three different symbols, but the symbol for implication certainly has different interpretations in classical, modal, and intuitionistic logic. – Nik Weaver Jun 28 '13 at 17:18