|
Abstract : |
Abstract. A new games model of the language FPC, a type theory with products, sums, function spaces and recursive types, is described. A definability result is proved, showing that every finite element of the model is the interpretation of some term of the language. 1. Introduction. The work of Lorenzen [24, 23] proposed dialogue games as a foundation for intuitionistic logic. The idea is simple: associated to a formula A is a set of moves for two players, each of which is either an attack on A---an attempt to refute its validity---or a defence. The players, O who wants to refute A and P who wants to prove A, take turns to make moves, |
