Page 19 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 11
There are two important principles in connection with modified realizabil- ity:
I. Axiom of Choice ACω: ∀x∃yA(x,y) → ∃f∀xA(x,fx), where A is any formula, and x and y are of any type.
II. Independence of Premises IPω∃free: (A → ∃zB(z)) → ∃z(A → B(z)), where A is ∃-free, B is any formula and z is of any type.
The last principle is a classical, but not intuitionistic, law. Theorem 2.3 (Soundness of modified realizability). Suppose that
HAω0 + ACω + IPω∃free + ∆ ⊢ A(z),
where ∆ is a set of ∃-free sentences and A(z that
) is an arbitrary formula (with the free variables as shown). Then there are closed terms t of appropriate types such
H A ω0 + ∆ ⊢ ∀ z
The proof is by induction on the length of formal proofs, and the terms are effectively constructed from the formal proofs. The principles ACω and IPω∃free disappear because they are automatically interpreted by the realizability no- tion. It must be noted that the recursors are only needed to check the induction axioms, while the logical axioms only need terms built by the combinators. Full extensionality is not automatically interpretable but the next best thing hap- pens: It is constituted by ∃-free sentences and, therefore, it is self-interpretable. Therefore, in the above theorem, we may replace the theory HAω0 by E-HAω.
2.2 Extraction, conservation and characterization for modified realizability
The following is an important consequence of the soundness theorem: Proposition 2.4 (Extraction and conservation). Suppose that
HAω0 + ACω + IPω∃free + ∆ ⊢ ∀x∃yA(x, y),
where ∆ is a set of ∃-free sentences and A is a ∃-free formula with free variables
among x and y. Then there is a closed term t of appropriate type such that HAω0 +∆⊢∀xA(x,tx).
Letting A be the sentence 0 = 1 and ∆ be empty, we conclude that the theory HAω0 + ACω + IPω∃free is consistent relative to HAω0 . This is not, however, terribly interesting.
Amr(t(z), z
).