How to prove that (P v (P ^ Q)) iff P?

How to prove (P v (P ^ Q)) ≡ P? I am not sure how to get rid of proposition Q. I am allowed to use Leibniz and apply Substitution. I already came across most calculation rules in the book: Logical Reasoning A First Course.

I am looking for a hint. Not necessarily the answer!

Edit: I'm sorry, I forgot that it needed to be solved using calculations. And I don't have access to weakening rules.

You can try to prove it by cases (∨–Elim). The general form is:

If you have: ⊢ (A ∨ B), A ⊢ C, and B ⊢ C

Then you can conclude: (A ∨ B) ⊢ C

This means that if you've proved (A ∨ B) and you have proved (i) C from assumption A, and (ii) C from assumption B, then you have proved C from assumption (A ∨ B). This rule will give you the → direction.

To get the other direction, that is, from P to P ∨ (P ∧ Q), there is a rule (∨–Intro) to the effect that:

If you have: ⊢ A

Then you can conclude: ⊢ A ∨ B                                                                          (for any sentence B)

Needless to say, if your system doesn't have those rules, then if it's complete (in the technical sense), then there must be some other set of rules or axioms that will allow you to prove the equivalence; your task in that case is to find those rules and apply them or find those axioms and instantiate them with the appropriate sentence letters.

I would suggest the following strategy derive two implications by making two arguments by assumption: Side 1:

``````(1) | P  as assumption
(2) | P  v (P ^ Q) by vI on 2
(3) P -> (P v (P ^ Q)) by proof 1-2
``````

Side 2:

``````(1) | P v (P ^ Q) as assumption
(2) | (P v P) & (P v Q) distribution on 1
(3) | P v P &E on 2
(4) | P by simplification of 3
(5) (P v (P ^ Q)) -> P by proof 1-4
``````

and you should be able to do the rest.

• this is the right answer.
– user5172
Mar 19 '14 at 17:25

Make a truth-table for the two propositions and see that they always share the same truth-values at each row.

• If you don't want to use a truth-table, then you'll have to specify the rules of inference or equivalence that you're permitted to use. For instance, you might use distribution to obtain the equivalence with (P v P) ^ (P v Q) which by idempotence is equivalent to P ^ (P v Q). This implies P, so you get that the left-hand expression implies the right. In the other direction, the result is immediate by the fact that P implies P v phi where phi is any sentence. Mar 17 '14 at 19:53

Why not do it in words?

If both P and Q are true then P is true. A fortiori if either P is true or both P and Q are true then P is true.

Converse is even easier - if P is true then either P is true or any R (including both P and Q) is true.

Here is a shortish proof starting with an assumption that the proposition is false:

`````` 1. |asm: ¬((P v (P ^ Q)) ≡ P)
2. |∴ (P v (P ^ Q)) v P)                       {from 1}
3. |∴ ¬((P v (P ^ Q)) ^ P)                     {from 1}
4. ||asm: P                                    {break 2}
5. ||∴ ¬(P v (P ^ Q))                          {from 3 and 4}
6. ||∴ ¬P                                      {from 5}
7. |∴ ¬P                                       {from 4; 4 contradicts 6}
8. |∴ (P v (P ^ Q))                            {from 2 and 7}
9. |∴ (P ^ Q)                                  {from 7 and 8}
10. |∴ P                                        {from 9}
11. ∴ ((P v (P ^ Q)) ≡ P)                       {from 1; 7 contradicts 10}
``````

Here is a proof that uses four different rules: conjunction elimination (∧E), disjunction elimination (∨E), disjunction introduction (∨I) and biconditional introduction (↔I). See forall x: Calgary Remix for a description of these rules.

Regarding the concern: I am not sure how to get rid of proposition Q.

Note that "Q" was not used to help the proof along. It appeared on line 3 as part of the second case to consider in the disjunction elimination of line 1, but as a conjunction with "P" it could be ignored since all we needed was "P".

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/