1
$\begingroup$

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

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ If you want a historical reference you should be able to find your answer in Heyting's own book "Intuitionism. An introduction." $\endgroup$
    – Kaveh
    Commented Jun 29, 2013 at 5:54

2 Answers 2

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – Jacques Carette
    Commented Jun 28, 2013 at 15:18
  • $\begingroup$ 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? $\endgroup$
    – Andreas Blass
    Commented Jun 28, 2013 at 15:45
  • $\begingroup$ 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. $\endgroup$
    – J Marcos
    Commented Jun 29, 2013 at 16:31
  • $\begingroup$ 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))$.) $\endgroup$
    – Emil Jeřábek
    Commented Jul 2, 2013 at 17:01
  • $\begingroup$ @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. $\endgroup$
    – Andreas Blass
    Commented Jul 2, 2013 at 18:07
4
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • 2
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Jun 28, 2013 at 14:48
  • 1
    $\begingroup$ 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. $\endgroup$
    – Nik Weaver
    Commented Jun 28, 2013 at 16:50
  • $\begingroup$ Yes, I should have done that - edited to include a link. So Halleck should have used 3 different symbols for implication? $\endgroup$
    – Jacques Carette
    Commented Jun 28, 2013 at 16:57
  • 2
    $\begingroup$ 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. $\endgroup$
    – Nik Weaver
    Commented Jun 28, 2013 at 17:18
  • $\begingroup$ Apparently Hackstaff (check page 10 of his book) uses different symbols for "material implication", "strict implication", "intuitionistic implication" and something he calls "strong implication". I currently don't have access to Ch.6 of the book, where the Intuitionistic System is introduced; it would seem inadvisable, at any rate, to use strict implication instead of intuitionistic implication in that formulation. $\endgroup$
    – J Marcos
    Commented Jun 29, 2013 at 16:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .