scholarly journals Extensional realizability for intuitionistic set theory

Author(s):  
Emanuele Frittaion ◽  
Michael Rathjen

Abstract In generic realizability for set theories, realizers treat unbounded quantifiers generically. To this form of realizability, we add another layer of extensionality by requiring that realizers ought to act extensionally on realizers, giving rise to a realizability universe $\mathrm{V_{ex}}(A)$ in which the axiom of choice in all finite types, ${\textsf{AC}}_{{\textsf{FT}}}$, is realized, where $A$ stands for an arbitrary partial combinatory algebra. This construction furnishes ‘inner models’ of many set theories that additionally validate ${\textsf{AC}}_{{\textsf{FT}}}$, in particular it provides a self-validating semantics for ${\textsf{CZF}}$ (constructive Zermelo–Fraenkel set theory) and ${\textsf{IZF}}$ (intuitionistic Zermelo–Fraenkel set theory). One can also add large set axioms and many other principles.

1951 ◽  
Vol 16 (3) ◽  
pp. 161-190 ◽  
Author(s):  
J. C. Shepherdson

One of the standard ways of proving the consistency of additional hypotheses with the basic axioms of an axiom system is by the construction of what may be described as ‘inner models.’ By starting with a domain of individuals assumed to satisfy the basic axioms an inner model is constructed whose domain of individuals is a certain subset of the original individual domain. If such an inner model can be constructed which satisfies not only the basic axioms but also the particular additional hypothesis under consideration, then this affords a proof that if the basic axiom system is consistent then so is the system obtained by adding to this system the new hypothesis. This method has been applied to axiom systems for set theory by many authors, including v. Neumann (4), Mostowski (5), and more recently Gödel (1), who has shown by this method that if the basic axioms of a certain axiomatic system of set theory are consistent then so is the system obtained by adding to these axioms a strong form of the axiom of choice and the generalised continuum hypothesis. Having been shown in this striking way the power of this method it is natural to inquire whether it has any limitations or whether by the construction of a sufficiently ingenious inner model one might hope to decide other outstanding consistency questions, such as the consistency of the negations of the axiom of choice and continuum hypothesis. In this and two following papers we prove some general theorems concerning inner models for a certain axiomatic system of set theory which lead to the result that as far as a fairly large family of inner models are concerned this method of proving consistency has been exhausted, that no essentially new consistency results can be obtained by the use of this kind of model.


Author(s):  
Alexander R. Pruss

This is a mainly technical chapter concerning the causal embodiment of the Axiom of Choice from set theory. The Axiom of Choice powered a construction of an infinite fair lottery in Chapter 4 and a die-rolling strategy in Chapter 5. For those applications to work, there has to be a causally implementable (though perhaps not compatible with our laws of nature) way to implement the Axiom of Choice—and, for our purposes, it is ideal if that involves infinite causal histories, so the causal finitist can reject it. Such a construction is offered. Moreover, other paradoxes involving the Axiom of Choice are given, including two Dutch Book paradoxes connected with the Banach–Tarski paradox. Again, all this is argued to provide evidence for causal finitism.


2010 ◽  
Vol 75 (3) ◽  
pp. 996-1006 ◽  
Author(s):  
Kyriakos Keremedis ◽  
Eleftherios Tachtsis

AbstractWe establish the following results:1. In ZF (i.e., Zermelo-Fraenkel set theory minus the Axiom of Choice AC), for every set I and for every ordinal number α ≥ ω, the following statements are equivalent:(a) The Tychonoff product of ∣α∣ many non-empty finite discrete subsets of I is compact.(b) The union of ∣α∣ many non-empty finite subsets of I is well orderable.2. The statement: For every infinite set I, every closed subset of the Tychonoff product [0, 1]Iwhich consists offunctions with finite support is compact, is not provable in ZF set theory.3. The statement: For every set I, the principle of dependent choices relativised to I implies the Tychonoff product of countably many non-empty finite discrete subsets of I is compact, is not provable in ZF0 (i.e., ZF minus the Axiom of Regularity).4. The statement: For every set I, every ℵ0-sized family of non-empty finite subsets of I has a choice function implies the Tychonoff product of ℵ0many non-empty finite discrete subsets of I is compact, is not provable in ZF0.


