Typical ambiguity and the axiom of choice

1984 ◽  
Vol 49 (4) ◽  
pp. 1074-1078 ◽  
Author(s):  
Marcel Crabbé

E. Specker has proved that the axiom of choice (AC) is false in NF [6]. Since AC is stratified, one can, according to another famous result of Specker [7], prove directly ¬AC in type theory (TT) plus some finite set of ambiguity axioms, i.e. sentences of the form φ ↔ φ+, where φ+ results from φ by adding one to its type indices.We shall in §2 of this paper give a disproof of AC directly in TT plus some axioms of ambiguity. The argument will be split into two parts. The first one (contained in Proposition 2) concerns cardinal arithmetic and has nothing to do with typical ambiguity. Though carried out in TT, it could have been done in other set theories such as Zermelo's Z or ZF. The second part is an application of this to the cardinals of the universes at different types. This is made possible through the introduction of an appropriate definition of 2α in §1 enabling one to express shifting sentences as “typed properties” of the universe, in Boffa's sense. The disproof of AC is then completed in TT plus two extra ambiguity axioms. In §3, we show that this is in a sense the best possible result: that means that every single ambiguity axiom is consistent with TT plus AC, thus giving a positive solution to a conjecture of Specker [7, p. 119].

1997 ◽  
Vol 62 (4) ◽  
pp. 1315-1332 ◽  
Author(s):  
Sara Negri ◽  
Silvio Valentini

In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology, using ideas from Coquand's proof in [7]. To deal with pointfree topology Coquand uses Johnstone's coverages. Because of the representation theorem in [3], from a mathematical viewpoint these structures are equivalent to formal topologies but there is an essential difference also. Namely, formal topologies have been developed within Martin Löf's constructive type theory (cf. [16]), which thus gives a direct way of formalizing them (cf. [4]).The most important aspect of our proof is that it is based on an inductive definition of the topological product of formal topologies. This fact allows us to transform Coquand's proof into a proof by structural induction on the last rule applied in a derivation of a cover. The inductive generation of a cover, together with a modification of the inductive property proposed by Coquand, makes it possible to formulate our proof of Tychonoff s theorem in constructive type theory. There is thus a clear difference to earlier localic proofs of Tychonoff's theorem known in the literature (cf. [9, 10, 12, 14, 27]). Indeed we not only avoid to use the axiom of choice, but reach constructiveness in a very strong sense. Namely, our proof of Tychonoff's theorem supplies an algorithm which, given a cover of the product space, computes a finite subcover, provided that there exists a similar algorithm for each component space.


1999 ◽  
Vol 64 (4) ◽  
pp. 1591-1594 ◽  
Author(s):  
Akira Suzuki

In 1970, Kenneth Kunen showed that there is no non-trivial elementary embedding of the universe V into itself [2] using the axiom of choice. Kunen remarked in his paper that the result can be formalized in Morse-Kelley theory of sets and classes. In this paper, we will work within ZF, Zermelo-Fraenkel axioms, and deal with embeddings definable with a formula and a parameter.In ZF, a “class” is usually synonymous with “property”, that is a class definable with a parameter, C = {x: φ(x,p)}, where φ is a formula in the language [∈}. Using this convention, let j be a class. Then “j is an elementary embedding of V into V” is not a single statement but a schema of statements “j preserves ψ” for each formula ψ. We prove that this schema is expressible in the language {∈} by a single formula:Lemma. An embedding j: V → V is elementary iff j preservesψ.Here ψ(α, ψ, a) is the property “a is an ordinal, φ is a formula and Vα.”The lemma is of course a schema of lemmas, one for each formula denning j and for each ψ to be preserved.Using this we prove our theorem in ZF (again, a schema of theorems.):Theorem 1.1. There is no nontrivial definable elementary embedding j: V → V.Many symbols and their definitions follow those used by Drake's book [1]. The formula Sat expresses the satisfaction relation . The formula Fmla(u) expresses that u is the Gödel-set for a formula.


Author(s):  
Asaf Karagila ◽  
Philipp Schlicht

Cohen’s first model is a model of Zermelo–Fraenkel set theory in which there is a Dedekind-finite set of real numbers, and it is perhaps the most famous model where the Axiom of Choice fails. We force over this model to add a function from this Dedekind-finite set to some infinite ordinal κ . In the case that we force the function to be injective, it turns out that the resulting model is the same as adding κ Cohen reals to the ground model, and that we have just added an enumeration of the canonical Dedekind-finite set. In the case where the function is merely surjective it turns out that we do not add any reals, sets of ordinals, or collapse any Dedekind-finite sets. This motivates the question if there is any combinatorial condition on a Dedekind-finite set A which characterises when a forcing will preserve its Dedekind-finiteness or not add new sets of ordinals. We answer this question in the case of ‘Adding a Cohen subset’ by presenting a varied list of conditions each equivalent to the preservation of Dedekind-finiteness. For example, 2 A is extremally disconnected, or [ A ] < ω is Dedekind-finite.


1975 ◽  
Vol 19 (1) ◽  
pp. 35-46 ◽  
Author(s):  
G. P. Monro

