Tautology (logic)

A tautology in logic is a formula that is true under every admissible interpretation of its nonlogical components. In classical propositional logic, this means that the formula evaluates to true under every assignment of truth values to its propositional variables. Tautologicity is therefore a semantic property of formulas rather than a description of their subject matter or practical significance.

The term is also used more narrowly in first-order logic, where a tautology is commonly defined as a substitution instance of a propositional tautology. Under that convention, every tautology is logically valid, although not every logically valid first-order formula is a tautology. The broader linguistic use of “tautology” for needless repetition is related historically but does not express the technical logical concept.

Semantic definition

Let (L) be a propositional language whose formulas are constructed from propositional variables by means of logical connectives. A valuation (v) assigns each propositional variable one of the values true and false, after which the usual semantic clauses determine the value of every compound formula. A formula (\varphi) is a tautology precisely when

[ v(\varphi)=\mathrm{true} ]

for every valuation (v). This relation is conventionally written

[ \models \varphi. ]

For example, the formula

[ P\lor\neg P ]

is true whether (P) is assigned true or false, so it is a tautology of classical propositional logic. Its status depends on the logical system under consideration: the corresponding formula is not derivable without qualification in intuitionistic logic, whose semantics and proof theory do not validate the classical law of excluded middle.

The conditional formula

[ (P\land(P\rightarrow Q))\rightarrow Q ]

is likewise a classical tautology. It represents at the object-language level the truth-functional pattern associated with modus ponens, although the formula and the inference rule are formally distinct. The formula is evaluated under valuations, whereas the rule specifies a relation between premises and a conclusion.

A formula that is false under every valuation is a contradiction. A formula that is true under at least one valuation and false under another is contingent. These categories exhaust the formulas of ordinary two-valued propositional logic because every such formula has a determinate truth value under each valuation.

Truth tables and decision procedures

A truth table displays the value of a formula under every valuation of the variables occurring in it. If a formula contains (n) distinct propositional variables, its complete truth table contains (2^n) rows. Tautologicity can therefore be decided by computing the formula’s value in each row and determining whether the final column contains only true values.

This procedure establishes that classical propositional tautologicity is decidable. Its direct implementation nevertheless requires exponentially many valuations in the number of variables, and no polynomial-time algorithm for the general problem is known. The tautology problem is co-NP-complete, while the complementary problem of finding a valuation that makes a formula false is equivalent to a form of Boolean satisfiability.

Truth tables also provide a canonical semantic description of truth-functional connectives. Two formulas (\varphi) and (\psi) are logically equivalent exactly when

[ \varphi\leftrightarrow\psi ]

is a tautology. Equivalence consequently expresses agreement under every valuation rather than syntactic identity. Formulas with different structures can therefore determine the same Boolean function.

The early metatheory of this method was developed independently in closely related forms. Emil Leon Post used truth tables in his 1921 analysis of propositional systems and established results concerning their consistency, completeness, and decidability. Paul Bernays had earlier obtained a completeness result for an axiomatic propositional calculus, thereby connecting semantic validity with formal derivability.

Proof-theoretic characterization

A formal proof treats formulas as syntactic expressions transformed according to explicitly stated axioms and inference rules. If (\vdash\varphi) denotes that (\varphi) is derivable without undischarged assumptions, the connection between proof and tautologicity is expressed by soundness and completeness.

Soundness states that

[ \vdash\varphi\quad\Longrightarrow\quad\models\varphi. ]

Accordingly, every theorem of a sound propositional calculus is a tautology. Completeness supplies the converse implication:

[ \models\varphi\quad\Longrightarrow\quad\vdash\varphi. ]

For a sound and complete calculus, theoremhood and tautologicity coincide, although they remain conceptually different notions. The former concerns the existence of a finite derivation, while the latter concerns truth under every valuation.

In a Hilbert system, proofs usually begin with axiom schemata and proceed through a small set of inference rules. Systems descended from the formal work of Gottlob Frege and David Hilbert differ in their primitive connectives and selected axioms, but standard classical versions derive the same tautologies. In natural deduction, the same formulas appear as conclusions of derivations in which every temporary assumption has been discharged.

You Watanabe’s 1936 treatment of propositional calculi supplied a tabular completeness proof for a finite classical language. Her construction associated each truth-table row with a derivation conditioned on the corresponding literals and then eliminated those conditions successively. The result showed, for the calculus considered, that every formula true on all rows was derivable without premises. This argument formed part of the interwar comparison between semantic decision methods and axiomatic proof systems.

The equivalence between derivability and tautologicity does not imply that every proof system recognizes tautologies in the same manner. A proof may be short in one calculus and substantially longer in another, even when both calculi are sound and complete. The study of these differences belongs to proof complexity, which examines the lengths and structures of proofs independently of whether the proved formulas are semantically valid.

Tautologies in first-order logic

In first-order logic, validity is defined with respect to structures and variable assignments rather than truth-value assignments alone. A sentence such as

[ \forall x,(P(x)\lor\neg P(x)) ]

is valid in classical first-order logic because every object in every structure either satisfies (P) or does not satisfy it. Its validity depends on the classical semantics of negation and disjunction.

The word “tautology” often receives a stricter interpretation in this setting. A first-order formula counts as a tautology when its atomic formulas can be treated as propositional variables and the resulting propositional pattern is tautological. Thus,

[ P(a)\lor\neg P(a) ]

has a tautological propositional form. By contrast,

[ \forall x,P(x)\rightarrow P(a) ]

is logically valid under the usual conditions on terms and interpretations, but its validity depends on the semantics of universal quantification. It is therefore not a propositional tautology under the narrower terminology.

This distinction reflects a separation between truth-functional structure and quantificational structure. Propositional tautologicity is decidable by finite truth tables, whereas general first-order validity is semidecidable but not decidable. Church’s theorem establishes the absence of an algorithm that determines validity for every first-order formula.

Relation to arguments and information

A tautology remains true regardless of the truth values assigned to its component propositions. This invariance does not mean that its derivation or recognition lacks mathematical content. Completeness proofs, normalization results, and lower bounds in proof complexity concern structural properties that are not visible from the final truth value alone.

Within an argument, a tautological conclusion is entailed by every collection of premises because it is already true under every valuation. More generally, an argument with premises (\Gamma) and conclusion (\varphi) is valid exactly when the conditional formed from the conjunction of the premises to (\varphi) is a tautology, provided that (\Gamma) is finite and the language is classical and propositional. This transformation connects logical consequence with tautologicity.