prove evaluate sign up sign in index info


The notation used here is a computer-friendly adaptation of an ordinary system of first-order logic.

Its nonlogical vocabulary consists of:

Eventually I'll get around to allowing subscripts.

For truth-functional logic, the syntax goes like this:

The parser understands order of operations so you can drop parentheses as usual.

The syntax of quantificational logic includes that of truth-functional logic plus:


The method of proof implemented here is adapted from the natural deduction system of E.J. Lemmon's Beginning Logic.

The proof system provides a collection of rules of inference. A rule of inference gives a condition under which a line can be added to a proof.

A line of a proof consists of a formula and a justification. A justification mentions the rule of inference under which the new line has been constructed, together with a citation of any prior lines whose construction is required by that rule.

But since this is a natural deduction system, each line signifies the assertion of its formula under some zero or more hypotheses. So a line will be decorated with numbers of earlier lines whose formulas together form the hypotheses of the assertion of the formula of that line. Here these decorations are generated automatically.

The rules of inference are available in Lemmon's book. The only difference is that constants are used instead of special instantial terms. These rules are given explicitly in this online text. But here are a couple of examples.

The rule of assumption (A) lets you add any formula at all without citing any prior lines. The new formula is asserted under itself as a hypothesis.

Given two lines whose formulas are P and P>Q, the rule of modus ponens (MP) lets you add the formula Q, citing the numbers of the two prior lines. The new formula inherits the hypotheses of the two earlier ones.

Suppose there's given a line whose formula is Q, which is asserted under the hypothesis of some formula P. The rule of conditional proof (CP) lets you add a new line of the form P>Q, citing the line of the assumption of P and the line where Q was deduced from it. The hypotheses of the new formula are the hypotheses of the earlier assertion of Q aside from P.

The other rules should be cited as: vI, vE, &I, &E, !I, !E, DN, EI, EE, AI and AE.