The generalised continuum hypothesis implies the axiom of choice in Coq

2021 ◽  
Author(s):  
Dominik Kirst ◽  
Felix Rech
Keyword(s):  
Continuum Hypothesis ◽  
Axiom Of Choice ◽  
The Axiom Of Choice

On the inadequacy of inner models

1972 ◽  
Vol 37 (3) ◽  
pp. 569-571
Author(s):  
Andreas Blass
Keyword(s):  
Standard Model ◽  
Continuum Hypothesis ◽  
Axiom Of Choice ◽  
Precise Statement ◽  
Relative Consistency ◽  
Inner Models ◽  
Generalized Continuum ◽  
The Axiom Of Choice

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.

Postulates for the calculus of binary relations

1940 ◽  
Vol 5 (3) ◽  
pp. 85-97 ◽  
Author(s):  
J. C. C. McKinsey
Keyword(s):  
Continuum Hypothesis ◽  
Axiom Of Choice ◽  
Binary Relations ◽  
Prove Theorem ◽  
Alfred Tarski ◽  
Cardinal Numbers ◽  
System A ◽  
Mathematical System ◽  
Generalized Continuum ◽  
The Axiom Of Choice

The theory of relations was discussed, along with the theory of classes, by Peirce and Schröder. While the calculus of classes has subsequently been presented (by Couturat, and by Huntington) as an abstract mathematical system, no similar formulation has been published of the calculus of relations. Professor Alfred Tarski has proposed to me, the problem of developing a similar formulation for the theory of relations. In this paper I present a set of postulates for the calculus of relations.The postulates have been chosen so as to enable us to prove Theorem A, below, which asserts a kind of completeness of the system. A set of postulates is called semi-categorical, if every two realizations which involve the same number of elements are isomorphic. From Theorem A one can easily prove that my postulates are semi-categorical, if one assumes the following theorem from Mengenlehre: if α and β are cardinal numbers such that , then α=β. This theorem has not been proved, however, except on the assumption of the axiom of choice and the generalized continuum hypothesis, and is not assumed in the present paper.It should be pointed out, that the sort of completeness I have chosen is not the only sort, or even necessarily the most interesting sort, of completeness which a set of postulates for the calculus of relations could possess. For example, the question arises, whether it would be possible to find a set of postulates from which all true equations (involving free variables and the operations used by Schröder) could be derived, and which was the weakest possible such set. The present work should therefore be regarded only as a first step in the investigation of the axiomatization of the calculus of relations.

Inner models for set theory—Part I

1951 ◽  
Vol 16 (3) ◽  
pp. 161-190 ◽  
Author(s):  
J. C. Shepherdson
Keyword(s):  
Set Theory ◽  
Continuum Hypothesis ◽  
Large Family ◽  
Axiom System ◽  
Axiom Of Choice ◽  
Axiomatic System ◽  
Additional Hypothesis ◽  
Inner Models ◽  
Inner Model ◽  
The Axiom Of Choice

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.

Sign in / Sign up

Export Citation Format

Share Document