Page 28 - Textos de Matemática Vol. 38

20 FERNANDO FERREIRA
The definition of implication is the harder to understand. G¨odel motivates
it as follows. First consider (A)D →(B)D, that is, the implication ∃x∀yAD(x ,y)→
∃z
z to ∀wBD(z
type computable functionals f such that ∀x
G¨odel invites us to interpret the inner implication in the following way: When- ever a counter-example w is given to BD(f(x),w)) then a counter-example y is given to AD(x, y). If the latter counter-example is given by a rule of computation in terms of the former, then there should be finite-type computable function- als g such that ¬BD(f(x),w)) → ¬AD(x,g(x,w)). Using the decidability of
quantifier-free formulas, we get the implication AD(x,g(x,w)) → BD(f(x),w as in the definition. The attentive reader will notice that several of the passages above are not intuitionistically justifiable. However, G¨odel’s definitions do sus- tain a soundness theorem. There are three important principles in connection with this theorem:
I. The axiom of choice ACω.
II. The principle of independence of premises stated for universal an-
∀wBD(z
, w). If this is done by a rule of computation, there should be finite-
, w). In other words, a witness x to ∀yAD(x, y) gives rise to a witness
(∀yAD(x
,y) → ∀wBD(f(x
), w)).
),
tecedents, denoted by IPω∀ (a formula is universal if it is of the form ∀x
Aqf (x
), III. Markov’s Principle MPω: ¬∀zAqf(z) → ∃z¬Aqf(z), where Aqf is a
for Aqf quantifier-free).
quantifier-free formula and z is of any type.
Markov’s principle strictu sensu applies only for z of type 0. The acceptance of this principle differentiates the school of Russian constructivism from the other constructivist schools. Its acceptance is based on the intuition that if ∀z0Aqf(z) leads to a contradiction then, if we test in succession each natural number z0 for the (decidable) truth of Aqf(z) then we will eventually find a z0 such that ¬Aqf(z). Note that this intuition does not apply for z of non-zero type. The name “Markov’s Principle” for non-zero types is a misnomer.
Using the decidability of quantifier-free formulas, we can see that MPω implies(∀zAqf(z)→Bqf)→∃z(Aqf(z)→Bqf),forAqf andBqf quantifier-free formulas. Note that MPω is the particular case when Aqf is ⊥.
Theorem 3.2 (Soundness of the Dialectica interpretation). Suppose that HAω0 +ACω +IPω∀ +MPω +∆⊢A(z),
where ∆ is a set of universal sentences and A is an arbitrary formula (with the free variables as shown). Then there are closed terms t of appropriate types such that
H A ω0 + ∆ ⊢ ∀ z
As usual, the proof is by induction on the length of formal proofs, and the terms are effectively constructed from the formal proofs. The discussion of the seemingly innocuous contraction axiom A → A ∧ A is subtle in two respects
∀yAD(t(z
),y,z
).