working on logic - fitch system

Question

Struggling with logic and fitch system,

I am trying, given (p ⇒ ¬q) and (¬q ∧ p ⇒ r) and p, to use the Fitch System in order to prove r.

Any ideas on how I should proceed?

Answer 1

1. (p ⇒ ¬q)
2. (¬q ∧ p ⇒ r)
3. p
4. ¬q (1 3 Implication Elimination)
5. ¬q ^ p (2 4 And Introduction)
6. r (2 5 Implication Elimination) ---> END

Answer 2

You may also try other formal proof systems that are available as computer-implemented proof checkers. Using the structured proof language of Isabelle you can write your proof like this:

theory Scratch
imports Main
begin

notepad
begin
  assume 1: "p ⟶ ¬ q"
    and 2: "¬ q ∧ p ⟶ r"
    and 3: p
  have "¬ q" using 1 and 3 ..
  then have "¬ q ∧ p" using 3 ..
  with 2 have r ..
end

end

Answer 3

The following proof uses Klement's Fitch-style natural deduction proof checker. Explanation of the rules are available in forallx.

The first three lines are the premises. Line 4 results from conditional elimination (→E), line 5 from conjunction introduction (∧I) and the final line from conditional elimination again.

---

References

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/