Kripke models for subtheories of CZF |
| |
Authors: | Rosalie Iemhoff |
| |
Institution: | (1) Institute of Information Science, Academia Sinica, Taipei, Taiwan; |
| |
Abstract: | In this paper a method to construct Kripke models for subtheories of constructive set theory is introduced that uses constructions
from classical model theory such as constructible sets and generic extensions. Under the main construction all axioms except
the collection axioms can be shown to hold in the constructed Kripke model. It is shown that by carefully choosing the classical
models various instances of the collection axioms, such as exponentiation, can be forced to hold as well. The paper does not
contain any deep results. It consists of first observations on the subject, and is meant to introduce some notions that could
serve as a foundation for further research. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|