Intuitionistic logic

Question

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?

Answer 1

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.

Answer 2

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