# Conditional Proof and lemmas

I'm trying to solve a problem of propositional logic. The problem is this:

$(H\vee P \vee L) \wedge (¬H \Rightarrow ¬P \vee ¬L ) \wedge (¬L\Rightarrow ¬P ) \wedge ¬H \Rightarrow L$

So I'm solving this problem through a conditional proof where I assume the antecendent and prove the consequent. In order to do this I proposed a lemma:

Lemma 1: $¬P$

$¬H \Rightarrow ¬P \vee ¬L$

$=\langle Def \Rightarrow \rangle$

$¬¬H \vee ¬P \vee ¬L$

$=\langle Double ¬\rangle$

$H \vee ¬P \vee ¬L$

$=\langle \text{Assumption: } ¬L\Rightarrow ¬P \rangle$

$H \vee ¬P \vee ¬P$

$=\langle \text{Assumption: } ¬H \text{ is true then } H \text{ is false }\rangle$

$false \vee ¬P \vee ¬P$

$=\langle \text{Identity }\vee\text{ and Idempotency}\rangle$

$¬P$

My first question is: Is valid to apply this assumption in the way that I did: $\langle\text{ Assumption: }¬L\Rightarrow ¬P \rangle$ and just replace ¬L by ¬P? I know Modus Ponens but don't know if it's valid in this case. If it is valid, can I always do this? If it's not, why?

My second question is: Now that I proved ¬P can I use it in another lemma by replacing it by true? Lemma 1 was enough to proof that ¬P is true?

Meaning:

Lemma 2: $L$

$H\vee P \vee L$

$=\langle \text{Lemma 1 : }¬P\equiv true, P\equiv false \rangle$

$H\vee false \vee L$

I want to know if this steps that I'm doing are valid or if there is another way to do them in a formal way.

(I don't know if this is relevant, but I'm studying with the book A Logical Approach to Discrete Math by David Gries and Fred Schneider).

Thank you.

• To make the text in the math environment more readable, use \text{} to enclose it. If the math on either side comes too near, use \; to make whitespace. – Bobson Dugnutt Feb 21 '16 at 23:01
• Thank you! I will edit it. – user3424545 Feb 21 '16 at 23:02

So, are you taking that first formula (the big conjunction) as hipotesis? In the affirmative case it is ok what you did when you replaced $\lnot L$ by $\lnot P$ in the disjunction but I can't see how from $H \lor \lnot P \lor \lnot P$ whic is equivalent to $H \lor \lnot P$, you conclude $\lnot P$.

For the second lemma, if you have already proved $\lnot P$ and you assume $H \lor P \lor L$ then it follows $H \lor L$

• Yes, the big conjuntion is my hipotesis. Ow, sorry, I missed a part of my lemma. I'm going to edit it. – user3424545 Feb 21 '16 at 23:24
• Sorry to ask, but I can always replace ¬L by ¬P if my hipotesis contains $¬L \Rightarrow ¬P$? – user3424545 Feb 21 '16 at 23:29
• Ok, but now your conclution is valid only under the assumption that $H$ is false, so if you want that to be a valid step you must add $\lnot H$ to your premises. To what you are asking: yes, you cand do that, it is always valid. – la flaca Feb 21 '16 at 23:34

Here are the questions:

My first question is: Is valid to apply this assumption in the way that I did: ⟨ Assumption: ¬L⇒¬P⟩ and just replace ¬L by ¬P? I know Modus Ponens but don't know if it's valid in this case. If it is valid, can I always do this? If it's not, why?

There is no rule in the proof checker that I am using that would permit that substitution. So I would have to try something different to derive $$¬P$$ (or find another proof checker). So, the step would not always be valid. It would depend on the rules one has available.

Here is what I would do: I would use modus ponens (conditional elimination: →E) and then check the cases on line 5. In each case I would need to derive $$¬P$$.

My second question is: Now that I proved ¬P can I use it in another lemma by replacing it by true? Lemma 1 was enough to proof that ¬P is true?

One could use $$¬P$$ to continue the proof to derive $$L$$. Here is one way to do that. I added $$¬P$$ to the premises to get the following: The DS is disjunctive syllogism. Note that after combining these two proofs together, it would take only 11 lines in this proof checker to derive $$L$$ counting four lines to state the premises. It may not be worth breaking this up into two parts.

The above proofs would be another way to approach the problem.

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