CS 245: Logic and Computation

Carmen Bruni

Estimated reading time: 34 minutes

Table of contents

Chapter 1: Introduction to Logic and Propositions

What Is Logic?

Logic is the science of reasoning — the systematic study of the forms of arguments. The Greek root logykos means “pertaining to reasoning,” and logic has been central to mathematics, philosophy, and computation since antiquity. Alan Turing observed in 1947 that digital computing machines would stimulate interest in symbolic logic, since the language in which one communicates with machines forms a sort of symbolic logic. CS 245 is the formal study of that connection.

The course covers four major units: propositional logic, predicate logic, program verification, and undecidability. These units address five essential questions: How do we model real-world phenomena using formal language? How do we define well-formed formulas? How do we interpret formulas? How do we perform reasoning and inference? And — crucially for computer science — are there problems that no algorithm can solve?

Logic is useful both as a practitioner and as a logician. A practitioner asks: how can I model specific scenarios? How do I determine whether two formulas are logically equivalent? How do I prove that a conclusion follows from premises? A logician asks deeper questions: does every well-formed formula have a unique interpretation? What is the smallest adequate set of connectives? Is everything provable true, and is everything true provable? These questions lead to the completeness and soundness theorems that make logic rigorous.

Applications of logic in computer science are pervasive. Circuit design uses Boolean logic gates directly. Logic programming languages like Prolog have roots in first-order logic. Expert systems use knowledge bases with inference engines — the MYCIN medical diagnosis system achieved acceptable therapy in 69% of cases, exceeding the performance of human infectious disease experts. Databases use first-order logic at their core; SQL is essentially relational algebra derived from predicate logic. Formal verification catches costly bugs — Intel’s Pentium FDIV bug in 1994 cost half a billion dollars, and software errors in the Therac-25 radiation therapy machine killed patients.

Propositions

A proposition is a declarative sentence that is either true or false, but never both simultaneously. The sentence must have enough information to determine its truth value. The following are propositions: “The sum of 3 and 5 is 8,” “$-1 \geq 5$,” “Program $p$ terminates on any input” (for a specific, fixed program $p$), and “Every even number greater than 2 is the sum of two primes” (the Goldbach conjecture — nobody knows if it’s true, but it is still a proposition). A sentence can be a proposition even if nobody can currently determine whether it is true or false.

The following are not propositions: questions (“Where shall we go to eat?”), commands (“Please pass the salt”), sentence fragments (“The dogs in the park”), nonsensical sentences (“Green ideas sleep furiously”), and paradoxes (“This sentence is false”). The paradox illustrates a key point: a proposition can never be both true and false. The liar’s paradox violates this requirement, so it falls outside the scope of propositional logic.

Logical Connectives

Simple propositions are combined into compound propositions using logical connectives. The five principal connectives and their meanings are:

Connective	Symbol	Meaning	Paraphrases
Negation	$\neg p$	not $p$	it is not the case that $p$; $p$ is false
Conjunction	$p \wedge q$	$p$ and $q$	$p$ but $q$; $p$ yet $q$; $p$ although $q$
Disjunction	$p \vee q$	$p$ or $q$	$p$ and/or $q$; $p$ unless $q$
Conditional	$p \to q$	if $p$ then $q$	$p$ implies $q$; $q$ if $p$; $p$ only if $q$; $q$ is necessary for $p$; $p$ is sufficient for $q$
Biconditional	$p \leftrightarrow q$	$p$ if and only if $q$	$p$ iff $q$; $p$ is equivalent to $q$; $p$ is necessary and sufficient for $q$

The disjunction $p \vee q$ is inclusive or — it is true when at least one of $p$ or $q$ is true. English is often ambiguous: “I will eat an apple or an orange but not both” requires the formula $(p \vee q) \wedge \neg(p \wedge q)$, i.e., exclusive or. The conditional $p \to q$ is one of the most subtle connectives. It is false only when $p$ is true and $q$ is false; when $p$ is false the conditional is vacuously true regardless of $q$.

English is genuinely ambiguous and must be translated carefully. “Pigs can fly and the grass is red or the sky is blue” can be parsed as $(p \wedge q) \vee r$ or $p \wedge (q \vee r)$, which are logically inequivalent. “He will fail unless he studies hard” can mean $\neg s \to f$ or $f \leftrightarrow \neg s$ depending on interpretation.

Chapter 2: Propositional Logic Syntax

Well-Formed Formulas

Propositional logic has a precise, inductively defined syntax. The propositional variables (atoms) are symbols from the set $\{p, q, r, s, \ldots\}$ along with the constants $\top$ (top, always true) and $\bot$ (bottom, always false). A well-formed formula (WFF) is built from atoms using connectives, defined inductively:

Every propositional variable is a WFF.
$\top$ and $\bot$ are WFFs.
If $\alpha$ is a WFF, then $(\neg \alpha)$ is a WFF.
If $\alpha$ and $\beta$ are WFFs, then $(\alpha \wedge \beta)$, $(\alpha \vee \beta)$, $(\alpha \to \beta)$, and $(\alpha \leftrightarrow \beta)$ are WFFs.
Nothing else is a WFF.

By convention, we drop outermost parentheses and observe precedence: $\neg$ binds most tightly, then $\wedge$, then $\vee$, then $\to$, then $\leftrightarrow$. Precedence allows us to write $\neg p \wedge q \to r$ for $((\neg p) \wedge q) \to r$.

Parse Trees

Every WFF has a unique parse tree (sometimes called a formula tree) that encodes how the formula was built by the inductive definition. For example, the formula $(p \to q) \wedge \neg r$ has a parse tree with root $\wedge$, left child $\to$ (with leaves $p$ and $q$), and right child $\neg$ (with leaf $r$. Parse trees are the foundation for defining the semantics of a formula: we evaluate a formula bottom-up through its parse tree.

The uniqueness of parse trees is a non-trivial theorem called the Unique Readability Theorem: every WFF has exactly one parse tree. This means the syntax of propositional logic is unambiguous — unlike English, every formula has a single, definite meaning. The proof relies on tracking balanced parentheses and showing that no proper prefix of a WFF is itself a WFF.

Structural Induction

Many proofs about WFFs use structural induction (also called induction on the structure of formulas). To prove that every WFF $\alpha$ has property $P$:

Base case: prove $P$ holds for every propositional variable, $\top$, and $\bot$.
Inductive step for $\neg$: assume $P(\alpha)$ (the induction hypothesis); prove $P((\neg \alpha))$.
Inductive step for binary connectives: assume $P(\alpha)$ and $P(\beta)$; prove $P((\alpha \star \beta))$ for each connective $\star \in \{\wedge, \vee, \to, \leftrightarrow\}$.

This mirrors the inductive definition of WFFs. For example, one can prove by structural induction that every WFF has at least as many parentheses as connectives, or that every WFF has an equal number of left and right parentheses.

The subformula relation is defined structurally: $\beta$ is a subformula of $\alpha$ if $\beta$ is any node in the parse tree of $\alpha$. Every formula is a subformula of itself. The immediate subformulas of $(\alpha \wedge \beta)$ are $\alpha$ and $\beta$.

Chapter 3: Propositional Logic Semantics

Truth Valuations

The semantics of propositional logic gives formulas their meaning. A truth valuation (or interpretation) is a function $t : \text{PropVars} \to \{T, F\}$ assigning truth values to propositional variables. Every valuation extends uniquely to all WFFs using the following truth tables:

$\alpha$	$\beta$	$\neg \alpha$	$\alpha \wedge \beta$	$\alpha \vee \beta$	$\alpha \to \beta$	$\alpha \leftrightarrow \beta$
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

The extension from variables to formulas is defined by structural induction, evaluating the formula bottom-up through its parse tree. The value of $\top$ is always T and the value of $\bot$ is always F under every valuation.

The truth table for $\to$ is the most counterintuitive: $\alpha \to \beta$ is false only when $\alpha$ is true and $\beta$ is false. When $\alpha$ is false, the conditional is vacuously true — “if 1 = 0 then the moon is made of cheese” is a true statement, because the hypothesis is false. This corresponds to the material conditional of classical logic.

Tautologies, Contradictions, and Satisfiability

A formula $\alpha$ is a tautology (or is valid, written $\models \alpha$) if it evaluates to T under every valuation. A formula is a contradiction (or unsatisfiable) if it evaluates to F under every valuation. A formula is satisfiable if there exists at least one valuation under which it is true.

The classification of formulas:

Tautology: true under all valuations. Example: $p \vee \neg p$ (law of excluded middle).
Contradiction: false under all valuations. Example: $p \wedge \neg p$.
Satisfiable but not tautology: true under some but not all valuations. Example: $p \wedge q$ (true when both are true).

Every tautology is satisfiable. Every contradiction is unsatisfiable. A formula is a tautology if and only if its negation is a contradiction.

Logical Equivalence

Two formulas $\alpha$ and $\beta$ are logically equivalent (written $\alpha \equiv \beta$) if they have the same truth value under every valuation. Equivalently, $\alpha \equiv \beta$ if and only if $\alpha \leftrightarrow \beta$ is a tautology.

\[ \neg(\alpha \wedge \beta) \equiv \neg \alpha \vee \neg \beta, \qquad \neg(\alpha \vee \beta) \equiv \neg \alpha \wedge \neg \beta \]\[ \alpha \to \beta \equiv \neg \alpha \vee \beta \]\[ \alpha \to \beta \equiv \neg \beta \to \neg \alpha \]

and the double negation law $\neg \neg \alpha \equiv \alpha$, the idempotency laws $\alpha \wedge \alpha \equiv \alpha$ and $\alpha \vee \alpha \equiv \alpha$, the absorption laws, the distributive laws, and the associative laws for $\wedge$ and $\vee$.

Entailment

\[ (\beta_1 \wedge \cdots \wedge \beta_n) \to \alpha \]

The special case $\emptyset \models \alpha$ means $\alpha$ is a tautology.

Soundness and completeness of propositional logic: the semantic notion of entailment ($\models$) and the syntactic notion of provability ($\vdash$) coincide. The soundness theorem says every provable formula is a tautology; the completeness theorem says every tautology is provable.

Adequate Sets of Connectives

An adequate (or functionally complete) set of connectives is a set from which every Boolean function can be expressed. The set $\{\neg, \wedge, \vee\}$ is adequate because every truth table can be represented in disjunctive normal form using only these connectives (and $\to$ and $\leftrightarrow$ can be defined in terms of them).

Even smaller adequate sets exist:

$\{\neg, \wedge\}$ is adequate (use De Morgan to eliminate $\vee$).
$\{\neg, \vee\}$ is adequate (use De Morgan to eliminate $\wedge$).
$\{\neg, \to\}$ is adequate (since $\alpha \vee \beta \equiv \neg \alpha \to \beta$).
The single connective NAND (Sheffer stroke), $\alpha \mid \beta \equiv \neg(\alpha \wedge \beta)$, is adequate: both $\neg \alpha \equiv \alpha \mid \alpha$ and $\alpha \wedge \beta \equiv (\alpha \mid \beta) \mid (\alpha \mid \beta)$.
NOR is also a single-connective adequate set.

The set $\{\wedge, \vee\}$ is not adequate because it cannot express negation — any formula built from only $\wedge$ and $\vee$ is monotone (replacing F with T in a variable never changes T to F).

Chapter 4: Normal Forms and Applications

Conjunctive and Disjunctive Normal Forms

\[ (l_{11} \vee \cdots \vee l_{1k_1}) \wedge \cdots \wedge (l_{n1} \vee \cdots \vee l_{nk_n}) \]

A formula is in disjunctive normal form (DNF) if it is a disjunction of conjunctions of literals.

Every formula can be converted to CNF or DNF. The procedure for CNF conversion:

Eliminate $\leftrightarrow$ using $\alpha \leftrightarrow \beta \equiv (\alpha \to \beta) \wedge (\beta \to \alpha)$.
Eliminate $\to$ using $\alpha \to \beta \equiv \neg \alpha \vee \beta$.
Push negations inward using De Morgan’s laws and double negation.
Distribute $\wedge$ over $\vee$ to achieve CNF.

CNF is particularly important because the resolution proof method (Chapter 5) and SAT solvers work on CNF formulas. DNF is useful because checking whether a DNF formula is satisfiable is easy: just check whether any disjunct is consistent (no variable appears both positive and negative).

Applications: Dead Code Elimination

Logical equivalences have direct applications in compilers. Dead code elimination removes code that can never execute. Consider a conditional if (P) then { A } else { B }. If the condition $P$ is a contradiction, the then-branch is dead code; if $P$ is a tautology, the else-branch is dead code.

More subtly, if we have if (P) then { if (Q) then { A } else { B } } else { B }, a compiler can detect that the two B branches share the else case and simplify the structure. Logical equivalence checking — determining whether two conditions always produce the same truth value — underlies these optimizations.

Adequacy of $\{\neg, \to\}$

\[ \alpha \wedge \beta \equiv \neg(\alpha \to \neg \beta) \]\[ \alpha \vee \beta \equiv \neg \alpha \to \beta \]\[ \alpha \leftrightarrow \beta \equiv (\alpha \to \beta) \wedge (\beta \to \alpha) \equiv \neg((\alpha \to \beta) \to \neg(\beta \to \alpha)) \]

This reduction is important for resolution and other proof systems that work with a minimal set of connectives.

Chapter 5: Resolution

The Resolution Proof Method

Resolution is a refutation-based proof method for propositional logic operating on formulas in CNF. It provides a decision procedure: given a finite set of clauses, resolution either derives the empty clause $\bot$ (proving unsatisfiability) or terminates without deriving $\bot$ (proving satisfiability).

\[ \frac{(C_1 \vee p) \quad (\neg p \vee C_2)}{C_1 \vee C_2} \]

where $C_1$ and $C_2$ are (possibly empty) disjunctions of literals and $p$ is a propositional variable appearing positively in one clause and negatively in the other. The variable $p$ is called the pivot. The resolvent $C_1 \vee C_2$ is a new clause added to the clause set.

To prove $\Sigma \models \alpha$ using resolution:

Convert $\Sigma \cup \{\neg \alpha\}$ to CNF, obtaining a set of clauses $S$.
Repeatedly apply the resolution rule to pairs of clauses in $S$, adding resolvents to $S$.
If the empty clause $\bot$ is derived, then $\Sigma \models \alpha$.
If no new clauses can be derived and $\bot$ has not appeared, then $\Sigma \not\models \alpha$.

Soundness of Resolution

The resolution rule is sound: any valuation satisfying both premises also satisfies the resolvent. Proof: suppose $t \models (C_1 \vee p)$ and $t \models (\neg p \vee C_2)$. If $t(p) = T$, then $t \models C_2$, so $t \models C_1 \vee C_2$. If $t(p) = F$, then $t \models C_1$, so $t \models C_1 \vee C_2$. In either case, $t \models C_1 \vee C_2$.

By the soundness of the resolution rule, any clause derivable by resolution from a satisfiable set of clauses is satisfiable. In particular, if the empty clause is derivable, the original clause set must be unsatisfiable. This is the Central Lemma for resolution soundness.

Completeness of Resolution

The resolution procedure is complete: if a set of clauses $S$ is unsatisfiable, then resolution will eventually derive the empty clause. The proof proceeds by induction on the number of propositional variables appearing in $S$.

Base case: if $S$ contains no variables, it consists only of $\top$ (empty disjunction, i.e., $\bot$) and the empty clause. If $S$ is unsatisfiable, it must contain $\bot$.

Inductive step: let $p$ be any variable in $S$. Define $S^+ = \{C \setminus \{p\} : C \in S, p \in C\}$ (clauses with $p$ removed) and $S^- = \{C \setminus \{\neg p\} : C \in S, \neg p \in C\}$ (clauses with $\neg p$ removed), and $S^0 = \{C \in S : p \notin C, \neg p \notin C\}$ (clauses not containing $p$ at all). The set $S' = S^0 \cup S^+ \cup S^-$ (with $p$ eliminated) is also unsatisfiable (since any satisfying valuation of $S'$ could be extended to satisfy $S$ by choosing the right value for $p$). By the induction hypothesis, resolution derives $\bot$ from $S'$. Each step in this derivation either involves a clause from $S^0$ (already in $S$) or a clause that is a resolvent of clauses from $S^+$ and $S^-$ — which can be derived from $S$ by resolving on $p$. Therefore, resolution derives $\bot$ from $S$ as well.

The combined soundness and completeness theorem: $\Sigma \models \alpha$ if and only if resolution derives $\bot$ from $\Sigma \cup \{\neg \alpha\}$ converted to CNF.

Chapter 6: Natural Deduction for Propositional Logic

The Natural Deduction System

Natural deduction is a proof system for propositional logic that mirrors human reasoning more closely than resolution. Rather than refutation, it proves formulas directly by deriving conclusions from premises using a collection of introduction and elimination rules — one pair for each connective.

A proof in natural deduction is a tree of formulas, where each formula is either a premise or follows from earlier formulas by one of the inference rules. We write $\Sigma \vdash \alpha$ to mean that $\alpha$ is provable from the set of assumptions $\Sigma$.

Inference Rules

The key rules are presented as: premises above the line, conclusion below.

\[ \frac{\alpha \quad \beta}{\alpha \wedge \beta} \;\wedge\text{I} \qquad \frac{\alpha \wedge \beta}{\alpha} \;\wedge\text{E}_1 \qquad \frac{\alpha \wedge \beta}{\beta} \;\wedge\text{E}_2 \]\[ \frac{\alpha}{\alpha \vee \beta} \;\vee\text{I}_1 \qquad \frac{\beta}{\alpha \vee \beta} \;\vee\text{I}_2 \qquad \frac{\alpha \vee \beta \quad [\alpha] \vdash \gamma \quad [\beta] \vdash \gamma}{\gamma} \;\vee\text{E} \]

The disjunction elimination rule discharges the assumptions $\alpha$ and $\beta$: we assume $\alpha$, derive $\gamma$, then assume $\beta$, derive $\gamma$, and conclude $\gamma$ from $\alpha \vee \beta$.

\[ \frac{[\alpha] \vdash \beta}{\alpha \to \beta} \;\to\text{I} \qquad \frac{\alpha \to \beta \quad \alpha}{\beta} \;\to\text{E (MP)} \]

Conditional introduction allows us to discharge the assumption $\alpha$: to prove $\alpha \to \beta$, assume $\alpha$ and derive $\beta$.

\[ \frac{[\alpha] \vdash \bot}{\neg \alpha} \;\neg\text{I} \qquad \frac{\neg \neg \alpha}{\alpha} \;\neg\text{E} \qquad \frac{\alpha \quad \neg \alpha}{\bot} \;\bot\text{I} \]\[ \frac{\bot}{\alpha} \;\bot\text{E} \]

From a contradiction, anything follows. This is the principle ex falso quodlibet.

\[ \frac{\alpha \to \beta \quad \beta \to \alpha}{\alpha \leftrightarrow \beta} \;\leftrightarrow\text{I} \qquad \frac{\alpha \leftrightarrow \beta \quad \alpha}{\beta} \;\leftrightarrow\text{E}_1 \qquad \frac{\alpha \leftrightarrow \beta \quad \beta}{\alpha} \;\leftrightarrow\text{E}_2 \]

Soundness and Completeness of Natural Deduction

\[ \Sigma \vdash \alpha \iff \Sigma \models \alpha \]

Soundness ($\Rightarrow$) means: every provable formula is semantically valid. Each inference rule preserves truth, and this property propagates through the proof tree.

Completeness ($\Leftarrow$) means: every semantically valid formula is provable. The proof of completeness is more involved and uses the fact that any satisfiable set of formulas can be consistently extended to a maximal satisfiable set, from which a canonical model can be constructed.

The equivalence of syntactic provability and semantic validity is a fundamental result. It means we can choose whichever method is more convenient for a given problem — truth tables and model theory for semantic arguments, or proof rules for syntactic arguments.

Chapter 7: Predicate Logic Syntax

Beyond Propositions

Propositional logic is powerful but limited: it cannot express statements like “all humans are mortal” or “there exists a prime number greater than 100.” These statements involve quantification over domains. Predicate logic (also called first-order logic) extends propositional logic with variables ranging over a domain, function symbols, predicate symbols, and the quantifiers $\forall$ (for all) and $\exists$ (there exists).

A predicate logic signature $\mathcal{L}$ consists of:

A set of constant symbols $c_1, c_2, \ldots$ (names for specific individuals).
A set of function symbols $f_1, f_2, \ldots$, each with an associated arity (number of arguments).
A set of predicate symbols $P_1, P_2, \ldots$, each with an associated arity.

For example, the signature of arithmetic might include constants $0, 1$, function symbols $+, \times$ (binary), and predicate symbols $=, <$ (binary).

Terms and Formulas

Terms represent objects in the domain and are defined inductively:

Every constant symbol is a term.
Every variable $x, y, z, \ldots$ is a term.
If $f$ is a function symbol of arity $n$ and $t_1, \ldots, t_n$ are terms, then $f(t_1, \ldots, t_n)$ is a term.

Atomic formulas (atoms) are the basic building blocks:

If $P$ is a predicate symbol of arity $n$ and $t_1, \ldots, t_n$ are terms, then $P(t_1, \ldots, t_n)$ is an atomic formula.
The special predicate $=$ gives atomic formulas $t_1 = t_2$ (equality).

Well-formed formulas (WFFs) are defined inductively:

Every atomic formula is a WFF.
If $\alpha$ is a WFF, then $\neg \alpha$ is a WFF.
If $\alpha$ and $\beta$ are WFFs, then $(\alpha \wedge \beta)$, $(\alpha \vee \beta)$, $(\alpha \to \beta)$, $(\alpha \leftrightarrow \beta)$ are WFFs.
If $\alpha$ is a WFF and $x$ is a variable, then $\forall x\, \alpha$ and $\exists x\, \alpha$ are WFFs.

Free and Bound Variables

An occurrence of a variable $x$ in a formula is bound if it lies within the scope of a quantifier $\forall x$ or $\exists x$; otherwise it is free. In $\forall x\, P(x, y)$, the variable $x$ is bound and $y$ is free.

A formula with no free variables is called a sentence. Only sentences have a definite truth value in a given interpretation; formulas with free variables are evaluated relative to an assignment of values to free variables.

The scope of a quantifier $\forall x$ or $\exists x$ in $(\forall x\, \alpha)$ is the formula $\alpha$. Care must be taken when a variable is both free in one part of a formula and bound in another.

Substitution

The substitution $\alpha[t / x]$ replaces every free occurrence of variable $x$ in formula $\alpha$ with term $t$. However, a naive substitution can lead to variable capture — a free variable in $t$ becoming bound after substitution.

For example, in $\exists y\, (x < y)$, substituting $y + 1$ for $x$ would give $\exists y\, (y + 1 < y)$, where the $y$ in $y + 1$ has been captured by the quantifier. This changes the meaning entirely.

A term $t$ is free for $x$ in $\alpha$ if no free variable of $t$ becomes bound after substituting $t$ for $x$. When capture would occur, we first rename the bound variable (alpha-conversion): replace $\exists y\, (x < y)$ by the equivalent $\exists z\, (x < z)$, then substitute freely.

Chapter 8: Predicate Logic Semantics

Interpretations and Satisfiability

An interpretation (or structure) $\mathcal{M}$ for a predicate logic signature $\mathcal{L}$ consists of:

A non-empty set $M$ called the domain (or universe).
For each constant symbol $c$, an element $c^\mathcal{M} \in M$.
For each function symbol $f$ of arity $n$, a function $f^\mathcal{M} : M^n \to M$.
For each predicate symbol $P$ of arity $n$, a relation $P^\mathcal{M} \subseteq M^n$.

A variable assignment $\sigma : \text{Vars} \to M$ assigns domain elements to variables. Given $\mathcal{M}$ and $\sigma$, every term $t$ denotes an element $t^{\mathcal{M},\sigma} \in M$:

$c^{\mathcal{M},\sigma} = c^\mathcal{M}$ for constants.
$x^{\mathcal{M},\sigma} = \sigma(x)$ for variables.
$(f(t_1,\ldots,t_n))^{\mathcal{M},\sigma} = f^\mathcal{M}(t_1^{\mathcal{M},\sigma},\ldots,t_n^{\mathcal{M},\sigma})$.

The satisfaction relation $\mathcal{M},\sigma \models \alpha$ is defined by induction:

$\mathcal{M},\sigma \models P(t_1,\ldots,t_n)$ iff $(t_1^{\mathcal{M},\sigma},\ldots,t_n^{\mathcal{M},\sigma}) \in P^\mathcal{M}$.
$\mathcal{M},\sigma \models \neg \alpha$ iff $\mathcal{M},\sigma \not\models \alpha$.
$\mathcal{M},\sigma \models \alpha \wedge \beta$ iff $\mathcal{M},\sigma \models \alpha$ and $\mathcal{M},\sigma \models \beta$.
$\mathcal{M},\sigma \models \forall x\, \alpha$ iff for every $d \in M$, $\mathcal{M},\sigma[x \mapsto d] \models \alpha$.
$\mathcal{M},\sigma \models \exists x\, \alpha$ iff there exists $d \in M$ such that $\mathcal{M},\sigma[x \mapsto d] \models \alpha$.

Here $\sigma[x \mapsto d]$ denotes the assignment identical to $\sigma$ except that $x$ maps to $d$.

Validity and Entailment in Predicate Logic

A sentence $\alpha$ is valid (written $\models \alpha$) if $\mathcal{M} \models \alpha$ for every interpretation $\mathcal{M}$. A sentence is satisfiable if $\mathcal{M} \models \alpha$ for some $\mathcal{M}$. A sentence is unsatisfiable if it is not satisfiable.

A set of sentences $\Sigma$ logically entails $\alpha$ (written $\Sigma \models \alpha$) if every interpretation satisfying all sentences in $\Sigma$ also satisfies $\alpha$.

\[ \forall x\, P(x) \to P(t) \quad \text{(universal instantiation, when } t \text{ is free for } x) \]\[ \forall x\, \alpha \equiv \neg \exists x\, \neg \alpha \qquad \exists x\, \alpha \equiv \neg \forall x\, \neg \alpha \]\[ \forall x\, \forall y\, \alpha \equiv \forall y\, \forall x\, \alpha \qquad \exists x\, \exists y\, \alpha \equiv \exists y\, \exists x\, \alpha \]

Note that $\forall x\, \exists y\, \alpha \not\equiv \exists y\, \forall x\, \alpha$ in general — the order of mixed quantifiers matters.

Equality Axioms

The equality predicate $=$ satisfies two fundamental axioms:

EQ1 (Reflexivity): $\forall x\, (x = x)$

\[ \forall x\, \forall y\, (x = y \to (\alpha[x/z] \to \alpha[y/z])) \]

That is, equals may be substituted for equals in any formula.

From EQ1 and EQ2, one can derive symmetry ($x = y \to y = x$) and transitivity ($x = y \wedge y = z \to x = z$), so equality is an equivalence relation. EQ2 also guarantees that any function applied to equal arguments gives equal results (congruence).

Peano Arithmetic

Peano arithmetic (PA) is a first-order theory of the natural numbers. Its signature includes constant $0$, unary function $S$ (successor), and binary functions $+$ and $\times$. The axioms are:

PA1: $\forall x\, \neg(S(x) = 0)$ — zero is not a successor.

PA2: $\forall x\, \forall y\, (S(x) = S(y) \to x = y)$ — the successor function is injective.

PA3 (Addition base): $\forall x\, (x + 0 = x)$.

PA4 (Addition step): $\forall x\, \forall y\, (x + S(y) = S(x + y))$.

PA5 (Multiplication base): $\forall x\, (x \times 0 = 0)$.

PA6 (Multiplication step): $\forall x\, \forall y\, (x \times S(y) = (x \times y) + x)$.

\[ (\alpha(0) \wedge \forall x\, (\alpha(x) \to \alpha(S(x)))) \to \forall x\, \alpha(x) \]

Gödel’s incompleteness theorems (discussed in Chapter 11) show that Peano arithmetic, despite its strength, cannot prove all true statements about natural numbers.

Chapter 9: Natural Deduction for Predicate Logic

Quantifier Rules

Natural deduction extends to predicate logic with rules for the quantifiers. The universal and existential quantifiers each have an introduction and an elimination rule.

\[ \frac{\forall x\, \alpha}{\alpha[t/x]} \;\forall\text{E} \]

We may instantiate a universally quantified formula with any term $t$ (as long as no variable capture occurs). This is the rule of universal instantiation.

\[ \frac{\alpha}{\forall x\, \alpha} \;\forall\text{I} \]

To prove $\forall x\, \alpha$, derive $\alpha$ for a variable $x$ that does not appear in any open assumption — $x$ is a “fresh” or “arbitrary” variable. The restriction ensures we are proving $\alpha$ holds for a genuinely arbitrary element of the domain.

\[ \frac{\alpha[t/x]}{\exists x\, \alpha} \;\exists\text{I} \]

We provide a witness $t$ to prove an existential statement.

\[ \frac{\exists x\, \alpha \quad [{\alpha}] \vdash \gamma}{\gamma} \;\exists\text{E} \]

To use an existential $\exists x\, \alpha$, we assume $\alpha$ with $x$ fresh — the anonymous witness — and derive the conclusion $\gamma$ which does not mention $x$. This mirrors how mathematicians reason: “Let $x$ be such that $\alpha(x)$. Then…”

Equality Rules

The equality predicate supports two proof rules corresponding to EQ1 and EQ2:

Equality Introduction: $\frac{}{t = t} \;{=}\text{I}$

Every term equals itself; no premises needed.

\[ \frac{s = t \quad \alpha[s/x]}{\alpha[t/x]} \;{=}\text{E} \]

This allows substituting $t$ for $s$ in any formula.

Soundness and Completeness

Natural deduction for predicate logic (with equality) is sound: every derivable formula is logically valid. The proof is by induction on the length of the derivation, verifying that each rule preserves semantic validity.

Gödel’s Completeness Theorem (1930): Natural deduction for first-order predicate logic is complete. That is, if $\Sigma \models \alpha$, then $\Sigma \vdash \alpha$. The proof constructs, for any consistent set of formulas, an explicit model using Henkin constants (witness terms).

Completeness has a striking consequence: any first-order sentence that is true in all interpretations is provable in finitely many steps. However, there is no algorithm that decides validity in first-order logic (this is the subject of Chapter 11). The decision problem for propositional logic is solvable (it is co-NP-complete via SAT), but first-order logic validity is not decidable.

Chapter 10: Program Verification

Hoare Logic

\[ \{P\}\; C\; \{Q\} \]

This asserts partial correctness: if the precondition $P$ holds before executing command $C$ and $C$ terminates, then the postcondition $Q$ holds after $C$ terminates. $P$ and $Q$ are formulas in some assertion language (typically predicate logic over program variables), and $C$ is a program command.

Partial correctness does not guarantee termination. Total correctness additionally requires that $C$ terminates whenever $P$ holds. We focus first on partial correctness.

The Hoare logic we study is for a simple imperative language called WLP4 (a fragment of C++ or Java with variables, assignments, conditionals, while loops, and arrays). Programs manipulate integer variables and arrays. Assertions are first-order formulas over the program variables.

Proof Rules

\[ \{P[e/x]\}\; x := e\; \{P\} \]

To verify an assignment, we work backwards: to establish postcondition $P$ after $x := e$, we require precondition $P[e/x]$ — the postcondition with every free occurrence of $x$ replaced by the expression $e$. This backward substitution is called the weakest precondition transformation.

Example: to prove $\{???\}\; x := x + 1\; \{x > 5\}$, we substitute: $?(x+1) > 5$, which simplifies to $x > 4$. So the triple $\{x > 4\}\; x := x + 1\; \{x > 5\}$ is valid.

\[ \frac{\{P\}\; C_1\; \{Q\} \quad \{Q\}\; C_2\; \{R\}}{\{P\}\; C_1; C_2\; \{R\}} \]

The intermediate assertion $Q$ is the postcondition of $C_1$ and the precondition of $C_2$.

\[ \frac{P' \models P \quad \{P\}\; C\; \{Q\} \quad Q \models Q'}{\{P'\}\; C\; \{Q'\}} \]

This is necessary to bridge gaps between the conditions that proof rules produce and the conditions we actually want to prove.

\[ \frac{\{P \wedge B\}\; C_1\; \{Q\} \quad \{P \wedge \neg B\}\; C_2\; \{Q\}}{\{P\}\; \mathtt{if}\; B\; \mathtt{then}\; C_1\; \mathtt{else}\; C_2\; \{Q\}\;} \]

In the then-branch, we know both $P$ and the condition $B$; in the else-branch, we know $P$ and $\neg B$.

\[ \frac{\{I \wedge B\}\; C\; \{I\}}{\{I\}\; \mathtt{while}\; B\; \mathtt{do}\; C\; \{I \wedge \neg B\}} \]

The formula $I$ is the loop invariant — an assertion that holds before the loop, after each iteration, and hence after the loop exits (at which point $B$ is false). The challenge of program verification often lies in finding the right invariant.

Finding a loop invariant requires insight about the loop’s behavior. A good invariant captures what the loop has achieved so far. For example, a loop summing the first $n$ elements of an array with index $i$ and running sum $s$ might have invariant $s = \sum_{j=0}^{i-1} a[j] \wedge 0 \leq i \leq n$.

Total Correctness and Termination

To prove total correctness $[P]\, C\, [Q]$ (which guarantees both partial correctness and termination), we additionally need a variant function (also called a loop variant or measure): a term (V$ that is:

A non-negative integer (or more generally, a well-founded quantity) when $I \wedge B$ holds.
Strictly decreasing with each iteration of the loop body.

The variant function ensures the loop cannot run forever: since $V$ is a non-negative integer that strictly decreases, it must eventually reach 0 or a base case, at which point $B$ becomes false and the loop exits. Typically, $V$ is expressed as a function of the loop counter or the remaining work.

Array Verification

\[ \{P[a \leftarrow a[i \to e]]/a\}\; a[i] := e\; \{P\} \]

where $a[i \to e]$ denotes the array identical to $a$ except at index $i$ where it has value $e$.

\[ I \equiv \forall j.\, (j < i \to a[j] = a_0[n-1-j]) \wedge (j \geq n-1-i \wedge j \leq n-1 \to a[j] = a_0[n-1-j]) \wedge \ldots \]

where $a_0$ is the original array value before the loop.

Chapter 11: Decidability and Undecidability

Decision Problems and Turing Machines

A decision problem is a problem with a yes/no answer parameterized by an input. Formally, it is a set $L$ of binary strings — the “yes” instances. A decision problem is decidable if there exists an algorithm (Turing machine) that always terminates and correctly answers yes or no on every input. It is undecidable if no such algorithm exists.

Turing machines are the formal model of computation. A Turing machine consists of a finite set of states, a tape (infinite in one or both directions) with a read-write head, and a transition function. On each step, based on the current state and the tape symbol under the head, the machine writes a symbol, moves the head left or right, and transitions to a new state. The machine accepts or rejects by entering a designated accept or reject state.

Many naturally arising problems are decidable:

Given a propositional formula, is it satisfiable? (SAT, decidable by truth table enumeration in exponential time — in fact, NP-complete.)
Given a context-free grammar, is the language it generates empty?
Given a regular expression and a string, does the string match?

The Collatz conjecture (does the sequence $n \to n/2$ if even, $n \to 3n+1$ if odd, always reach 1?) is a decision problem for each starting $n$ individually, but the general question “does it always reach 1 for all inputs?” is a single statement that is (as of 2026) unresolved.

The Halting Problem

The Halting Problem asks: given an arbitrary program $P$ and input $x$, does $P$ halt on $x$?

Theorem: The Halting Problem is undecidable. No algorithm can solve it for all programs and inputs.

Proof by diagonalization. Suppose for contradiction that a program $H$ solves the Halting Problem: $H(P, x) = \text{yes}$ if $P$ halts on $x$, and $H(P, x) = \text{no}$ if $P$ loops forever on $x$. Construct a new program $D$ as follows:

D(P):
  if H(P, P) = "yes":
    loop forever
  else:
    halt

Now ask: what does $D$ do on input $D$ itself?

If $D(D)$ halts: then $H(D, D) = \text{yes}$, so $D$ loops forever. Contradiction.
If $D(D)$ loops: then $H(D, D) = \text{no}$, so $D$ halts. Contradiction.

In both cases we get a contradiction. Therefore the assumed program $H$ cannot exist. The Halting Problem is undecidable. $\square$

This proof is a diagonal argument — the program $D$ is constructed so that its behavior on any program differs from what $H$ predicts.

Reductions

Reductions are the main tool for proving new problems undecidable. If problem $A$ reduces to problem $B$ (written $A \leq_m B$, a many-one reduction), and $B$ is decidable, then $A$ is decidable. Equivalently: if $A$ is undecidable and $A \leq_m B$, then $B$ is undecidable.

A many-one reduction from $A$ to $B$ is a computable function $f$ such that for all inputs $x$: $x \in A \iff f(x) \in B$. To use a reduction to prove $B$ is undecidable, we show how to solve $A$ (the already-known undecidable problem) using an assumed solver for $B$.

Standard reductions from the Halting Problem:

Does program $P$ halt on every input? This is undecidable: if it were decidable, we could solve the Halting Problem (reduce “does $P$ halt on $x$” to “does the modified program $P_x$ that ignores input and runs $P$ on $x$, halt on every input?”).

Does program $P$ produce output 42 on input $x$? Undecidable by reduction from the Halting Problem (modify $P$ to print 42 after halting).

Is program $P$ correct with respect to specification $S$? Undecidable for non-trivial specifications, by Rice’s Theorem: any non-trivial property of the language recognized by a Turing machine is undecidable.

Cantor’s Diagonal Argument and Countability

Undecidability is closely connected to Cantor’s diagonal argument about the sizes of infinite sets. A set is countable if its elements can be listed as a sequence $a_1, a_2, a_3, \ldots$ (finite or infinite). The natural numbers $\mathbb{N}$, integers $\mathbb{Z}$, and rationals $\mathbb{Q}$ are all countable.

Cantor’s Theorem: The real numbers $\mathbb{R}$ are uncountable — they cannot be listed in a sequence.

Proof: Suppose for contradiction that all real numbers in $[0,1]$ can be listed as $r_1, r_2, r_3, \ldots$. Write each in decimal: $r_i = 0.d_{i1}d_{i2}d_{i3}\ldots$. Construct a new number $d = 0.d_1d_2d_3\ldots$ where $d_i \neq d_{ii}$ (and $d_i \neq 9$ to avoid the $0.999\ldots = 1$ issue). Then $d$ differs from $r_i$ in the $i$-th decimal place, so $d \neq r_i$ for all $i$. But $d \in [0,1]$, contradicting completeness of the list. $\square$

The connection to undecidability: there are countably many programs (each is a finite string over a finite alphabet), but uncountably many decision problems (subsets of $\mathbb{N}$). Therefore, most decision problems have no algorithm. The Halting Problem is one explicit undecidable problem; by cardinality, “most” problems are undecidable.

Implications for Logic

Gödel’s Incompleteness Theorems (1931) show that any consistent formal system powerful enough to express Peano arithmetic contains true statements that are unprovable within the system. Specifically:

First Incompleteness Theorem: Any consistent, recursive axiom system extending Peano arithmetic is incomplete — there exists a sentence $G$ such that neither $G$ nor $\neg G$ is provable.

Second Incompleteness Theorem: Such a system cannot prove its own consistency.

The proof of the first theorem encodes “this statement is not provable” in arithmetic, mimicking the liar’s paradox. The undecidability of the Halting Problem and Gödel’s incompleteness theorems are deeply related — both arise from self-referential constructions and diagonal arguments.

For predicate logic specifically: while propositional logic is decidable (truth tables), first-order predicate logic validity is undecidable (Church’s theorem, 1936). No algorithm can decide, for an arbitrary first-order sentence, whether it is valid in all interpretations.

Automated Verification Tools

Despite undecidability, automated verification tools have practical value:

Dafny is a programming language with built-in Hoare-logic-style verification. Programmers write preconditions, postconditions, and loop invariants as annotations, and Dafny’s verifier (using an SMT solver) checks partial correctness automatically. Dafny cannot prove all correct programs correct (since the verification problem is undecidable), but it handles a useful fragment and provides strong guarantees for programs it does verify.

SMT solvers (Satisfiability Modulo Theories) extend SAT solving with theories for arithmetic, arrays, and other domains. Tools like Z3 and CVC5 are used inside verification systems, compilers, and security analysis tools. They are not decision procedures for all inputs but are remarkably effective in practice.

Model checking verifies finite-state systems exhaustively. Systems with finitely many states (hardware circuits, communication protocols) can be verified completely. For infinite-state systems (programs with unbounded integers), model checking uses abstractions and is necessarily incomplete.

The lesson of undecidability is not despair but precision: we now know exactly what automation can and cannot achieve, which guides the design of verification tools that are both sound and useful within their domains.

Connective	Symbol	Meaning	Paraphrases
Negation	\(\neg p\)	not \(p\)	it is not the case that \(p\); \(p\) is false
Conjunction	\(p \wedge q\)	\(p\) and \(q\)	\(p\) but \(q\); \(p\) yet \(q\); \(p\) although \(q\)
Disjunction	\(p \vee q\)	\(p\) or \(q\)	\(p\) and/or \(q\); \(p\) unless \(q\)
Conditional	\(p \to q\)	if \(p\) then \(q\)	\(p\) implies \(q\); \(q\) if \(p\); \(p\) only if \(q\); \(q\) is necessary for \(p\); \(p\) is sufficient for \(q\)
Biconditional	\(p \leftrightarrow q\)	\(p\) if and only if \(q\)	\(p\) iff \(q\); \(p\) is equivalent to \(q\); \(p\) is necessary and sufficient for \(q\)

\(\alpha\)	\(\beta\)	\(\neg \alpha\)	\(\alpha \wedge \beta\)	\(\alpha \vee \beta\)	\(\alpha \to \beta\)	\(\alpha \leftrightarrow \beta\)
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