Computability, Decidability, Incompleteness |
||
Lecturer | Prof. Dr. Benedikt Löwe | |
---|---|---|
Description |
Content. Limitative Theorems are mathematical results that show the limits of a particular method. Turing's analysis of the halting problem shows that not every set can be computed, the unsolvability of the famous Hilbert-Ackermann Entscheidungsproblem shows that there is no algorithm that determines whether a formula is valid, and finally Gödel's incompleteness theorem shows that not every true sentence of arithmetic can be provable in a given formal system that satisfies some basic principles. These three limitative theorems for the concepts of Computability, Decidability, and Completeness are closely connected and their proofs intrinsically intertwined. In this course, we shall provide an introduction to the three concepts and prove all three limitative theorems. Lecture mode. Lectures I to III, XII, and XIII will be delivered in person in lecture room Geom H3; the other lectures will be delivered via Zoom. Students can use Geom H3 to follow the lectures in a lecture room environment. Material. The material of Parts C and D, covering Computability and Decidability, follow closely Chapter 4 of the Lecture Notes of the course Automata & Formal Languages, given in Cambridge in Michaelmas term 2022. The material of Part I, covering Incompleteness is based on Lectures XI to XIII of the course Recursion Theory, given in Hamburg in Wintersemester 2021/22. The corresponding lecture notes can be found here:
| |
Lectures |
Lecture I: 4 April 2023. Geom H3.
Limitative Theorems: asymmetry between positive and negative results.
Hilbert's problems: Hilbert's 10th problem, Entscheidungsproblem.
Turing: halting problem. Hilbert's "Wir müssen wissen, wir werden wissen".
Completeness of a proof system. Statement of Gödel's incompleteness theorem.
Turing machines. Register machines. Alphabets, letters, words, concatenation, length, instructions.
Formal definition of register machine and intuitive description. Upper register index.
Lecture Notes. Lecture II: 11 April 2023. Geom H3.
Registers, configurations, states and register content, transformation of a configuration by a register machine,
computation sequence, halting, halting time. Strong equivalence of register machines. Irrelevance of set of states.
There are countably many register machines up to strong equivalence. Padding Lemma. Notation for partial functions.
Performing a partial function. Examples: "never halt" and "always halt". Questions and answering questions. Examples: "Is register \(i\) empty?" and "Does register \(i\) end with letter \(a\)?". Concatenation Lemma and Case Distinction Lemma.
Formal proofs of the existence of a register machine in natural language.
Lecture Notes Lecture III: 18 April 2023. Geom H3. Examples of operations performed by machines and questions answered by machines. Computable partial functions. Examples. Characteristic and pseudocharacteristic functions. Computable and computably enumerable sets. Basic properties. Lecture Notes. 25 April 2023. No lecture. Lecture IV: 2 May 2023. Online. The shortlex ordering \(\). Isomorphism between \((\mathbb{W},<)\) and \((\mathbb{N},<)\). Difference between shortlex and the standard lexicographic order. The shortlex order is a computable set and the successor function is a computable function. Church's basic functions are all computable. Closure under composition, recursion, and minimisation. The recursive and primitive recursive functions. All primitive recursive functions are total. All recursive functions are computable (no proof yet). Examples of (primitive) recursive functions: addition and multiplication. Lecture Notes. Lecture V: 9 May 2023. Online. Proof that all recursive functions are computable. Cantor's zigzag function. Merging and splitting words. Coding of register machines as words. The computation sequence is computable. The truncated computation function is computable and total. The Software Principle. The \(s\)-\(m\)-\(n\) Theorem. Lecture Notes. 16 May 2023. No lecture: Pentecostal break. Lecture VI: 23 May 2023. Online. Turing's Halting Problem: computably enumerable, but not computable. \(\Sigma_1\) sets, \(\Pi_1\) sets, and \(\Delta_1\) sets. A set if computably enumerable if and only if it is \(\Sigma_1\). A set is computable if and only if it is \(\Delta_1\). Closure properties: computable sets are closed under intersections, unions, and complement; computably enumerable sets are closed under intersection, union, but not complement. Reduction functions and many-one reducibility. Many-one reducibility preserves computability and computable enumerability. Hardness and completeness. Lecture Notes. Lecture VII: 30 May 2023. Online. The halting problem is \(\Sigma_1\)-complete. Many-one equivalence and degrees of unsolvability. Turing join: the Turing join of two sets is the least upper bound in the degrees of unsolvability. Index sets. Trivial index sets. Examples of index sets. Nontrivial index sets are infinite. Rice's Theorem: nontrivial index sets are not computable. Properties of the example index sets. The index set \(\mathbf{Fin}\) is neither \(\Sigma_1\) nor \(\Pi_1\) (no proof). Decidability: interpreting the informal word algorithm or algorithmic procedure as computation by a register machine Lecture Notes. Lecture VIII: 6 June 2023. Online. Recapitulation: decision problems and their algorithmic solutions. Robustness of notions: the concept of computability is robust, since Turing machines, register machines, Church recursive functions, and WHILE programs give the same notion of computability. The notion of computation is not robust. The Church-Turing Thesis. Nature of the Church-Turing Thesis. Decidability. Mathematical presentation of decision problems. The word problem, the emptiness problem, and the equivalence problem for c.e. languages. All three problems are not decidable. Lecture Notes. Lecture IX: 13 June 2023. Online. Decision problems restricted to subclasses of the c.e. sets: silly examples; finite automata & regular languages; rewrite systems, generative grammars, and context-free languages (without proofs). Encoding logical languages in finite alphabets. General idea of reducing the Entscheidungsproblem to the halting problem. Encoding of computations in a logical language: configurations and machines. Lecture Notes. Lecture X: 20 June 2023. Online. Reminder: syntax built up in Lecture IX; encoding of machines, configurations, and sequences of words as words. Formulas describing that \(M\) is a machine coded by \(w\) and that \(x\) and that \(M\) halts at input \(x\). List of all axioms governing the syntactic behaviour. The formula describing ``the machine coded by \(w\) halts at input \(w\)''. Proof that the function is a reduction function: undecidability of the Entscheidungsproblem. Lecture Notes. Lecture XI: 27 June 2023. Online. Clarification of the formula used in the reduction function in Lecture X. Reminder of the model \(\mathbf{HF}\) of hereditarily finite sets. Reminder of the limitations of first-order logic: infinite models cannot be described up to isomorphism (upwards Löwenheim-Skolem). Describing infinite models up to elementary equivalence: the theory of a model, negation-completeness, agreement of provability and truth. Statement of Gödel's incompleteness theorem: there is no decidable, negation-complete \(S\) such that \(\mathbf{HF}\models S\). Proof strategy in two steps: proving that for decidable \(S\), the set of \(S\)-consequences is \(\Sigma_1\); proving that the set of true sentences in \(\mathbf{HF}\) is \(\Pi_1\)-hard. Natural deduction systems, rules, and calculi. Computability of a rule, computability of a calculus. The standard proof predicate is computable. Lecture Notes. Lecture XII: 4 July 2023. Geom H3. Proof that the set of provable formulas is \(\Sigma_1\). Proof that the set of true formulas is \(\Pi_1\)-hard. Fixed point lemma (without proof). Gödel sentences and an alternative proof of the incompleteness theorem. [The proof of the relevant fixed point result is in the following note: Gödel's Fixed Point Lemma.] Discussion of the second incompleteness theorem, its proof sketch, and the consistency strength hierarchy. An example of a theory that is consistent, but not consistent with its own consistency statement. Lecture Notes. |