Realizability and intuitionistic logic (Q792319)

The paper is largely expository and attempts to clarity the relationship between the well-known proof-interpretation of intuitionistic logical operators on the one hand and realizability interpretations on the other hand, in particular in connection with the theory of types as formulated by \textit{P. Martin-Löf} [see his paper in Logic, methodology and philosophy of science VI, Proc. 6th int. Congr., Hannover 1979, Stud. Logic Found. Math. 104, 153-175 (1982)]. Two typed systems are considered: \(\underset \tilde{} M\underset \tilde{} L_ 0\), the fragment of Martin- Löf's theory without universes, and a weaker system \(\underset \tilde{} M\underset \tilde{} L^ i_ 0\) obtained by dropping extensionality for equality; these systems are compared with \(\underset \tilde{} A\underset \tilde{} P\underset \tilde{} P\), the arithmetical part of \textit{S. Feferman's} theory \(\underset \tilde{} E\underset \tilde{} M_ 0\upharpoonright\) [see his paper in Logic colloquium '78, Proc., Mons/Belgium 1978, Stud. Logic Found. Math. Vol. 97, 159-224 (1979; Zbl 0441.03022)]. It is shown that \(\underset \tilde{} M\underset \tilde{} L^ i_ 0\) can be interpreted straightforwardly in \(\underset \tilde{} A\underset \tilde{} P\underset \tilde{} P\), in such a way that the interpretation of logic in \(\underset \tilde{} M\underset \tilde{} L^ i_ 0\) corresponds to abstract realizability. For \(\underset \tilde{} M\underset \tilde{} L_ 0\) an embedding is defined such that logic in \(\underset \tilde{} M\underset \tilde{} L_ 0\) corresponds to a form of extensional realizability in \(\underset \tilde{} A\underset \tilde{} P\underset \tilde{} P\). \(\underset \tilde{} M\underset \tilde{} L^ i_ 0\) is similar to the fragment without universes of the type theory described in an earlier paper by \textit{P. Martin-Löf} [Logic Colloq. '73, Proc., Bristol 1973, 73-118 (1975; Zbl 0334.02016)]. It should be pointed out that the present paper gives no adequate description of the semantics associated with Martin-Löf's theories.