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

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

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

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

Here is a formal proof in Fitch:

enter image description here


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.


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/

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.