Investigating Streamless Sets
In this paper we look at streamless sets, recently investigated by Coquand and Spiwack. A set is streamless if every stream over that set contain a duplicate. It is an open question in constructive mathematics whether the Cartesian product of two streamless sets is streamless.
We look at some settings in which the Cartesian product of two streamless sets is indeed streamless; in particular, we show that this holds in Martin-Loef intentional type theory when at least one of the sets have decidable equality. We go on to show that the addition of functional extensionality give streamless sets decidable equality, and then investigate these results in a few other constructive systems.
Type theory
Constructive Logic
Finite Sets
187-201
Regular Paper
Erik
Parmann
Erik Parmann
10.4230/LIPIcs.TYPES.2014.187
Michael Beeson. Goodman’s theorem and beyond. Pacific Journal of Mathematics, 84(1):1-16, 1979.
M. Bezem, K. Nakata, and T. Uustalu. On streams that are finitely red. Logical Methods in Computer Science, 2011. URL: http://www.cs.ioc.ee/~keiko/papers/finiteness.pdf.
http://www.cs.ioc.ee/~keiko/papers/finiteness.pdf
The Coq Development Team. The Coq Reference Manual, version 8.4, August 2012. Available electronically at URL: http://coq.inria.fr/doc.
http://coq.inria.fr/doc
Thierry Coquand and Arnaud Spiwack. Constructively finite? In Contribuciones científicas en honor de Mirian Andrés Gómez, pages 217-230. Universidad de La Rioja, 2010.
Per Martin-Löf. An intuitionistic theory of types: predicative part. In H. E. Rose and J. C. Shepherdson, editors, Proceedings of the Logic Colloquium 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975.
Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 17. Bibliopolis Naples, 1984.
F. P. Ramsey. On a problem of formal logic. Proceedings of the London Mathematical Society, 2(1):264-286, 1930.
F. Richman and G. Stolzenberg. Well quasi-ordered sets. Advances in Mathematics, 97(2):145-153, 1993.
Anne Sjerp Troelstra and Dirk Van Dalen. Constructivism in mathematics, volume 2. Elsevier, 1988.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
http://homotopytypetheory.org/book
Wim Veldman and Marc Bezem. Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society, 2(2):193-211, 1993.
Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop when you are almost-full. In Interactive Theorem Proving, pages 250-265. Springer, 2012.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode