Propositional logic (also called sentential logic or the propositional calculus) constitutes the foundational layer of mathematical logic and provides the formal apparatus for the rigorous analysis of deductive reasoning. It studies propositions — declarative sentences that can be unambiguously assigned a truth value — and the ways in which they combine via logical connectives.
The present treatment offers a systematic and complete account: the formal language, syntax, truth-functional semantics, equivalences and fundamental laws, tautologies and logical consequence, normal forms, deductive systems, and the metalogical theorems of soundness and completeness.
Contents
- Propositions and Formal Language
- Syntax of Well-Formed Formulas
- Semantics and Interpretations
- Logical Connectives and Functional Completeness
- Truth Tables
- Logical Equivalences
- Fundamental Laws
- Tautologies, Satisfiability, and Logical Consequence
- Normal Forms (CNF and DNF)
- Deductive Systems
- Soundness and Completeness
- Worked Examples
Propositions and Formal Language
A proposition (or statement) is a meaningful declarative sentence which, by virtue of the principle of bivalence, takes exactly one of two truth values: true (\(T\) or \(1\)) or false (\(F\) or \(0\)).
A proposition is called atomic (or a simple statement) if it does not contain any other proposition combined by means of logical operators. Propositions obtained by combining atomic ones via logical connectives are said to be compound (or molecular).
We fix a countable set of propositional variables, generally denoted by lowercase Latin letters:
\[ \mathcal{P} = \{p_1, p_2, p_3, \dots\} = \{p, q, r, \dots\} \]
The language of propositional logic \(\mathcal{L}\) consists of the following symbols:
- the propositional variables in \(\mathcal{P}\);
- the logical connectives: \(\neg,\ \land,\ \lor,\ \rightarrow,\ \leftrightarrow\);
- the auxiliary symbols: parentheses \((,\ )\).
Syntax of Well-Formed Formulas
The set \(\mathcal{F}\) of well-formed formulas (wffs) is the smallest set of strings over the alphabet of \(\mathcal{L}\) defined inductively by the following clauses:
- Base clause: every propositional variable \(p \in \mathcal{P}\) is a wff;
- Inductive clauses:
- if \(A \in \mathcal{F}\), then \((\neg A) \in \mathcal{F}\);
- if \(A, B \in \mathcal{F}\), then \((A \land B),\ (A \lor B),\ (A \rightarrow B),\ (A \leftrightarrow B) \in \mathcal{F}\);
- Closure clause: no other string is a wff.
In BNF notation, the grammar of the language reads:
\[ A ::= p \mid (\neg A) \mid (A \land A) \mid (A \lor A) \mid (A \rightarrow A) \mid (A \leftrightarrow A) \]
By precedence convention, connectives are assigned the following decreasing order of binding strength, allowing parentheses to be omitted without ambiguity:
\[ \neg \;>\; \land \;>\; \lor \;>\; \rightarrow \;>\; \leftrightarrow \]
A word of caution. While the precedence of \(\neg\) over all other connectives, and that of \(\rightarrow,\ \leftrightarrow\) as the loosest binders, is universally accepted, the relative ranking of \(\land\) and \(\lor\) is not uniform in the literature: some authors (by analogy with \(\cdot\) and \(+\) in Boolean algebra) give \(\land\) higher precedence than \(\lor\), while others (e.g. Mendelson) place them on the same level and require explicit parentheses. It is therefore good practice, whenever ambiguity may arise, to use parentheses explicitly between \(\land\) and \(\lor\): one should write, for instance, \( (A \land B) \lor C \) rather than \( A \land B \lor C \).
The principle of structural induction on wffs states that, in order to prove a property \(P\) for every \(A \in \mathcal{F}\), it suffices to establish:
- (base step) \(P\) holds for every atomic proposition;
- (inductive step) \(P\) is preserved under the application of each connective.
Semantics and Interpretations
The semantics of propositional logic is truth-functional: the truth value of a compound formula is uniquely determined by the truth values of its subformulas.
An interpretation (or valuation, or truth assignment) is a function:
\[ v : \mathcal{P} \to \{T, F\} \]
which extends uniquely to a function \(\hat{v} : \mathcal{F} \to \{T, F\}\) via the following recursive clauses:
- \( \hat{v}(\neg A) = T \iff \hat{v}(A) = F \);
- \( \hat{v}(A \land B) = T \iff \hat{v}(A) = T \text{ and } \hat{v}(B) = T \);
- \( \hat{v}(A \lor B) = T \iff \hat{v}(A) = T \text{ or } \hat{v}(B) = T \) (possibly both);
- \( \hat{v}(A \rightarrow B) = F \iff \hat{v}(A) = T \text{ and } \hat{v}(B) = F \);
- \( \hat{v}(A \leftrightarrow B) = T \iff \hat{v}(A) = \hat{v}(B) \).
If a formula contains \(n\) distinct propositional variables, the number of possible interpretations (restricted to those variables) is \(2^n\).
An important remark. The connective \(\lor\) denotes inclusive disjunction (corresponding to the Latin vel): \(A \lor B\) is true whenever at least one of the two propositions is true, including the case in which both are true. It must be distinguished from exclusive disjunction (corresponding to the Latin aut, denoted \(\oplus\) or XOR), where \(A \oplus B\) is true if and only if \(A\) and \(B\) have different truth values. Symbolically:
\[ A \oplus B \;\equiv\; (A \lor B) \land \neg(A \land B) \;\equiv\; \neg(A \leftrightarrow B) \]
In ordinary English, the word "or" is genuinely ambiguous between the two readings; formal logic resolves this ambiguity by adopting the inclusive reading by default.
Logical Connectives and Functional Completeness
Logical connectives are truth-functional operators, that is, functions \(\{T,F\}^n \to \{T,F\}\):
- negation \(\neg\) is a unary operator;
- conjunction \(\land\), disjunction \(\lor\), conditional (or implication) \(\rightarrow\), and biconditional \(\leftrightarrow\) are binary operators.
A set of connectives is said to be functionally complete (or adequate) if every truth function \(\{T,F\}^n \to \{T,F\}\) can be expressed by combinations of those connectives. The following sets are all functionally complete:
\[ \{\neg, \land, \lor\}, \quad \{\neg, \land\}, \quad \{\neg, \lor\}, \quad \{\neg, \rightarrow\} \]
Moreover, there exist single binary connectives that are functionally complete on their own: Sheffer's stroke (NAND), denoted \(\uparrow\), and Peirce's arrow (NOR), denoted \(\downarrow\).
The semantic definitions justify the following reductions, which show that \(\rightarrow\) and \(\leftrightarrow\) are definable in terms of \(\{\neg, \land, \lor\}\):
\[ A \rightarrow B \equiv \neg A \lor B \]
\[ A \leftrightarrow B \equiv (A \rightarrow B) \land (B \rightarrow A) \equiv (A \land B) \lor (\neg A \land \neg B) \]
Truth Tables
A truth table is a tabular representation of the truth function associated with a formula. For a formula containing \(n\) distinct variables, the table has \(2^n\) rows, one for each possible interpretation.
The truth tables of the basic connectives are as follows:
| \(A\) | \(B\) | \(\neg A\) | \(A \land B\) | \(A \lor B\) | \(A \rightarrow B\) | \(A \leftrightarrow B\) |
|---|---|---|---|---|---|---|
| T | T | F | T | T | T | T |
| T | F | F | F | T | F | F |
| F | T | T | F | T | T | F |
| F | F | T | F | F | T | T |
Notice that the conditional \(A \rightarrow B\) is false only when the antecedent \(A\) is true and the consequent \(B\) is false: this is the sole row in which it takes the value \(F\).
Logical Equivalences
Two formulas \(A\) and \(B\) are said to be logically equivalent, written \(A \equiv B\), if they take the same truth value under every interpretation:
\[ A \equiv B \iff \forall v,\ \hat{v}(A) = \hat{v}(B) \]
The relation \(\equiv\) is an equivalence relation on \(\mathcal{F}\) (reflexive, symmetric, transitive) and a congruence: the substitution theorem states that if \(A \equiv B\) and \(C[A]\) is a formula containing \(A\) as a subformula, then \(C[A] \equiv C[B]\), where \(C[B]\) is obtained by replacing (an occurrence of) \(A\) by \(B\) in \(C\).
It is essential to distinguish \(\equiv\) (a metalinguistic relation between formulas) from \(\leftrightarrow\) (a connective of the object language); indeed,
\[ A \equiv B \iff \models A \leftrightarrow B \]
that is, \(A\) and \(B\) are logically equivalent if and only if \(A \leftrightarrow B\) is a tautology.
Fundamental Laws
The following equivalences, all provable by truth tables, constitute the fundamental laws of the propositional calculus (here \(\top\) denotes any tautology, \(\bot\) any contradiction):
- Idempotence: \(A \land A \equiv A\), \(\quad A \lor A \equiv A\)
- Commutativity: \(A \land B \equiv B \land A\), \(\quad A \lor B \equiv B \lor A\)
- Associativity: \((A \land B) \land C \equiv A \land (B \land C)\), and similarly for \(\lor\)
- Distributivity: \(A \land (B \lor C) \equiv (A \land B) \lor (A \land C)\), \(\quad A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)\)
- Double negation: \(\neg \neg A \equiv A\)
- De Morgan's laws: \(\neg(A \land B) \equiv \neg A \lor \neg B\), \(\quad \neg(A \lor B) \equiv \neg A \land \neg B\)
- Absorption: \(A \land (A \lor B) \equiv A\), \(\quad A \lor (A \land B) \equiv A\)
- Identity: \(A \land \top \equiv A\), \(\quad A \lor \bot \equiv A\)
- Domination: \(A \lor \top \equiv \top\), \(\quad A \land \bot \equiv \bot\)
- Law of excluded middle: \(A \lor \neg A \equiv \top\)
- Law of non-contradiction: \(A \land \neg A \equiv \bot\)
- Contraposition: \(A \rightarrow B \equiv \neg B \rightarrow \neg A\)
- Exportation: \((A \land B) \rightarrow C \equiv A \rightarrow (B \rightarrow C)\)
Tautologies, Satisfiability, and Logical Consequence
Let \(A \in \mathcal{F}\). One says that:
- \(A\) is a tautology (or a logically valid formula), written \(\models A\), if \(\hat{v}(A) = T\) under every interpretation \(v\);
- \(A\) is a contradiction (or an unsatisfiable formula) if \(\hat{v}(A) = F\) under every \(v\);
- \(A\) is satisfiable if there exists at least one interpretation \(v\) such that \(\hat{v}(A) = T\);
- \(A\) is contingent if it is satisfiable but not a tautology.
The four categories are linked by the duality:
\[ A \text{ is a tautology} \iff \neg A \text{ is a contradiction} \]
Let \(\Gamma \subseteq \mathcal{F}\) be a (possibly infinite) set of formulas, and \(B \in \mathcal{F}\). One says that \(B\) is a (semantic) logical consequence of \(\Gamma\), written
\[ \Gamma \models B \]
if for every interpretation \(v\) such that \(\hat{v}(A) = T\) for all \(A \in \Gamma\), one has \(\hat{v}(B) = T\). Equivalently: every model of \(\Gamma\) is a model of \(B\).
Semantic deduction theorem:
\[ \Gamma \cup \{A\} \models B \iff \Gamma \models A \rightarrow B \]
In particular, taking \(\Gamma = \emptyset\), we obtain \(A \models B\) if and only if \(\models A \rightarrow B\).
Normal Forms (CNF and DNF)
A literal is either a propositional variable or its negation: \(p\) or \(\neg p\). Accordingly:
- a disjunctive clause is a disjunction of literals: \(\ell_1 \lor \ell_2 \lor \dots \lor \ell_k\);
- a conjunctive clause is a conjunction of literals: \(\ell_1 \land \ell_2 \land \dots \land \ell_k\).
A formula is in:
- Conjunctive Normal Form (CNF) if it is a conjunction of disjunctive clauses;
- Disjunctive Normal Form (DNF) if it is a disjunction of conjunctive clauses.
Theorem (existence of normal forms). Every formula \(A \in \mathcal{F}\) is logically equivalent to a formula in CNF and to a formula in DNF.
Reduction procedure:
- eliminate the biconditional: \(A \leftrightarrow B \equiv (A \rightarrow B) \land (B \rightarrow A)\);
- eliminate the conditional: \(A \rightarrow B \equiv \neg A \lor B\);
- push negations inward until they apply only to variables (De Morgan's laws and double negation), yielding the negation normal form (NNF);
- apply distributivity to obtain the desired form: \(\lor\) over \(\land\) for DNF, \(\land\) over \(\lor\) for CNF.
Example:
\[ A \rightarrow (B \lor C) \;\equiv\; \neg A \lor (B \lor C) \;\equiv\; \neg A \lor B \lor C \]
which is simultaneously in CNF (a single disjunctive clause) and in DNF (a disjunction of conjunctive clauses reduced to single literals).
Deductive Systems
A deductive system (or logical calculus) is a purely syntactic apparatus consisting of axioms and inference rules, allowing one to derive formulas from premises without recourse to semantics. The key notion is that of derivability: one writes
\[ \Gamma \vdash A \]
to indicate that there exists a derivation of the formula \(A\) from the premises \(\Gamma\) within the chosen system.
The most widely used deductive systems for propositional logic are:
- Hilbert-style (axiomatic) systems: a few axiom schemes and a single inference rule (modus ponens);
- Natural deduction (Gentzen, Prawitz): introduction and elimination rules for each connective;
- Sequent calculus (Gentzen): rules acting on sequents \(\Gamma \Rightarrow \Delta\);
- Semantic tableaux (Beth, Smullyan): a refutation method based on trees.
The most important inference rules are:
Modus Ponens (\(\rightarrow\)-elimination):
\[ \dfrac{A \qquad A \rightarrow B}{B} \]
Modus Tollens (the contrapositive rule):
\[ \dfrac{A \rightarrow B \qquad \neg B}{\neg A} \]
Hypothetical syllogism (transitivity of the conditional):
\[ \dfrac{A \rightarrow B \qquad B \rightarrow C}{A \rightarrow C} \]
Disjunctive syllogism:
\[ \dfrac{A \lor B \qquad \neg A}{B} \]
Conjunction introduction and elimination:
\[ \dfrac{A \qquad B}{A \land B} \qquad\qquad \dfrac{A \land B}{A} \qquad\qquad \dfrac{A \land B}{B} \]
Reductio ad absurdum (proof by contradiction):
\[ \dfrac{\Gamma, \neg A \vdash \bot}{\Gamma \vdash A} \]
Soundness and Completeness
The relationship between syntactic derivability \(\vdash\) and semantic consequence \(\models\) is captured by the two fundamental metalogical theorems of propositional logic.
Soundness theorem. For every \(\Gamma \subseteq \mathcal{F}\) and every \(A \in \mathcal{F}\):
\[ \Gamma \vdash A \;\Longrightarrow\; \Gamma \models A \]
Whatever can be derived syntactically is genuinely a semantic consequence of the premises.
Completeness theorem (Post, 1921). For every \(\Gamma \subseteq \mathcal{F}\) and every \(A \in \mathcal{F}\):
\[ \Gamma \models A \;\Longrightarrow\; \Gamma \vdash A \]
Every semantic consequence can effectively be derived in the calculus.
Combining the two yields the equivalence between syntax and semantics:
\[ \Gamma \vdash A \iff \Gamma \models A \]
Two further metalogical results are worth mentioning:
- Compactness theorem: \(\Gamma\) is satisfiable if and only if every finite subset of \(\Gamma\) is satisfiable;
- Decidability: there exists an algorithm (for instance, the truth-table method) which, in finitely many steps, decides whether a given formula is a tautology.
Worked Examples
Example 1 — Reduction to normal form
Reduce \( (A \rightarrow B) \land \neg B \) to CNF and DNF.
Result
CNF: \( (\neg A \lor B) \land \neg B \) — DNF: \( \neg A \land \neg B \)
Solution
Eliminate the conditional via \( A \rightarrow B \equiv \neg A \lor B \):
\[ (A \rightarrow B) \land \neg B \;\equiv\; (\neg A \lor B) \land \neg B \]
which is already in CNF (a conjunction of two disjunctive clauses). To obtain the DNF, distribute \(\land\) over \(\lor\):
\[ (\neg A \lor B) \land \neg B \;\equiv\; (\neg A \land \neg B) \lor (B \land \neg B) \;\equiv\; \neg A \land \neg B \]
since \( B \land \neg B \equiv \bot \) by the law of non-contradiction. The result \( \neg A \land \neg B \) is a degenerate DNF: it consists of a single conjunctive clause, viewable as a disjunction with only one disjunct. By convention, a single conjunctive clause counts as being in DNF (just as a single disjunctive clause counts as being in CNF), even though no \(\lor\) appears explicitly.
Example 2 — Verifying a tautology (hypothetical syllogism)
Show that \( ((A \rightarrow B) \land (B \rightarrow C)) \rightarrow (A \rightarrow C) \) is a tautology.
Solution
We argue by contradiction: suppose there is an interpretation \(v\) under which the formula is false. For a conditional to be false, its antecedent must be true and its consequent false; hence:
- \( \hat{v}((A \rightarrow B) \land (B \rightarrow C)) = T \), so \( \hat{v}(A \rightarrow B) = T \) and \( \hat{v}(B \rightarrow C) = T \);
- \( \hat{v}(A \rightarrow C) = F \), whence \( \hat{v}(A) = T \) and \( \hat{v}(C) = F \).
From \( \hat{v}(A) = T \) and \( \hat{v}(A \rightarrow B) = T \) it follows that \( \hat{v}(B) = T \) (otherwise the conditional would be false). From \( \hat{v}(B) = T \) and \( \hat{v}(B \rightarrow C) = T \) we get \( \hat{v}(C) = T \), contradicting \( \hat{v}(C) = F \). Hence the formula is a tautology.
Example 3 — Logical consequence and the resolution rule
Verify that \( \{A \lor B,\ \neg A \lor C\} \models B \lor C \).
Solution
Let \(v\) be an interpretation satisfying both premises. We split into two cases according to the value of \( \hat{v}(A) \):
- if \( \hat{v}(A) = T \), then from \( \hat{v}(\neg A \lor C) = T \) we must have \( \hat{v}(C) = T \), hence \( \hat{v}(B \lor C) = T \);
- if \( \hat{v}(A) = F \), then from \( \hat{v}(A \lor B) = T \) we have \( \hat{v}(B) = T \), hence \( \hat{v}(B \lor C) = T \).
In both cases \( \hat{v}(B \lor C) = T \), proving the entailment. This principle is the resolution rule, the cornerstone of automated theorem proving: from the clauses \( A \lor B \) and \( \neg A \lor C \) one infers the resolvent \( B \lor C \).
Propositional logic represents the first level of formalisation of mathematical reasoning. Despite its limited expressive power — it cannot describe the internal structure of propositions — it provides the conceptual foundations for tackling first-order logic, axiomatic theories, metalogic, and the associated algebraic structures (Boolean algebras, lattices). Mastering it is an indispensable prerequisite for any rigorous study of mathematics and theoretical computer science.