Non-deterministic inductive definitions

DOI10.1007/s00153-012-0309-4zbMath1403.03111arXiv1104.2744MaRDI QIDQ1935375

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 theory; constructive set theory; formal topology; predicativity; inductive and coinductive types

Mathematics Subject Classification ID

03E70: Nonclassical and second-order set theories

03F65: Other constructive mathematics

Related Items

ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION, Generalized geometric theories and set-generated classes, Eliminating disjunctions by disjunction elimination, Equivalents of the finitary non-deterministic inductive definitions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Derived rules for predicative set theory: an application of sheaves
• Non-well-founded trees in categories
• The strength of some Martin-Löf type theories
• Some points in formal topology.
• Wellfounded trees in categories
• Constructive completions of ordered sets, groups and fields
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Aspects of general topology in constructive set theory
• Maximal and partial points in formal spaces
• The axiom of multiple choice and models for constructive set theory
• Real and Ideal in Constructive Mathematics
• Generalized geometric theories and set-generated classes
• Completeness and cocompleteness of the categories of basic pairs and concrete spaces