Part I: Logical Foundations

Every mathematical claim is a logical claim. Logic is the infrastructure through which mathematical truth flows. Without a precise account of valid inference, no theorem can be distinguished from a plausible-sounding mistake.

1.1 Propositional Logic

Objects: Propositions (truth-bearers), logical connectives (¬, ∧, ∨, →, ↔), truth values {T, F}.

Structure: A propositional language L is a set of atomic sentences p, q, r, … closed under the connectives. An interpretation is a function assigning a truth value to each atomic sentence, extended compositionally to all compound sentences by the standard truth tables.

Tautologies: A sentence φ is a tautology if it is true under every interpretation. The paradigm: p ∨ ¬p (excluded middle), ¬(p ∧ ¬p) (non-contradiction).

Completeness: The deductive calculus of propositional logic (using modus ponens and axiom schemas) is complete: every tautology is provable. Every satisfiable formula has a truth-value assignment making it true.

Decidability: Propositional logic is decidable. Truth-table evaluation is an algorithm that terminates in finite time on any formula.

Honest limit: Propositional logic cannot express quantification — "for all x" or "there exists x" — and therefore cannot state most mathematical theorems.

1.2 First-Order Logic (FOL)

Objects: Individual variables (x, y, z, …), constants, function symbols, relation symbols, quantifiers (∀, ∃), logical connectives. A first-order language L specifies the non-logical vocabulary: a signature of function and relation symbols with arities.

Semantics: A structure M for L consists of:

• A non-empty set |M| (the domain or universe)
• For each n-ary function symbol f: a function fᴹ : |M|ⁿ → |M|
• For each n-ary relation symbol R: a set Rᴹ ⊆ |M|ⁿ
• For each constant c: an element cᴹ ∈ |M|

A sentence φ is true in M (written M ⊨ φ) according to Tarski's compositional truth definition.

Gödel's Completeness Theorem (1929): A sentence φ is provable from a set of axioms Γ if and only if it is true in every structure satisfying Γ. That is, syntactic derivability and semantic entailment coincide: ⊢ ↔ ⊨.

Compactness Theorem: If every finite subset of Γ has a model, then Γ itself has a model. This has profound consequences: the reals have non-standard models containing infinitesimals; the natural numbers have models containing infinite elements.

Löwenheim-Skolem Theorem: Any first-order theory with an infinite model has models of every infinite cardinality. In particular, the axioms of set theory — intended to describe an enormous universe of sets — also have countable models (Skolem's paradox).

Undecidability: FOL is semi-decidable: there is an algorithm that will eventually confirm any provable statement, but may run forever on unprovable ones. There is no algorithm that decides, for arbitrary sentence φ, whether φ is a tautology of FOL. (Church, Turing, 1936.)

1.3 Second-Order Logic

Extension: Second-order logic (SOL) adds quantification over predicates and functions, not just individuals. One can say "there exists a property P such that P(x) iff x is prime."

Expressive power: Categorical theories become possible. The second-order Peano axioms uniquely characterize the natural numbers up to isomorphism — no non-standard models. The second-order axioms of real analysis uniquely characterize ℝ.

Cost: SOL's semantics is not recursively axiomatizable. The set of valid SOL sentences is not even semi-decidable. Completeness fails: there is no deductive system for SOL that proves all and only the valid sentences.

Honest limit: SOL is extremely expressive but loses the proof-theoretic tractability that makes FOL foundationally central.

1.4 Type Theory

Objects: Types (base types and type constructors), terms (expressions with a type), type judgments (assertions that a term has a type).

History: Introduced by Russell to block his paradox: the set {x : x ∉ x} is ill-typed if sets are stratified by type; no set can be a member of itself.

Curry-Howard Correspondence: There is a profound isomorphism between:

• Propositions and types
• Proofs and programs
• Proof normalization and program execution

Under this correspondence, constructing a proof of proposition P is the same activity as writing a program of type P. This isomorphism is foundational to modern proof assistants (Coq, Lean, Agda).

Homotopy Type Theory (HoTT): A recent synthesis of type theory and homotopy theory. Propositions become spaces; proofs become paths; the identity type (the type of proof that a = b) has the structure of the fundamental groupoid. The Univalence Axiom states that equivalent types are identical.

1.5 Modal Logic

Extension: Modal logic adds operators □ ("necessarily") and ◇ ("possibly") to propositional or first-order logic.

Kripke Semantics: A Kripke frame is a pair (W, R) where W is a set of "possible worlds" and R ⊆ W×W is an "accessibility relation." □φ is true at world w if φ is true at all worlds accessible from w; ◇φ if φ is true at some accessible world.

Applications: Temporal logic (worlds are times, accessibility is the order relation) is the foundation of model checking in computer science. Epistemic logic (accessible worlds are those consistent with an agent's knowledge) governs formal epistemology.

---