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))You can add logical symbols by clicking the buttons above, or by using this correspondence:

Logical symbol | Keyboard character |
---|---|

→ | > |

∀ | @ |

∃ | ! |

¬ | - |

∧ | * |

∨ | + |