Page 27 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 19
translation, the translation destroys existential statements – replacing them by negated universal statements – with the consequence that realizers yield no computational information. Of course, this shortcoming is related with the fact that Markov’s principle is not benign. That notwithstanding, bounded modified realizability (and Kohlenbach’s monotone modified realizability) supports many classical principles that go beyond intuitionistic logic.
Question 3. Find numerical applications of bounded or monotone modified real- izability.
In order to deal with full classical reasoning, we must use the more sophis- ticated tool of the functional interpretation, introduced by Kurt G¨odel. This is the subject of the second part of the course.
3 Third lecture
3.1 G¨odel’s Dialectica interpretation
In 1958, G¨odel published an article in an issue of the journal Dialectica dedicated to the seventieth anniversary of Paul Bernays. The article presents an interpretation of first-order Heyting arithmetic into a quantifier-free theory with finite-type functionals (Go¨del’s theory T). This theory is, essentially, the quantifier-free part of HAω0 . G¨odel’s Dialectica interpretation appeared as a con- tribution to an extended Hilbert’s program by means of the novel notion of computable functional of finite type. In the sequel, we present G¨odel’s interpre- tation extended to finite-type arithmetic HAω0 .
Definition 3.1. To each formula A of the language Lω0 we assign formulas (A)D and AD so that (A)D is of the form ∃x∀yAD(x, y) with AD(x, y) a quantifier-free formula, according to the following clauses:
1. (A)D and AD are simply A, for atomic formulas A.
If we have already interpretations for A and B given by ∃x
∀yAD(x
,y) and
∃z
∀wBD(z
2. (A∧B)D is∃x,z
3. (A∨B)D is∃n0,x,z
4. (A→B)D is∃f,g∀x,w
5. (∀zA(z))D is ∃f∀z∀yAD(f(z),y,z).
, w) (respectively) then we define:
(AD(x,y)∧BD(z,w
((n = 0 → AD(x, y)) ∧ (n ̸= 0 → BD(z, w
(AD(x,g(x,w)) → BD(f(x),w)). ∀yAD(x, y, z).
∀y,w ∀y,w
)),
))),
6. (∃zA(z))D is ∃z, x