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

⊢(∀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. 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! Jun 12 '18 at 14:53

Here is a formal proof in Fitch: 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. 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. 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/