Talk:General 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 $\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 $\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., $\forall x(x=x)$ or the related quantifier-free formula $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)

$\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:

${\frac {\longrightarrow x=x\qquad }{\longrightarrow \exists x\,(x=x)}}$

The first line is an axiom of equality, the second line is an $\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., $\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

$\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

$\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 $S(x)=x\cup \{x\}$. However, I didn't understand why "Adjunction implies that if $x$ is a set, so is $S(x)$...". To use Adjunction, we need to assert that $\{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, $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)

Peano arithmetic

GST does not seem to include any induction- or foundation-like axiom (scheme), how does it interpret Peano Arithmetic? 2003:C5:8F16:A154:4970:6F4A:E249:2A4E (talk) 18:32, 9 September 2020 (UTC)

ST

In the Peano Arithmetic section:

The most remarkable fact about ST (and hence GST), is that these tiny fragments of set theory give rise to such rich metamathematics. While ST is a small fragment of the well-known canonical set theories ZFC and NBG, ST interprets Robinson arithmetic (Q), so that ST inherits the nontrivial metamathematics of Q. For example, ST is essentially undecidable because Q is, and every consistent theory whose theorems include the ST axioms is also essentially undecidable.[2] This includes GST and every axiomatic set theory worth thinking about, assuming these are consistent. In fact, the undecidability of ST implies the undecidability of first-order logic with a single binary predicate letter.

There is no mention of ST anywhere before this in the article. Maybe ST is Burgess's equivalent of Tarski's S', mentioned later in the article as "GST with Empty Set replacing the axiom schema of specification"? But if so, it needs to be mentioned earlier. Especially if so much of this article is going to be about the surprising power of ST, rather than that of GST. And of course there needs to be some justification, or at least mention, of the fact that anything that can be done with ST can still be done if you replace empty set with the axiom schema of separation, not just left for people to guess.

Because I'm only _guessing_ that this is what ST refers to, I don't want to edit the article in a possibly incorrect way; someone who actually knows what's intended needs to fix it. --157.131.154.133 (talk) 03:32, 22 December 2020 (UTC)