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.

2 Answers 2


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

enter image description here

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

Post a comment below if something isn't clear.

Here is a completion of the proof:

enter image description here


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

enter image description here

  • 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
  • I found the link on your profile and downloaded it. Here is the link for others: dcproof.com Oct 24, 2018 at 20:22
  • @FrankHubeny Apparently modal logic is just a working subset of FOL. See the answer to my question at math.stackexchange.com/questions/2976552/… So you should be able to do modal logic in DC Proof. You just have to avoid or restrict your use of the various rules of inference on the Logic menu. Oct 29, 2018 at 21:53
  • Modal logic has its diamond and box inference rules, but from what I've seen of it used in Fitch's Symbolic Logic they have introduction and elimination rules as well. I haven't started using your product, but I would like to get familiar with it. I just started following your blog. Oct 29, 2018 at 23:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .