3
$\begingroup$

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)

$\endgroup$
1
  • $\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, 2015 at 23:46

5 Answers 5

Reset to default
4
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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)
$\endgroup$
5
  • $\begingroup$ The user doesn't have the deduction theorem. The user has conditional introduction. $\endgroup$
    – Doug Spoonwood
    Nov 5, 2015 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, 2015 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, 2015 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, 2015 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, 2015 at 14:10
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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
$\endgroup$
0
$\begingroup$

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
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .