1

giclab

Derive the following without assumptions:

¬∃xFx↔∀x¬Fx

How do I solve this derivation?

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.

enter image description here

"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/

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.