Monadic predicate logic theoremhood checker

Monadic predicate logic (with identity) is decidable (Boolos, Burgess, and Jeffrey 2007, Ch. 21. The result goes back to Löwenheim-Skolem 1915).

This website lets you check whether a formula is a theorem. If it's not a theorem, you will be shown a counter-example.

Add symbols:
Propositional logic sentence letters such as P are not currently supported. Only predicate logic sentence letters with a variable, such as Px, are supported.
Example formulae:
You can add logical symbols by clicking the buttons above, or by using this correspondence:
Logical symbol   Keyboard character
¬ -
By Tom Adamczewski. Code on GitHub.
Leave feedback. I read every message.