Friedman's translation is a well-known transformation of formulas. The Friedman translation has two properties: i) it validates intuitionistic theorems -- if a formula is intuitionistically provable, then so it is its Friedman translation; ii) it is suitable for program extraction from classical proofs -- the intuitionistic provability of the Friedman translation of the negative translation of a for-all-exist-formula implies the intuitionistic provability of the formula itself. However, the Friedman translation does not validate classical principle, like the Excluded Middle.
Here, we define a restricted Friedman translation which both validates the Excluded Middle and Skolem axiom schemata restricted to $\Sigma^0_1$-formulas and it is also suitable for program extraction from classical proofs using such principles: the intuitionistic provability of the restricted Friedman translation of a for-all-exist-formula implies the intuitionistic provability of the formula itself. Then we introduce a learning-based Realizability Semantics for Heyting Arithmetic with all finite types, extended with the two previous axiom schemata. We call this semantics "Interactive Realizability", and we characterize it as the composition of our Friedman translation with Kreisel modified realizability. As a corollary, we show that Interactive Realizability is, in a sense, "axiom-driven", while the other Realizability Semantics for Classical Arithmetic, like the semantics of Krivine, are "goal-driven".
(