Page 18 - Textos de Matemática Vol. 38

10 FERNANDO FERREIRA
normalization yields an oracle computation (the oracle is only invoked to effect contractions of the form (v)α).
2 Second lecture
2.1 Modified realizability
The method of realizability is reminiscent of the BHK (Brouwer-Heyting- Kolmogorov) interpretation of the intuitionistic connectives. We introduce a version of realizability, called modified realizability, due to Georg Kreisel in the setting of finite type arithmetic.
We present Kreisel’s modified realizability in a slightly unfamiliar way. Instead of saying what realizing tuples of functionals are, we associate to each formula of the language an existential formula. We need a preliminary definition:
Definition2.1.AformulaofLω0 iscalled∃-freeifitisbuiltfromatomicformulas by means of conjunctions, implications and universal quantifications.
We are ready to define the assignment of modified realizability: Definition 2.2. To each formula A of the language Lω0 we assign formulas (A)mr
) a ∃-free formula, and Amr so that (A)mr is of the form ∃xAmr(x) with Amr(x
according to the following clauses:
1. (A)mr and Amr are simply A, for atomic formulas A.
If we have already interpretations for A and B given by ∃xAmr(x) and ∃yBmr(y) (respectively) then, we define:
2. (A ∧ B)mr is ∃x
, y(Amr(x) ∧ Bmr(y)),
3. (A∨B)mr is ∃n0∃x,y(n=0→Amr(x 4. (A → B)mr is ∃f∀x(Amr(x) → Bmr(f(x 5. (∀zA(z))mr is ∃f∀zAmr(f(z),z),
6. (∃zA(z))mr is ∃z,x
Amr(x, z).
extracting constructive information from negated formulas.
)) ∧ (n ̸= 0 → Bmr(y)),
))),
, we say that x realizes A. Notice that the tuple x may be empty. The realizers of a disjunction include a flag n of type 0 that decides which way to go. Similarly, the realizers of an existential quantifier include an existential witness. It is easy to check that the interpretation of negation (¬A)mr is ∀x¬Amr(x). Notice that (¬A)mr is always an ∃-free formula and, therefore, has no realizers. Realizability is unsuitable for
If Amr(x) holds for a certain sequence of functionals x