publication . Preprint . 2017

Some Brouwerian Counterexamples Regarding Nominal Sets in Constructive Set Theory

Swan, Andrew;
Open Access English
  • Published: 06 Feb 2017
Abstract
The existence of least finite support is used throughout the subject of nominal sets. In this paper we give some Brouwerian counterexamples showing that constructively, least finite support does not always exist and in fact can be quite badly behaved. On this basis we reinforce the point that when working constructively with nominal sets the use of least finite support should be avoided. Moreover our examples suggest that this problem can't be fixed by requiring nominal sets to have least finite support by definition or by using the notion of subfinite instead of finite.
Subjects
free text keywords: Mathematics - Logic, 03F55
Download from

[1] P. Aczel and M. Rathjen. Notes on constructive set theory. Technical Report 40, Institut Mittag-Leffler, 2001.

[2] P. Aczel and M. Rathjen. Notes on constructive set theory. Book draft available at http://www1.maths.leeds.ac.uk/~rathjen/book.pdf, 2010.

[3] P. Choudhury. Constructive representation of nominal sets in agda. Master's thesis, Robinson College, University of Cambridge, June 2015. Available at https://www.cl.cam.ac.uk/~amp12/agda/choudhury/choudhury-dissertation.pdf.

[4] A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013.

[5] A. M. Pitts. Nominal presentation of cubical sets models of type theory. In H. Herbelin, P. Letouzey, and M. Sozeau, editors, 20th International Conference on Types for Proofs and Programs (TYPES 2014), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[6] M. Rathjen. Realizability for constructive Zermelo-Fraenkel set theory. In V. Stoltenberg-Hansen and J. Va¨a¨n¨anen, editors, Logic Colloquium '03. Association for Symbolic Logic, 2006.

[7] A. W. Swan. An algebraic weak factorisation system on 01-substitution sets: a constructive proof. arXiv:1409.1829, September 2014.

Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue