LogicalZooAn atlas of formal logics

Classical Logics

PL

Classical Propositional Logic

The logic of truth-functional combinations of propositions, forming a foundation for classical inference and the SAT problem.

Definition and Syntax

Classical propositional logic treats propositions as either true or false. Formulas are built from propositional variables p,q,\ldots using negation and conjunction:

\varphi ::= p \mid \neg\varphi \mid (\varphi\land\varphi).

Disjunction and implication can be defined in terms of these connectives; for example, \varphi\to\psi := \neg(\varphi\land\neg\psi).

Semantics and Example

A valuation v:\mathrm{Prop}\to\{0,1\} determines the truth value of every formula according to the classical truth tables. A formula is satisfiable if some valuation makes it true, and valid if every valuation makes it true.

For example, (p\land(p\to q))\to q is valid and expresses modus ponens.

Properties and Complexity

Sound and complete proof calculi exist. Semantic entailment is compact. For finite input formulas, satisfiability is NP-complete and validity is coNP-complete. The NP-completeness result follows from the Cook–Levin theorem [1].

First-order logic adds quantifiers and relations; K adds modal operators.

References

  1. Stephen A. Cook (1971). The Complexity of Theorem-Proving Procedures. STOC, 151–158. Original paper.

Related logics

  • FOL — First-Order Logic
  • HOL — Classical Higher-Order Logic
  • K — Basic Normal Modal Logic K

Links to this entry

  • FOL — First-Order Logic
  • HOL — Classical Higher-Order Logic
  • SDL — Standard Deontic Logic (SDL)

Published on Oct. 31, 2026 · Version 2