ELEMENTARY RECURSION THEORY AND ITS APPLICATIONS TO FORMAL SYSTEMS - Saul Kripke.pdf

(694 KB) Pobierz
87563416 UNPDF
ELEMENTARY RECURSION THEORY AND ITS APPLICATIONS
TO FORMAL SYSTEMS
By Professor Saul Kripke
Department of Philosophy, Princeton University
Notes by Mario Gómez-Torrente,
revising and expanding notes by John Barker
Copyright © 1996 by Saul Kripke. Not for reproduction or quotation without express
permission of the author.
Elementary Recursion Theory. Preliminary Version
Copyright © 1995 by Saul Kripke
CONTENTS
Lecture I
1
First Order Languages / Eliminating Function Letters / Interpretations / The
Language of Arithmetic
Lecture II
8
The Language RE / The Intuitive Concept of Computability and its Formal
Counterparts / The Status of Church's Thesis
Lecture III
18
The Language Lim / Pairing Functions / Coding Finite Sequences
Lecture IV
27
Gödel Numbering / Identification / The Generated Sets Theorem / Exercises
Lecture V
36
Truth and Satisfaction in RE
Lecture VI
40
Truth and Satisfaction in RE (Continued) / Exercises
Lecture VII
49
The Enumeration Theorem. A Recursively Enumerable Set which is Not Recursive /
The Road from the Inconsistency of the Unrestricted Comprehension Principle to
the Gödel-Tarski Theorems
Lecture VIII
57
Many-one and One-one Reducibility / The Relation of Substitution / Deductive
Systems / The Narrow and Broad Languages of Arithmetic / The Theories Q and
PA / Exercises
Lecture IX
66
Cantor's Diagonal Principle / A First Version of Gödel's Theorem / More Versions
of Gödel's Theorem / Q is RE-Complete
Lecture X
73
True Theories are 1-1 Complete / Church's Theorem / Complete Theories are
Decidable / Replacing Truth by ω-Consistency / The Normal Form Theorem for RE
i
Elementary Recursion Theory. Preliminary Version
Copyright © 1995 by Saul Kripke
/ Exercises
Lecture XI
81
An Effective Form of Gödel's Theorem / Gödel's Original Proof / The
Uniformization Theorem for r.e. Relations / The Normal Form Theorem for Partial
Recursive Functions
Lecture XII
87
An Enumeration Theorem for Partial Recursive Functions / Reduction and
Separation / Functional Representability / Exercises
Lecture XIII
95
Languages with a Recursively Enumerable but Nonrecursive Set of Formulae / The
S n Theorem / The Uniform Effective Form of Gödel's Theorem / The Second
Incompleteness Theorem
Lecture XIV
103
The Self-Reference Lemma / The Recursion Theorem / Exercises
Lecture XV
112
The Recursion Theorem with Parameters / Arbitrary Enumerations
Lecture XVI
116
The Tarski-Mostowski-Robinson Theorem / Exercises
Lecture XVII
124
The Evidence for Church's Thesis / Relative Recursiveness
Lecture XVIII
130
Recursive Union / Enumeration Operators / The Enumeration Operator Fixed-Point
Theorem / Exercises
Lecture XIX
138
The Enumeration Operator Fixed-Point Theorem (Continued) / The First and
Second Recursion Theorems / The Intuitive Reasons for Monotonicity and
Finiteness / Degrees of Unsolvability / The Jump Operator
Lecture XX
145
More on the Jump Operator / The Arithmetical Hierarchy / Exercises
ii
Elementary Recursion Theory. Preliminary Version
Copyright © 1995 by Saul Kripke
Lecture XXI
153
The Arithmetical Hierarchy and the Jump Hierarchy / Trial-and-Error Predicates /
The Relativization Principle / A Refinement of the Gödel-Tarski Theorem
Lecture XXII
160
The
ω
-rule / The Analytical Hierarchy / Normal Form Theorems / Exercises
Lecture XXIII
167
Relative
's and
Π
's / Another Normal Form Theorem / Hyperarithmetical Sets
Lecture XXIV
173
Hyperarithmetical and ∆
1 Sets / Borel Sets / Π
1 Sets and Gödel's Theorem /
Arithmetical Truth is
∆
Lecture XXV
182
The Baire Category Theorem / Incomparable Degrees / The Separation Theorem for
S 1 Sets / Exercises
iii
Σ
1
1
1
1
Elementary Recursion Theory. Preliminary Version
Copyright © 1996 by Saul Kripke
Lecture I
First Order Languages
In a first order language L, all the primitive symbols are among the following:
Connectives: ~ ,
⊃
.
Parentheses: ( , ).
Variables: x 1 , x 2 , x 3 , . . . .
Constants: a 1 , a 2 , a 3 , . . . .
Function letters:
f 1 , f 2 , ...
(one-place);
f 1 , f 2 , ...
(two-place);
:
:
Predicate letters: P 1 , P 2 , ...
(one-place);
P 1 , P 2 , ...
(two-place);
:
:
Moreover, we place the following constraints on the set of primitive symbols of a first order
language L. L must contain all of the variables, as well as the connectives and parentheses.
The constants of L form an initial segment of a 1 , a 2 , a 3 , . . ., i.e., either L contains all the
constants, or it contains all and only the constants a 1 , . . ., a n for some n, or L contains no
constants. Similarly, for any n, the n-place predicate letters of L form an initial segment of
P 1 , P 2 , ... and the n-place function letters form an initial segment of f 1 , f 2 , ... However, we
require that L contain at least one predicate letter; otherwise, there would be no formulae of
L.
(We could have relaxed these constraints, allowing, for example, the constants of a
language L to be a 1 , a 3 , a 5 , . . . However, doing so would not have increased the expressive
power of first order languages, since by renumbering the constants and predicates of L, we
could rewrite each formula of L as a formula of some language L' that meets our
constraints. Moreover, it will be convenient later to have these constraints.)
A first order language L is determined by a set of primitive symbols (included in the set
described above) together with definitions of the notions of a term of L and of a formula of
L. We will define the notion of a term of a first order language L as follows:
1

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin