Anyone here familiar with propositional logic?

**The Dude** · February 13, 2011, 01:30 PM

I guess this is the most fitting forum for this topic. I'm in need of some help here with natural deduction. I'll post the formula and my problem with it if there's anyone here who can help me out. Thanks for whoever can help in advance.

**John Doe** · February 13, 2011, 03:36 PM

I've studied some set theory (mainly in vector space) and when I wikied "propositional logic" it looked familiar. Don't get your hope to high with me though, it was years ago, I don't have my notes with me and I was stone 24/7 when I was a student. Post your problem, may be I still have a few neurons connected together.

**The Dude** · February 13, 2011, 04:16 PM

Haha, alright well I'll take any help I can get at this point. Basically I have to work out the following formula:

((P v Q) ^ (P v R)) => (P v (Q ^ R))

It's part of a much larger formula where I first tried to prove it in the exact opposite direction. I've pulled that off. But due to (P v Q) and (P v R) being disjunctions I can't properly isolate anything to then mash it together in another form. I get the feeling I'm overlooking something direly basic but I have no idea what. The general gist that I understand to be the direction I have to work in is something along these lines:

Line X (P v Q) => (P v (Q ^ R))
...
Line Y (P v R) => (P v (Q ^R))
...
Line Z ((P v Q) ^ (P v R)) => (P v (Q ^ R))

But that could be entirely wrong aswell. I don't know. XD

**John Doe** · February 13, 2011, 05:08 PM

((P v Q) ^ (P v R)) => (P v (Q ^ R))

In Boolean it's straight forward: ~~p.q+p.r = p.(q+r)~~
EDIT I was wrong, boolean formula is (p+q).(p+r)=p+q.r

You mentioned going the way back, usually you need use the ¬ somewhere along the line:
¬(P v Q) => ¬P ^ ¬Q

**The Dude** · February 13, 2011, 05:22 PM

Yeah I've been pondering negations. Wasn't sure of how to apply them though, I'll give your suggestion a go.

**John Doe** · February 13, 2011, 06:38 PM

Could you post the full problem please.

I've had a read at this and I would like to test what I understood on a concrete case, it looks fun, especially section 5 & 6, as for 7 it's a real

**The Dude** · February 14, 2011, 03:39 AM

Ah, sure. The full problem is this

The index of rules in the right column use dutch abbreviations but I guess it shouldn't be too hard to figure out what they mean since the symbols are included. I've managed to proceed up to line 17, as you can see I've proven the problem to be valid in one direction but can't do it the other way around. It shouldn't be difficult I feel, but for some reason I can't make it work. A double implication is effectively nothing but two implications in either direction joined together, so once I've proven both I'll be done.

**John Doe** · February 14, 2011, 06:28 AM

at line five you proved P v (Q^R) -> (PvQ)^(PvR)

now you want the other way

1 (PvQ)^(PvR) premise
2 PvQ
3 PvR
4 ¬P^¬Q negative 2
5 ¬P^¬R negative 3
6 ¬P^(¬Qv¬R) 4&5
7 Pv(Q^R) negative 6

I'm not 100% sure about line 6, may be it needs to be decomposed further.

EDIT: I think it should be like that

1 (PvQ)^(PvR) premise
2 PvQ
3 PvR
----------------------
4 ¬P^¬Q equivalent negative 2
5 ¬P^¬R equivalent negative 3
--------------------
6 (¬P^¬Q)v(¬P^¬R) 4&5
7 ¬P^(¬Qv¬R) equivalent distributive 6
8 Pv(Q^R) equivalent negative 7

I just realised that propositional logic is the way to solve a sudoku.