Page 81 - Textos de Matemática Vol. 38

ORDINALS, COMPUTATIONS, AND MODELS OF SET THEORY 73
with stack contents ⟨α0, α1, α2, . . . , αn−1, α¯⟩. By the inductive hypothesis, P will then get to state SubLoop with stack contents ⟨α0, α1, α2, . . . , αn−1⟩ and valueset to F(α¯). Then the program will compute H(αn−1,α¯,F(α¯)) = 1 and move into alternative 3. The register value obtains the value F(αn−1) = 1 and the program moves to state SubLoop with the last stack element removed: stack= ⟨α0, α1, α2, . . . , αn−1⟩, as required.
Case 2: α¯ = α. Then F(α¯) = 0. By b), P will get to stateMainLoopwith stack contents α0, α1, α2, . . . , αn−1, α¯ = αn−1. Inspection of the program shows that it will get into alternative 1, set stack:= ⟨α0, α1, α2, . . . , αn−1⟩, value= 0 and move to SubLoop, which proves a) in this case.
Finally, c) follows readily from a) and inspection of the program. ✷ 8.3 A recursive truth predicate
The go¨del pairing function G allows to code finite sequences α0, . . . , αn−1 of ordinals into single ordinals. The coding can be made computable in the sense that usual operations on finite sequences like concatenation or substitution are computable as well. By these techniques one can also code formal languages in a computable way.
We shall consider a language LR appropriate for first-order structures of the form
(α,<,G,R)
where the Go¨del function G is viewed as a ternary relation on α and R is a unary relation on α. The terms of the language are variables vn for n < ω and constant symbols cξ for ξ ∈ Ord; the symbol cξ will be interpreted as the ordinal ξ. The language has atomic formulas t1 ≡ t2, t1 < t2, G˙ (t1, t2, t3) and R˙ (t1). If φ and ψ are (compound) formulas of the language and t is a term then
¬φ,(φ∨ψ),and∃vn <tφ
are also formulas; thus we are only working with bounded quantification. We
arrange the computable coding in a way that a bounded existential quantifica-
tion ∃vn < cξ φ is coded by a larger ordinal than each of its instances φ cζ with
ζ < ξ:
vn
φcζ <(∃vn<cξφ). vn
An LR-formula is an LR-sentence if it does not have free variables. If φ is an LT -sentence so that all constants symbols cξ in φ have indices ξ < α then the satisfaction relation
(α,<,G,R) φ
is defined as usual. Bounded sentences are absolute for sufficiently long initial segments of the ordinals. If φ is a bounded sentence such that every constant symbol cξ occurring in φ satisfies ξ < β < α then
(α,<,G,R) φ iff (β,<,G,R) φ.