Propositional logic (also known as sentential logic or statement logic) is the branch of logic that studies the logical relationships between propositions treated as indivisible wholes. It deals with truth-functional connectives such as "and", "or", "not", "if...then", and "if and only if", and uses symbols to represent propositions and connectives. The primary concern is the validity of arguments based solely on the form of the component propositions, not on their internal structure. Propositional logic forms the foundation for more advanced logics and is widely used in mathematics, computer science, and philosophy.

1 Introduction

1.1 Historical Background

The systematic study of propositional logic dates back to ancient Greek philosophers, particularly the Stoics, who developed a rudimentary system of propositional reasoning. Later, medieval logicians refined these ideas. Modern propositional logic was formalized in the 19th and early 20th centuries by figures such as George Boole (who introduced an algebraic approach) and Gottlob Frege (who developed a formal language). The work of Bertrand Russell and Alfred North Whitehead in *Principia Mathematica* (1910–1913) further solidified the field.

1.2 Basic Concepts

1.2.1 Propositions and Truth Values

A proposition is a declarative statement that is either true or false, but not both. The two truth values are typically denoted as True (T, 1) and False (F, 0). In propositional logic, atomic propositions are represented by propositional variables (e.g., *p*, *q*, *r*). Complex propositions are built from these using logical connectives.

1.2.2 Logical Connectives

Logical connectives (also called logical operators) combine propositions to form new propositions. Each connective is defined by a truth function.

1.2.2.1 Negation

Negation (symbol: ¬, ~, or not) reverses the truth value of a proposition. If *p* is true, ¬*p* is false; if *p* is false, ¬*p* is true.

1.2.2.2 Conjunction

Conjunction (symbol: ∧, &, or and) is true only when both conjuncts are true. *p* ∧ *q* is true if and only if *p* is true and *q* is true.

1.2.2.3 Disjunction

Disjunction (symbol: ∨, or or) is true when at least one disjunct is true. Inclusive disjunction (the standard interpretation) allows both to be true. *p* ∨ *q* is true if *p* is true, *q* is true, or both are true.

1.2.2.4 Implication (Conditional)

Implication (symbol: →, ⇒, or if...then) is true except when the antecedent is true and the consequent is false. *p* → *q* is false only when *p* is true and *q* is false. This truth-functional interpretation is known as material implication.

1.2.2.5 Biconditional

Biconditional (symbol: ↔, ⇔, or if and only if) is true when both sides have the same truth value. *p* ↔ *q* is true if *p* and *q* are both true or both false.

2 Syntax

2.1 Alphabet of Propositional Logic

The alphabet consists of:

  • A countable set of propositional variables: *p*, *q*, *r*, ... (often with subscripts).
  • Logical connectives: ¬, ∧, ∨, →, ↔ (or alternative symbols).
  • Auxiliary symbols: left and right parentheses ( , ).

2.2 Well-Formed Formulas (WFFs)

2.2.1 Formation Rules

A well-formed formula (WFF) is defined inductively:

  1. Every propositional variable is a WFF.
  2. If *φ* is a WFF, then ¬*φ* is a WFF.
  3. If *φ* and *ψ* are WFFs, then (*φ* ∧ *ψ*), (*φ* ∨ *ψ*), (*φ* → *ψ*), and (*φ* ↔ *ψ*) are WFFs.
  4. Nothing else is a WFF.

2.2.2 Precedence and Parentheses

To reduce parentheses, precedence rules are used: ¬ binds most strongly, then ∧ and ∨ (often with ∧ binding tighter than ∨), then → and ↔. Parentheses override the default precedence. Common conventions: implication is right-associative.

3 Semantics

3.1 Truth Assignments and Valuations

A truth assignment (or valuation) is a function *v* that assigns a truth value (T or F) to each propositional variable. This assignment extends uniquely to all WFFs by applying the truth functions of the connectives.

3.2 Truth Tables

3.2.1 Truth Tables for Basic Connectives

The truth tables for the five connectives are:

*p*¬*p*
TF
FT
*p**q**p* ∧ *q**p* ∨ *q**p* → *q**p* ↔ *q*
TTTTTT
TFFTFF
FTFTTF
FFFFTT

3.2.2 Constructing Truth Tables for Complex Formulas

For a formula with *n* variables, the truth table has 2^n rows. Columns are built stepwise from subformulas. Example: for (*p* ∧ ¬*q*) → *r*, compute ¬*q*, then *p* ∧ ¬*q*, then the implication.

3.3 Tautologies, Contradictions, and Contingencies

A tautology is a formula true under every truth assignment (e.g., *p* ∨ ¬*p*). A contradiction is false under every assignment (e.g., *p* ∧ ¬*p*). A contingency is neither a tautology nor a contradiction (it is true under at least one assignment and false under at least one).

3.4 Logical Equivalence

Two formulas *φ* and *ψ* are logically equivalent (denoted *φ* ≡ *ψ*) if they have the same truth value under every truth assignment. Equivalently, *φ* ↔ *ψ* is a tautology.

