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)*(Bx)))>(@x((Ax)+(Bx)))
Tree representation of your formula:
→
├── ∃
│   ├── x
│   └── ∧
│       ├── A
│       │   └── x
│       └── B
│           └── x
└── ∀
    ├── x
    └── ∨
        ├── A
        │   └── x
        └── B
            └── x
Theoremhood: false
Counter-example:
  c0:
    B: true
    A: true
  c1:
    B: false
    A: false