Robert Passmann: The de Jongh Property for a Subtheory of CZF

Tuesday, November 6, 2018, 10:30
Seminar room N0.003, Mathematical Institute, University of Bonn

Speaker: Robert Passmann (Amsterdam)

Title: The de Jongh Property for a Subtheory of CZF

Abstract:

After recalling intuitionistic logic, Kripke semantic, and (Heyting) algebra-valued models for set theory, we will introduce the notions of loyalty and faithfulness: An algebra-valued model is called loyal if its propositional logic is the propositional logic of its underlying algebra; it is called faithful if all elements of the underlying algebra are truth values of sentences in the language of set theory in the model. We will then analyse the loyalty and faithfulness of a particular construction of Kripke models of set theory due to Iemhoff, and, by using classical models of ZFC set theory and the forcing technique, prove the de Jongh property for the constructive set theory CZF${}^*$ satisfied by Iemhoff’s models, i.e., for any propositional formula $\phi(p_0,…,p_{n-1})$ with propositional letters $p_0,…,p_{n-1}$, it holds that intuitionistic logic IPC proves $\phi(p_0,…,p_{n-1})$ if and only if CZF${}^*$ proves $\phi(\psi_0,…,\psi_{n-1})$ for all set theoretical sentences $\psi_0,…,\psi_{n-1}$. More precisely, we show that CZF${}^*$ has the de Jongh property with respect to every logic that can be characterised by a class of Kripke frames.

Leave a Reply

Your email address will not be published. Required fields are marked *

Time limit is exhausted. Please reload CAPTCHA.

This site uses Akismet to reduce spam. Learn how your comment data is processed.