Mathematical logic Study Guide

📖 Core Concepts Mathematical Logic – Formal study of logical systems used to reason about mathematics; explores what can be expressed and proved. Formal Language – Set of symbols + formation rules; sentences are built from connectives (∧, ∨, ¬, →) and quantifiers (∀, ∃). Model – A structure giving meaning to the symbols of a theory; a sentence is true in a model if it holds under that interpretation. Proof System – Syntactic rules (Hilbert, natural deduction, sequent calculus) that generate formal proofs from axioms. Consistency – No contradiction can be derived; Completeness – every semantically true sentence has a syntactic proof. Computability – Functions that can be calculated by a Turing machine (or equivalent formalism). Set‑theoretic Foundations – Zermelo–Fraenkel set theory (ZF) + Axiom of Choice (AC) is the standard baseline for most of mathematics. --- 📌 Must Remember Gödel 1st Incompleteness: Any consistent, effectively axiomatized theory strong enough for arithmetic contains a true statement it cannot prove. Gödel 2nd Incompleteness: Such a theory cannot prove its own consistency. Compactness Theorem (FOL): A set of first‑order sentences has a model iff every finite subset has a model. Gödel Completeness: If a sentence is true in all models of a theory, a finite formal proof exists. Löwenheim–Skolem: If a countable first‑order theory has an infinite model, it has models of every infinite cardinality. Halting Problem: No algorithm decides for every program \(P\) and input \(x\) whether \(P\) halts on \(x\). Undecidability of Entscheidungsproblem: No algorithm can decide the truth of arbitrary first‑order statements. Continuum Hypothesis (CH): No set with cardinality strictly between \(\aleph0\) (integers) and \(2^{\aleph0}\) (reals). CH is independent of ZF + AC. Axiom of Choice (AC): For any family \(\{Ai\neq\varnothing\}{i\in I}\) there exists a set \(C\) with \(|C\cap Ai|=1\) for each \(i\). Cut Elimination: Any proof in sequent calculus can be transformed into a cut‑free proof, often shortening it and revealing its constructive content. --- 🔄 Key Processes Proof of Gödel’s First Incompleteness Encode syntax of the theory into natural numbers (Gödel numbering). Construct a sentence \(G\) that asserts “\(G\) is not provable.” Show: if the theory is consistent, \(G\) is true but unprovable; if it proved \(G\), it would be inconsistent. Compactness Argument To prove a property holds for some infinite structure, exhibit that every finite fragment can be satisfied. Apply the Compactness Theorem to infer existence of a model satisfying the whole (often infinite) set of sentences. Cut Elimination (Gentzen) Identify cuts (applications of the cut rule) in a sequent proof. Systematically replace each cut by a composition of smaller proofs (using permutation and reduction steps). Terminate with a cut‑free proof, yielding the subformula property. Diagonalization for the Halting Problem Assume a decider \(H(P,x)\) exists. Construct program \(D\) that on input \(p\) runs \(H(p,p)\); if \(H\) says “halts,” loop forever; otherwise halt. Run \(D\) on its own code → contradiction, proving \(H\) cannot exist. Independence Proof (CH) Gödel (1940): Build constructible universe \(L\); show ZF + AC + CH holds in \(L\). Cohen (1963): Use forcing to add a subset of \(\omega\) that creates a cardinal strictly between \(\aleph0\) and \(2^{\aleph0}\); obtain ZF + AC + ¬CH. --- 🔍 Key Comparisons First‑order vs. Higher‑order Logic First‑order: quantifies only over elements; enjoys completeness & compactness. Higher‑order: quantifies over sets/functions; can axiomatize arithmetic categorically but lacks completeness & compactness. Classical vs. Intuitionistic Logic Classical: accepts law of excluded middle (LEM) \(P\lor\neg P\). Intuitionistic: rejects LEM; proof of existence must provide a construction. Recursive vs. Recursively Enumerable (r.e.) Sets Recursive: decidable; both membership and its complement are computable. r.e.: semidecidable; there is an algorithm that lists all members (e.g., halting set) but may never halt on non‑members. Zermelo–Fraenkel (ZF) vs. ZF + Choice (ZFC) ZF: all standard set axioms without AC. ZFC: adds AC, enabling results like Banach–Tarski; many mainstream theorems assume AC. --- ⚠️ Common Misunderstandings “Gödel proved arithmetic is incomplete” → It’s any consistent, sufficiently strong effectively axiomatized theory, not just Peano Arithmetic. “Compactness means every infinite theory has a model.” → Only if every finite subset is satisfiable; an inconsistent finite subset kills the whole. “Higher‑order logic is just ‘first‑order with more variables.’” → It quantifies over sets/functions, changing the semantics fundamentally. “The halting problem is unsolvable for some specific machines only.” → It is unsolvable uniformly: no single algorithm works for all programs. “AC is false because it gives paradoxes.” → Paradoxes (e.g., Banach–Tarski) arise if AC is accepted; they do not prove AC false, only that it has non‑intuitive consequences. --- 🧠 Mental Models / Intuition Gödel sentences are “self‑referential mirrors”: they say “I am not provable.” Think of a liar‑type statement that can only be true if the system cannot prove it. Compactness = “finite consistency ⇒ global consistency.” Imagine building a puzzle: if every small piece fits together, the whole picture can be assembled. Cut elimination = “remove detours.” A proof with cuts is like a road with unnecessary loops; eliminating cuts yields the shortest, most direct route. Forcing = “adding a new generic object without breaking existing structure.” Picture extending a universe by sprinkling in a new set that behaves like a random coin toss, yet preserving ZF axioms. --- 🚩 Exceptions & Edge Cases Löwenheim–Skolem does not apply to uncountable languages; the theorem requires a countable signature. Compactness fails for infinitary logics (allowing infinite conjunctions/disjunctions). Gödel’s completeness holds for first‑order logic only; higher‑order logic lacks a completeness theorem. Axiom of Choice is independent of ZF; both ZF + ¬AC and ZF + AC are consistent if ZF itself is. Cut elimination may increase proof length exponentially; it guarantees existence, not practical efficiency. --- 📍 When to Use Which Prove existence of a model? – Use Compactness (show every finite subset satisfiable). Need a categorical characterization of ℕ or ℝ? – Switch to higher‑order logic (allows full second‑order induction). Reason about program correctness? – Apply intuitionistic logic (constructive proofs correspond to algorithms via Curry–Howard). Show a problem is undecidable? – Reduce from the halting problem or use diagonalization. Analyze the expressive power of a logical language? – Use Löwenheim–Skolem (compare cardinalities of models). --- 👀 Patterns to Recognize “If every finite subset … then …” → Spot a potential Compactness argument. “Self‑reference → unprovable” → Likely a Gödel‑type construction. “Add a new set without violating axioms” → Think forcing / independence proof. “Quantifier elimination → decidability” – When a theory admits QE (e.g., real‑closed fields), its decision problem is tractable. “Reduction to halting” – Classic template for proving undecidability of a new problem. --- 🗂️ Exam Traps Choosing “first‑order” when the question mentions “categorical.” – First‑order cannot uniquely characterize infinite structures; the correct answer is often “higher‑order.” Confusing Gödel’s two incompleteness theorems. – The first gives an unprovable true statement; the second states the system cannot prove its own consistency. Assuming AC is provable from ZF. – The independence results of Gödel and Cohen show AC is undecidable in ZF. Believing compactness works for infinitary logics. – It does not; many infinitary statements violate the finite‑subset condition. Thinking “the halting problem is only about Turing machines.” – Any computably equivalent model (lambda calculus, register machines) inherits the same undecidability. ---