Non-deterministic inductive definitions

DOI10.1007/S00153-012-0309-4MaRDI QIDQ1935375zbMATH OpenOpenAlexFDO

Authors Benno van den Berg

Publication date 15 February 2013

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1104.2744

zbMATH Keywords

type theoryformal topologypredicativityconstructive set theoryinductive and coinductive types

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Other constructive mathematics (03F65)

Abstract: We study a new proof principle in the context of constructive Zermelo-Fraenkel set theory based on what we will call "non-deterministic inductive definitions". We give applications to formal topology as well as a predicative justification of this principle.

Recommendations

• Non-deterministic inductive definitions and fullness
• scientific article; zbMATH DE number 2247249
• Inductive-inductive definitions
• Local constructive set theory and inductive definitions
• ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS

Cites work

• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 42735 (Why is no real title available?)
• scientific article; zbMATH DE number 5200719 (Why is no real title available?)
• Aspects of general topology in constructive set theory
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Completeness and cocompleteness of the categories of basic pairs and concrete spaces
• Constructive completions of ordered sets, groups and fields
• Derived rules for predicative set theory: an application of sheaves
• Generalized geometric theories and set-generated classes
• Maximal and partial points in formal spaces
• Non-well-founded trees in categories
• Real and ideal in constructive mathematics
• Some points in formal topology.
• The axiom of multiple choice and models for constructive set theory
• The strength of some Martin-Löf type theories
• Wellfounded trees in categories

Cited in

(8)

• Equivalents of the finitary non-deterministic inductive definitions
• scientific article; zbMATH DE number 6868322 (Why is no real title available?)
• Generalized geometric theories and set-generated classes
• Non-deterministic inductive definitions and fullness
• scientific article; zbMATH DE number 2247249 (Why is no real title available?)
• Variations on inductive-recursive definitions
• Eliminating disjunctions by disjunction elimination
• Eliminating disjunctions by disjunction elimination

This page was built for publication: Non-deterministic inductive definitions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1935375)