Bsrhrki

I am having trouble with this problem as I have just started doing logic. Is this the same as

P → Q

Prove: ￢P ∨ Q

?

In a natural deduction system (if that is what you are using) to prove a conditional, such as is P → Q, you must use a Conditional
Proof.

This takes the form of assuming the antecedent (that is P) aiming to derive the consequent (that is Q) through valid inferences (also using the premises; that is ￢P ∨ Q). Then discharging the assumption allow the deduction of the conditional (that is P → Q).

Now to prove Q from an assumption of P and the premise of ￢P ∨ Q, either use Disjunctive Syllogism, or a Proof by Cases.

In this particular case, the two statements are equivalent:
(￢P ∨ Q) ⊢ (P → Q) and (P → Q) ⊢ (￢P ∨ Q)
are both provably true statements, so (￢P ∨ Q) ≡ (P → Q).

But in order to prove that equivalence, we need to prove both directions separately. To see why, consider the case where instead of (￢P ∨ Q) and (P → Q), we have these two statements:

• P


• P ∨ Q

We can trivially prove that (P ∨ Q) follows from P; this is more or less the definition of the addition rule. But P does not necessarily follow from (P ∨ Q), since (￢P ∧ Q) also satisfies that clause. We can prove it in one direction, but they are not equivalent statements.

If one uses a truth table generator one can show that (¬P ∨ Q) ↔ (P → Q). To see this, insert the following input into the Stanford Truth Table Tool: (~P or Q)<=>(P=>Q)

This shows that the two statements are equivalent.

However, the question asks one to prove P → Q given the premise ¬P ∨ Q. Here is how one might do this using a natural deduction proof checker:

See the links below for an explanation of the rules used by this proof.

The proof would not be the same if we wanted to prove ¬P ∨ Q given the premise P → Q. That proof would look like this:

Although the statements are equivalent based on a truth table generator, the proofs from one to the other may be different depending on which is the premise and which the conclusion.

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/