This paper gives simple saturated sets for disjunction and second-order existential quantification by using the idea of segments in Prawitz's strong validity. Saturated sets for disjunction are defined by Pi-0-1 comprehension and those for second-order existential quantification are defined by Sigma-1-1 comprehension. Saturated-set semantics and a simple strong normalization proof are given to the system with disjunction, second-order existential quantification, and their permutative conversions. This paper also introduces the contraction property to saturated sets, which gives us saturated sets closed under union. This enables us to have saturated-set semantics for the system with union types, second-order existential types, and their permutative conversions, and prove its strong normalization. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Tatsuta, M. (2007). Simple saturated sets for disjunction and second-order existential quantification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4583 LNCS, pp. 366–380). Springer Verlag. https://doi.org/10.1007/978-3-540-73228-0_26
Mendeley helps you to discover research relevant for your work.