Axioms ◽  
2018 ◽  
Vol 7 (4) ◽  
pp. 86 ◽  
Author(s):  
Dmitri Shakhmatov ◽  
Víctor Yañez

We give a “naive” (i.e., using no additional set-theoretic assumptions beyond ZFC, the Zermelo-Fraenkel axioms of set theory augmented by the Axiom of Choice) example of a Boolean topological group G without infinite separable pseudocompact subsets having the following “selective” compactness property: For each free ultrafilter p on the set N of natural numbers and every sequence ( U n ) of non-empty open subsets of G, one can choose a point x n ∈ U n for all n ∈ N in such a way that the resulting sequence ( x n ) has a p-limit in G; that is, { n ∈ N : x n ∈ V } ∈ p for every neighbourhood V of x in G. In particular, G is selectively pseudocompact (strongly pseudocompact) but not selectively sequentially pseudocompact. This answers a question of Dorantes-Aldama and the first listed author. The group G above is not pseudo- ω -bounded either. Furthermore, we show that the free precompact Boolean group of a topological sum ⨁ i ∈ I X i , where each space X i is either maximal or discrete, contains no infinite separable pseudocompact subsets.


1962 ◽  
Vol 20 ◽  
pp. 105-168 ◽  
Author(s):  
Katuzi Ono

The theory of mathematical objects, developed in this work, is a trial system intended to be a prototype of set theory. It concerns, with respect to the only one primitive notion “proto-membership”, with a field of mathematical objects which we shall hereafter simply call objects, it is a very simple system, because it assumes only one axiom scheme which is formally similar to the aussonderung axiom of set theory. We shall show that in our object theory we can construct a theory of sets which is stronger than the Zermelo set-theory [1] without the axiom of choice.


2013 ◽  
Vol 23 (6) ◽  
pp. 1234-1256 ◽  
Author(s):  
THOMAS STREICHER

In a sequence of papers (Krivine 2001; Krivine 2003; Krivine 2009), J.-L. Krivine introduced his notion of classical realisability for classical second-order logic and Zermelo–Fraenkel set theory. Moreover, in more recent work (Krivine 2008), he has considered forcing constructions on top of it with the ultimate aim of providing a realisability interpretation for the axiom of choice.The aim of the current paper is to show how Krivine's classical realisability can be understood as an instance of the categorical approach to realisability as started by Martin Hyland in Hyland (1982) and described in detail in van Oosten (2008). Moreover, we will give an intuitive explanation of the iteration of realisability as described in Krivine (2008).


1972 ◽  
Vol 37 (3) ◽  
pp. 569-571
Author(s):  
Andreas Blass

The method of inner models, used by Gödel to prove the (relative) consistency of the axiom of choice and the generalized continuum hypothesis [2], cannot be used to prove the (relative) consistency of any statement which contradicts the axiom of constructibility (V = L). A more precise statement of this well-known fact is:(*)For any formula θ(x) of the language of ZF, there is an axiom α of the theory ZF + V ≠ L such that the relativization α(θ) is not a theorem of ZF.On p. 108 of [1], Cohen gives a proof of (*) in ZF assuming the existence of a standard model of ZF, and he indicates that this assumption can be avoided. However, (*) is not a theorem of ZF (unless ZF is inconsistent), because (*) trivially implies the consistency of ZF. What assumptions are needed to prove (*)? We know that the existence of a standard model implies (*) which, in turn, implies the consistency of ZF. Is either implication reversible?From our main result, it will follow that, if the converse of the first implication is provable in ZF, then ZF has no standard model, and if the converse of the second implication is provable in ZF, then so is the inconsistency of ZF. Thus, it is quite improbable that either converse is provable in ZF.


Sign in / Sign up

Export Citation Format

Share Document