THE LOGIC NOTES

Theorem, Tautology Glossary

Definition

A theorem is a formula provable as the conclusion of a sequent with no premises (i.e. with the empty set on the left).

A tautology is a formula which is true for every interpretation.

Comments

Given that the deductive system is sound and complete for the semantics, the theorems and the tautologies are the same formulae. The two definitions are different, however.

On the standard definition of logical consequence, any theorem follows from any formula whatsoever, including its own negation. A common technique for proving that a formula A is a theorem is to derive it from NOTA and then discharge the assumption by NOTI or RAA.

Examples

  1. Wherever a sequent A ⊢ B is provable, the formula A IMP B is a theorem, as it can be obtained from the sequent by applying the rule IMPI. More generally, if A1, ..., A1 ⊢ B is provable, (A1 AND ... AND A1) IMP B is a theorem.
  2. Certain disjunctions are theorems although neither disjunct is a theorem on its own. These formulae are tautologies according to classical truth tables, though they are not theorems of constructive logic and are not provable without using NOTNOTE. The most obvious example is p OR NOTp. Another is (p IMP q) OR (q IMP r).

Links