scholarly journals Grothendieck Universes

2020 ◽  
Vol 28 (2) ◽  
pp. 211-215
Author(s):  
Karol Pąk

Summary The foundation of the Mizar Mathematical Library [2], is first-order Tarski-Grothendieck set theory. However, the foundation explicitly refers only to Tarski’s Axiom A, which states that for every set X there is a Tarski universe U such that X ∈ U. In this article, we prove, using the Mizar [3] formalism, that the Grothendieck name is justified. We show the relationship between Tarski and Grothendieck universe. First we prove in Theorem (17) that every Grothendieck universe satisfies Tarski’s Axiom A. Then in Theorem (18) we prove that every Grothendieck universe that contains a given set X, even the least (with respect to inclusion) denoted by GrothendieckUniverseX, has as a subset the least (with respect to inclusion) Tarski universe that contains X, denoted by the Tarski-ClassX. Since Tarski universes, as opposed to Grothendieck universes [5], might not be transitive (called epsilon-transitive in the Mizar Mathematical Library [1]) we focused our attention to demonstrate that Tarski-Class X ⊊ GrothendieckUniverse X for some X. Then we show in Theorem (19) that Tarski-ClassX where X is the singleton of any infinite set is a proper subset of GrothendieckUniverseX. Finally we show that Tarski-Class X = GrothendieckUniverse X holds under the assumption that X is a transitive set. The formalisation is an extension of the formalisation used in [4].

Author(s):  
John P. Burgess

In the late nineteenth century, Georg Cantor created mathematical theories, first of sets or aggregates of real numbers (or linear points), and later of sets or aggregates of arbitrary elements. The relationship of element a to set A is written a∈A; it is to be distinguished from the relationship of subset B to set A, which holds if every element of B is also an element of A, and which is written B⊆A. Cantor is most famous for his theory of transfinite cardinals, or numbers of elements in infinite sets. A subset of an infinite set may have the same number of elements as the set itself, and Cantor proved that the sets of natural and rational numbers have the same number of elements, which he called ℵ0; also that the sets of real and complex numbers have the same number of elements, which he called c. Cantor proved ℵ0 to be less than c. He conjectured that no set has a number of elements strictly between these two. In the early twentieth century, in response to criticism of set theory, Ernst Zermelo undertook its axiomatization; and, with amendments by Abraham Fraenkel, his have been the accepted axioms ever since. These axioms help distinguish the notion of a set, which is too basic to admit of informative definition, from other notions of a one made up of many that have been considered in logic and philosophy. Properties having exactly the same particulars as instances need not be identical, whereas sets having exactly the same elements are identical by the axiom of extensionality. Hence for any condition Φ there is at most one set {x|Φ(x)} whose elements are all and only those x such that Φ(x) holds, and {x|Φ(x)}={x|Ψ(x)} if and only if conditions Φ and Ψ hold of exactly the same x. It cannot consistently be assumed that {x|Φ(x)} exists for every condition Φ. Inversely, the existence of a set is not assumed to depend on the possibility of defining it by some condition Φ as {x|Φ(x)}. One set x0 may be an element of another set x1 which is an element of x2 and so on, x0∈x1∈x2∈…, but the reverse situation, …∈y2∈y1∈y0, may not occur, by the axiom of foundation. It follows that no set is an element of itself and that there can be no universal set y={x|x=x}. Whereas a part of a part of a whole is a part of that whole, an element of an element of a set need not be an element of that set. Modern mathematics has been greatly influenced by set theory, and philosophies rejecting the latter must therefore reject much of the former. Many set-theoretic notations and terminologies are encountered even outside mathematics, as in parts of philosophy: pair {a,b} {x|x=a or x=b} singleton {a} {x|x=a} empty set ∅ {x|x≠x} union ∪X {a|a∈A for some A∈X} binary union A∪B {a|a∈A or a∈B} intersection ∩X {a|a∈A for all A∈X} binary intersection A∩B {a|a∈A and a∈B} difference A−B {a|a∈A and not a∈B} complement A−B power set ℘(A) {B|B⊆A} (In contexts where only subsets of A are being considered, A-B may be written -B and called the complement of B.) While the accepted axioms suffice as a basis for the development not only of set theory itself, but of modern mathematics generally, they leave some questions about transfinite cardinals unanswered. The status of such questions remains a topic of logical research and philosophical controversy.


2016 ◽  
Vol 95 (2) ◽  
pp. 177-182 ◽  
Author(s):  
NATTAPON SONPANOW ◽  
PIMPEN VEJJAJIVA

Forster [‘Finite-to-one maps’, J. Symbolic Logic68 (2003), 1251–1253] showed, in Zermelo–Fraenkel set theory, that if there is a finite-to-one map from ${\mathcal{P}}(A)$, the set of all subsets of a set $A$, onto $A$, then $A$ must be finite. If we assume the axiom of choice (AC), the cardinalities of ${\mathcal{P}}(A)$ and the set $S(A)$ of permutations on $A$ are equal for any infinite set $A$. In the absence of AC, we cannot make any conclusion about the relationship between the two cardinalities for an arbitrary infinite set. In this paper, we give a condition that makes Forster’s theorem, with ${\mathcal{P}}(A)$ replaced by $S(A)$, provable without AC.


2019 ◽  
Vol 13 (3) ◽  
pp. 541-592
Author(s):  
WALTER DEAN

AbstractThis paper explores the relationship borne by the traditional paradoxes of set theory and semantics to formal incompleteness phenomena. A central tool is the application of the Arithmetized Completeness Theorem to systems of second-order arithmetic and set theory in which various “paradoxical notions” for first-order languages can be formalized. I will first discuss the setting in which this result was originally presented by Hilbert & Bernays (1939) and also how it was later adapted by Kreisel (1950) and Wang (1955) in order to obtain formal undecidability results. A generalization of this method will then be presented whereby Russell’s paradox, a variant of Mirimanoff’s paradox, the Liar, and the Grelling–Nelson paradox may be uniformly transformed into incompleteness theorems. Some additional observations are then framed relating these results to the unification of the set theoretic and semantic paradoxes, the intensionality of arithmetization (in the sense of Feferman, 1960), and axiomatic theories of truth.


2001 ◽  
Vol 7 (2) ◽  
pp. 237-261 ◽  
Author(s):  
Lorenz Halbeisen ◽  
Saharon Shelah

AbstractIf we assume the axiom of choice, then every two cardinal numbers are comparable. In the absence of the axiom of choice, this is no longer so. For a few cardinalities related to an arbitrary infinite set, we will give all the possible relationships between them, where possible means that the relationship is consistent with the axioms of set theory. Further we investigate the relationships between some other cardinal numbers in specific permutation models and give some results provable without using the axiom of choice.


1997 ◽  
Vol 36 (04/05) ◽  
pp. 315-318 ◽  
Author(s):  
K. Momose ◽  
K. Komiya ◽  
A. Uchiyama

Abstract:The relationship between chromatically modulated stimuli and visual evoked potentials (VEPs) was considered. VEPs of normal subjects elicited by chromatically modulated stimuli were measured under several color adaptations, and their binary kernels were estimated. Up to the second-order, binary kernels obtained from VEPs were so characteristic that the VEP-chromatic modulation system showed second-order nonlinearity. First-order binary kernels depended on the color of the stimulus and adaptation, whereas second-order kernels showed almost no difference. This result indicates that the waveforms of first-order binary kernels reflect perceived color (hue). This supports the suggestion that kernels of VEPs include color responses, and could be used as a probe with which to examine the color visual system.


Author(s):  
Tim Button ◽  
Sean Walsh

In this chapter, the focus shifts from numbers to sets. Again, no first-order set theory can hope to get anywhere near categoricity, but Zermelo famously proved the quasi-categoricity of second-order set theory. As in the previous chapter, we must ask who is entitled to invoke full second-order logic. That question is as subtle as before, and raises the same problem for moderate modelists. However, the quasi-categorical nature of Zermelo's Theorem gives rise to some specific questions concerning the aims of axiomatic set theories. Given the status of Zermelo's Theorem in the philosophy of set theory, we include a stand-alone proof of this theorem. We also prove a similar quasi-categoricity for Scott-Potter set theory, a theory which axiomatises the idea of an arbitrary stage of the iterative hierarchy.


Author(s):  
Tim Lyon

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.


1991 ◽  
Vol 15 (2) ◽  
pp. 123-138
Author(s):  
Joachim Biskup ◽  
Bernhard Convent

In this paper the relationship between dependency theory and first-order logic is explored in order to show how relational chase procedures (i.e., algorithms to decide inference problems for dependencies) can be interpreted as clever implementations of well known refutation procedures of first-order logic with resolution and paramodulation. On the one hand this alternative interpretation provides a deeper insight into the theoretical foundations of chase procedures, whereas on the other hand it makes available an already well established theory with a great amount of known results and techniques to be used for further investigations of the inference problem for dependencies. Our presentation is a detailed and careful elaboration of an idea formerly outlined by Grant and Jacobs which up to now seems to be disregarded by the database community although it definitely deserves more attention.


2007 ◽  
Vol 72 (1) ◽  
pp. 119-122 ◽  
Author(s):  
Ehud Hrushovski ◽  
Ya'acov Peterzil

AbstractWe use a new construction of an o-minimal structure, due to Lipshitz and Robinson, to answer a question of van den Dries regarding the relationship between arbitrary o-minimal expansions of real closed fields and structures over the real numbers. We write a first order sentence which is true in the Lipshitz-Robinson structure but fails in any possible interpretation over the field of real numbers.


1982 ◽  
Vol 47 (2) ◽  
pp. 423-435 ◽  
Author(s):  
James H. Schmerl ◽  
Stephen G. Simpson

The purpose of this paper is to study a formal system PA(Q2) of first order Peano arithmetic, PA, augmented by a Ramsey quantifier Q2 which binds two free variables. The intended meaning of Q2xx′φ(x, x′) is that there exists an infinite set X of natural numbers such that φ(a, a′) holds for all a, a′ Є X such that a ≠ a′. Such an X is called a witness set for Q2xx′φ(x, x′). Our results would not be affected by the addition of further Ramsey quantifiers Q3, Q4, …, Here of course the intended meaning of Qkx1 … xkφ(x1,…xk) is that there exists an infinite set X such that φ(a1…, ak) holds for all k-element subsets {a1, … ak} of X.Ramsey quantifiers were first introduced in a general model theoretic setting by Magidor and Malitz [13]. The system PA{Q2), or rather, a system essentially equivalent to it, was first defined and studied by Macintyre [12]. Some of Macintyre's results were obtained independently by Morgenstern [15]. The present paper is essentially self-contained, but all of our results have been directly inspired by those of Macintyre [12].After some preliminaries in §1, we begin in §2 by giving a new completeness proof for PA(Q2). A by-product of our proof is that for every regular uncountable cardinal k, every consistent extension of PA(Q2) has a k-like model in which all classes are definable. (By a class we mean a subset of the universe of the model, every initial segment of which is finite in the sense of the model.)


Sign in / Sign up

Export Citation Format

Share Document