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:

@x!y(x=y)

@x(Ax > (Ax*Bx))

!x(Ax*Bx) > @x(Ax+Bx)

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.