Mathematical Logic

Last updated: August 2026

Disclaimer: These are my personal notes compiled for my own reference and learning. They may contain errors, incomplete information, or personal interpretations. While I strive for accuracy, these notes are not peer-reviewed and should not be considered authoritative sources. Please consult official textbooks, research papers, or other reliable sources for academic or professional purposes.

Contents

  1. Propositional logic: syntax and semantics
  2. Natural deduction and soundness
  3. Completeness of propositional logic
  4. Compactness, and a graph-coloring application
  5. Resolution: a complete proof system for SAT
  6. Predicate logic, stated without proof
  7. Cantor's theorem and uncountability
  8. Computation
  9. Common pitfalls
  10. Connections
  11. References

1. Propositional logic: syntax and semantics

Definition

Formulas: $\varphi::=p\mid\neg\varphi\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\varphi\to\varphi$, built from atoms $p,q,r,\ldots$. A truth assignment $v$ maps atoms to $\{T,F\}$, extended recursively in the usual way. $\Gamma\models\varphi$ ("$\Gamma$ entails $\varphi$") if every $v$ satisfying every formula in $\Gamma$ also satisfies $\varphi$; $\varphi$ is a tautology ($\models\varphi$) if $\varnothing\models\varphi$.

$\models$ is a semantic notion — defined by checking truth values across every possible assignment, in principle a search over $2^n$ cases for $n$ atoms. Section 2 introduces a purely syntactic notion, $\vdash$ (derivability by explicit rules, with no reference to truth values at all), and Sections 2–3 prove the two coincide exactly — a genuinely nontrivial fact, not a matter of definition.

2. Natural deduction and soundness

Definition (Natural deduction rules)

$\land I$: from $\Gamma\vdash\varphi$, $\Gamma\vdash\psi$, infer $\Gamma\vdash\varphi\land\psi$. $\land E$: from $\Gamma\vdash\varphi\land\psi$, infer $\Gamma\vdash\varphi$ (or $\psi$). $\lor I$: from $\Gamma\vdash\varphi$, infer $\Gamma\vdash\varphi\lor\psi$. $\lor E$: from $\Gamma\vdash\varphi\lor\psi$, $\Gamma,\varphi\vdash\chi$, $\Gamma,\psi\vdash\chi$, infer $\Gamma\vdash\chi$. $\to I$: from $\Gamma,\varphi\vdash\psi$, infer $\Gamma\vdash\varphi\to\psi$. $\to E$ (modus ponens): from $\Gamma\vdash\varphi\to\psi$, $\Gamma\vdash\varphi$, infer $\Gamma\vdash\psi$. $\neg I$: from $\Gamma,\varphi\vdash\bot$, infer $\Gamma\vdash\neg\varphi$. $\neg E$: from $\Gamma\vdash\varphi$, $\Gamma\vdash\neg\varphi$, infer $\Gamma\vdash\bot$. $RAA$: from $\Gamma,\neg\varphi\vdash\bot$, infer $\Gamma\vdash\varphi$ (the classical rule — proof by contradiction).

$\Gamma\vdash\varphi$ means $\varphi$ is derivable from $\Gamma$ by a finite tree of applications of these rules. This is exactly the type-theoretic system of the type theory note's Section 4, one connective at a time ($\to I/\to E$ are literally that note's Abs/App rules); the one addition here is $RAA$, whose absence is precisely what makes that note's system intuitionistic rather than classical (Section 9's third pitfall there).

Theorem (Soundness)

$\Gamma\vdash\varphi\Rightarrow\Gamma\models\varphi$.

Proof. By induction on the derivation tree, i.e. on which rule was applied last. Two representative cases: for $\to I$, the induction hypothesis is $\Gamma,\varphi\models\psi$; take any $v$ satisfying $\Gamma$ — either $v(\varphi)=F$, making $\varphi\to\psi$ true under $v$ regardless of $\psi$, or $v(\varphi)=T$, in which case $v$ satisfies $\Gamma,\varphi$, so by the induction hypothesis $v(\psi)=T$, again making $\varphi\to\psi$ true. Either way $\Gamma\models\varphi\to\psi$. For $RAA$, the induction hypothesis is $\Gamma,\neg\varphi\models\bot$ — no assignment satisfies $\Gamma\cup\{\neg\varphi\}$; so any $v$ satisfying $\Gamma$ must have $v(\neg\varphi)=F$, i.e. $v(\varphi)=T$, giving $\Gamma\models\varphi$. The remaining rules are similarly direct readings of the semantic definition of each connective. ∎

Soundness says derivability never overshoots truth: nothing false-under-some-model is ever provable. Section 3 is the converse, and is the harder half.

3. Completeness of propositional logic

Lemma (Kalmár)

Let $\varphi$ have atoms $p_1,\ldots,p_n$ and let $v$ be any truth assignment. Write $\psi^v=\psi$ if $v(\psi)=T$, else $\psi^v=\neg\psi$. Then $p_1^v,\ldots,p_n^v\vdash\varphi^v$.

Proof. By induction on the structure of $\varphi$. Base case $\varphi=p_i$: trivial, $p_i^v\vdash p_i^v$. Case $\varphi=\psi\land\chi$: the induction hypothesis gives $\vdash\psi^v$ and $\vdash\chi^v$ (from the relevant literals). If $v(\varphi)=T$ then $v(\psi)=v(\chi)=T$, so $\varphi^v=\psi\land\chi$ follows from $\psi^v=\psi,\chi^v=\chi$ by $\land I$. If $v(\varphi)=F$, some conjunct is false under $v$, say $v(\psi)=F$; then $\psi^v=\neg\psi$ is derivable, and assuming $\psi\land\chi$ gives $\psi$ by $\land E$, contradicting $\neg\psi$ by $\neg E$, so $\neg I$ discharges to $\vdash\neg(\psi\land\chi)=\varphi^v$. The $\lor,\to,\neg$ cases are proved the same way, one direct case split on $v$'s value at $\varphi$ followed by the matching introduction or contradiction-then-$\neg I$ argument. ∎
Theorem (Completeness, tautologies)

If $\models\varphi$, then $\vdash\varphi$.

Proof (sketch). By induction on the number of atoms $n$ in $\varphi$, eliminating one hypothesis at a time from Kalmár's Lemma. Since $\models\varphi$, $\varphi^v=\varphi$ regardless of $v$, so the Lemma gives, for the last atom $p_n$: $p_1^v,\ldots,p_{n-1}^v,p_n\vdash\varphi$ (taking $v(p_n)=T$) and $p_1^v,\ldots,p_{n-1}^v,\neg p_n\vdash\varphi$ (taking $v(p_n)=F$) — the same conclusion $\varphi$ either way, for every choice of $v$ on the first $n-1$ atoms. A short derived rule ("proof by cases": from $\Gamma,\chi\vdash\varphi$ and $\Gamma,\neg\chi\vdash\varphi$, derive $\Gamma\vdash\varphi$, itself provable via two applications of $RAA$) then removes $p_n$'s literal entirely: $p_1^v,\ldots,p_{n-1}^v\vdash\varphi$. Repeating for $p_{n-1},\ldots,p_1$ removes every hypothesis, leaving $\vdash\varphi$. ∎

For general (finite) $\Gamma$, $\Gamma\models\varphi$ reduces to the tautology case via $\models(\gamma_1\land\cdots\land\gamma_k)\to\varphi$, then $\to E$ and $\land I$ recover $\Gamma\vdash\varphi$ from $\vdash(\gamma_1\land\cdots\land\gamma_k)\to\varphi$. Soundness (Section 2) and Completeness together say $\vdash$ and $\models$ are the same relation — a purely syntactic, mechanically checkable notion of proof exactly tracks a semantic, in-principle-infinite-search notion of truth, for the whole of propositional logic.

4. Compactness, and a graph-coloring application

Theorem (Compactness)

A (possibly infinite) set of formulas $\Gamma$ is satisfiable iff every finite subset of $\Gamma$ is satisfiable.

Proof. ($\Rightarrow$) Any assignment satisfying $\Gamma$ satisfies every subset of it. ($\Leftarrow$, contrapositive) If $\Gamma$ is unsatisfiable, $\Gamma\models\bot$ vacuously (no assignment satisfies $\Gamma$, so the entailment holds trivially); by Completeness (Section 3, which extends to infinite $\Gamma$ unchanged, since a derivation tree is always finite and so uses only finitely many premises from $\Gamma$), $\Gamma\vdash\bot$ using some finite $\{\gamma_1,\ldots,\gamma_k\}\subseteq\Gamma$. That finite subset derives $\bot$, so by Soundness (Section 2) it is unsatisfiable. ∎
Application (De Bruijn–Erdős theorem)

A graph $G$ (possibly with infinitely many vertices) is $k$-colorable iff every finite subgraph of $G$ is $k$-colorable.

Proof. Encode "vertex $v$ gets color $i$" as an atom $p_{v,i}$. Let $\Gamma$ contain: $p_{v,1}\lor\cdots\lor p_{v,k}$ for every vertex $v$ (some color assigned); $\neg(p_{v,i}\land p_{v,j})$ for $i\neq j$ (at most one color); $\neg(p_{u,i}\land p_{v,i})$ for every edge $\{u,v\}$ and color $i$ (properly colored). A satisfying assignment for $\Gamma$ is exactly a proper $k$-coloring of $G$, and (since each formula in $\Gamma$ mentions only finitely many vertices) a satisfying assignment for any finite subset of $\Gamma$ corresponds exactly to a proper $k$-coloring of the finite subgraph on the vertices those formulas mention. So: every finite subgraph $k$-colorable $\iff$ every finite subset of $\Gamma$ satisfiable $\iff$ (Compactness) $\Gamma$ satisfiable $\iff$ $G$ is $k$-colorable. ∎

This is a genuinely surprising transfer: a purely local, finite-checkable condition (every finite piece behaves) controls a global, possibly-infinite structure, via nothing but the syntactic finiteness of proofs. Chromatic number and coloring algorithms proper belong to graph theory rather than logic; this application is included here because the mechanism making it work is entirely a logic fact.

5. Resolution: a complete proof system for SAT

Definition

A clause is a disjunction of literals (an atom or its negation); a CNF formula is a conjunction of clauses. The resolution rule: from clauses $\alpha\lor p$ and $\beta\lor\neg p$, derive the resolvent $\alpha\lor\beta$. The empty clause $\square$ (derived when $\alpha,\beta$ are both empty) represents a contradiction.

Theorem (Soundness of resolution)

Any assignment satisfying both $\alpha\lor p$ and $\beta\lor\neg p$ satisfies their resolvent $\alpha\lor\beta$.

Proof. If $v(p)=T$: $v(\neg p)=F$, so $\beta\lor\neg p$ true forces $v(\beta)=T$, so $\alpha\lor\beta$ is true. If $v(p)=F$: $\alpha\lor p$ true forces $v(\alpha)=T$, so $\alpha\lor\beta$ is true. ∎
Theorem (Refutation completeness)

A set of clauses is unsatisfiable iff repeated resolution eventually derives $\square$.

