# Intuitionistic logic

In propositional logic, I have now the following formulas.

$X\equiv A \implies (B \vee C)$,

$Y\equiv (A \implies B) \vee (A \implies C)$.

I have already proven that Y implies X. But does X imply Y? Who can help me with a derivation, of a intuitionistic counterexample?

-
Which kind of counterexamples do you recognize? – Henning Makholm Jul 10 '12 at 11:37
I suddenly wonder: Are you aware that "intuitionistic" is a technical term in logic? That is, are you looking for an answer to whether $X$ implies $Y$ in the particular restricted system of logic called "intuitionistic logic", or do you just want an intuitive explanation of what happens in ordinary (classical, aka non-intuitionistic) propositional calculus. The answers to those to questions are not the same! – Henning Makholm Jul 10 '12 at 11:53

Assuming that you do mean intuitionistic logic: Intuitively (!), $X$ does not ituitionistically imply $Y$.

What $X$ says is "If you give me an $A$, then I'm going to give you a $B$ or a $C$ in return, but I will not tell you which before I get to see your $A$."

On the other hand in intuitionistic logic, the meaning of $Y$ is: "I'm going to promise you either that if you give me an $A$ I will give you a $B$, or that if you give me an $A$ I will give you a $C$ -- and you can ask me which of these it will be before I even see your $A$."

Having somebody who promises me $X$ is not going to help me satisfy contract $Y$.

Arguments in this style use the Brouwer-Heyting-Kolmogorov interpretation of what an intuitionistic proof ought to be. It is connected to the Curry-Howard isomorphism.

-
I am indeed looking for a derivation/proof in the particular restricted system of logic called "intuitionistic logic". This exercise is in the propostional logic, where I am used to prove things in Gentzen's system of natural deduction. At the moment I have no idea if I should look for a proof or a counterexample. We would have a counterexample if for instance, from X, Y is reckless. Also, I have seen Kripkemodels being used as counterexamples for this kind of exercises (i.e. X yields on all nodes, but Y doesn't). – Maaike Jul 10 '12 at 12:09
@Maaike: "I have no idea if I should look for a proof or a counterexample" -- well, since I'm telling you that the implication is not intuitionistically valid, looking for a proof would be futile. But it still confuses me that you keep speaking alternately about "intuitionistic logic" and "the propositional logic" as if they were the same thing. Usually "propositional logic" without a qualifier means classical propositional logic. And your implication is classically valid. – Henning Makholm Jul 10 '12 at 12:16
You say "reckless" as if that was a technical term. I'm not aware of what it would mean. – Henning Makholm Jul 10 '12 at 12:17
Reckless is indeed a technical term in intuitionistic mathematics/logic. It means that something is not necessarily true (in intuitionistic (int.) logic). For instance, the statement 'A or not-A' is reckless in int. logic. This is because there is an int. counterexample for this Law of Excluded Middle. – Maaike Jul 10 '12 at 12:28
By your first explanation, I am now confinced that the implication is not intuitionistically valid. Thank you for that! But do you know a more technical counterexample? I.e. Your answer showed what the difference between both is, but doesn't show a case where X is true but Y isn't. – Maaike Jul 10 '12 at 12:33

Let $\mathfrak{A}$ be the frame of open subsets of the real line $\mathbb{R}$. A frame is a complete Heyting algebra, so intuitionistic propositional logic can be interpreted in $\mathfrak{A}$.

Let $B = (-\infty, 0)$ and $C = (0, \infty)$ and let $A = B \cup C$. Then, $(A \Rightarrow B \cup C) = \top$ (of course!) but $(A \Rightarrow B) = B$ and $(A \Rightarrow C) = C$, so $(A \Rightarrow B) \cup (A \Rightarrow C) = B \cup C = A$. But $\top \nleq A$ in $\mathfrak{A}$, so we cannot intuitionistically infer $(A \Rightarrow B) \lor (A \Rightarrow C)$ from $A \Rightarrow (B \lor C)$.

-
Thank you for this answer. I understand it almost completely, except for one thing: You say that (A->B)=C but isn't it (A->B)=B? Since B is a subset of A? Not that this would matter for the argument following after it.. Just to be sure. – Maaike Jul 10 '12 at 14:16
@Maaike: Sorry, yes, of course. – Zhen Lin Jul 10 '12 at 14:35