Does Choice Really Imply Excluded Middle? Part II: Historical, Philosophical, and Foundational Reflections on the Goodman–Myhill Result†

2020 ◽  
Author(s):  
Neil Tennant
Keyword(s):  
Set Theory ◽  
Middle Part ◽  
Critical Attention ◽  
Separating Property ◽  
Constructive Set Theory ◽  
Excluded Middle

ABSTRACT Our regimentation of Goodman and Myhill’s proof of Excluded Middle revealed among its premises a form of Choice and an instance of Separation. Here we revisit Zermelo’s requirement that the separating property be definite. The instance that Goodman and Myhill used is not constructively warranted. It is that principle, and not Choice alone, that precipitates Excluded Middle. Separation in various axiomatizations of constructive set theory is examined. We conclude that insufficient critical attention has been paid to how those forms of Separation fail, in light of the Goodman–Myhill result, to capture a genuinely constructive notion of set.

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.

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

Mathematical Existence

2005 ◽  
Vol 11 (3) ◽  
pp. 351-376 ◽  
Author(s):  
Penelope Maddy
Keyword(s):  
Set Theory ◽  
Elliptic Functions ◽  
Mathematical Truth ◽  
Mathematical Methods ◽  
Explicit Representations ◽  
Mathematical Existence ◽  
Synthetic Approaches ◽  
Areas Of Interest ◽  
Compare And Contrast ◽  
Excluded Middle

Despite some discomfort with this grandly philosophical topic, I do in fact hope to address a venerable pair of philosophical chestnuts: mathematical truth and existence. My plan is to set out three possible stands on these issues, for an exercise in compare and contrast. A word of warning, though, to philosophical purists (and perhaps of comfort to more mathematical readers): I will explore these philosophical positions with an eye to their interconnections with some concrete issues of set theoretic method.Let me begin with a brief look at what to count as ‘philosophy’. To some extent, this is a matter of usage, and mathematicians sometimes classify as ‘philosophical’ any considerations other than outright proofs. So, for example, discussions of the propriety of particular mathematical methods would fall under this heading: should we prefer analytic or synthetic approaches in geometry? Should elliptic functions be treated in terms of explicit representations (as in Weierstrass) or geometrically (as in Riemann)? Should we allow impredicative definitions? Should we restrict ourselves to a logic without bivalence or the law of the excluded middle? Also included in this category would be the trains of thought that shaped our central concepts: should a function always be defined by a formula? Should a group be required to have an inverse for every element? Should ideal divisors be defined contextually or explicitly, treated computationally or abstractly? In addition, there are more general questions concerning mathematical values, aims and goals: Should we strive for powerful theories or low-risk theories? How much stress should be placed on the fact or promise of physical applications? How important are interconnections between the various branches of mathematics? These philosophical questions of method naturally include several peculiar to set theory: should set theorists focus their efforts on drawing consequences for areas of interest to mathematicians outside mathematical logic? Should exploration of the standard axioms of ZFC be preferred to the exploration and exploitation of new axioms? How should axioms for set theory be chosen? What would a solution to the Continuum Problem look like?

VERking in constructive set theory

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

Extending Gödel's negative interpretation to ZF

1975 ◽  
Vol 40 (2) ◽  
pp. 221-229 ◽  
Author(s):  
William C. Powell
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Stable Sets ◽  
Class Theory ◽  
Heyting Arithmetic ◽  
Inner Model ◽  
Order Arithmetic ◽  
Definition Of ◽  
Excluded Middle ◽  
Negative Sense

In [5] Gödel interpreted Peano arithmetic in Heyting arithmetic. In [8, p. 153], and [7, p. 344, (iii)], Kreisel observed that Gödel's interpretation extended to second order arithmetic. In [11] (see [4, p. 92] for a correction) and [10] Myhill extended the interpretation to type theory. We will show that Gödel's negative interpretation can be extended to Zermelo-Fraenkel set theory. We consider a set theory T formulated in the minimal predicate calculus, which in the presence of the full law of excluded middle is the same as the classical theory of Zermelo and Fraenkel. Then, following Myhill, we define an inner model S in which the axioms of Zermelo-Fraenkel set theory are true.More generally we show that any class X that is (i) transitive in the negative sense, ∀x ∈ X∀y ∈ x ¬ ¬ x ∈ X, (ii) contained in the class St = {x: ∀u(¬ ¬ u ∈ x→ u ∈ x)} of stable sets, and (iii) closed in the sense that ∀x(x ⊆ X ∼ ∼ x ∈ X), is a standard model of Zermelo-Fraenkel set theory. The class S is simply the ⊆-least such class, and, hence, could be defined by S = ⋂{X: ∀x(x ⊆ ∼ ∼ X→ ∼ ∼ x ∈ X)}. However, since we can only conservatively extend T to a class theory with Δ01-comprehension, but not with Δ11-comprehension, we will give a Δ01-definition of S within T.

Sign in / Sign up

Export Citation Format

Share Document