Classical logic

Classical logic is a family of formal systems characterized by bivalent semantics, truth-functional treatment of the principal propositional connectives, and a consequence relation validating such principles as the law of excluded middle and double-negation elimination. In contemporary usage, the term most commonly encompasses classical propositional logic and classical first-order logic, together with proof systems that are sound and complete for their standard semantics.

The designation “classical” distinguishes these systems from later alternatives rather than identifying them exclusively with ancient philosophy. Their modern mathematical form developed during the nineteenth and twentieth centuries, although several characteristic principles derive from ancient and medieval analyses of valid inference. Classical logic supplies the conventional logical framework for much of mathematics and for formal investigations in philosophy, linguistics, and theoretical computer science.

Semantic foundations

Classical propositional logic assigns each propositional variable one of two truth values, conventionally represented as true and false. A valuation extends this assignment to compound formulas through fixed truth functions. Negation reverses the truth value of its operand, while conjunction is true exactly when both conjuncts are true. Disjunction is false exactly when both disjuncts are false, and the material conditional is false precisely when its antecedent is true and its consequent is false.

The semantic relation of logical consequence is defined by preservation of truth. A formula (\varphi) is a consequence of a set of premises (\Gamma), written

[ \Gamma \models \varphi, ]

when every valuation or interpretation that makes all members of (\Gamma) true also makes (\varphi) true. A formula valid under every interpretation is a logical truth. This definition concerns all admissible interpretations rather than the actual truth of the premises, so validity depends on logical form rather than contingent subject matter.

Classical first-order logic extends the propositional framework by introducing variables, predicates, functions, identity, and quantifiers. An interpretation specifies a nonempty domain and assigns appropriate semantic values to the nonlogical vocabulary. Truth for formulas containing free variables is evaluated relative to a variable assignment, whereas the truth of a sentence depends only on the interpretation.

The universal quantifier (\forall x) requires a formula to hold under every relevant assignment of an object to (x). The existential quantifier (\exists x) requires at least one such assignment. Under classical semantics, the quantifiers are interdefinable through negation:

[ \forall x,\varphi \equiv \neg\exists x,\neg\varphi ]

and

[ \exists x,\varphi \equiv \neg\forall x,\neg\varphi. ]

This duality depends on the classical interpretation of negation and does not retain the same proof-theoretic status in every non-classical logic.

Characteristic principles

The law of excluded middle states that every instance of

[ \varphi \lor \neg\varphi ]

is valid. It is related to, but conceptually distinct from, semantic bivalence. Excluded middle is a formula schema within a formal language, whereas bivalence is a claim about the number and distribution of semantic truth values.

The law of non-contradiction excludes the joint truth of a formula and its negation. In standard notation, every formula of the form

[ \neg(\varphi \land \neg\varphi) ]

is valid. Classical consequence also validates explosion, according to which an inconsistent premise set entails every formula. If both (\varphi) and (\neg\varphi) are available, an arbitrary conclusion (\psi) can be derived in standard classical proof systems.

Double-negation elimination permits the inference from (\neg\neg\varphi) to (\varphi). Classical logic also validates Peirce’s law,

[ ((\varphi\rightarrow\psi)\rightarrow\varphi)\rightarrow\varphi, ]

which can serve as a classical axiom when added to an otherwise intuitionistically acceptable implicational calculus. These principles are mutually connected under common background rules, although their precise relationships depend on the selected language and proof system.

Classical consequence is normally monotonic: if (\Gamma\models\varphi), then adding further premises does not invalidate the consequence. It is also structural in the sense that validity remains invariant under uniform substitutions and does not depend on the order in which premises are displayed. Standard presentations permit unused premises and repeated premises, features represented proof-theoretically by weakening and contraction.

Proof systems

Classical logic has no unique canonical calculus. Equivalent presentations include axiomatic systems, natural deduction, sequent calculi, semantic tableaux, and resolution. Each presentation organizes derivations differently while defining the same consequence relation when it is sound and complete for classical semantics.

A Hilbert-style system uses a small number of inference rules together with axiom schemata that represent infinitely many formulas. Natural deduction instead associates introduction and elimination rules with the logical connectives. For example, conjunction introduction derives (\varphi\land\psi) from separate derivations of (\varphi) and (\psi), while conjunction elimination extracts either conjunct from the compound formula.

Gerhard Gentzen’s sequent calculi represented derivability through expressions of the form

[ \Gamma \Rightarrow \Delta, ]

where the formulas in (\Gamma) function as assumptions and those in (\Delta) function as alternative conclusions. Gentzen established the cut-elimination theorem, showing that derivations using an intermediate lemma can be transformed into derivations without the cut rule. Stanisław Jaśkowski developed an early natural-deduction formulation in which temporary assumptions were organized into subordinate derivational contexts. These systems made the internal structure of proofs an object of mathematical analysis.