3.4.1 Important Equivalences

Key equivalences include:

  • Double negation: ¬¬*p* ≡ *p*
  • De Morgan’s laws: ¬(*p* ∧ *q*) ≡ ¬*p* ∨ ¬*q*; ¬(*p* ∨ *q*) ≡ ¬*p* ∧ ¬*q*
  • Commutativity: *p* ∧ *q* ≡ *q* ∧ *p*; *p* ∨ *q* ≡ *q* ∨ *p*
  • Associativity: (*p* ∧ *q*) ∧ *r* ≡ *p* ∧ (*q* ∧ *r*); similarly for ∨
  • Distributivity: *p* ∧ (*q* ∨ *r*) ≡ (*p* ∧ *q*) ∨ (*p* ∧ *r*); *p* ∨ (*q* ∧ *r*) ≡ (*p* ∨ *q*) ∧ (*p* ∨ *r*)
  • Implication: *p* → *q* ≡ ¬*p* ∨ *q*
  • Biconditional: *p* ↔ *q* ≡ (*p* → *q*) ∧ (*q* → *p*)

3.4.2 Substitution of Equivalents

If two subformulas are equivalent, replacing one with the other in a larger formula preserves logical equivalence. This principle (substitution of equivalents) is used in simplifying formulas.

3.5 Satisfiability and Validity

A formula is satisfiable if there exists at least one truth assignment that makes it true. It is valid (a tautology) if it is true under all assignments. Satisfiability is a central concept in computer science (see SAT problems). A formula is unsatisfiable (a contradiction) if no assignment makes it true.

4 Deductive Systems

4.1 Axiomatic Systems

4.1.1 Hilbert-Style Axioms

A Hilbert-style axiomatic system for propositional logic uses a small set of axiom schemas and a single inference rule (modus ponens). One common axiomatization (for the connectives → and ¬) includes:

  • (A1) *φ* → (*ψ* → *φ*)
  • (A2) (*φ* → (*ψ* → *χ*)) → ((*φ* → *ψ*) → (*φ* → *χ*))
  • (A3) (¬*ψ* → ¬*φ*) → (*φ* → *ψ*)

Modus ponens: from *φ* and *φ* → *ψ*, infer *ψ*.

4.1.2 Derivations and Proofs

A proof (or derivation) is a finite sequence of formulas, each of which is either an axiom or follows from earlier formulas by modus ponens. A theorem is the last formula of a proof. Soundness and completeness theorems guarantee that exactly the tautologies are provable.

4.2 Natural Deduction

4.2.1 Introduction and Elimination Rules

Natural deduction mimics intuitive reasoning. For each connective, there are introduction (I) and elimination (E) rules. Examples:

  • ∧I: from *φ* and *ψ*, infer *φ* ∧ *ψ*
  • ∧E: from *φ* ∧ *ψ*, infer *φ* (or *ψ*)
  • →I: from a subproof assuming *φ* that derives *ψ*, infer *φ* → *ψ*
  • →E (modus ponens): from *φ* and *φ* → *ψ*, infer *ψ*
  • ¬I: from a subproof assuming *φ* that derives a contradiction, infer ¬*φ*
  • ¬E (reductio ad absurdum): from ¬*φ* and a contradiction, infer *φ* (depending on version)

4.2.2 Proof Strategies

Common strategies include:

  • To prove a conjunction, prove each conjunct separately.
  • To prove an implication, assume the antecedent and derive the consequent.
  • To prove a disjunction, prove one disjunct (or use case analysis from a disjunction).
  • To prove a negation, assume the opposite and derive a contradiction.

These correspond to the introduction rules.

4.3 Sequent Calculus

4.3.1 Sequents and Rules

A sequent is an expression Γ ⊢ Δ, where Γ and Δ are finite sets (or multisets) of formulas. Intuitively, it means "the conjunction of Γ implies the disjunction of Δ." The calculus uses rules that introduce connectives on the left or right side. For example, the rule for ∧ on the right:

Γ ⊢ Δ, A    Γ ⊢ Δ, B
----------------------
   Γ ⊢ Δ, A ∧ B

And on the left:

A, B, Γ ⊢ Δ
-------------
  A ∧ B, Γ ⊢ Δ

4.3.2 Cut Elimination

The cut rule (if Γ ⊢ Δ, A and A, Γ ⊢ Δ, then Γ ⊢ Δ) is redundant in propositional logic: any proof using cut can be transformed into one without cut. This cut-elimination theorem (Gentzen) yields consistency and subformula property: every formula in a cut-free proof is a subformula of the conclusion.

4.4 Resolution

4.4.1 Clausal Form

Resolution works on formulas in conjunctive normal form (CNF). A formula is expressed as a conjunction of clauses, each clause being a disjunction of literals (propositional variables or their negations). Converting to CNF involves eliminating → and ↔, pushing ¬ inward, and distributing ∨ over ∧.

4.4.2 The Resolution Rule

