| |
| |
| Preface | |
| |
| |
| |
| What Godel's Theorems say | |
| |
| |
| Basic arithmetic | |
| |
| |
| Incompleteness | |
| |
| |
| More incompleteness | |
| |
| |
| Some implications? | |
| |
| |
| The unprovability of consistency | |
| |
| |
| More implications? | |
| |
| |
| What's next? | |
| |
| |
| |
| Decidability and enumerability | |
| |
| |
| Functions | |
| |
| |
| Effective decidability, effective computability | |
| |
| |
| Enumerable sets | |
| |
| |
| Effective enumerability | |
| |
| |
| Effectively enumerating pairs of numbers | |
| |
| |
| |
| Axiomatized formal theories | |
| |
| |
| Formalization as an ideal | |
| |
| |
| Formalized languages | |
| |
| |
| Axiomatized formal theories | |
| |
| |
| More definitions | |
| |
| |
| The effective enumerability of theorems | |
| |
| |
| Negation-complete theories are decidable | |
| |
| |
| |
| Capturing numerical properties | |
| |
| |
| Three remarks on notation | |
| |
| |
| A remark about extensionality | |
| |
| |
| The language L[subscript A] | |
| |
| |
| A quick remark about truth | |
| |
| |
| Expressing numerical properties and relations | |
| |
| |
| Capturing numerical properties and relations | |
| |
| |
| Expressing vs. capturing: keeping the distinction clear | |
| |
| |
| |
| The truths of arithmetic | |
| |
| |
| Sufficiently expressive languages | |
| |
| |
| More about effectively enumerable sets | |
| |
| |
| The truths of arithmetic are not effectively enumerable | |
| |
| |
| Incompleteness | |
| |
| |
| |
| Sufficiently strong arithmetics | |
| |
| |
| The idea of a 'sufficiently strong' theory | |
| |
| |
| An undecidability theorem | |
| |
| |
| Another incompleteness theorem | |
| |
| |
| |
| Interlude: Taking stock | |
| |
| |
| Comparing incompleteness arguments | |
| |
| |
| A road-map | |
| |
| |
| |
| Two formalized arithmetics | |
| |
| |
| BA, Baby Arithmetic | |
| |
| |
| BA is negation complete | |
| |
| |
| Q, Robinson Arithmetic | |
| |
| |
| Q is not complete | |
| |
| |
| Why Q is interesting | |
| |
| |
| |
| What Q can prove | |
| |
| |
| Systems of logic | |
| |
| |
| Capturing less-than-or-equal-to in Q | |
| |
| |
| Adding '[less than or equal]' to Q | |
| |
| |
| Q is order-adequate | |
| |
| |
| Defining the [Delta subscript 0], [Sigma subscript 1] and [Pi subscript 1] wffs | |
| |
| |
| Some easy results | |
| |
| |
| Q is [Sigma subscript 1]-complete | |
| |
| |
| Intriguing corollaries | |
| |
| |
| Proving Q is order-adequate | |
| |
| |
| |
| First-order Peano Arithmetic | |
| |
| |
| Induction and the Induction Schema | |
| |
| |
| Induction and relations | |
| |
| |
| Arguing using induction | |
| |
| |
| Being more generous with induction | |
| |
| |
| Summary overview of PA | |
| |
| |
| Hoping for completeness? | |
| |
| |
| Where we've got to | |
| |
| |
| Is PA consistent? | |
| |
| |
| |
| Primitive recursive functions | |
| |
| |
| Introducing the primitive recursive functions | |
| |
| |
| Defining the p.r. functions more carefully | |
| |
| |
| An aside about extensionality | |
| |
| |
| The p.r. functions are computable | |
| |
| |
| Not all computable numerical functions are p.r. | |
| |
| |
| Defining p.r. properties and relations | |
| |
| |
| Building more p.r. functions and relations | |
| |
| |
| Further examples | |
| |
| |
| |
| Capturing p.r. functions | |
| |
| |
| Capturing a function | |
| |
| |
| Two more ways of capturing a function | |
| |
| |
| Relating our definitions | |
| |
| |
| The idea of p.r. adequacy | |
| |
| |
| |
| Q is p.r. adequate | |
| |
| |
| More definitions | |
| |
| |
| Q can capture all [Sigma subscript 1] functions | |
| |
| |
| L[subscript A] can express all p.r. functions: starting the proof | |
| |
| |
| The idea of a [beta]-function | |
| |
| |
| L[subscript A] can express all p.r. functions: finishing the proof | |
| |
| |
| The p.r. functions are [Sigma subscript 1] | |
| |
| |
| The adequacy theorem | |
| |
| |
| Canonically capturing | |
| |
| |
| |
| Interlude: A very little about Principia | |
| |
| |
| Principia's logicism | |
| |
| |
| Godel's impact | |
| |
| |
| Another road-map | |
| |
| |
| |
| The arithmetization of syntax | |
| |
| |
| Godel numbering | |
| |
| |
| Coding sequences | |
| |
| |
| Term, Atom, Wff, Sent and Prf are p.r. | |
| |
| |
| Some cute notation | |
| |
| |
| The idea of diagonalization | |
| |
| |
| The concatenation function | |
| |
| |
| Proving that Term is p.r. | |
| |
| |
| Proving that Atom and Wff are p.r. | |
| |
| |
| Proving Prf is p.r. | |
| |
| |
| |
| PA is incomplete | |
| |
| |
| Reminders | |
| |
| |
| 'G is true if and only if it is unprovable' | |
| |
| |
| PA is incomplete: the semantic argument | |
| |
| |
| 'G is of Goldbach type' | |
| |
| |
| Starting the syntactic argument for incompleteness | |
| |
| |
| [omega]-incompleteness, [omega]-inconsistency | |
| |
| |
| Finishing the syntactic argument | |
| |
| |
| 'Godel sentences' and what they say | |
| |
| |
| |
| Godel's First Theorem | |
| |
| |
| Generalizing the semantic argument | |
| |
| |
| Incompletability | |
| |
| |
| Generalizing the syntactic argument | |
| |
| |
| The First Theorem | |
| |
| |
| |
| Interlude: About the First Theorem | |
| |
| |
| What we've proved | |
| |
| |
| The reach of Godelian incompleteness | |
| |
| |
| Some ways to argue that G[subscript T] is true | |
| |
| |
| What doesn't follow from incompleteness | |
| |
| |
| What does follow from incompleteness? | |
| |
| |
| |
| Strengthening the First Theorem | |
| |
| |
| Broadening the scope of the incompleteness theorems | |
| |
| |
| True Basic Arithmetic can't be axiomatized | |
| |
| |
| Rosser's improvement | |
| |
| |
| 1-consistency and [Sigma subscript 1]-soundness | |
| |
| |
| |
| The Diagonalization Lemma | |
| |
| |
| Provability predicates | |
| |
| |
| An easy theorem about provability predicates | |
| |
| |
| G and Prov | |
| |
| |
| Proving that G is equivalent to Prov(G) | |
| |
| |
| Deriving the Lemma | |
| |
| |
| |
| Using the Diagonalization Lemma | |
| |
| |
| The First Theorem again | |
| |
| |
| An aside: 'Godel sentences' again | |
| |
| |
| The Godel-Rosser Theorem again | |
| |
| |
| Capturing provability? | |
| |
| |
| Tarski's Theorem | |
| |
| |
| The Master Argument | |
| |
| |
| The length of proofs | |
| |
| |
| |
| Second-order arithmetics | |
| |
| |
| Second-order arithmetical languages | |
| |
| |
| The Induction Axiom | |
| |
| |
| Neat arithmetics | |
| |
| |
| Introducing PA[subscript 2] | |
| |
| |
| Categoricity | |
| |
| |
| Incompleteness and categoricity | |
| |
| |
| Another arithmetic | |
| |
| |
| Speed-up again | |
| |
| |
| |
| Interlude: Incompleteness and Isaacson's conjecture | |
| |
| |
| Taking stock | |
| |
| |
| Goodstein's Theorem | |
| |
| |
| Isaacson's conjecture | |
| |
| |
| Ever upwards | |
| |
| |
| Ancestral arithmetic | |
| |
| |
| |
| Godel's Second Theorem for PA | |
| |
| |
| Defining Con | |
| |
| |
| The Formalized First Theorem in PA | |
| |
| |
| The Second Theorem for PA | |
| |
| |
| On [omega]-incompleteness and [omega]-consistency again | |
| |
| |
| How should we interpret the Second Theorem? | |
| |
| |
| How interesting is the Second Theorem for PA? | |
| |
| |
| Proving the consistency of PA | |
| |
| |
| |
| The derivability conditions | |
| |
| |
| More notation | |
| |
| |
| The Hilbert-Bernays-Lob derivability conditions | |
| |
| |
| G, Con, and 'Godel sentences' | |
| |
| |
| Incompletability and consistency extensions | |
| |
| |
| The equivalence of fixed points for Prov | |
| |
| |
| Theories that 'prove' their own inconsistency | |
| |
| |
| Lob's Theorem | |
| |
| |
| |
| Deriving the derivability conditions | |
| |
| |
| Nice theories | |
| |
| |
| The second derivability condition | |
| |
| |
| The third derivability condition | |
| |
| |
| Useful corollaries | |
| |
| |
| The Second Theorem for weaker arithmetics | |
| |
| |
| Jeroslow's Lemma and the Second Theorem | |
| |
| |
| |
| Reflections | |
| |
| |
| The Second Theorem: the story so far | |
| |
| |
| There are provable consistency sentences | |
| |
| |
| What does that show? | |
| |
| |
| The reflection schema: some definitions | |
| |
| |
| Reflection and PA | |
| |
| |
| Reflection, more generally | |
| |
| |
| 'The best and most general version' | |
| |
| |
| Another route to accepting a Godel sentence? | |
| |
| |
| |
| Interlude: About the Second Theorem | |
| |
| |
| 'Real' vs 'ideal' mathematics | |
| |
| |
| A quick aside: Godel's caution | |
| |
| |
| Relating the real and the ideal | |
| |
| |
| Proving real-soundness? | |
| |
| |
| The impact of Godel | |
| |
| |
| Minds and computers | |
| |
| |
| The rest of this book: another road-map | |
| |
| |
| |
| [Mu]-Recursive functions | |
| |
| |
| Minimization and [Mu]-recursive functions | |
| |
| |
| Another definition of [Mu]-recursiveness | |
| |
| |
| The Ackermann-Peter function | |
| |
| |
| The Ackermann-Peter function is [Mu]-recursive | |
| |
| |
| Introducing Church's Thesis | |
| |
| |
| Why can't we diagonalize out? | |
| |
| |
| Using Church's Thesis | |
| |
| |
| |
| Undecidability and incompleteness | |
| |
| |
| Q is recursively adequate | |
| |
| |
| Nice theories can only capture recursive functions | |
| |
| |
| Some more definitions | |
| |
| |
| Q and PA are undecidable | |
| |
| |
| The Entscheidungsproblem | |
| |
| |
| Incompleteness theorems again | |
| |
| |
| Negation-complete theories are recursively decidable | |
| |
| |
| Recursively adequate theories are not recursively decidable | |
| |
| |
| What's next? | |
| |
| |
| |
| Turing machines | |
| |
| |
| The basic conception | |
| |
| |
| Turing computation defined more carefully | |
| |
| |
| Some simple examples | |
| |
| |
| 'Turing machines' and their 'states' | |
| |
| |
| |
| Turing machines and recursiveness | |
| |
| |
| [Mu]-Recursiveness entails Turing computability | |
| |
| |
| [Mu]-Recursiveness entails Turing computability: the details | |
| |
| |
| Turing computability entails [Mu]-recursiveness | |
| |
| |
| Generalizing | |
| |
| |
| |
| Halting problems | |
| |
| |
| Two simple results about Turing programs | |
| |
| |
| The halting problem | |
| |
| |
| The Entscheidungsproblem again | |
| |
| |
| The halting problem and incompleteness | |
| |
| |
| Another incompleteness argument | |
| |
| |
| Kleene's Normal Form Theorem | |
| |
| |
| Kleene's Theorem entails Godel's First Theorem | |
| |
| |
| |
| The Church-Turing Thesis | |
| |
| |
| From Euclid to Hilbert | |
| |
| |
| 1936 and all that | |
| |
| |
| What the Church-Turing Thesis is not | |
| |
| |
| The status of the Thesis | |
| |
| |
| |
| Proving the Thesis? | |
| |
| |
| The project | |
| |
| |
| Vagueness and the idea of computability | |
| |
| |
| Formal proofs and informal demonstrations | |
| |
| |
| Squeezing arguments | |
| |
| |
| The first premiss for a squeezing argument | |
| |
| |
| The other premisses, thanks to Kolmogorov and Uspenskii | |
| |
| |
| The squeezing argument defended | |
| |
| |
| To summarize | |
| |
| |
| |
| Looking back | |
| |
| |
| Further reading | |
| |
| |
| Bibliography | |
| |
| |
| Index | |