1
$\begingroup$
  1. $\quad\bullet\;p\rightarrow\left(q\wedge r\right)$ --- Assumption
  2. $\quad\bullet\quad\bullet\; p$ --- Assumption
  3. $\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,2
  4. $\quad\bullet\quad\bullet\; q$ --- $\wedge$ Elim 3
  5. $\quad\bullet\quad\bullet\; r$ --- $\wedge$ Elim 3
  6. $\quad\bullet\; p\rightarrow q$ --- $\rightarrow$ Intro 2,4
  7. $\quad\bullet\; p\rightarrow r$ --- $\rightarrow$ Intro 2,5
  8. $\quad\bullet\;\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)$ --- $\wedge$ Intro 6,7
  9. $\;\left(p\rightarrow\left(q\wedge r\right)\right)\rightarrow\left(\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)\right)$ --- $\rightarrow$ Intro 1,8

I'm concerned about introducing two implications(6 & 7) from same subproof.

$\endgroup$
  • 1
    $\begingroup$ I don't think there is any problem with introducing two implications from the same subproof. $\endgroup$ – Kenny Lau Sep 14 '17 at 5:07
1
$\begingroup$

Semantically that is of course perfectly valid, and it is indeed no problem in most formal proof systems!

$\endgroup$
1
$\begingroup$

Well, of course you can do it without introducing two implications from the same subproof:

  1. $\quad\bullet\;p\rightarrow\left(q\wedge r\right)$ --- Assumption
  2. $\quad\bullet\quad\bullet\; p$ --- Assumption
  3. $\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,2
  4. $\quad\bullet\quad\bullet\; q$ --- $\wedge$ Elim 3
  5. $\quad\bullet\; p\rightarrow q$ --- $\rightarrow$ Intro 2-4
  6. $\quad\bullet\quad\bullet\; p$ --- Assumption
  7. $\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,6
  8. $\quad\bullet\quad\bullet\; r$ --- $\wedge$ Elim 3
  9. $\quad\bullet\; p\rightarrow r$ --- $\rightarrow$ Intro 6-8
  10. $\quad\bullet\;\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)$ --- $\wedge$ Intro 5,9
  11. $\;\left(p\rightarrow\left(q\wedge r\right)\right)\rightarrow\left(\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)\right)$ --- $\rightarrow$ Intro 1-10
$\endgroup$
0
$\begingroup$

The OP is concerned with the following:

I'm concerned about introducing two implications(6 & 7) from same subproof.

Here is a proof checker that accepts those two implications from the same subproof.

enter image description here


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/

$\endgroup$

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.