Given two clauses (A ∨ *p*) and (B ∨ ¬*p*), the resolvent is (A ∨ B). The variable *p* is eliminated. The rule is applied iteratively to derive new clauses.

4.4.3 Refutation Completeness

Resolution is refutation complete: if a set of clauses is unsatisfiable, the empty clause (a contradiction) can be derived by repeated resolution. This property makes it a foundation for automated theorem proving (e.g., SAT solvers).

5 Metatheory

5.1 Soundness

A deductive system is sound if every provable formula is a tautology (valid). Soundness ensures that the rules do not allow deriving false conclusions from true premises. For propositional logic, standard axiomatic systems, natural deduction, and sequent calculus are all sound.

5.2 Completeness

A system is complete if every tautology is provable. Propositional logic is complete for the standard semantics.

5.2.1 Proof of Completeness for Propositional Logic

One common proof uses the Lindenbaum lemma: every consistent set of formulas can be extended to a maximal consistent set. Then a truth assignment is defined based on membership in that set. This assignment satisfies the original set, showing that if a formula is not provable (i.e., its negation is consistent), it is not a tautology. Contrapositively, every tautology is provable. Alternative proofs use truth-table construction or cut elimination.

5.3 Compactness

Propositional logic satisfies the compactness theorem: a set of formulas is satisfiable if and only if every finite subset is satisfiable. This is a corollary of completeness and the finitary nature of proofs. Compactness has important consequences in model theory and non-standard analysis.

5.4 Decidability

Propositional logic is decidable: there is an effective procedure (algorithm) to determine whether any given formula is a tautology, satisfiable, or contradictory. The truth-table method is one such algorithm (exponential in the number of variables), but more efficient methods exist (e.g., tableaux, resolution, BDDs). The satisfiability problem (SAT) is NP-complete, so no polynomial-time algorithm is known (unless P=NP).

6 Applications

6.1 Digital Circuit Design

Propositional logic directly models digital circuits. Logic gates correspond to connectives: AND (conjunction), OR (disjunction), NOT (negation), NAND, NOR, XOR (exclusive or). Boolean algebra is used to simplify circuits. Truth tables describe the behavior of combinational circuits.

6.2 Propositional Logic in Computer Science

6.2.1 Boolean Satisfiability (SAT) Problems

The SAT problem asks whether a given Boolean formula has a satisfying assignment. It is the canonical NP-complete problem. Despite its complexity, modern SAT solvers (using DPLL, conflict-driven clause learning) handle large instances efficiently. Applications include hardware verification, software testing, planning, and constraint solving.

6.2.2 Automated Theorem Proving

Propositional logic forms the core of many automated reasoning systems. Resolution-based provers, tableau methods, and SAT solvers are used to validate logical entailments. In interactive theorem provers, propositional reasoning is often handled by built-in decision procedures.

6.3 Philosophical Applications

6.3.1 Analysis of Arguments

Propositional logic provides a precise language to analyze the validity of natural language arguments. By translating statements into propositional formulas, one can check whether the conclusion follows from premises. This is a basic tool in logic and critical reasoning.

6.3.2 Paradoxes and Puzzles

Several classical paradoxes illustrate features of propositional logic. For example, the material implication paradoxes (e.g., a false antecedent makes any conditional true) are often discussed. Puzzles such as knights and knaves (where inhabitants always tell truth or lie) are solved using propositional logic. The statement "This sentence is false" is a self-referential paradox that cannot be directly expressed in standard propositional logic.

7 Variants and Extensions

7.1 Many-Valued Logics

In many-valued logics, the number of truth values is extended beyond two. For example, three-valued logics (with values true, false, and unknown) are used to handle incomplete information. Kleene's strong three-valued logic and Łukasiewicz logics are classic examples. Many-valued logics have applications in computer science (e.g., database query evaluations, fuzzy logic).

7.2 Intuitionistic Propositional Logic

Intuitionistic logic rejects the law of excluded middle (*p* ∨ ¬*p*) and the principle of double negation elimination (¬¬*p* → *p*). It is motivated by constructive reasoning: a proof of *p* ∨ *q* requires a specific proof of one of them. Intuitionistic propositional logic is weaker than classical logic; its semantics is given by Kripke structures or Heyting algebras.

7.3 Modal Propositional Logic

Modal logic extends propositional logic with operators □ (necessarily) and ◇ (possibly). It is used to reason about necessity, possibility, knowledge, belief, time, and obligations. The semantics involves possible worlds and accessibility relations. Common axiomatic systems include K, T, S4, and S5.

8 See Also

9 References

  • Enderton, H. B. (2001). *A Mathematical Introduction to Logic* (2nd ed.). Academic Press.
  • van Dalen, D. (2013). *Logic and Structure* (5th ed.). Springer.
  • Huth, M., & Ryan, M. (2004). *Logic in Computer Science: Modelling and Reasoning about Systems* (2nd ed.). Cambridge University Press.
  • Smullyan, R. M. (1995). *First-Order Logic*. Dover Publications.