# How to get proof using proof editor and checker

How can I use Natural deduction proof editor and checker or The Logic Daemon to derive the given conclusion from the given premise:

(∃x) ( Fx ∙ (y) (Fy → y = x) )

/ (∃x) (y) (Fy ≡ y = x)

It tells me that my premise is not well formed. Anyone who knows how to use these tools, your help would be greatly appreciated.

For the first link here is a screenshot of how to enter the premise and conclusion:

Note that the FOL (First Order Logic) button is on, not the TFL (Truth Functional Logic) button. The default is TFL. That would trigger a premise not being well formed message.

Note that "(y)" is entered as "Ay" without parentheses and with and "A".

Note there are no parentheses around "Ex".

Here is a completion of the proof:

Reference

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

• You also need to prove the converse for equivalence. Oct 24, 2018 at 16:52
• @DanChristensen Yes, I do see that a converse might be needed here. Thanks for pointing it out. Oct 24, 2018 at 19:45

Using DC Proof 2.0 (another proof editor and checker)

Color-coded variables

• Black = bound variable
• Green = free variable to which either universal or existential generalizations may be applied
• Red = free variable to which only existential generalizations may be applied

• Do you have a link to this? I am also looking for a proof checker for modal logic. Oct 24, 2018 at 19:36
• DC Proof 2.0 is based on classical logic, but it is possible to define your axioms in it. Send me a full list of your axioms and I will see what I can do to get you started. To download DC Proof and for a contact link, visit my homepage. Oct 24, 2018 at 20:18