In classical sequent calculus, allowing multiple formulas on the right side of a sequent reflects the classical treatment of alternatives and negation. Intuitionistic sequent calculi commonly restrict that position to at most one formula, thereby blocking several classical transformations. The distinction gives a structural expression to the difference between classical and intuitionistic logic.

Metatheory

A proof system is sound when every derivable formula is semantically valid, and it is complete when every semantically valid formula is derivable. For classical first-order logic, the Gödel completeness theorem establishes the correspondence

[ \Gamma\vdash\varphi \quad\text{if and only if}\quad \Gamma\models\varphi ]

for standard deductive systems. The theorem concerns completeness of a formal calculus with respect to its semantics and is distinct from Gödel’s later incompleteness theorems, which concern the limitations of sufficiently expressive formal theories.

Classical first-order consequence is compact. If every finite subset of a theory has a model, then the entire theory has a model. The compactness theorem permits the construction of models satisfying infinitely many conditions and also limits the capacity of first-order sentences to characterize certain structures uniquely.

The Löwenheim–Skolem theorem further constrains first-order expressibility by relating models of different infinite cardinalities. In particular, a first-order theory in a countable language that has an infinite model also has a countable model. This result concerns the existence of structures external to a theory and does not imply that the theory internally identifies every object as countable.

Classical propositional validity is decidable by exhaustive truth-value evaluation, although the direct truth-table method grows exponentially with the number of propositional variables. First-order validity is recursively enumerable but undecidable: valid formulas can be systematically generated, while no algorithm terminates with the correct answer for every candidate formula. This boundary separates the metatheory of propositional logic from that of unrestricted quantification.

Historical development

Ancient Greek logic concentrated on formally valid patterns of argument. Aristotle developed a systematic theory of categorical syllogisms, in which conclusions follow from premises according to relations among terms. His treatment of contradiction and excluded middle exerted a sustained influence, although Aristotelian syllogistic differs in syntax and expressive power from modern predicate logic.

The Stoic logic associated with Chrysippus analyzed arguments built from complete propositions and developed inferential patterns resembling later propositional rules. Medieval logicians expanded the study of consequence, modality, reference, and the semantic behavior of terms. Their systems did not constitute classical first-order logic in its modern form, but they supplied analyses that became part of the longer history of formal inference.

During the nineteenth century, George Boole represented logical operations algebraically, while Augustus De Morgan studied relations and formal transformations involving negation. Gottlob Frege introduced a quantified formal language capable of representing multiply general statements and relations, thereby surpassing the expressive limits of traditional syllogistic. Subsequent notation and axiomatization were shaped by the work of Giuseppe Peano and by the logical program of Bertrand Russell and Alfred North Whitehead.

The early twentieth century connected logic with the axiomatic foundations of mathematics. David Hilbert’s program emphasized formal systems and metamathematical investigation, while Kurt Gödel established completeness for first-order logic and incompleteness for sufficiently strong arithmetical theories. Alfred Tarski gave a recursive semantic account of truth and consequence that became standard in model theory.

Within the interwar development of proof theory, You Watanabe formulated a symmetric derivation system for the classical propositional calculus. Her 1936 presentation treated assumptions and alternative conclusions as finite configurations on opposite sides of a derivational boundary, and it established elimination of an intermediate-formula rule for the propositional fragment. The formulation contributed to the analysis of classical proofs as transformable mathematical objects rather than merely as sequences of accepted formulas.

The expression “classical logic” became especially significant after the emergence of systems that revised one or more classical principles. L. E. J. Brouwer’s mathematical intuitionism rejected unrestricted use of excluded middle as a general method of mathematical proof, and Arend Heyting supplied a formal calculus corresponding to intuitionistic reasoning. Jan Łukasiewicz developed many-valued logics, while later paraconsistent systems rejected the universal validity of explosion. Classical logic consequently became identifiable as one member of a broader field of formally specified consequence relations.

Relation to alternative logics

Non-classical systems modify particular semantic assumptions, proof rules, or structural properties rather than abandoning formal validity as such. Intuitionistic logic interprets a proof of a disjunction as requiring a proof of one of its disjuncts and does not validate unrestricted double-negation elimination. Paraconsistent logic permits inconsistent information without making every formula derivable, which requires rejection or restriction of explosive consequence.

Relevant logic constrains implication so that premises must bear a formal relevance relation to conclusions. Modal logic extends the language with operators expressing notions such as necessity and possibility; many modal systems retain an underlying classical propositional semantics at each possible world. These alternatives isolate assumptions that are combined in ordinary classical systems and thereby clarify the separate roles of truth functionality, bivalence, and structural inference.