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
→	>
∀	@
∃	!
¬	-
∧	*
∨	+

    formula with added parentheses: (@x(!y(x=y)))
Tree representation of your formula:
∀
├── x
└── ∃
    ├── y
    └── =
        ├── x
        └── y
Theoremhood: true

By Tom Adamczewski. Code on GitHub.

Leave feedback. I read every message.