Book contents
- Frontmatter
- Contents
- Preface to the Fifth Edition
- COMPUTABILITY THEORY
- BASIC METALOGIC
- 9 A Précis of First-Order Logic: Syntax
- 10 A Précis of First-Order Logic: Semantics
- 11 The Undecidability of First-Order Logic
- 12 Models
- 13 The Existence of Models
- 14 Proofs and Completeness
- 15 Arithmetization
- 16 Representability of Recursive Functions
- 17 Indefinability, Undecidability, Incompleteness
- 18 The Unprovability of Consistency
- FURTHER TOPICS
- Annotated Bibliography
- Index
15 - Arithmetization
Published online by Cambridge University Press: 05 June 2012
- Frontmatter
- Contents
- Preface to the Fifth Edition
- COMPUTABILITY THEORY
- BASIC METALOGIC
- 9 A Précis of First-Order Logic: Syntax
- 10 A Précis of First-Order Logic: Semantics
- 11 The Undecidability of First-Order Logic
- 12 Models
- 13 The Existence of Models
- 14 Proofs and Completeness
- 15 Arithmetization
- 16 Representability of Recursive Functions
- 17 Indefinability, Undecidability, Incompleteness
- 18 The Unprovability of Consistency
- FURTHER TOPICS
- Annotated Bibliography
- Index
Summary
In this chapter we begin to bring together our work on logic from the past few chapters with our work on computability from earlier chapters (specifically, our work on recursive functions from Chapters 6 and 7). In section 15.1 we show how we can ‘talk about’ such syntactic notions as those of sentence and deduction in terms of recursive functions, and draw among others the conclusion that, once code numbers are assigned to sentences in a reasonable way, the set of valid sentences is semirecursive. Some proofs are deferred to sections 15.2 and 15.3. The proofs consist entirely of showing that certain effectively computable functions are recursive. Thus what is being done in the two sections mentioned is to present still more evidence, beyond that accumulated in earlier chapters, in favor of Church's thesis that all effectively computable functions are recursive. Readers who feel they have seen enough evidence for Church's thesis for the moment may regard these sections as optional.
Arithmetization of Syntax
A necessary preliminary to applying our work on computability, which pertained to functions on natural numbers, to logic, where the objects of study are expressions of a formal language, is to code expressions by numbers. Such a coding of expressions is called a Gödel numbering. One can then go on to code finite sequences of expressions and still more complicated objects.
- Type
- Chapter
- Information
- Computability and Logic , pp. 187 - 198Publisher: Cambridge University PressPrint publication year: 2007