Timeline for Heyting's Intuitionist PC
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 2, 2013 at 18:07 | comment | added | Andreas Blass | @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. | |
| Jul 2, 2013 at 17:01 | comment | added | Emil Jeřábek | 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))$.) | |
| Jun 29, 2013 at 16:31 | comment | added | J Marcos | 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. | |
| Jun 28, 2013 at 15:45 | comment | added | Andreas Blass | 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? | |
| Jun 28, 2013 at 15:18 | comment | added | Jacques Carette | 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. | |
| Jun 28, 2013 at 15:06 | history | answered | Andreas Blass | CC BY-SA 3.0 |