# Proof of (P → Q) from ¬P?

I'm trying to figure out how to prove P → Q from just ¬P. I can deduce it using informal logic. Since the only way a conditional is False is in the case of T → F, if P is False, P → Q must always be true.

But I can't seem to prove it formally using a combination of these:(negation/conjunction/disjunction/conditional - introduction/elimination).

Ultimately I want to use this to prove ¬(P → Q) → P by negation elimination.

-
Contrapositive you mean? – K.Power Mar 3 at 21:18
I could not prove it, it seems to me like taking a hyptothesis for granted. – Programmer 400 Mar 3 at 21:27
I'm trying to prove P from assumptions: ¬P, ¬(P → Q), (P → Q) and negation elimination. But I don't know how to get to (P → Q). – user1869558 Mar 3 at 21:27
@user1869558 I want to recommend this text about similar problems: amazon.com/Modern-Logic-Text-Elementary-Symbolic/dp/0195080297 – Programmer 400 Mar 3 at 21:28
@user1869558 What do you mean by "Prove $P$ from assumptions: $\neg P$, ..."? – Adam Francey Mar 3 at 21:53

I’m going to answer on the basis of the derivational system suggested by the terminology that you’re using for your rules. What I’m doing may not be quite like what you’ve been taught, but I hope that it’s at least close.

You have $\neg P$ as hypothesis, and from that you want to derive $P\to Q$. To get $P\to Q$ by conditional introduction, you’ll need to start by taking $P$ as an assumption:

\begin{align*} &1.\quad \neg P\tag{Premise}\\ &2.\quad|\,P\tag{Assumption} \end{align*}

We want to end up concluding $Q$ within the scope of the assumption, since conditional introduction will then give us $P\to Q$. Introduce a second assumption layer:

\begin{align*} &1.\quad \neg P\tag{Premise}\\ &2.\quad|\,P\tag{Assumption}\\ &3.\quad||\,\neg Q\tag{Assumption}\\ &4.\quad||\,P\\ &5.\quad||\,\neg P\\ &6.\quad||\,\bot\\ &7.\quad|\,\neg\neg Q\\ \end{align*}

Here $\bot$ is a standard symbol for a contradiction, and deriving the contradiction from the assumption $\neg Q$ gives me $\neg\neg Q$ by negation introduction, thereby discharging the inner assumption; I’ll leave the other justifications so far to you.

Now you need some steps deriving $Q$ from $\neg\neg Q$; I’ll leave them to you. (You may have done or seen this derivation already.) Once those are in place, you can discharge the outer assumption by conditional introduction to get $P\to Q$.

-
I like this, and it answers the nonintuitive side of what is being asked really well: supposing you can discharge an assumption (in favor of its negation) once a contradiction is reached, the "trivial truths" arise by assuming an arbitrary conclusion once you have already secretly-derived a contradiction but not yet asserted it -- then negating that arbitrary conclusion gives you a trivial truth. – CR Drost Mar 3 at 23:16

The details of the proof will depend on the proof system you want to use.

• Clue 1: P → Q is classically equivalent to $(\neg P \vee Q)$
• Clue 2: $(\neg P \vee Q)$ is a dilution of $\neg P$
-

The simplest way would be to use a truth table, which is just as rigorous if not as appealing. If you can't though then I'd consider the following.

$$\neg P \to Q \lor \neg P$$

and then using a simple variation of what is considered a definition by some texts $$Q \lor \neg P \iff \neg(\neg P)\to Q$$ implies what you want.

-
What if P is false? – Programmer 400 Mar 3 at 21:51
We're given that P is false? That's the starting point of the question – K.Power Mar 3 at 21:56
But how can you know P is distinct from Q? – Programmer 400 Mar 3 at 21:59
@Programmer400 What is the problem if $P$ is false? – Marco Disce Mar 3 at 22:15
"which is just as rigorous" -- provided that you've already proved the theorem that every tautology is provable in propositional calculus. The proof of that theorem is potentially a moment at which all this business about manipulating axioms using rules of procedure goes out the window so far as propositional calculus is concerned, and we just throw truth tables at anything with a manageable number of atoms ;-) – Steve Jessop Mar 4 at 2:22