Realizability and intuitionistic logic
type: Item
instance of: scholarly article
title: Realizability and intuitionistic logic
zbMATH Open document ID: 0537.03043
DOI: 10.1007/BF00485463
author: A. S. Troelstra
author: Justus Diller
published in: Synthese
publication date: 1984-01-01T00:00:00Z
review text: 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 associat…
Mathematics Subject Classification ID: 03F65
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03F25
zbMATH DE Number: 3853070
zbMATH Keywords: proof-interpretation
zbMATH Keywords: formulae-as-types
zbMATH Keywords: proof-interpretation of intuitionistic logical operators
zbMATH Keywords: realizability interpretations
zbMATH Keywords: typed systems
zbMATH Keywords: abstract realizability
zbMATH Keywords: extensional realizability
zbMATH Keywords: type theory
describes a project that uses: Automath
MaRDI profile type: Publication
cites work: Goodman's theorem and beyond
cites work: Q3898494
cites work: Q5610115
cites work: Q5565113
cites work: Q4133603
cites work: Q4128540
cites work: Q3882452
cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
cites work: Q5613908
cites work: Intuitionism. An introduction
cites work: Q4077976
cites work: On the interpretation of intuitionistic number theory
cites work: Q5343325
cites work: Q3214888
cites work: Q5597507
cites work: Q5633976
cites work: Q5619069
cites work: Q4099613
cites work: Q4099614
cites work: The Overlap of Random Particles and Similar Problems: Expressions for Variance of Coverage and its Analogue
cites work: Constructions, proofs and the meaning of logical constants
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Q4145690
full work available at URL: https://doi.org/10.1007/bf00485463
OpenAlex ID: W4232423688
description: scientific article; zbMATH DE number 3853070