1

⊢(∀x)(Fx V ~Fx) How can I prove this with natural deduction?

1
  • I made an edit for spelling. You may roll this back or continue editing if my edit was inappropriate. Welcome to this SE! Commented Jun 12, 2018 at 14:29

3 Answers 3

2

It depends on the rules you are allowed to use...

Here is a proof using Double Negation elimination :

1) ¬ (Fx ∨ ¬Fx) --- assumed [a]

2) Fx --- assumed [b]

3) Fx ∨ ¬Fx --- from 2) by ∨-intro

4) ⊥ --- from 1) and 3)

5) ¬Fx --- from 2) and 4) by ¬-intro, discharging [b]

6) Fx ∨ ¬Fx --- from 5) by ∨-intro

7) ⊥ --- from 1) and 6)

8) Fx ∨ ¬Fx --- from 1) and 7) by ¬¬-elim, discharging [a]

9) ∀x (Fx ∨ ¬Fx) --- from 8) by ∀-intro

3
  • Is it possible to assume ¬ (Fx ∨ ¬Fx) without arbitrary name? I can use 12 basic rules of natural deduction.
    – abed199605
    Commented Jun 12, 2018 at 14:46
  • @abed199605 - you can assume ¬ (Fa ∨ ¬Fa) with a arbitrary: nothing changes. Commented Jun 12, 2018 at 14:48
  • Oh, I see. Thanks for your answer! It is very helpful!
    – abed199605
    Commented Jun 12, 2018 at 14:53
1

Here is a formal proof in Fitch:

enter image description here

1

The question is: ⊢(∀x)(Fx V ~Fx) How can I prove this with natural deduction?

I will provide two proofs, one indirect and one direct.

The indirect proof uses conversion of quantifiers (CQ), the De Morgan rule (DeM), double negation elimination (DNE), indirect proof (IP) as well as introduction and elimination rules.

enter image description here

The next proof uses the law of the excluded middle (LEM). It may seem that is what we are trying to show, but the question seems rather to be can we use the universal introduction rule given the law of the excluded middle.

enter image description here

See forall x: Calgary Remix for more information and examples of how to use these rules.


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/

You must log in to answer this question.

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