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?

  • 0
    Which kind of counterexamples do you recognize?2012-07-10
  • 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
    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).2012-07-10
  • 0
    @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.2012-07-10
  • 0
    You say "reckless" as if that was a technical term. I'm not aware of what it would mean.2012-07-10
  • 0
    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.2012-07-10
  • 0
    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.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
    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.2012-07-10
  • 0
    @Maaike: Sorry, yes, of course.2012-07-10