A Dedekind-finite set is one not equinumerous with any of its proper subsets; it is well known that the axiom of choice implies that all such sets are finite. In this paper we show that in the absence of the axiom of choice it is possible to construct Dedekind-finite sets which are large, in the sense that they can be mapped onto large ordinals; we extend the result to proper classes. It is also shown that the axiom of choice for countable sets is not implied by the assumption that all Dedekind-finite sets are finite.


Author(s):  
John P. Burgess

the ‘universe’ of constructible sets was introduced by Kurt Gödel in order to prove the consistency of the axiom of choice (AC) and the continuum hypothesis (CH) with the basic (ZF) axioms of set theory. The hypothesis that all sets are constructible is the axiom of constructibility (V = L). Gödel showed that if ZF is consistent, then ZF + V = L is consistent, and that AC and CH are provable in ZF + V = L.


2017 ◽  
Vol 57 (5-6) ◽  
pp. 607-616 ◽  
Author(s):  
Jan Mycielski ◽  
Grzegorz Tomkowicz

Author(s):  
Simon Boulier ◽  
Nicolas Tabareau

Abstract Model categories constitute the major context for doing homotopy theory. More recently, homotopy type theory (HoTT) has been introduced as a context for doing syntactic homotopy theory. In this paper, we show that a slight generalization of HoTT, called interval type theory (⫿TT), allows to define a model structure on the universe of all types, which, through the model interpretation, corresponds to defining a model structure on the category of cubical sets. This work generalizes previous works of Gambino, Garner, and Lumsdaine from the universe of fibrant types to the universe of all types. Our definition of ⫿TT comes from the work of Orton and Pitts to define a syntactic approximation of the internal language of the category of cubical sets. In this paper, we extend the work of Orton and Pitts by introducing the notion of degenerate fibrancy, which allows to define a fibrant replacement, at the heart of the model structure on the universe of all types. All our definitions and propositions have been formalized using the Coq proof assistant.


1989 ◽  
Vol 21 (62) ◽  
pp. 55-66
Author(s):  
José Alfredo Amor

The so called Generalized Continuum Hypothesis (GCH) is the sentence: "If A is an infinile set whose cardinal number is K and 2K denotes the cardinal number of the set P(A) of subsets of A (the power set of A), and K + denotes the succesor cardinal of K, then 2K = K +". The Continuum Hypothesis (CH) asserts the particular case K = o. It is clear that GCH implies CH. Another equivalent version of GCH, is the sentence: 'Any subset of the set of subsets of a given infinite set is or of cardinality less or equal than the cardinality of the given set, or of the cardinality of all the set of subsets". Gödel in 1939, and Cohen in 1963, settled the relative consistency of the Axiom of Choice (AC) and of its negation not-AC, respectively, with respecllo the Zermelo-Fraenkel set theory (ZF). On the other hand, Gödel in 1939, and Cohen in 1963 settled too, the relative consistency of GCH , CH and of its negations not-GCH, not-CH, respectively, with respect to the Zermelo-Fraenkel set theory with the Axiom of Choice (ZF + AC or ZFC). From these results we know that GCH and AC are undecidable sentences in ZF set theory and indeed, the most famous undecidable sentences in ZF; but, which is the relation between them? From the above results, in the theory ZF + AC is not demonstrated GCH; it is clear then that AC doesn't imply GCH in ZF theory, Bul does GCH implies AC in ZF theory? The answer is yes! or equivalently, there is no model of ZF +GCH + not-AC. A very easy proof can be given if we have an adecuate definition of cardinal number of a set, that doesn't depend of AC but depending from the Regularity Axiom, which asserls that aIl sets have a range, which is an ordinal number associated with its constructive complexity. We define the cardinal number of A, denoted |A|, as foIlows: |A|= { The least ordinal number equipotent with A, if A is well orderable The set of all sets equipotent with A and of minimum range, in other case. It is clear that without AC, may be not ordinal cardinals and all cardinals are ordinal cardinals if all sets are well orderable (AC). Now we formulate: GCH*: For all ordinal cardinal I<, 2K = I< + In the paper is demonstrated that this formulation GCH* is implied by the traditional one, and indeed equivalent to it. Lemma, The power set of any well orderable set is well orderable if and only if AC. This is one of the many equivalents of AC in ZF,due lo Rubin, 1960. Proposition. In ZF is a theorem: GCH* implies AC. Supose GCH*. Let A be a well orderable set; then |A| = K an ordinal cardinal, so A is equipotent with K and then P~A) is equipotent with P(K); therefore |P(A)I|= |P(K)| = 2K = K+. But then |P(A)|= K+ and P(A) 'is equipotent with K+ and K+ is an ordinal cardinal; therefore P(A) is well orderable with the well order induced by means of the bijection, from the well order of K+. Corolary: In ZF are theorems: GCH impIies AC and GCH is equivalent to GCH*. We see from this proof, that GCH asserts that the cardinal number of the power set of a well orderable set A is an ordinal, which is equivalent to AC, but GCH asserts also that that ordinal cardinal is |A|+ , the ordinal cardinal succesor of the ordinal cardinal of the well orderable set A.


Sign in / Sign up

Export Citation Format

Share Document