# Talk:General set theory

WikiProject Mathematics (Rated Start-class, Low-priority)
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
 Start Class
 Low Priority
Field: Foundations, logic, and set theory

## existential axioms

Maybe it's just me, but i think the axiom of separation assures the existence of the empty set *if a set already exists*. None of these axioms assures the existence of any set, since their first quantifier is universal, so they suppose a set already exists. It must be just me anyway, because i can't imagine that GST would be mentinned if it really had the flaw of reasoning on entities while being unable to prove their existence... i'm still puzzled, though. Spiritofhere 09:54, 10 August 2007 (UTC)

I am not familiar with Boolos' work, but it is common to take ${\displaystyle \exists x(x=x)}$ as an axiom of logic. Perhaps that is the case here. — Carl (CBM · talk) 13:00, 10 August 2007 (UTC)
Separation assures the existence of an empty set in GST in the same way that existence is assured in ZF. Just let φ(x) be always false. Starting from the empty set, Adjunction assures the existence, by elementary recursion, of the sets needed for von Neumann's ordinals and Peano arithmetic.
When nonempty domain is not a pre-assumption, Separation alone cannot assert the existence of the empty set directly. The articles "Axiom of empty set" and "Zermelo–Fraenkel set theory" give detailed account on this aspect. I prefer to spell it out as a non-logical axiom as I cannot verify that it is common to take the existential sentence take ${\displaystyle \exists x(x=x)}$ as an axiom. Quite the contrary, a number of proof systems, e.g., Hilbert-style, Tait-style and sequent calculi, take the universal counterpart, i.e., ${\displaystyle \forall x(x=x)}$ or the related quantifier-free formula ${\displaystyle x=x}$ as an axiom (of equality). Taking non-empty domain assumption as done in this article is also acceptable to me.Tomlee2060 (talk) 15:20, 12 November 2010 (UTC)
${\displaystyle \exists x(x=x)}$ is usually not taken directly as an axiom, but it is certainly provable in usual formalisms of first-order logic. (I'm sure that's what Carl meant.) For example, in sequent calculus:
${\displaystyle {\frac {\longrightarrow x=x\qquad }{\longrightarrow \exists x\,(x=x)}}}$
The first line is an axiom of equality, the second line is an ${\displaystyle \exists }$-right inference.—Emil J. 15:35, 12 November 2010 (UTC)
Thanks again Emil J. Your explanation makes me clear about a subtle but important property of many proof cacluli. Many of them pre-assume a non-empty domain, i.e., ${\displaystyle \forall x\varphi (x)\vdash \exists x\varphi (x)}$. If the empty domain is under consideration, it is better not to use a calculus with such a pre-assumption. Back to the question by Spiritofhere, I would like to summarize my understanding as follow:
In this article, non-empty domain is preassumed (and stated in the discussion section). Thus set existence is asserted! Additional existential axiom is not needed with such a pre-assumption. One way to formalize such a pre-assumption is by choosing a suitable proof system, e.g., sequent calculus chosen by Emil J.
Tomlee2060 (talk) 06:36, 15 November 2010 (UTC)
Carl, what you call an axiom of logic strikes me as an assertion that the domain is nonempty. No problem in this corner, as the logic of empty domains ("free" logic) has always struck me as vacuous, pedantic, and uninteresting. Your assumption is part of the bare minimum needed to get mathematics up and running.202.36.179.65 06:53, 15 September 2007 (UTC)

## Third existential quantifier

The article said that there were only two existential quantifiers in the three axioms. This is incorrect. The property φ may contain some existential quantifiers. Furthermore, the axiom of extensionality

${\displaystyle \forall x\forall y[\forall z[z\in x\leftrightarrow z\in y]\rightarrow x=y]\,}$

contains an existential quantifier because it is logically equivalent to

${\displaystyle \forall x\forall y[x\neq y\rightarrow \exists z([z\in x\land z\notin y]\lor [z\notin x\land z\in y])]\,.}$

JRSpriggs (talk) 02:08, 4 June 2009 (UTC)

It's patently absurd to count quantifiers when neither theory can be finitely axiomatized. Both GST and ZF use and require infinitely many quantifiers, not two, three, seven, or what have you. — Emil J. 10:27, 4 June 2009 (UTC)
And even if they could be counted, what one would probably be interested in is the depth of quantifier alternation, not the mere number of quantifiers. I have a vague sense that counting existential quantifiers in this way is a Boolos-ism. I have seen other articles where editors, not aware that Boolos was writing in a abbreviated way, misinterpreted what he was saying. Maybe that is the case here. — Carl (CBM · talk) 11:44, 4 June 2009 (UTC)
To EmilJ: Thank you for fixing many errors in this article. JRSpriggs (talk) 08:58, 5 June 2009 (UTC)

## Problem with the successor function

The article discusses the successor function ${\displaystyle S(x)=x\cup \{x\}}$. However, I didn't understand why "Adjunction implies that if ${\displaystyle x}$ is a set, so is ${\displaystyle S(x)}$...". To use Adjunction, we need to assert that ${\displaystyle \{x\}}$ is a set. In ZFC, Pairing and Separation assert that. In GST, we don't have Pairing. None of the 3 axioms does that. What did I miss? Tomlee2060 (talk) 15:46, 12 November 2010 (UTC)

You apparently misunderstand the adjunction axiom. It says that for any sets x and y, ${\displaystyle x\cup \{y\}}$ is also a set. Specialize with x = y to get the successor of x.—Emil J. 11:28, 13 November 2010 (UTC)
Thanks. Indeed, I misread the Axiom. —Tomlee2060 (talk) 04:06, 15 November 2010 (UTC)