42.01.01 · mathematical-logic / first-order-logic-completeness

Propositional Logic as a Formal System

shipped3 tiersLean: none

Anchor (Master): Enderton 2001 *A Mathematical Introduction to Logic* 2e Ch. 1 in full (functional completeness, normal forms, the compactness theorem for sentential logic, completeness of the deductive calculus); Mendelson 2015 *Introduction to Mathematical Logic* 6e (CRC) Ch. 1; Post 1921 *Amer. J. Math.* 43 (truth-table completeness); Cook 1971 (the NP-completeness of satisfiability)

Intuition Beginner

You already know how to fill in a truth table: take a sentence built from smaller sentences using and, or, not, and if-then, try every combination of true and false for the small parts, and read off whether the whole thing comes out true. That practical skill is the starting point. This unit asks a sharper question: what is a sentence of logic, exactly, as an object you could hand to a machine, and what does it mean for one sentence to follow from others?

The move is the same one mathematics makes everywhere. To study numbers carefully you first say precisely what counts as a number and what counts as a legal operation. To study logical reasoning carefully you first say precisely what counts as a formula and what counts as a legal step of reasoning. A formula stops being an informal English sentence and becomes a string built by fixed rules from a fixed alphabet, like a well-formed arithmetic expression with its parentheses in the right places.

Two different questions then pull apart. One is about meaning: under which assignments of true and false does a formula come out true? That is the world of truth tables. The other is about proof: starting from some assumptions, which formulas can you reach by mechanical rules that never mention truth at all? The headline result of the subject is that these two questions give the same answer. Everything true-in-all-cases is provable, and everything provable is true-in-all-cases.

This is the warm-up. Every idea here — a language, its meanings, a proof system, and the match between them — returns in a harder form when we add for all and there exists later in the chapter.

Visual Beginner

A formula is a built-up thing. The same way an arithmetic expression like $(3 + 4) \times 2$ has a tree showing which operation is on the outside, every logical formula has one connective on the very outside and smaller formulas hanging below it. The diagram shows the construction tree of one formula, alongside its truth table.

   Formula:  ( (not p)  or  q )

   Construction tree (outermost connective on top):

                 OR
                /    \
             NOT      q
              |
              p

   Truth table (work bottom-up: first not-p, then or with q):

      p | q | not p | (not p) or q
      --+---+-------+--------------
      T | T |   F   |      T
      T | F |   F   |      F
      F | T |   T   |      T
      F | F |   T   |      T

Read the tree from the bottom. The atoms $p$ and $q$ are the leaves. The branch on the left applies not to $p$ . The root applies or to the two pieces below it. The truth table just walks the same tree: you compute the value at each leaf, then each node above, until you reach the root. The outermost connective — here or — is what the whole formula "is."

input row	value of $p$	value of $q$	whole formula
1	T	T	T
2	T	F	F
3	F	T	T
4	F	F	T

The formula comes out false in exactly one of the four cases, so it is true in most rows but not all — it is not a formula that holds no matter what.

Worked example Beginner

We test whether the formula "if $p$ then $q$ " together with " $p$ " forces " $q$ " — the pattern called modus ponens. The claim to check is that whenever the two assumptions are both true, the conclusion $q$ is also true.

Step 1. Write the assumptions. The first is the conditional $p \to q$ , read "if $p$ then $q$ ." The second is just $p$ . The candidate conclusion is $q$ .

Step 2. Recall the meaning of the conditional. The expression $p \to q$ is false only in the single case where $p$ is true and $q$ is false; in the other three rows it is true. This is the standard truth table for "if-then" in logic.

Step 3. Build the table for both assumptions and the conclusion.

$p$	$q$	$p \to q$	both assumptions true?	$q$
T	T	T	yes ( $p$ true and $p \to q$ true)	T
T	F	F	no	F
F	T	T	no ( $p$ is false)	T
F	F	T	no ( $p$ is false)	F

Step 4. Look only at the rows where both assumptions are true. There is exactly one such row, the first. In that row $q$ is true.

Step 5. Conclude. In every case where $p \to q$ and $p$ are both true, $q$ is true as well.

What this tells us: the conclusion $q$ holds in every situation that makes the assumptions hold, so $q$ genuinely follows from ${p \to q, p}$ . The next sections make "follows from" precise as a relation written with the symbol $⊨$ , and then build a separate proof machine that reaches the same conclusions by rule-pushing.

Check your understanding Beginner

Formal definition Intermediate+

The sentential language is built from a fixed alphabet. Fix a countable set of sentence symbols $A_{1}, A_{2}, A_{3}, \dots$ (the propositional variables), the five connective symbols $\neg, \land, \lor, \to, \leftrightarrow$ , and the two parentheses. An expression is any finite string over this alphabet. The well-formed formulas (wffs) form the smallest set $W$ of expressions containing every sentence symbol and closed under the five formula-building operations $$ \mathcal{E}{\neg}(\alpha) = (\neg \alpha), \qquad \mathcal{E}{\wedge}(\alpha,\beta) = (\alpha \wedge \beta), $$ and likewise $E_{\lor}, E_{\to}, E_{\leftrightarrow}$ . Equivalently $W = ⋃_{n} W_{n}$ where $W_{0}$ is the set of sentence symbols and $W_{n + 1}$ adjoins all $E_{c}$ -images of members of $W_{n}$ ^{[Enderton §1.1]}. Sentential variables $α, β, γ$ range over wffs.

