# Logic proof on biconditional [closed]

(P → Q) ↔ ( ¬P ∨ Q) is the goal, there's no premises

3.||_ P......................

4., _ ~P....................

5., |....................RULE: | INTRO 3, 4

6., Q......................RULE: | ELIM 5

7.|| Q.......................RULE: ?

8.| Q........................RULE: ?

9.| ~P V Q...................RULE: V INTRO 8 END 1ST SUBPROOF

10.|_ ~P V Q.................

11.||_ ~P....................

12., _ P....................

13., |...................RULE: | INTRO 11, 12

14., P -> Q................RULE: | ELIM 13

15.|| P ->Q..................RULE: ?

END 1ST ASSUMPTION

16.||_ Q.....................

17., _ ~Q...................

18., |...................RULE: | INTRO 16, 17

19., P -> Q................RULE: | ELIM 18

20.|| P -> Q.................RULE: ? END 2ND ASSUMPTION

21.|P -> Q...................RULE: V ELIM 10, 11-15, 16-20

1. (P -> Q) <-> (~P V Q)....RULE: <-> INTRO 2-9, 10-21

This is what I have so far, I am missing a few rules on how it can be apply, if anyone can help :)

• Welcome to Philosophy Stack Exchange. It will be easier to help with your question if you state how your text has defined P --> Q or the context in which the result is stated. – Nick Dec 11 '15 at 3:36
• I don't particular understand the syntax you're using. You might want to work on the formatting. Also, where is your list of rules coming from? – virmaior Dec 11 '15 at 9:58

The best way to do the proof depends greatly on what rules of inference you are allowed to use and whether you can do proof by truth tables. For general information, see How do I check if two logical expressions are equivalent?

# With Material Implication

The simplest proof is you are allowed to do material implication:

`````` 1. | P  -> Q                 A
2. | ~P v Q                  Material Implication 1
3. (P -> Q) -> (~P v Q)      CP 1,2
4. | ~P v Q                  A
5. | P -> Q                  Material Implication 4
6. (~P v Q) -> (P -> Q)      CP 4,5
7. (P -> Q) <--> (~P v Q)    Biconditional Introduction 3,6
``````

# Without Material Implication with DeMorgan

`````` 1. | P  -> Q                 A
2. | | ~ (~P v Q)            A
3. | | ~~P & ~Q              Dem 3
4. | | ~~P                   &E 3
5. | | P                     DN 4
6. | | Q                     MP 1,5
7. | | ~Q                    &E 3
8. | (~ P v Q)               Contradiction Elim. 2-7
9. (P -> Q)  -> (~P v Q)    CP 1-8
``````

And then repeat similarly for the opposite side...

# Truth Table Proof

``````P   |  Q  |  P -> Q  | ~P v Q
T   |  T  |    T     |    T
T   |  F  |    F     |    F
F   |  T  |    T     |    T
F   |  F  |    T     |    T
``````