Enter a formula of standard propositional, predicate, or modal logic. The page will try to find either a countermodel or a tree proof (a.k.a. semantic tableau).
Examples (click!):
- (p∨(q∧r)) → ((p∨q) ∧ (p∨r))
- ∃y∀x(Fy → Fx)
- ∃y∃z∀x((Fx → Gy) ∧ (Gz → Fx)) → ∀x∃y(Fx ↔ Gy)
- N(0) ∧ ∀i(N(i) → N(s(i))) → N(s(s(s(0))))
- ∀x(∃y(Fy ∧ x=f(y)) → Fx) ↔ ∀x(Fx → Ff(x))
- □(p→q) → □p→□q
- ∀x□Fx → □∀xFx
- ∀y∃xFxy → ∃x∀yFxy
- p∨q, ¬p |= q
Entering formulas
To enter logic symbols, use the buttons above the text field, or type ~ for ¬, & for ∧, v for ∨, -> for →, <-> for ↔, ! for ∀, ? for ∃, [] for □, <> for ◇. You can also use LaTeX commands.
Premises
If you want to test an argument with premises and conclusion, use |= to separate the premises from the conclusion, and use commas to separate the premises. See the last example in the list above.
Syntax of formulas
Any alphabetic character is allowed as a propositional constant, predicate, individual constant, or variable. Numeral digits can be used either as singular terms or as indices (as in Fx1), but don't mix the two uses. '+', '*', and '-' can be used as function expressions. Predicates (except identity) and function terms must be in prefix notation. Function terms must have their arguments enclosed in brackets. So F2x17, Rab, R(a,b), Raf(b), F(+(1,2)) are ok, but not Animal(Fred), aRb, or F(1+2). (In fact, these are also ok, but they won't be parsed as you might expect.) The order of precedence among connectives is ¬, ∧, ∨, →, ↔. Association is to the right. Quantifier symbols in sequences of quantifiers must not be omitted: write ∀x∀yRxy instead of ∀xyRxy.
Supported logics
Besides classical propositional logic and first-order predicate logic (with functions and identity), a few normal modal logics are supported. If you enter a modal formula, you will see a choice of how the accessibility relation should be constrained. For modal predicate logic, constant domains and rigid terms are assumed.
Source code
The source is on github.
Contact
Comments, bug reports and suggestions are always welcome: