# Logic

Logic makes **proof itself** the object of study. It fixes a
formal language, a precise notion of truth, and rules of inference — then
asks what those rules can reach and where they must stop.


_Figure 001 — A natural-deduction proof tree: premises at the leaves, each inference bar
discharging them toward the conclusion.
_

_Figure 002 — Propositional semantics: a truth table computing a connective, filled
column by column.
_

Propositional logic comes first. A handful of connectives — _and_,
_or_, _not_, _implies_ — combine atoms into formulas,
and a truth table settles every question about them by brute enumeration.


Two views run in parallel. **Syntax** is the game of symbols
and inference rules; **semantics** is what those symbols mean
once you interpret them. Keeping the two apart is the whole discipline.


_Figure 003 — A structure interprets a language: a domain and its relations, made to
satisfy a first-order sentence.
_

First-order logic adds **quantifiers**. With _for all_
and _there exists_ ranging over a domain, the language can finally
state real mathematics — orderings, arithmetic, the theory of a structure.


The **soundness** and **completeness** theorems
then tie the two views together: a sentence is provable exactly when it is
true in every model. Deduction and truth turn out to be the same reach.


_Figure 004 — Resolution: clauses resolved pairwise on complementary literals, cascading
to the empty clause ⊥.
_

That equivalence makes proof _mechanical_. Resolution refutes an
unsatisfiable set by resolving clauses until it derives the empty clause —
a contradiction — which is the engine underneath automated theorem provers.


But mechanising proof runs into a wall. Validity in first-order logic is
undecidable, and once a theory can talk about its own arithmetic, it can
talk about its own provability.


_Figure 005 — The Gödel sentence: a formula that, by self-reference, asserts its own
unprovability.
_

Gödel's **incompleteness** theorems close the subject: any
consistent theory strong enough for arithmetic has true sentences it cannot
prove, and it can never prove its own consistency — the boundary logic set
for itself.


---

## Contents

### 1. Foundations

1. [Logic as a Mathematical Model of Deduction](/logic/foundations/logic-as-a-mathematical-model)

### 2. Sentential Logic

1. [Formal Languages and Well-Formed Formulas](/logic/sentential-logic/formal-languages-and-well-formed-formulas)
2. [Truth Assignments, Tautologies, and Consequence](/logic/sentential-logic/truth-assignments-and-tautologies)
3. [Unique Readability and a Parsing Algorithm](/logic/sentential-logic/unique-readability-and-parsing)
4. [Induction and Recursion on Formulas](/logic/sentential-logic/induction-and-recursion)
5. [Sentential Connectives and Normal Forms](/logic/sentential-logic/expressive-completeness-and-normal-forms)
6. [Switching Circuits](/logic/sentential-logic/boolean-circuits)
7. [Compactness and Effectiveness](/logic/sentential-logic/compactness-and-effectiveness)

### 3. First-Order Languages and Structures

1. [First-Order Languages](/logic/first-order-languages/first-order-languages)
2. [Structures, Truth, and Satisfaction](/logic/first-order-languages/structures-truth-and-satisfaction)
3. [Definability and Elementary Equivalence](/logic/first-order-languages/definability-and-elementary-equivalence)
4. [Parsing, Substitution, and Substitutability](/logic/first-order-languages/terms-substitution-and-parsing)

### 4. The Deductive Calculus and Its Metatheorems

1. [A Deductive Calculus for First-Order Logic](/logic/deductive-calculus/a-deductive-calculus)
2. [The Deduction Theorem and Derived Rules](/logic/deductive-calculus/deduction-theorem-and-derived-rules)
3. [The Soundness Theorem](/logic/deductive-calculus/soundness)
4. [The Completeness Theorem](/logic/deductive-calculus/completeness-and-consistency)

### 5. Models, Compactness, and Theories

1. [Compactness and the Löwenheim–Skolem Theorems](/logic/models-and-theories/compactness-and-lowenheim-skolem)
2. [Theories, Elementary Classes, and Categoricity](/logic/models-and-theories/theories-elementary-classes-and-categoricity)
3. [Interpretations Between Theories](/logic/models-and-theories/interpretations-between-theories)
4. [Nonstandard Analysis](/logic/models-and-theories/nonstandard-analysis)

### 6. Number Theory and Definability

1. [The Structure of Arithmetic and Definability](/logic/arithmetic-and-definability/definability-in-arithmetic)
2. [Natural Numbers with Successor](/logic/arithmetic-and-definability/natural-numbers-with-successor)
3. [Reducts: Order, Addition, and Multiplication](/logic/arithmetic-and-definability/presburger-and-reducts)
4. [A Subtheory of Number Theory and Representability](/logic/arithmetic-and-definability/a-subtheory-and-representability)

### 7. Arithmetization and the Incompleteness Theorems

1. [Arithmetization of Syntax](/logic/incompleteness/arithmetization-of-syntax)
2. [Incompleteness, Undecidability, and Church's Theorem](/logic/incompleteness/incompleteness-and-undecidability)
3. [The Second Incompleteness Theorem](/logic/incompleteness/second-incompleteness-theorem)

### 8. Recursive Functions and Representability

1. [Recursive Functions and Church's Thesis](/logic/computability-and-representability/recursive-functions)
2. [Representing Exponentiation and the β-Function](/logic/computability-and-representability/representing-exponentiation)

### 9. Second-Order Logic and Beyond

1. [Second-Order Languages](/logic/second-order-logic/second-order-languages)
2. [Skolem Functions and Many-Sorted Logic](/logic/second-order-logic/skolem-functions-and-many-sorted-logic)
3. [General (Henkin) Structures](/logic/second-order-logic/general-structures)