Non-deterministic inductive definitions

作者：van den Berg Benno^*

来源：Archive for Mathematical Logic, 2013, 52(1-2): 113-135.

DOI：10.1007/s00153-012-0309-4

• Constructive set theory
• Type theory
• Predicativity
• Formal topology
• Inductive and coinductive types

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.

• 出版日期2013-2