Derive the following without assumptions:
¬∃xFx↔∀x¬Fx
How do I solve this derivation?
1
3
The following is a proof using Klement's proof checker and the rules described in forall x. You may need to use something different with the software you are using, but this may give you an idea how to proceed.
"CQ" refers to the change of quantifiers rule. A derivation of the CQ rule is given in forall x (see link below) on pages 260-1.
Each conditional is derived separately. The biconditional introduction (line 5) is permitted by these rules when I reference both of the conditionals on lines 1-2 and lines 3-4.
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/
