Page 76 - Textos de Matemática Vol. 40
P. 76

64 Chapter 2. Explicit Mathematics Theorem 2.2.2. There exists a formula Acc(a,b,x) such that NEM proves for
arbitrary formulae φ(x):
(Acc.1) R(a)∧R(b)→Closed(a,b,Acc(a,b,·)),
(Acc.2) R(a)∧R(b)∧Closed(a,b,φ)→∀x.Acc(a,b,x)→φ(x).
Proof. Let us assume R(a, A) and R(b, B). We set Ax = {y ∈ A|(y, x) ∈ B}, i.e., the subset of A consisting of all B-predecessors of x. By elementary comprehension, there exists a closed term pd so that R(pd (a, b, x), Ax).
By use of the Recursion Theorem, we can define a term f satisfying the equation:
f (a,b,c) ≃ j(pd(a,b,c),λy.f(a,b,y)). (⋆) Hence, f maps an element c ∈ A to the disjoint union of all f-images of B-
predecessors of c. Using f, we define the formula Acc in the following way: Acc(a,b,c) := c ∈˙ a ∧ R(f (a,b,c)).
If Acc(a,b,c) holds we say that “c is accessible”. The idea of its definition is the following. pd(a,b,c) is the name of the type Ac which contains all B- predecessors of c in A. Using join, we associate this type with a type of elements which can be proven to be names if f (a, b, c) is a name. This trick, called Studer’s trick, allows us to encode arbitrary objects of our language by names, and then name induction can be used to prove the required properties.
(Acc.1) To show Closed(a, b, Acc(a, b, ·)), we choose an element c of A such that
∀y ∈˙ a.(y,c) ∈˙ b → Acc(a,b,y). The definition of pd yields
∀y.y∈˙ pd(a,b,c)→Acc(a,b,y). This implies by the definition of Acc that
∀y.y ∈˙ pd(a,b,c) → R(f (a,b,y)). ¿From the axioms about join, we obtain
R(j (pd (a, b, c), f)).
By the equation (⋆), this means R(f (a, b, c)). Together with the assumption c ∈˙ a we have Acc(a, b, c). Since c was chosen arbitrarily, the proof of Closed(a, b, Acc) is completed.
(Acc.2) To prove the second assertion we first show two auxiliary state- ments (A) and (B).
(A) says that if c is accessible, then all its b predecessors are accessible, too.
Acc(a,b,c)→(∀x∈˙ pd(a,b,c).Acc(a,b,x)). (A)


































































































   74   75   76   77   78