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:

- p,q,r as propositional letters
- a, b and c as constants
- F,G, and H as monadic predicates, and
- R,S, and T as dyadic predicates.

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

- every propositional letter is a formula
- if P and Q are formulas, then
- ! is the absurdity formula
- ~P is the negation of P
- (P>Q) is the conditional with antecedent P and consequent Q
- (P&Q) is the conjunction with conjuncts P and Q
- (PvQ) is the disjunction with disjuncts P and Q

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

- x,y,z are variables
- variables and constants are terms
- a monadic predicate followed by one term is a formula
- a dyadic predicate followed by two terms is a formula
- if s and t are terms then s=t is a formula, and
- if P is a formula and u is a variable, then
- EuP is the existential generalization of P with respect to u
- AuP is the universal generalization of P with respect to u.

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.