Proof (sketch, by induction on the number of variables $n$). $n=0$: an unsatisfiable set with no variables must already contain $\square$ (there is nothing else it could contain to be unsatisfiable). Inductive step: given an unsatisfiable clause set $S$ over $n$ variables including $p$, let $S_0$ (over the remaining $n-1$ variables) consist of every clause in $S$ not mentioning $p$, together with every resolvent, on $p$, of a clause containing $p$ against one containing $\neg p$. One checks directly that $S_0$ is unsatisfiable iff $S$ is (any assignment satisfying $S_0$ extends to satisfy $S$ by choosing $p$'s value to satisfy every $p$-clause not already handled, unless some resolvent in $S_0$ specifically blocks that choice — exactly what the resolution step was constructed to capture). By the induction hypothesis, $S_0$'s resolution closure contains $\square$; every clause used to derive it is either already in $S$ or itself one resolution step away from clauses in $S$, so $S$'s closure contains $\square$ too. ∎

This variable-elimination strategy (essentially the Davis–Putnam procedure) is the direct ancestor of every modern SAT solver; Figure 1 runs it in full on a minimal unsatisfiable example, and its "resolve away one variable at a time" structure is the same proof technique as Section 3's Kalmár completeness argument, one level more operational.

A directed graph showing four clauses (p or q), (p or not q), (not p or q), (not p or not q) resolved pairwise down to the single-literal clauses (p) and (not p), which are then resolved together to the empty clause, representing a contradiction.
Figure — Resolving a minimal unsatisfiable formula down to the empty clause. $(p\lor q),(p\lor\neg q),(\neg p\lor q),(\neg p\lor\neg q)$ has no satisfying assignment (every one of the four truth assignments to $p,q$ falsifies some clause). Resolving on $q$ collapses the four clauses to $(p)$ and $(\neg p)$; resolving those on $p$ derives $\square$ — the empty clause, a direct certificate of unsatisfiability, exactly as Section 5's theorem guarantees.

6. Predicate logic, stated without proof

Extending atoms to predicates $P(x_1,\ldots,x_n)$ over a domain, with quantifiers $\forall x,\exists x$, gives first-order (predicate) logic. Its metatheory is a substantially larger undertaking than propositional logic's (the domain can be infinite, and satisfaction is defined relative to a structure rather than a finite truth table); the headline results are recorded here without proof.

Gödel's Completeness Theorem (1929)

For first-order logic, $\Gamma\models\varphi\iff\Gamma\vdash\varphi$ still holds, for the analogous natural-deduction-style system extended with quantifier rules.

Compactness and the Löwenheim–Skolem theorem

First-order compactness holds by the same route as Section 4 (via completeness). Löwenheim–Skolem: if a first-order theory has an infinite model, it has models of every infinite cardinality — in particular, a theory intended to describe an uncountable structure (like $\mathbb R$) always also has a countable model, a genuinely counterintuitive consequence known as Skolem's paradox.

(See Enderton, 2001, Ch. 2, or Mendelson, 2015, Ch. 2, for full statements and proofs.) Gödel's incompleteness theorems are a different, later result about a much stronger system (first-order arithmetic capable of encoding its own syntax) and are not a contradiction of completeness above — completeness says provability and truth coincide for a fixed, agreed-upon proof system; incompleteness says no single such system, strong enough to talk about arithmetic, can prove every arithmetic truth, however the rules are chosen.

7. Cantor's theorem and uncountability

Theorem (Cantor)

For any set $A$, there is no surjection $f:A\to\mathcal P(A)$.

Proof. Suppose $f:A\to\mathcal P(A)$ is surjective. Let $D=\{a\in A:a\notin f(a)\}\in\mathcal P(A)$. By surjectivity, $D=f(b)$ for some $b\in A$. Then $b\in D\iff b\notin f(b)=D$ — a direct contradiction, so no surjective $f$ exists. ∎

Taking $A=\mathbb N$: $\mathcal P(\mathbb N)$ is strictly larger than $\mathbb N$, so uncountable; since $\mathcal P(\mathbb N)$ is in bijection with binary sequences, and (via binary expansion) with a set essentially equivalent in size to $\mathbb R$, this gives the uncountability of the reals by the same mechanism as the more commonly quoted digit-diagonalization argument. The construction of $D$ — an object built specifically to disagree with $f(a)$ at coordinate $a$, for every $a$ — is the identical idea behind the computability note's proof that the Halting Problem is undecidable (its Section 5) and the type theory note's $\Omega$ term: self-reference constructed precisely to contradict whatever it is being compared against.

A 6 by 6 grid of binary membership values for a proposed enumeration f(1) through f(6) of subsets of {1,...,6}, with the diagonal cells outlined, and a final row D constructed by flipping each diagonal value, shown to differ from every row above it.
Figure — $D$ disagrees with every $f(i)$ at the diagonal cell $i$, so $D\neq f(i)$ for any $i$. For a concrete proposed listing $f(1),\ldots,f(6)$ of six subsets of $\{1,\ldots,6\}$, flipping each diagonal entry (outlined) produces $D=\{1,3\}$ — checked directly against all six rows, $D$ differs from every single one, at exactly the coordinate the construction targets. The same mechanism, run over all of $\mathbb N$ instead of $\{1,\ldots,6\}$, is Section 7's full proof.

8. Computation

The figures above are generated by logic/generate_figures.py. The snippet below reproduces the diagonal-set check and the resolution derivation.

f = {1: {2,4,6}, 2: {1,2,3}, 3: set(), 4: {1,3,4,5,6}, 5: {5}, 6: {1,2,3,4,5,6}}
n = 6
D = {i for i in range(1, n+1) if i not in f[i]}
print("D =", D)
for i in range(1, n+1):
    print(f"f({i}) = {f[i]}   D == f({i})? {D == f[i]}")

def resolve(c1, c2):
    return [frozenset((c1 - {l}) | (c2 - {-l})) for l in c1 if -l in c2]

C1, C2, C3, C4 = frozenset({1,2}), frozenset({1,-2}), frozenset({-1,2}), frozenset({-1,-2})
C5 = resolve(C1, C2)[0]
C6 = resolve(C3, C4)[0]
C7 = resolve(C5, C6)[0]
print("C5:", set(C5), " C6:", set(C6), " C7:", set(C7), "<- empty clause")

Actual output:

D = {1, 3}
f(1) = {2, 4, 6}   D == f(1)? False
f(2) = {1, 2, 3}   D == f(2)? False
f(3) = set()       D == f(3)? False
f(4) = {1, 3, 4, 5, 6}   D == f(4)? False
f(5) = {5}         D == f(5)? False
f(6) = {1, 2, 3, 4, 5, 6}   D == f(6)? False

C5: {1}   C6: {-1}   C7: set() <- empty clause

Every one of the six comparisons fails, exactly as the proof demands ($D$ must differ from every $f(i)$, not most); and the three-step resolution derivation lands on the empty clause exactly, a direct, checkable certificate that the original four clauses have no common satisfying assignment.

9. Common pitfalls

Pitfall — $RAA$ (or excluded middle) is not derivable without being assumed

Dropping $RAA$ from Section 2's rule set gives intuitionistic logic — the very system underlying the type theory note's Curry-Howard correspondence — in which $\varphi\lor\neg\varphi$ is not provable for arbitrary $\varphi$. Section 3's completeness proof genuinely needs $RAA$ (in the "proof by cases" derived rule); completeness for the intuitionistic fragment is a different, separate theorem with a different proof (via Kripke models, not truth tables), not a restriction of this one.

Pitfall — compactness gives existence of a model, not a description of one

Section 4's De Bruijn–Erdős application proves an infinite graph is $k$-colorable whenever every finite piece is — but the proof (via completeness, itself nonconstructive in general, resting on the law of excluded middle) gives no algorithm for actually producing the coloring. "Every finite subgraph is colorable" is a checkable, local condition; "the whole graph is colorable" being equivalent to it is a genuine theorem, not an obvious transfer, and the equivalence itself is where all the content lives.

Pitfall — completeness and decidability are different claims

Section 3 says every tautology has a proof — but propositional satisfiability checking is still NP-complete (computability note, Section 7's Cook–Levin theorem), and first-order validity (Section 6) is outright undecidable (a consequence of the computability note's Section 5, via a reduction from the Halting Problem). Completeness guarantees a proof exists somewhere in principle; it says nothing about how expensive finding one is.

Pitfall — Gödel's completeness and incompleteness theorems are not in tension

Section 6's completeness theorem is about first-order logic's proof system tracking first-order semantic entailment exactly. Gödel's (unrelated, despite the shared name and author) incompleteness theorems are about a specific, much stronger theory — first-order Peano arithmetic — having true arithmetic statements no proof in that theory can derive. The first says "this proof system is exactly as strong as this semantics"; the second says "this semantics (the true statements about $\mathbb N$) is strictly stronger than any single recursively axiomatized proof system can capture." Different systems, different theorems.

10. Connections

11. References