Can p → q |- ¬p ∨ q in intuitionistic logic?

December 1, 2016 3:42 PM

Can you prove p → q |- ¬p ∨ q without using the law of the excluded middle or its equivalent? I'm going through a logic book (introductory) and I have an intuition that proving this isn't possible constructively, but I'd like a confirmation.
posted by Monday, stony Monday to Computers & Internet (14 answers total)

I don't know what the |- symbol means here?
posted by RustyBrooks at 4:27 PM on December 1, 2016

Certainly you have p → p, so this would let you get ¬p ∨ p.
posted by eruonna at 4:27 PM on December 1, 2016 [1 favorite]

I don't know what the |- symbol means here?
I think it's a metalanguage symbol for deduction.

Is the truth table for "->" different in intuitionistic logic? Because in classical logic, your formula is a tautology. "p->q" is true where p is false, or where q is true. It is only false where p is true and q is false. And " ¬p ∨ q" has the exact same truth-conditions .
posted by thelonius at 4:36 PM on December 1, 2016

Oh, I see - appealing to my tautology argument misses the point; you can't do that in intuitionistic logic.
posted by thelonius at 4:39 PM on December 1, 2016

Response by poster: "|-" is my rendition of "entails".
posted by Monday, stony Monday at 5:00 PM on December 1, 2016

I don't think so. I'm not an expert in this but I think of intuitionistic logic as replacing the notion of "true" by "provable." There could certainly be a proof that p -> q without there being a proof of "not p" or a proof of q.
posted by escabeche at 5:26 PM on December 1, 2016 [3 favorites]

You can find the theorems for interdefinability of operators here
I get this far

p → q ⊢ ¬(p ∧ ¬q)
p → q ⊢ ¬(¬p ∨ ¬¬q)

But then I'm stuck because I can't remove the outer negation.
posted by jouke at 5:27 PM on December 1, 2016 [1 favorite]

Best answer: It can't be done.

van Dalen in Logic and Structure has a section on intuitionistic logic, and he has a list of theorems that can be proven. As you can see at (13), you can prove the reverse, but not what you have.

Here's an image of the page: http://imgur.com/a/7IuIS
posted by Dalby at 6:15 PM on December 1, 2016 [6 favorites]

Response by poster: Thank you!
posted by Monday, stony Monday at 6:28 PM on December 1, 2016 [1 favorite]

i don't know if this is a help, but when i was learning this stuff i used ttfp (free download). looking at my notes, i apparently got some useful help from sci.logic on google groups. (tbh i didn't get very far and don't remember anything now).
posted by andrewcooke at 2:23 AM on December 2, 2016

Yeah, part of the point of intuitionistic logic is that the law of the excluded middle ISN'T a theorem.
posted by Elementary Penguin at 3:36 AM on December 2, 2016

Response by poster: Thank you for the reference, Dalby! Just a little bit later I had to prove that ¬(p ∧ q) → ¬p ∨ ¬q, and I wondered if I could do it without the LEM -- turns out I can't, as shown in van Dalen.
posted by Monday, stony Monday at 8:06 PM on December 2, 2016

While of course Dalby is correct (and van Dalen's book is a great reference for this kind of thing, as you now know!), and escabeche has exactly the right intuitive idea why, no one in the thread actually proved that you can't do it. So even though this is marked "answered," as an ex-logician, I had to add a proof that this is unprovable, based on the soundness¹ of intuitionistic logic with respect to Kripke semantics².

It's gross to write math (or logic) without using LaTeX, which MeFi doesn't support, so here's a PDF. Hope this helps illuminate why you can't prove this!

[1] Sometimes there are other, non-semantic, purely syntactic ways to show unprovability, which would technically require fewer concepts than techniques like this one do, but I'm not aware of a purely syntactic proof for this, and for interesting logics they're usually more complicated anyway.
[2] I'm using Kripke semantics (Wikipedia has an intro, though their notation is different), just because van Dalen uses them and you are looking at his work, but you can use any semantics for intuitionistic logic to do this. In particular, if you're a math person and have a background in analysis or topology these Heyting algebra semantics might be an easy way to understand this. You can translate my basic techniques in the argument to the the open-subsets-of-R Heyting algebra which that Wikipedia article introduces and it amounts to the same thing, if you're more comfortable with that.
posted by acroyear2 at 11:25 PM on December 2, 2016 [2 favorites]

Agh, just noticed that there is a mistake in the PDF--in the definition of soundness, I have things backwards on what that means with respect to semantic entailment. Soundness ensures the fact that when a formula B is provable from a formula A , B is semantically entailed by A, not the other way around as I have it written. (This other direction--truth implying provability--is called "completeness" and is much more complicated.)
posted by acroyear2 at 12:21 AM on December 3, 2016