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

Question

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

Answer 1

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

Answer 2

Here is a formal proof in Fitch:

Answer 3

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/