Non Definability in Intuitionistic Logic

Andrew Swan

University of Leeds, UK

In this talk I will describe a simple technique using Kripke models for showing that certain formulas in certain intuitionisitic theories have no definable witnessess, with some simple examples from intuitionisic ordered fields. I will then describe how the techique can be developed to show that certain sentences in CZF have no definable witnessess. This will include defining "Kripke - realizability" models that incorperate realizability into the definition of Kripke models.