| |

| |

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 | |