A Diller-Nahm-style functional interpretation of
$\hbox{\sf KP} \omega$ |
| |
| Authors: | Wolfgang Burr |
| |
| Institution: | Institut für Mathematische Logik und Grundlagenforschung der Westf?lischen Wilhelms-Universit?t Münster, Einsteinstr. 62, D-48149 Münster, Germany (e-mail: Wolfgang.Burr@math.uni-muenster.de), DE
|
| |
| Abstract: | The Dialectica-style functional interpretation of Kripke-Platek set theory with infinity () given in 1] uses a choice functional (which is not a definable set function of (). By means of a Diller-Nahm-style interpretation (cf. 4]) it is possible to eliminate the choice functional and give an
interpretation by set functionals primitive recursive in . This yields the following characterization: The class of -definable set functions of coincides with the collection of set functionals of type 1 primitive recursive in .
Received: 26 August 1998 |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
