Instructions

These tools share the same syntax normalizer. You can type Unicode symbols (¬,∧,∨,→,∀,∃) or use the ASCII shortcuts below. Variables can be any letters or alphanumerics (e.g. x,y,z,x1).

Common syntax & shortcuts

MeaningUnicodeASCII you can type
not¬φ~φ, not φ
andφ ∧ ψφ /\ ψ, φ & ψ, φ and ψ
orφ ∨ ψφ \/ ψ, φ v ψ, φ or ψ
impliesφ → ψφ -> ψ, φ => ψ
forall∀x φforall x φ, Axφ
exists∃x φexists x φ, Exφ
predicatesRxy, F xapplication by juxtaposition or parentheses
propositional constantsP, Q, Rtreated as 0-ary predicates

We also accept spaced forms such as ∀ x (Fx → Gx). The shorthands Ax, Ex bind a single variable character immediately after the A/E.

Proof Checker

This checker works for proofs in the style of How Logic Works. Paste a proof in pipe format, one step per line. Each line should consist of four columns -- dependencies, line number, formula, justification -- separated by the pipe symbol "|". For example:

1 | 1 | P | A
2 | 2 | Q | A
1,2 | 3 | P & Q | 1,2 &I
The columns don't need to be aligned.

Permissible rules

  • A — Assumption
  • MP — Modus Ponens
  • MT — Modus Tollens
  • DN — Double Negation
  • CP — Conditional Proof
  • ∧I / &I — And-Introduction
  • ∧E / &E — And-Elimination
  • ∨I / vI — Or-Introduction
  • ∨E / vE — Or-Elimination
  • ∀E / UI — Universal Elimination
  • ∀I / UE — Universal Introduction
  • ∃I / EI — Existential Introduction
  • ∃E / EE — Existential Elimination
  • RAA — Reductio ad Absurdum

Both short (UI, EI, etc.) and symbolic forms (&I, vE, ∀I, ∃E) are accepted.

Open the Proof Checker →

Model Checker

Build a finite structure and evaluate a closed sentence in it.

  • Domain: comma-separated elements (e.g. a,b,c).
  • Constants: map to elements (e.g. c = a).
  • Symbols: add rows with a name, an arity (0–3), and an extension:
    • Arity 0: T or F (propositional constant).
    • Arity 1: list of elements (e.g. a,b).
    • Arity 2–3: tuples in angle brackets (e.g. <a,b>, <a,b,c>).
  • Uninterpreted symbols produce a clear error (no “guessing”).
Example sentence:
Ax (Fx -> ∃y Rxy)

Open the Model Checker →

Truth Tables

Enter a purely propositional sentence (only 0-ary symbols like P, Q, R—no predicates with arguments). The tool generates all valuations and the truth value of the sentence.

(P -> Q) v R
~(P & Q) -> (Q v R)
  • If a non-propositional symbol is detected, you’ll get a “non_propositional” error.
  • The table header shows the pretty-printed sentence instead of “Value”.
  • ASCII forms like ->, ~, /\, \/, and words “and/or/not” all work.

Open the Truth-Table tool →

FAQ / Tips

  • Variables: you can use x,y,z,x1, etc. Quantifiers bind one variable at a time.
  • Spacing: spaces around operators are optional. Parentheses work as usual.
  • Shorthands: prefer Ax, Ex for speed; they normalize to ∀x, ∃x.
  • Errors: messages reference the normalized input (post-shortcut), so your ASCII is translated first.