There are in general two ways of arriving at tautologies in any logical system. One is done semantically, via a truth function on the set of propositional variables, and extending the function to the larger set consisting of all (well-formed) formulas, and then declaring a tautology as any formula that is always mapped to $\top$ (the value representing ``true'') regardless of the truth functions.

The second way is done mechanically, or in logical jargon, syntactically, via a special set of well-formed formulas, called logical axioms, together witha (finite) set of rules of inference. Any formula $f$ that is ``provable'' from these axioms by applying the rules of inferences is called a tautology. By ``provable'' it is loosely meant that the formula $f$ in question can be obtained by a finite sequence $$f_0,f_1,\ldots,f_n$$ of formulas, such that $f_0$ is an axiom, $f_n=f$ , and any element $f_i$ in between ($0<i<n$ ) is either an axiom or a formula that can be obtained by applying rules of inferences to any combinations of elements $f_j$ prior to $f_i$ , that is, $j<i$ . In other words, tautologies are recursively derived.

For example, in classical propositional logic, or sometimes known as Boolean propositional logic, the following collection constitutes a set of axioms:

1. $a\to (b\to a)$
2. $(a\to(b\to c))\to ((a\to b)\to(a\to c))$
3. $(\neg a\to \neg b)\to(b\to a)$

• $a\vee b:=\neg a\to b$
• $a\wedge b:=\neg(\neg a\vee \neg b)$
• $a\leftrightarrow b:=(a\to b)\wedge (b\to a)$

It is worth noting that in the above set, we are actually looking at three smaller sets, each set containing formulas of a specific form. Any such a set of axioms is called an axiom scheme, or axiom schema. The whole collection of axioms is sometimes called the axiom schemata. So in the above example, there are three axiom schemes comprising the axiom schemata of the logical system.

Associating with the axioms of the classical propositional logic is a single rule of reference, called modus ponens. Any formula $f$ that is ``provable'' from the above set of axioms by modus ponens is called a ``tautology''. When this is the case, we usually write $$\vdash f.$$ With the above axioms, one may show, for example, that $\vdash (a\vee b)\leftrightarrow (b\vee a)$ , and in fact, all of the standard commutative and associative laws with respect to $\vee$ and $\wedge$ , as well as other familiar laws one finds in the study of Boolean algebras.

Fix the set $S$ of tautologies provable from the axioms and modus ponens specified above, and denote this fact by $\vdash S$ . By fixing $S$ , we make one observation: there is no unique set of axioms and rules of inferences such that the set $S$ is provable from. Indeed, together with modus ponens, the following axiom schemata for the classical propositional logic also produces $S$ (that is, $S$ is provable):

1. $a\to (b\to a)$
2. $(a\to(b\to c))\to ((a\to b)\to(a\to c))$
3. $a\to (a\vee b)$
4. $b\to (a\vee b)$
5. $(a\to c)\to ((b\to c)\to((a\vee b)\to c))$
6. $(a\wedge b)\to a$
7. $(a\wedge b)\to b$
8. $(c\to a)\to ((c\to b)\to (c\to (a\wedge b)))$
9. $(a\to \neg b)\to (b\to \neg a)$
10. $\neg(a\to a)\to b$
11. $a\vee \neg a$ (law of the excluded middle)

Here, with the exception of the biconditional ($\leftrightarrow$ ), all of the rest of the logical connectives appear in the axioms, and therefore, there is no need to define the conjunctive ($\wedge$ ) and the disjunctive ($\vee$ ) connectives (the result of defining these is a case of Occam Razor). The biconditional may be defined the same way as before. Typically, the more axiom schemes we have, the easier it is to show that a formula is a tautology (the shorter the proof sequence).

It is interesting to note that it is possible to form $S$ using just one axiom schema and modus ponens. The axiom schema was discovered by C. Meredith, and it looks like: $$\Big[\Big(\big((a\to b)\to (\neg c\to \neg d)\big)\to c\Big)\to e\Big]\to \big((e\to a)\to (d\to a)\big)$$ Remarkably, it is also possible to form tautologies of the classical propositional logic without any axioms at all. Not surprisingly, additional rules of inference are necessary for this to work.

Bibliography

1

D. Monk: Mathematical Logic, Springer-Verlag, New York (1976).

2

H. Enderton: A Mathematical Introduction to Logic, Academic Press, San Diego (1972).

3

P. Halmos, S. Givant: Logic as Algebra, The Mathematical Association of America, (1998).

4

H. Rasiowa: Post Algebras as a Semantic Foundation of $m$ -Valued Logics, Studies in Algebraic Logic, The Mathematical Association of America, (1974).