1985 | OriginalPaper | Buchkapitel
Realizability
verfasst von : Michael J. Beeson
Erschienen in: Foundations of Constructive Mathematics
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In 1945 Kleene forged a link between the two previously unconnected areas of intuitionism and recursive function theory, by finding a way to interpret the intuitionistic logic using recursive functions for the “we can find” of the intuitionistic “there exists”. He defined the notion of “recursive realizability”, which is a precisely-defined concept designed to interpret the “rules” which are inherent in the constructive meaning of the logical operations, especially the quantifier combination ∀x∃y and implication. For example, a statement ∀n∃mR (nm) will be “recursively realized” by an index e such that for every n, R(n,{e}(n)), at least in case R is recursive. In general, one should think of realizability as a sort of “constructive model”: the intuition is that, when defining a model of a constructive theory, one ought not only to give an interpretation to the constants and variables (as in classical model theory) but also to the logical operations. Some notion of “rule” is implicit in the intuitionistic logic — that notion ought to be modeled.