I'm stuck with a big proof in my homework. I have to use natural deduction to prove something, and I think if I can prove this somehow then I can finish the full proof. Can anyone help?

P v Q, ¬P : Q

I have to do it from first principles though, I can't use DM's laws.

I can use the following rules:

implication intro, implication elim, conjunction intro, conjunction elim, disjunction intro, disjunction elim, (double) negation elimination, negation introduction (using Reductio Ad Absurdum)

  • $\begingroup$ Well, obviously you have to use disjunction elimination. So you need a way to deduce $Q$ from $P, \lnot P$. $\endgroup$ – Zhen Lin Nov 4 '15 at 23:46

The proof goes as follow:

  1. $p\lor q$ [premise]
  2. $p$
    2.1. $\neg p$ [premise]
    2.2 $\bot$ [$\rightarrow_e$ 2 and 2.1]
    2.3. $q$ [absurdity rule 2.2]
  3. $q$
    3.1. $q$ [copy 3]
  4. $q$ [$\lor_e$ 2 - 3.1]

I hope it is clear what I meant. Any further questions/comments?


You can show that $P\Rightarrow Q$ with those assumptions. You just assume $P$ and note that $\neg Q\Rightarrow P$ and $\neg Q\Rightarrow\neg P$ (via implication introduction via the assuming $\neg Q$) and conclude that $Q$.

Then you have by the implication introduction that the asssuming $P$ and that $Q$ is amoung your assumption that $P\implies Q$. But as $Q\Rightarrow Q$ also holds $Q$ follows from disjunction elimination.

  1. $P\lor Q, \neg P, P, \neg Q \vdash \neg P$
  2. $P\lor Q, \neg P, P \vdash \neg Q \Rightarrow \neg P$ (1+II)
  3. $P\lor Q, \neg P, P, \neg Q \vdash P$
  4. $P\lor Q, \neg P, P \vdash \neg Q \Rightarrow P$ (3+II)
  5. $P\lor Q, \neg P, P \vdash \neg\neg Q$ (2+4+NI)
  6. $P\lor Q, \neg P, P \vdash Q$ (5+DNE)
  7. $P\lor Q, \neg P \vdash P\Rightarrow Q$ (6+II)
  8. $P\lor Q, \neg P, Q \vdash Q$
  9. $P\lor Q, \neg P \vdash Q\Rightarrow Q$ (8+II)
  10. $P\lor Q, \neg P \vdash P\lor Q$
  11. $P\lor Q, \neg P \vdash Q$ (7+9+10+DE)
  • $\begingroup$ The user doesn't have the deduction theorem. The user has conditional introduction. $\endgroup$ – Doug Spoonwood Nov 5 '15 at 13:26
  • $\begingroup$ @DougSpoonwood My understanding is that "deduction theorem", "conditional introduction" (which by the way wasn't mentioned eiter) and "implication introduction" is different names for basically the same thing: you assume the premise $P$ and by being able to prove $Q$ by doing so you can conclude $P\Rightarrow Q$. $\endgroup$ – skyking Nov 5 '15 at 13:37
  • $\begingroup$ Proof-theoretically, The Deduction Theorem consists of a meta-theorem that you can metalogically prove for an axiomatic system. It says that given a set of premises $\gamma$, two well-formed formulas P and Q, and letting $\vdash$ stand for syntactic consequence, then if ($\gamma$ U {P}) $\vdash$ Q, then $\gamma$ $\vdash$ (P $\rightarrow$ Q) for the system at hand. The user probably has a natural deduction system with no axioms and thus can't metalogically prove the Deduction Theorem (unless you count circular reasoning). $\endgroup$ – Doug Spoonwood Nov 5 '15 at 13:47
  • $\begingroup$ @DougSpoonwood And what is "conditional introduction" and "implication introduction"? It's basically the same usage-wise, but if it makes you happier I've removed references to the DT and calls it II instead. $\endgroup$ – skyking Nov 5 '15 at 13:56
  • $\begingroup$ Conditional introduction and implication introduction consist of transformation rules, or in other terms functions that transform certain premises and return a conclusion. They say from (γ U {P}) ⊢ Q we may infer γ ⊢ (P → Q) or with $\gamma$ understood from P $\vdash$ Q we may infer $\vdash$ (P $\rightarrow$ Q). The Deduction Meta-Theorem doesn't qualify as a transformation rule or function in that way. $\endgroup$ – Doug Spoonwood Nov 5 '15 at 14:10

Natural deduction? If you have the choice between p and q, probably both but p is not allowed then q remain to be chosen. That is the natural argument which can be formalized: $[p\vee q]\wedge \neg p\equiv [p\wedge\neg p]\vee [\neg p\wedge q]$. There it is.


I use Polish notation. The formation rules go:

  1. All lower case letters of the Latin alphabet stand as well-formed formulas.
  2. If $\alpha$ and $\beta$ qualify as formulas, so do A$\alpha$$\beta$, C$\alpha$$\beta$, and N$\alpha$.
assumption                        1 Apq
assumption                        2 Np
hypothesis                        3 | p
hypothesis                        4 || Nq
4, 3, 2, negation introduction    5 | NNq
5 negation elimination            6 | q
3-6 conditional introduction      7 Cpq
hypothesis                        8 | q
8-8 conditional introduction      9 Cqq
1, 7, 9 disjunction introduction 10 q

P ∨ Q, ~P : Q

{1}       1.   P ∨ Q                       Prem.
{2}       2.   ~P                          Prem.
{3}       3.   P                           Assum. (1. 1st Disj.)
{4}       4.   ~Q                          Assum.
{3,4}     5.   P & ~Q                      3,4 &I
{3,4}     6.   P                           5 &E
{3}       7.   ~Q → P                      3,4 CP
{2,3}     8.   ~~Q                         2,7 MT
{2,3}     9.   Q                           9 DNE (1. 1st Concl.)
{10}      10.  Q                           Assum. (1. 1st Disj.; 1st Concl.)
{1,2}     11.  Q                           1,3,9,10,10 ∨E

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.