John Myhill. Constructive set theory. The journal of symbolic logic, vol. 40 (1975), pp. 347–382. - Harvey Friedman. Set theoretic foundations for constructive analysis. Annals of mathematics, ser. 2 vol. 105 (1977), pp. 1–28.

1981 ◽  
Vol 46 (4) ◽  
pp. 868-870
Author(s):  
R. J. Grayson
Keyword(s):  
Set Theory ◽  
Symbolic Logic ◽  
Constructive Analysis ◽  
Constructive Set Theory ◽  
Theoretic Foundations

scholarly journals Homotopy type-theoretic interpretations of constructive set theories

2019 ◽  
pp. 1-32
Author(s):  
Cesare Gallozzi
Keyword(s):  
Comparative Analysis ◽  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Axiom Of Choice ◽  
Homotopy Type Theory ◽  
Constructive Set Theory

Abstract We introduce a family of (k, h)-interpretations for 2 ≤ k ≤ ∞ and 1 ≤ h ≤ ∞ of constructive set theory into type theory, in which sets and formulas are interpreted as types of homotopy level k and h, respectively. Depending on the values of the parameters k and h, we are able to interpret different theories, like Aczel’s CZF and Myhill’s CST. We also define a proposition-as-hproposition interpretation in the context of logic-enriched type theories. The rest of the paper is devoted to characterising and analysing the interpretations considered. The formulas valid in the prop-as-hprop interpretation are characterised in terms of the axiom of unique choice. We also analyse the interpretations of CST into homotopy type theory, providing a comparative analysis with Aczel’s interpretation. This is done by formulating in a logic-enriched type theory the key principles used in the proofs of the two interpretations. Finally, we characterise a class of sentences valid in the (k, ∞)-interpretations in terms of the ΠΣ axiom of choice.

Constructive set theory with operations

2014 ◽  
pp. 47-83 ◽  
Author(s):  
Andrea Cantini ◽  
Laura Crosilla
Keyword(s):  
Set Theory ◽  
Constructive Set Theory

VERking in constructive set theory

1981 ◽  
Vol 6 (3) ◽  
pp. 58-60
Author(s):  
Robert L. Constable
Keyword(s):  
Set Theory ◽  
Constructive Set Theory

scholarly journals Principles Weaker than BD-N

2013 ◽  
Vol 78 (3) ◽  
pp. 873-885 ◽  
Author(s):  
Robert S. Lubarsky ◽  
Hannes Diener
Keyword(s):  
Set Theory ◽  
Constructive Logic ◽  
Constructive Analysis ◽  
Cauchy Sequences

AbstractBD-N is a weak principle of constructive analysis. Several interesting principles implied by BD-N have already been identified, namely the closure of the anti-Specker spaces under product, the Riemann Permutation Theorem, and the Cauchyness of all partially Cauchy sequences. Here these are shown to be strictly weaker than BD-N, yet not provable in set theory alone under constructive logic.

Sign in / Sign up

Export Citation Format

Share Document