0
$\begingroup$

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?

  • 1
    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!2012-07-10

2 Answers 2

4

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.

  • 0
    $B$y 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.2012-07-10
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)$.

  • 0
    @Maaike: Sorry, yes, of course.2012-07-10