Instructions

Writing formulas

Meaning	Symbol	You can also type
not	¬φ	~φ not φ
and	φ ∧ ψ	φ /\ ψ φ & ψ φ and ψ
or	φ ∨ ψ	φ \/ ψ φ v ψ φ or ψ
if … then	φ → ψ	φ -> ψ φ => ψ
if and only if	φ ↔ ψ	φ <-> ψ
every	∀x φ	forall x φ Axφ
some	∃x φ	exists x φ Exφ
predicates	Fx, Rxy	written straight after the letter
sentence letters	P, Q, R	predicates with no arguments

Spaces around operators are optional, and parentheses work as usual. Variables may be any letter, optionally with a digit: x, y, x1. The shorthands Ax and Ex bind the single variable written straight after them.

Proof checker

This checks proofs in the style of How Logic Works. Write one step per line, with four columns separated by a vertical bar: dependencies, line number, formula, justification.

1   | 1 | P     | A
2   | 2 | Q     | A
1,2 | 3 | P & Q | 1,2 &I

The columns need not line up. Leave the dependency column empty when a line depends on nothing.

Rules

Rule names are not case-sensitive, so cp and CP both work.

Rule	Name	Also accepted	Lines cited
A	Assumption	Assumption	—
MP	Modus Ponens	—	2
MT	Modus Tollens	—	2
DN	Double Negation	—	1
CP	Conditional Proof	—	2
∧I	And-Introduction	&I, ANDI, /\\I	2
∧E	And-Elimination	&E, ANDE, /\\E	1
∨I	Or-Introduction	vI, \\/I, ORI	1
∨E	Or-Elimination	vE, \\/E, ORE	5
RAA	Reductio ad Absurdum	RA, ¬I, ~I	2
↔I	Biconditional Introduction	<->I, IFFI, BIDI	2
↔E	Biconditional Elimination	<->E, IFFE, BIDE	2
∀E	Universal Elimination	UE, ForallE	1
∀I	Universal Introduction	UI, ForallI	1
∃I	Existential Introduction	EI, ExistsI	1
∃E	Existential Elimination	EE, ExistsE	3
QN	Quantifier Negation	—	1
=I	Identity Introduction	—	—
=E	Identity Elimination	—	2
LEM	Law of Excluded Middle	—	—
prop taut	Propositional Tautology	—	any number

Propositional tautology accepts any formula that follows truth-functionally from the lines it cites:

1   | 1 | AxFx v EyGy | A
2   | 2 | ~AxFx       | A
1,2 | 3 | EyGy        | 1,2 prop taut

Working on paper? Print the proof template, then photograph your proof and have it read and checked for you.

Open the proof checker →

Model checker

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

Domain — comma-separated elements, such as a,b,c.
Constants — each maps to an element, such as c = a.
Symbols — a name, an arity from 0 to 3, and an extension:
- arity 0: T or F;
- arity 1: a list of elements, such as a,b;
- arity 2 or 3: tuples, such as <a,b>.

A symbol you have not interpreted produces a clear error rather than a guess.

Ax (Fx -> Ey Rxy)

Open the model checker →

Truth tables

Enter a purely propositional sentence — sentence letters only, no predicates with arguments. The tool lists every valuation and the value of the sentence under each.

(P -> Q) v R
~(P & Q) -> (Q v R)

A predicate with arguments produces a non_propositional error. The DNF converter rewrites a sentence in disjunctive normal form.

Open the truth-table tool →

Symbolic Logic Tools How Logic Works

Writing formulas

Proof checker

Rules

Model checker

Truth tables