Equalisers of Frames in Constructive Set Theory

2011 ◽  
pp. 221-228
Author(s):  
Peter Aczel
Keyword(s):  
Set Theory ◽  
Constructive Set Theory

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

The natural numbers in constructive set theory

2008 ◽  
Vol 54 (1) ◽  
pp. 83-97 ◽  
Author(s):  
Michael Rathjen
Keyword(s):  
Set Theory ◽  
Natural Numbers ◽  
Constructive Set Theory

Does Choice Really Imply Excluded Middle? Part I: Regimentation of the Goodman–Myhill Result, and Its Immediate Reception†

2020 ◽  
Vol 28 (2) ◽  
pp. 139-171
Author(s):  
Neil Tennant
Keyword(s):  
Set Theory ◽  
Middle Part ◽  
Free Logic ◽  
Abstraction Principle ◽  
Constructive Set Theory ◽  
Informal Proof ◽  
The One ◽  
Excluded Middle

ABSTRACT The one-page 1978 informal proof of Goodman and Myhill is regimented in a weak constructive set theory in free logic. The decidability of identities in general ($a\!=\!b\vee\neg a\!=\!b$) is derived; then, of sentences in general ($\psi\vee\neg\psi$). Martin-Löf’s and Bell’s receptions of the latter result are discussed. Regimentation reveals the form of Choice used in deriving Excluded Middle. It also reveals an abstraction principle that the proof employs. It will be argued that the Goodman–Myhill result does not provide the constructive set theorist with a dispositive reason for not adopting (full) Choice.

Sign in / Sign up

Export Citation Format

Share Document