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.

@x!y(x=y)

@x(Ax > (Ax*Bx))

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

Logical symbol	Keyboard character
→	>
∀	@
∃	!
¬	-
∧	*
∨	+

    formula with added parentheses: (@x((Ax)>((Ax)*(Bx))))
Tree representation of your formula:
∀
├── x
└── →
    ├── A
    │   └── x
    └── ∧
        ├── A
        │   └── x
        └── B
            └── x
Theoremhood: false
Counter-example:
  c0:
    B: false
    A: true