Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barbanera, F., Dezani-Ciancaglini, M.: Intersection and Union Types: Syntax and Semantics. Information and Computation 119, 202–230 (1995)
David, R., Nour, K.: A short proof of the strong normalization of classical natural deduction with disjunction. Journal of Symbolic Logic 68(4), 1277–1288 (2003)
de Groote, P.: On the strong normalisation of intuitionistic natural deduction with permutation-conversions. Information and Computation 178, 441–464 (2002)
Joachimski, F., Matthes, R.: Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel’s T. Archive for Mathematical Logic 42, 59–87 (2003)
Matthes, R.: Non-strictly positive fixed-points for classical natural deduction. Annals of Pure and Applied Logic 133(1-3), 205–230 (2005)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10(3), 470–502 (1988)
Nour, K., Saber, K.: A semantical proof of the strong normalization theorem for full propositional classical natural deduction. Archive for Mathematical Logic 45(3), 357–364 (2006)
Prawitz, D.: Natural Deduction. Almquist and Wiksell (1965)
Prawitz, D.: Ideas and results of proof theory. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Logic Symposium, pp. 235–307. North-Holland, Amsterdam (1971)
Tatsuta, M., Mints, G.: A simple proof of second-order strong normalization with permutative conversions. Annals of Pure and Applied Logic 136(1-2), 134–155 (2005)
Tatsuta, M.: Second order permutative conversions with Prawitz’s strong validity. Progress in Informatics 2, 41–56 (2005)
Tatsuta, M., Dezani-Ciancaglini, M.: Normalisation is Insensible to lambda-term Identity or Difference. lambda-term Identity or Difference. In: Proceedings of Twenty First Annual IEEE Symposium on Logic in Computer Science, pp. 327–336 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Tatsuta, M. (2007). Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-73228-0_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73227-3
Online ISBN: 978-3-540-73228-0
eBook Packages: Computer ScienceComputer Science (R0)