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, rigid terms are assumed. By default, the quantifiers are given a "possibilist" interpretation with a constant domain across worlds. If you enter a quantified modal formula, a checkbox lets you switch to an "actualist" interpretation on which the quantifiers at a world range only over the individuals that exist at that world. Behind the scenes, this is implemented by relativizing all quantifiers to an existence predicate E: ∀xA becomes ∀x(Ex→A) and ∃xA becomes ∃x(Ex∧A); the relativized formulas are what you will see in the tableau. World domains are allowed to be empty, predicates may be true of individuals that don't exist at the world of evaluation, and no existence assumptions are made for singular terms.
Source code
The source is on github.
Contact
Comments, bug reports and suggestions are always welcome: