Equivalents of the finitary non-deterministic inductive definitions

Annals of Pure and Applied Logic 170 (10):1256-1272 (2019)
  Copy   BIBTEX

Abstract

We present statements equivalent to some fragments of the principle of non-deterministic inductive definitions (NID) by van den Berg (2013), working in a weak subsystem of constructive set theory CZF. We show that several statements in constructive topology which were initially proved using NID are equivalent to the elementary and finitary NIDs. We also show that the finitary NID is equivalent to its binary fragment and that the elementary NID is equivalent to a variant of NID based on the notion of biclosed subset. Our result suggests that proving these statements in constructive topology requires genuine extensions of CZF with the elementary or finitary NID.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,709

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Non-deterministic inductive definitions.Benno van den Berg - 2013 - Archive for Mathematical Logic 52 (1-2):113-135.
Ordinal analysis of non-monotone-definable inductive definitions.Wolfram Pohlers - 2008 - Annals of Pure and Applied Logic 156 (1):160-169.
A flexible type system for the small Veblen ordinal.Florian Ranzi & Thomas Strahm - 2019 - Archive for Mathematical Logic 58 (5-6):711-751.
A note on theories for quasi-inductive definitions.Riccardo Bruni - 2009 - Review of Symbolic Logic 2 (4):684-699.
Quantifiers, games and inductive definitions.Peter Aczel - 1975 - Journal of Symbolic Logic 82 (2):1--14.
Abstract inductive and co-inductive definitions.Giovanni Curi - 2018 - Journal of Symbolic Logic 83 (2):598-616.
Functional interpretation and inductive definitions.Jeremy Avigad & Henry Towsner - 2009 - Journal of Symbolic Logic 74 (4):1100-1120.

Analytics

Added to PP
2019-05-31

Downloads
19 (#796,059)

6 months
3 (#965,065)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Subsystems of Second Order Arithmetic.Stephen G. Simpson - 1999 - Studia Logica 77 (1):129-129.
Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
Aspects of general topology in constructive set theory.Peter Aczel - 2006 - Annals of Pure and Applied Logic 137 (1-3):3-29.
Maximal and partial points in formal spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1-3):291-298.

View all 8 references / Add more references