A truth assignment is a function $v : {A_{1}, A_{2}, \dots} \to {F, T}$ on the sentence symbols (or on a subset containing those that occur in the formulas under discussion). Its recursive extension $\overset{v}{ˉ} : W \to {F, T}$ is the unique extension agreeing with $v$ on sentence symbols and respecting the connectives by their truth tables: $\overset{v}{ˉ} ((\neg α)) = T$ iff $\overset{v}{ˉ} (α) = F$ ; $\overset{v}{ˉ} ((α \land β)) = T$ iff both are $T$ ; $\overset{v}{ˉ} ((α \lor β)) = T$ iff at least one is $T$ ; $\overset{v}{ˉ} ((α \to β)) = F$ iff $\overset{v}{ˉ} (α) = T$ and $\overset{v}{ˉ} (β) = F$ ; and $\overset{v}{ˉ} ((α \leftrightarrow β)) = T$ iff the two agree. Uniqueness of $\overset{v}{ˉ}$ is the content of the parsing theorem below.

A wff $τ$ is a tautology if $\overset{v}{ˉ} (τ) = T$ for every truth assignment $v$ ; satisfiable if $\overset{v}{ˉ} (τ) = T$ for at least one. A set $Σ$ of wffs tautologically implies $τ$ , written $Σ ⊨ τ$ , if every $v$ with $\overset{v}{ˉ} (σ) = T$ for all $σ \in Σ$ also has $\overset{v}{ˉ} (τ) = T$ . Two wffs are tautologically equivalent when each implies the other. The notion $\emptyset ⊨ τ$ , abbreviated $⊨ τ$ , is exactly tautologyhood. This semantic consequence relation is the precise form of the "follows from" of the Beginner tier, sharpening the truth-table check of 25.01.01 into a relation on arbitrary formula sets ^{[Enderton §1.2]}.

Counterexamples to common slips Intermediate+

"A formula is just any string of symbols and connectives." Only the inductively generated strings are wffs. The string $) \neg \land A_{1} ($ is an expression but not a wff; the closure clause, not mere symbol membership, defines $W$ , which is why the parsing theorem has content.
" $Σ ⊨ τ$ means $τ$ is a tautology." It means $τ$ is true under every assignment that satisfies $Σ$ , a weaker demand relative to the restricted class of assignments. ${A_{1}} ⊨ A_{1}$ holds though $A_{1}$ is not a tautology. Tautologyhood is the special case $Σ = \emptyset$ .
"If $Σ$ is unsatisfiable then $Σ ⊨ τ$ fails for every $τ$ ." The reverse holds: an unsatisfiable $Σ$ tautologically implies every wff, vacuously, since there are no assignments to satisfy the premise. Inconsistency is maximal, not minimal, in consequence.
"The conditional $α \to β$ asserts a causal or relevance link between $α$ and $β$ ." It is the material conditional: false in the single row $\overset{v}{ˉ} (α) = T$ , $\overset{v}{ˉ} (β) = F$ and true otherwise. A false antecedent makes it true regardless of $β$ , which has no bearing on relevance.

Key theorem with proof Intermediate+

The signature theorem of the language layer is unique readability: the inductive definition of wffs is genuinely a definition by recursion, because every non-atomic wff decomposes in exactly one way. Without it the extension $\overset{v}{ˉ}$ would be ambiguous and truth-value assignment ill-defined.

Theorem (Unique readability / the parsing theorem). Every wff $α$ is exactly one of: a sentence symbol; or $(\neg β)$ for a unique wff $β$ ; or $(β □ γ)$ for a unique binary connective $□ \in {\land, \lor, \to, \leftrightarrow}$ and unique wffs $β, γ$ . In particular no wff is a proper initial segment of another, and the main connective and immediate subformulas of a non-atomic wff are determined by the string alone ^{[Enderton §1.2]}.

Proof. Assign to each symbol a weight: each left parenthesis counts $+ 1$ , each right parenthesis $- 1$ , each binary connective $- 1$ , and sentence symbols and $\neg$ count $0$ . Define the balance of an expression as the running total of weights read left to right. A first induction on the construction of wffs shows that every wff has total balance $0$ and every proper nonempty initial segment of a wff has balance $\geq 1$ (it begins with a surplus left parenthesis never yet closed). The base case: a sentence symbol has balance $0$ and no proper nonempty initial segment. The inductive step for $(\neg β)$ and $(β □ γ)$ tracks the leading "(" which raises the count to $1$ and is closed only by the final ")".

This balance property gives the non-segment claim: if $α$ were a proper initial segment of $α^{'}$ , then $α$ has balance $0$ while being a proper initial segment, contradicting that proper initial segments of the wff $α^{'}$ have balance $\geq 1$ . For uniqueness of decomposition, a non-atomic wff begins with "(" by construction, so it is $(\neg \dots)$ or $(β □ γ \dots)$ . If it is $(\neg β)$ the remainder after $\neg$ up to the matching ")" is forced. If it is $(β □ γ)$ , the first place where the running balance (started after the opening "(") returns to $0$ marks the end of $β$ ; since no proper initial segment of the wff $β$ has balance $0$ , the substring $β$ is determined, hence so is the connective $□$ immediately after it and the remaining wff $γ$ . Thus the decomposition is unique. $□$

Corollary (recursion principle). Given a set $V$ , functions $h_{c}$ for each connective, and a function $h_{0}$ on sentence symbols, there is a unique $\overset{ˉ}{h} : W \to V$ with $\overset{ˉ}{h} (A_{i}) = h_{0} (A_{i})$ and $\overset{ˉ}{h} (E_{c} (\dots)) = h_{c} (\overset{ˉ}{h} (\dots))$ . Applying this with $V = {F, T}$ and the connective truth tables yields the unique extension $\overset{v}{ˉ}$ of any truth assignment $v$ , so the semantics of the Formal definition is well posed.

Bridge. Unique readability is the foundational reason the semantics of the language is unambiguous, and it is exactly the parsing fact that lets a truth assignment extend by recursion to a single value on every formula. This builds toward functional completeness — once $\overset{v}{ˉ}$ is well defined, a wff is a Boolean function of its atoms and one asks which functions arise — and it appears again in first-order logic 42.01.03 pending, where the same balance argument is re-run for terms and formulas with quantifiers and the recursion principle underwrites Tarski's satisfaction definition. The central insight is that an inductively built syntax admits definition by recursion precisely when its constructors are injective with disjoint ranges; this is exactly the unique-readability condition, and it generalises from the five sentential connectives to any algebraic signature. Putting these together, the language layer (syntax plus its unambiguous semantics) is now fixed, and the rest of the unit runs two parallel developments over it — the space of Boolean functions a formula can express, and a proof calculus that reaches the tautologies by rule — meeting in the soundness and completeness theorem.

Exercises Intermediate+

Exercise 3 (medium, symbolic).

Show that ${α \to β, α} ⊨ β$ (modus ponens is sound as a tautological implication), and that $⊨ (α \to β) \leftrightarrow ((\neg β) \to (\neg α))$ (contraposition is a tautology).

Hint

For the first, examine the rows with $\overset{v}{ˉ} (α) = T$ . For the second, both sides are false in exactly the same row.

Answer

For modus ponens, suppose $\overset{v}{ˉ} (α \to β) = T$ and $\overset{v}{ˉ} (α) = T$ . Since $α \to β$ is false only when $\overset{v}{ˉ} (α) = T, \overset{v}{ˉ} (β) = F$ , and that case is excluded by $\overset{v}{ˉ} (α \to β) = T$ , we get $\overset{v}{ˉ} (β) = T$ . Every assignment satisfying both premises satisfies $β$ , so ${α \to β, α} ⊨ β$ . For contraposition, $\overset{v}{ˉ} (α \to β) = F$ iff $\overset{v}{ˉ} (α) = T, \overset{v}{ˉ} (β) = F$ ; and $\overset{v}{ˉ} ((\neg β) \to (\neg α)) = F$ iff $\overset{v}{ˉ} (\neg β) = T, \overset{v}{ˉ} (\neg α) = F$ , i.e. $\overset{v}{ˉ} (β) = F, \overset{v}{ˉ} (α) = T$ — the same row. The two sides have identical truth tables, so the biconditional is true under every $v$ and is a tautology. Rubric: full credit for isolating the single false-row of each conditional and matching them.

Exercise 7 (hard, symbolic).

Prove the disjunctive-normal-form theorem: every wff $φ$ in sentence symbols $A_{1}, \dots, A_{n}$ is tautologically equivalent to a DNF, and deduce functional completeness of ${\neg, \land, \lor}$ .

Hint

For each assignment $v$ with $\overset{v}{ˉ} (φ) = T$ , form the conjunction of literals $ℓ_{i}^{v}$ where $ℓ_{i}^{v} = A_{i}$ if $v (A_{i}) = T$ and $\neg A_{i}$ otherwise. Disjoin these clauses.

Answer

If $φ$ is unsatisfiable, it is equivalent to $A_{1} \land \neg A_{1}$ , a (degenerate) DNF. Otherwise let $S = {v : \overset{v}{ˉ} (φ) = T}$ , a nonempty finite set of assignments to $A_{1}, \dots, A_{n}$ . For $v \in S$ set $C_{v} = ℓ_{1}^{v} \land \dots \land ℓ_{n}^{v}$ with $ℓ_{i}^{v} = A_{i}$ if $v (A_{i}) = T$ and $ℓ_{i}^{v} = \neg A_{i}$ if $v (A_{i}) = F$ . Then $\overset{w}{ˉ} (C_{v}) = T$ iff $w$ agrees with $v$ on all $A_{i}$ , i.e. iff $w = v$ on the relevant symbols. Let $ψ = ⋁_{v \in S} C_{v}$ . For any assignment $w$ : $\overset{w}{ˉ} (ψ) = T$ iff $w$ equals some $v \in S$ iff $\overset{w}{ˉ} (φ) = T$ . Hence $φ$ and $ψ$ are tautologically equivalent, and $ψ$ is a DNF using only $\neg, \land, \lor$ . Every Boolean function $f : {F, T}^{n} \to {F, T}$ is the function computed by some such $φ$ (take any wff with that table, e.g. build $ψ$ directly from $f$ 's true rows), so ${\neg, \land, \lor}$ realises every Boolean function and is functionally complete. Rubric: full credit for the clause construction, the agreement lemma $\overset{w}{ˉ} (C_{v}) = T \Leftrightarrow w = v$ , and the deduction to completeness.

Exercise 8 (hard, symbolic).

A binary connective is adequate by itself (functionally complete as a singleton) only if its truth table is not truth-preserving (sends all- $T$ to $T$ ) and not falsity-preserving (sends all- $F$ to $F$ ). Use this to show ${\to}$ alone is not functionally complete, while NAND is.

Hint

Evaluate each connective on the all-true assignment. A connective preserving truth can never produce a formula false everywhere from premises true everywhere.

Answer

The implication $\to$ is truth-preserving: $\overset{v}{ˉ} (α \to β) = T$ whenever $\overset{v}{ˉ} (α) = \overset{v}{ˉ} (β) = T$ . By induction on formula structure, any wff built solely from $\to$ takes value $T$ under the all-true assignment $v_{T}$ (base case: each sentence symbol is $T$ ; step: a $\to$ of two formulas evaluating to $T$ evaluates to $T$ ). Therefore no $\to$ -only formula computes $\neg A_{1}$ , which is $F$ under $v_{T}$ ; the negation function is unreachable, so ${\to}$ is not complete. NAND fails both preservation tests: $T ∣ T = F$ (not truth-preserving) and $F ∣ F = T$ (not falsity-preserving). Together with self-duality bookkeeping this is exactly Post's criterion permitting NAND to be singly adequate, and Exercise 5 exhibits the explicit encodings of $\neg$ and $\lor$ . Rubric: full credit for the truth-preservation invariant blocking $\to$ and the two-row computation showing NAND escapes both preservation classes.

Advanced results Master

The semantics fixes which Boolean functions formulas compute; the deductive calculus reaches the tautologies syntactically; and the two layers are identified by soundness and completeness, after which compactness and the complexity of the decision problem follow.

Theorem 1 (functional completeness and Post's adequacy criterion). Every function $f : {F, T}^{n} \to {F, T}$ is computed by some wff in $A_{1}, \dots, A_{n}$ ; the disjunctive-normal-form construction exhibits one, so ${\neg, \land, \lor}$ is functionally complete, as are ${\neg, \land}$ , ${\neg, \lor}$ , ${\neg, \to}$ , the Sheffer stroke $∣$ (NAND), and the joint denial $↓$ (NOR) ^{[Post 1921]}. A set of connectives is adequate if and only if it is not contained in any of the five Post maximal closed classes: the truth-preserving, the falsity-preserving, the monotone, the self-dual, and the affine (linear) functions. The stroke lies outside all five, which is why it is singly adequate; ${\to}$ lies in the truth-preserving class and is not. Both DNF and the dual conjunctive normal form (a conjunction of disjunctions of literals) exist for every wff, the CNF being read from the falsifying rows.

Theorem 2 (a Hilbert-style deductive calculus and the deduction theorem). Fix the three axiom schemata over wffs (with $\neg, \to$ as primitive and the others defined): $$ \text{(A1)}\ \alpha\rightarrow(\beta\rightarrow\alpha), \quad \text{(A2)}\ (\alpha\rightarrow(\beta\rightarrow\gamma))\rightarrow((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma)), \quad \text{(A3)}\ ((\neg\beta)\rightarrow(\neg\alpha))\rightarrow(\alpha\rightarrow\beta), $$ with the single rule modus ponens: from $α$ and $α \to β$ infer $β$ . A deduction of $τ$ from $Σ$ is a finite sequence of wffs ending in $τ$ , each an axiom, a member of $Σ$ , or a modus-ponens consequence of two earlier entries; one writes $Σ ⊢ τ$ ^{[Mendelson Ch. 1]}. The deduction theorem holds: $Σ \cup {α} ⊢ β$ iff $Σ ⊢ (α \to β)$ , proved by induction on the length of the deduction using A1 and A2. The turnstile $⊢$ is the purely syntactic counterpart of $⊨$ , defined without reference to truth.

Theorem 3 (soundness and completeness of sentential logic). For every set $Σ$ of wffs and every wff $τ$ , $$ \Sigma \vdash \tau \quad\Longleftrightarrow\quad \Sigma \models \tau. $$ The forward direction (soundness) is the induction: each axiom is a tautology and modus ponens preserves tautological consequence, so every deducible $τ$ is a tautological consequence. The reverse direction (completeness) reduces to: every consistent $Σ$ is satisfiable. One extends $Σ$ to a maximal consistent $Σ^{*}$ by a Lindenbaum enumeration (adjoin each wff or its negation, preserving consistency), then the assignment $v (A_{i}) = T \Leftrightarrow A_{i} \in Σ^{*}$ satisfies $Σ^{*} \supseteq Σ$ , because membership in a maximal consistent set respects the connectives ^{[Enderton §1.7]}. The full Henkin/Lindenbaum apparatus reappears with witnessing constants for the first-order completeness theorem 42.01.06 pending; here no witnesses are needed.

Theorem 4 (compactness for sentential logic). A set $Σ$ of wffs is satisfiable if and only if every finite subset of $Σ$ is satisfiable; equivalently $Σ ⊨ τ$ iff $Σ_{0} ⊨ τ$ for some finite $Σ_{0} \subseteq Σ$ ^{[Enderton §1.7]}. The deductive route is immediate: $Σ$ is satisfiable iff $Σ$ is consistent (by Theorem 3), and consistency is a finitary condition because a deduction of a contradiction uses only finitely many premises. A purely semantic proof runs through König's lemma on the binary tree of partial assignments, or through the topological compactness of ${F, T}^{ω}$ (Tychonoff), of which this theorem is the namesake instance. Compactness is the first theorem genuinely about infinite premise sets and is co-produced as 42.01.02 pending.

Theorem 5 (decidability and the complexity of validity). Tautologyhood is decidable: the truth-table algorithm tests all $2^{n}$ assignments to the $n$ sentence symbols of $τ$ and accepts iff all give $T$ , a terminating procedure. The associated decision problems are satisfiability (SAT) — does some assignment satisfy $τ$ — and its complement, validity. By Cook's theorem SAT is NP-complete, so validity (tautologyhood) is co-NP-complete ^{[Cook 1971]}; the truth-table procedure is correct but runs in time $Θ (2^{n})$ up to polynomial factors, and a polynomial decision procedure would prove $P = NP$ . The complexity story is developed in 25.03.01; logically, decidability is what sharply separates the propositional warm-up from first-order logic, where validity is only semi-decidable (Church-Turing).

Synthesis. The four layers built here — language, semantics, deductive calculus, and the metatheorem linking them — are the foundational reason propositional logic is the template for the whole chapter: unique readability makes the recursion that defines $\overset{v}{ˉ}$ well posed, functional completeness shows a wff is a Boolean function and fixes how much the language can say, and the calculus $⊢$ reaches exactly the tautologies, which is the central insight that $⊢$ and $⊨$ coincide. This is exactly the soundness-completeness pair, and it generalises: the same architecture — a recursively defined language, a Tarskian satisfaction relation, a Hilbert or natural-deduction calculus, and a Lindenbaum-Henkin completeness proof — is re-run with quantifiers and structures to give Gödel's first-order completeness theorem 42.01.06 pending. Putting these together, compactness is dual to the finitary nature of deduction: a contradiction needs only finitely many premises, so unsatisfiability is finitely witnessed, and this is the bridge from the syntactic finiteness of proofs to the semantic statement about infinite theories that powers the Löwenheim-Skolem and nonstandard-model phenomena of model theory. The decidability of propositional validity, contrasted with the mere semi-decidability of first-order validity, marks precisely where the warm-up ends and the genuine difficulty of logic begins.

Full proof set Master

Proposition 1 (soundness of the sentential calculus). If $Σ ⊢ τ$ then $Σ ⊨ τ$ .

Proof. Induct on the length of a deduction $α_{1}, \dots, α_{m} = τ$ from $Σ$ . For each $k$ we show $Σ ⊨ α_{k}$ . If $α_{k} \in Σ$ this is immediate. If $α_{k}$ is an axiom, then $α_{k}$ is a tautology: A1, A2, A3 are checked tautologies by their truth tables (each is false in no row), and a tautology is implied by every $Σ$ , vacuously on the premise side. If $α_{k}$ follows by modus ponens from $α_{i}$ and $α_{j} = (α_{i} \to α_{k})$ with $i, j < k$ , then by induction $Σ ⊨ α_{i}$ and $Σ ⊨ (α_{i} \to α_{k})$ ; for any $v$ satisfying $Σ$ , $\overset{v}{ˉ} (α_{i}) = T$ and $\overset{v}{ˉ} (α_{i} \to α_{k}) = T$ force $\overset{v}{ˉ} (α_{k}) = T$ by the conditional's truth table. Hence $Σ ⊨ α_{k}$ . Taking $k = m$ gives $Σ ⊨ τ$ . $□$

Proposition 2 (deduction theorem). $Σ \cup {α} ⊢ β$ iff $Σ ⊢ (α \to β)$ .

Proof. If $Σ ⊢ (α \to β)$ then adjoining $α$ to the premises and one modus ponens yields $β$ , so $Σ \cup {α} ⊢ β$ . Conversely let $β_{1}, \dots, β_{m} = β$ be a deduction from $Σ \cup {α}$ . By induction on $k$ we show $Σ ⊢ (α \to β_{k})$ . If $β_{k}$ is an axiom or lies in $Σ$ , then from $β_{k}$ and the instance $β_{k} \to (α \to β_{k})$ of A1, modus ponens gives $α \to β_{k}$ . If $β_{k} = α$ , then $α \to α$ is a theorem (a standard A1/A2 derivation), so $Σ ⊢ (α \to β_{k})$ . If $β_{k}$ comes by modus ponens from $β_{i}$ and $β_{j} = (β_{i} \to β_{k})$ , then by induction $Σ ⊢ (α \to β_{i})$ and $Σ ⊢ (α \to (β_{i} \to β_{k}))$ ; the A2 instance $(α \to (β_{i} \to β_{k})) \to ((α \to β_{i}) \to (α \to β_{k}))$ with two modus ponens steps yields $Σ ⊢ (α \to β_{k})$ . At $k = m$ this is $Σ ⊢ (α \to β)$ . $□$

Proposition 3 (completeness — Lindenbaum and the canonical assignment). If $Σ$ is consistent (no wff $γ$ has $Σ ⊢ γ$ and $Σ ⊢ \neg γ$ ) then $Σ$ is satisfiable; consequently $Σ ⊨ τ \Rightarrow Σ ⊢ τ$ .

Proof. Enumerate all wffs $γ_{0}, γ_{1}, \dots$ (the language is countable). Define $Σ_{0} = Σ$ and, having defined consistent $Σ_{k}$ , set $Σ_{k + 1} = Σ_{k} \cup {γ_{k}}$ if that is consistent, else $Σ_{k + 1} = Σ_{k} \cup {\neg γ_{k}}$ . At least one choice is consistent: if both $Σ_{k} \cup {γ_{k}}$ and $Σ_{k} \cup {\neg γ_{k}}$ were inconsistent, the deduction theorem would give $Σ_{k} ⊢ \neg γ_{k}$ and $Σ_{k} ⊢ \neg\neg γ_{k}$ , contradicting consistency of $Σ_{k}$ . Let $Σ^{*} = ⋃_{k} Σ_{k}$ . Then $Σ^{*}$ is consistent (any deduction of a contradiction uses finitely many premises, hence lies in some $Σ_{k}$ ) and maximal: for every $γ$ , exactly one of $γ, \neg γ$ is in $Σ^{*}$ .

Maximal consistent sets respect the connectives: $\neg γ \in Σ^{*} \Leftrightarrow γ \in / Σ^{*}$ , and $(γ \to δ) \in Σ^{*} \Leftrightarrow (γ \in / Σ^{*} or δ \in Σ^{*})$ , each a short derivation from the axioms and the deduction theorem. Define $v (A_{i}) = T \Leftrightarrow A_{i} \in Σ^{*}$ . A structural induction on wffs $γ$ , using the connective-respecting clauses, gives $\overset{v}{ˉ} (γ) = T \Leftrightarrow γ \in Σ^{*}$ . In particular $\overset{v}{ˉ} (σ) = T$ for every $σ \in Σ \subseteq Σ^{*}$ , so $v$ satisfies $Σ$ and $Σ$ is satisfiable. For the consequence: if $Σ ⊨ τ$ but $Σ \neq ⊢ τ$ , then $Σ \cup {\neg τ}$ is consistent (else the deduction theorem gives $Σ ⊢ \neg\neg τ$ and $Σ ⊢ τ$ ), hence satisfiable by some $v$ with $\overset{v}{ˉ} (\neg τ) = T$ , i.e. $\overset{v}{ˉ} (τ) = F$ while $v$ satisfies $Σ$ — contradicting $Σ ⊨ τ$ . Thus $Σ ⊢ τ$ . $□$

Proposition 4 (compactness via completeness). $Σ$ is satisfiable iff every finite $Σ_{0} \subseteq Σ$ is satisfiable.

Proof. The forward direction is immediate, as a satisfying assignment for $Σ$ satisfies each subset. Conversely, suppose $Σ$ is unsatisfiable. By Proposition 3 (contrapositive) $Σ$ is inconsistent, so $Σ ⊢ γ$ and $Σ ⊢ \neg γ$ for some $γ$ . Each deduction is finite and uses only finitely many premises from $Σ$ ; let $Σ_{0}$ be their union, a finite subset with $Σ_{0} ⊢ γ$ and $Σ_{0} ⊢ \neg γ$ . Then $Σ_{0}$ is inconsistent, hence by soundness (Proposition 1) unsatisfiable. So some finite subset is unsatisfiable, the contrapositive of the claim. $□$

Proposition 5 (disjunctive normal form and functional completeness). Every wff $φ$ in $A_{1}, \dots, A_{n}$ is tautologically equivalent to a disjunctive normal form over ${\neg, \land, \lor}$ , and every Boolean function ${F, T}^{n} \to {F, T}$ is realised by such a wff.

Proof. If $φ$ is satisfied by no assignment, it is equivalent to $A_{1} \land \neg A_{1}$ . Otherwise let $S = {v : \overset{v}{ˉ} (φ) = T} \neq = \emptyset$ on the symbols $A_{1}, \dots, A_{n}$ . For $v \in S$ put $C_{v} = ⋀_{i = 1}^{n} ℓ_{i}^{v}$ with $ℓ_{i}^{v} = A_{i}$ if $v (A_{i}) = T$ , else $\neg A_{i}$ . Then for any assignment $w$ , $\overset{w}{ˉ} (C_{v}) = T$ iff $w$ and $v$ agree on all $A_{i}$ . Set $ψ = ⋁_{v \in S} C_{v}$ . For each $w$ : $\overset{w}{ˉ} (ψ) = T$ iff $w$ agrees with some $v \in S$ iff $\overset{w}{ˉ} (φ) = T$ , so $φ \equiv ψ$ and $ψ$ is a DNF. Given an arbitrary $f : {F, T}^{n} \to {F, T}$ , apply the construction to its set of true rows $S_{f} = {v : f (v) = T}$ to obtain a wff $ψ_{f}$ with $\overset{v}{ˉ} (ψ_{f}) = f (v)$ for all $v$ ; if $S_{f} = \emptyset$ take $A_{1} \land \neg A_{1}$ . Hence every Boolean function is realised over ${\neg, \land, \lor}$ , which is therefore functionally complete; the encodings $α \land β \equiv \neg (\neg α \lor \neg β)$ and the stroke identities of the Intermediate exercises pass completeness to ${\neg, \lor}$ , ${\neg, \land}$ , and NAND. $□$

Connections Master

Propositional logic and truth tables 25.01.01 is the elementary entry point this unit supersedes in rigor: that unit teaches the truth-table reading of $\neg, \land, \lor, \to, \leftrightarrow$ and the informal notion of tautology and validity for a working logician, and it remains the right first contact with the connectives. This unit rebuilds the same material as a formal system — the inductively defined language with unique readability, the semantic consequence relation $⊨$ on arbitrary premise sets, a Hilbert-style calculus with $⊢$ , and the soundness-completeness identification — so that the truth-table check of 25.01.01 is recovered here as the decision procedure for the $⊨$ defined formally.
Compactness for propositional and first-order logic, co-produced as 42.01.02 pending, extends Theorem 4: this unit proves sentential compactness as a corollary of completeness and as the namesake instance of Tychonoff compactness of ${F, T}^{ω}$ , and 42.01.02 pending develops the first-order compactness theorem and its model-theoretic harvest (nonstandard models, Löwenheim-Skolem interaction, finite-axiomatisability failures). The connection matters because compactness is the first place the finitary nature of proof — a deduction has finitely many premises — visibly controls the semantics of infinite theories.
First-order logic: syntax, terms, and formulas, co-produced as 42.01.03 pending, re-runs the language layer of this unit with quantifiers: the balance/unique-readability argument of the Key theorem is re-proved for terms and formulas with $\forall, \exists$ , the recursion principle underwrites Tarski's satisfaction relation in place of the truth-assignment extension $\overset{v}{ˉ}$ , and the Hilbert calculus gains quantifier axioms. This unit owns the propositional skeleton — connectives, $\overset{v}{ˉ}$ , $⊢$ , completeness via Lindenbaum — that 42.01.03 pending and the first-order completeness theorem 42.01.06 pending specialise and extend with Henkin witnesses.
The complexity of satisfiability and NP-completeness 25.03.01 is the computational face of Theorem 5: Cook's theorem identifies SAT as NP-complete, making propositional validity co-NP-complete, so the truth-table decision procedure proved correct here is exponential and the existence of a polynomial one is the $P$ vs $NP$ question. The connection routes the decidability statement of this unit into computational complexity, where the propositional satisfiability problem is the canonical hard problem.

Historical & philosophical context Master

The truth-functional analysis of the connectives crystallised in the early twentieth century. Gottlob Frege's Begriffsschrift (1879) introduced a formal proof system with a conditional and negation as primitives and modus ponens as the rule, the ancestor of the Hilbert-style calculus of Theorem 2. Bertrand Russell and Alfred North Whitehead's Principia Mathematica (1910-13) systematised propositional inference, taking $\neg$ and $\lor$ as primitive. Ludwig Wittgenstein's Tractatus Logico-Philosophicus (1921) presented the truth-table as displaying the sense of a proposition as a truth-function of its constituents.

Emil Post's 1921 paper Introduction to a general theory of elementary propositions ^{[Post 1921]} is the metatheoretic turning point: Post proved the truth-table method a complete decision procedure, established functional completeness and the classification of adequate connective sets (the five maximal closed classes now bearing his name), and proved the Post-completeness of the propositional calculus. Henry Sheffer had shown in 1913 that a single connective — the stroke — suffices, the result re-derived in the exercises. The soundness and completeness of the calculus relative to truth-table semantics, with the Lindenbaum maximal-consistent-set construction of Proposition 3, became the standard treatment in Hilbert and Ackermann's Grundzüge der theoretischen Logik (1928) and Mendelson's textbook ^{[Mendelson Ch. 1]}. Stephen Cook's 1971 theorem ^{[Cook 1971]} placed the decision problem in complexity theory by proving SAT NP-complete, recasting the practical cost of the truth-table procedure as the defining hard problem of the class NP.

Bibliography Master

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@book{mendelson2015logic,
  author    = {Mendelson, Elliott},
  title     = {Introduction to Mathematical Logic},
  edition   = {6},
  publisher = {CRC Press},
  year      = {2015}
}

@article{post1921propositions,
  author  = {Post, Emil L.},
  title   = {Introduction to a general theory of elementary propositions},
  journal = {American Journal of Mathematics},
  volume  = {43},
  number  = {3},
  year    = {1921},
  pages   = {163--185}
}

@incollection{cook1971complexity,
  author    = {Cook, Stephen A.},
  title     = {The complexity of theorem-proving procedures},
  booktitle = {Proceedings of the Third Annual ACM Symposium on Theory of Computing (STOC)},
  publisher = {ACM},
  year      = {1971},
  pages     = {151--158}
}

@book{frege1879begriffsschrift,
  author    = {Frege, Gottlob},
  title     = {Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens},
  publisher = {Louis Nebert, Halle},
  year      = {1879}
}

@book{wittgenstein1921tractatus,
  author    = {Wittgenstein, Ludwig},
  title     = {Tractatus Logico-Philosophicus},
  publisher = {Annalen der Naturphilosophie; Kegan Paul (1922 English ed.)},
  year      = {1921}
}

@book{hilbertackermann1928,
  author    = {Hilbert, David and Ackermann, Wilhelm},
  title     = {Grundz\"{u}ge der theoretischen Logik},
  publisher = {Springer},
  year      = {1928}
}

@article{sheffer1913stroke,
  author  = {Sheffer, Henry M.},
  title   = {A set of five independent postulates for Boolean algebras, with application to logical constants},
  journal = {Transactions of the American Mathematical Society},
  volume  = {14},
  number  = {4},
  year    = {1913},
  pages   = {481--488}
}

Prerequisites

none — this is a leaf unit

Tier anchors

beginner: Enderton 2001 *A Mathematical Introduction to Logic* 2e (Harcourt/Academic Press) §1.0-1.1 (the sentence symbols, the connectives, and reading a formula as a built-up expression, before any induction); the truth-table reading of the connectives done by hand on small formulas
intermediate: Enderton 2001 *A Mathematical Introduction to Logic* 2e §1.1-1.3 and §1.7 (the inductive definition of well-formed formulas, unique readability, truth assignments and their recursive extension, tautological implication, the deductive calculus and the soundness/completeness of sentential logic)
master: Enderton 2001 *A Mathematical Introduction to Logic* 2e Ch. 1 in full (functional completeness, normal forms, the compactness theorem for sentential logic, completeness of the deductive calculus); Mendelson 2015 *Introduction to Mathematical Logic* 6e (CRC) Ch. 1; Post 1921 *Amer. J. Math.* 43 (truth-table completeness); Cook 1971 (the NP-completeness of satisfiability)

References

Enderton, H. B. — A Mathematical Introduction to Logic · 2nd edition, Harcourt/Academic Press (2001), Chapter 1. §1.1 fixes the sentential language: a countable set of sentence symbols A_1, A_2, ... and the five connective symbols ¬, ∧, ∨, →, ↔ together with parentheses; well-formed formulas (wffs) are defined inductively as the smallest set containing the sentence symbols and closed under the formula-building operations E_¬, E_∧, E_∨, E_→, E_↔. §1.2-1.3 proves unique readability (the parsing theorem): every wff is either a sentence symbol or has a unique main connective and unique immediate subformulas, so the recursion principle applies and a truth assignment v on the sentence symbols extends uniquely to a function v-bar on all wffs via the connective truth tables. A wff is a tautology if v-bar = T for every v; Σ tautologically implies τ (Σ ⊨ τ) if every v satisfying all of Σ satisfies τ. §1.5 establishes functional completeness: every n-ary Boolean function is realised by some wff, the sets {¬,∧,∨}, {¬,∧}, {¬,∨}, {¬,→} are complete, the Sheffer stroke (NAND) and the joint denial (NOR) are each complete by themselves, and disjunctive and conjunctive normal forms exist. §1.7 gives a Hilbert-style deductive calculus (axiom schemata plus modus ponens) with the syntactic turnstile ⊢ and proves the soundness theorem (⊢ ⇒ ⊨) and the completeness theorem (⊨ ⇒ ⊢) for sentential logic, via the deduction theorem and a maximal-consistent-set (Lindenbaum) construction; the compactness theorem (a set is satisfiable iff every finite subset is) follows. The decidability of tautologyhood by the finite truth-table check is noted as the algorithmic decision procedure.
Mendelson, E. — Introduction to Mathematical Logic · 6th edition, CRC Press / Chapman & Hall (2015), Chapter 1 ('The Propositional Calculus'). Develops the statement-connective language, truth tables, tautologies and the adequacy (functional completeness) of connective sets including the stroke; presents the Hilbert-style axiom system L with three axiom schemata and modus ponens, proves the deduction theorem, soundness, and completeness via Lindenbaum's lemma, and derives the compactness theorem for the propositional calculus.
Post, E. L. — Introduction to a general theory of elementary propositions · American Journal of Mathematics 43 (1921), 163-185. Introduces the truth-table method as a complete decision procedure for the propositional calculus, proves the functional completeness of the connectives, and establishes the (Post-)completeness of the propositional calculus: every truth-table tautology is provable and the system cannot be consistently extended by a non-derivable schema.
Cook, S. A. — The complexity of theorem-proving procedures · Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), 151-158. Proves that the satisfiability problem for propositional formulas (SAT) is NP-complete, so propositional validity is co-NP-complete: the truth-table decision procedure is correct but runs in time exponential in the number of sentence symbols, and a polynomial-time test would collapse NP to P.

Estimated time

beginner: 18m
intermediate: 50m
master: 85m