مدلهاي كريپكي براي زيرنظريه هاي CZF

چكيده انگليسي :

Kripke models for subtheories of CZF Zahra Bagherzadeh z bagherzadeh@math iut ac ir 2016 Department of Mathematical Sciences Isfahan University of Technology Isfahan 84156 83111 Iran Supervisor Dr Mojtaba Aghaei aghaei@cc iut ac ir 2010 MSC 03F50 03F65 03C90 Keywords Kripke models constructible sets generic extension intuitionistic logic AbstractKripke models are produced by attaching the classical models to the nodes of a partial order andare useful to study semantics of logics such as the constructive and modal logics Although variousmodels of CZF such as intuitionistic logic and Heyting arithmetic as well as others in topos theoryand in the form of Heyting algebras are developed so far Kripke models have not been paid attentionenough This thesis is an extension of the work done by R Iemho 1 In this thesis a method ispresented to construct the Kripke models for subtheories of CZF by using constructions from classicalmodel theory such as the constructible sets and generic extensions It is shown how Kripke modelsare produced for various forms of collection by using speci c properties of certain generic extensions Several instances and variations of the collection axioms can be recovered via requirements on thepartial orders on which the generic extensions are based on such as the countable chain condition For example a bounded form of exponentiation and replacement can be forced to hold In this thesis in particular the relation between properties of Kripke models and the generic extensions on whichthey are based on can be pushed further and will ultimately lead to models of full CZF In this thesis the Kripke models of Constructive Zermlo Fraenkel set theory are investigated Kripkemodels are useful tools to study constructive theories Due to the simplicity of Kripke models theyhave been applied to non classical logics in general and intuitionistic logic and Heyting arithmetic inparticular successfully The aim is to construct a Kripke model on a given frame using the classicalmodel theories such as the constructible sets and generic extensions The obtained model which is amodel of CZF is constructed by connecting the classical models to the vertices of the given frame Moreover a method is introduced in this thesis to construct Kripke models for subtheories of construc tive set theory that utilize constructions from classical model theory such as constructible sets andgeneric extensions It is shown that all axioms except the collection axioms hold in the constructedKripke model under the main construction It is shown that various instances of the collection axioms such as exponentiation can be forced to hold as well by choosing the classical models carefully Thisthesis consists of rst observations on the subject and is meant to introduce some notions that couldserve as a foundation for further research Several examples are included in each section to illustratethe given theorems and lemmas

باقرزاده، زهرا

مدلهاي كريپكي براي زيرنظريه هاي CZF

مجموعه هاي ساختي , گسترش جنريك , منطق شهودي