Thread: Assumptions of Set Theory

Hello again math forumites. I have returned with yet another exciting, yet possibly poorly-worded set theory question.

I have been trying in my spare time to develop a solid understanding of the essential basics of logic and set theory. I've had a small amount of graduate coursework in set theory (my field is computer science), but most of my math work is autodidactic. Eventually, I want to understand the concepts well enough that I could instruct others. I think it was Einstein who said something like: you never truly understand something until you can explain it to a child of six. Or maybe that's a misquote. Anyway, here's my question...

What are the minimal assumptions necessary in order to construct and assess the consistency (as best as one possibly can) of the majority of mathematics? AFAIK, the only two foundational bases for math are set theory and topoi theory, and I'm much more familiar with set theory, so I'll start there. Here's what I know we need:

1) One undefinable concept/object (set)
2) One undefinable binary predicate (membership)
3) Five axioms (extensionality, pairing, union, power set, induction)
4) One axiom schema (separation)

With the exception of logic theory (which is my the crux of my question, below), the above covers pretty much everything in "normal" math. You can strengthen these by adding choice, make metatheory simpler by adding regularity, and improve the schema of separation to the stronger version (replacement) to make some proofs simpler and to allow investigation into large cardinal theory; but these are not needed for the founding of most of applied mathematics.

Anyway, the one thing I left out above is logic theory...and this is where things get confusing. Numerous references, including Friedman, who I was lucky enough to have as an instructor in one case, and books I have read, have commented that the "bootstrapping" (something I actually understand well) between logic and set theory is not an argument of circular reasoning. The basic description seems to run like this:

A) You start with intuitive logic.
B) From this you can describe proofs in set theory, and show how set theory implies the existence of things that can be used to model objects like functions.
C) Since set theory is strong enough to model the discrete math of logic, you can prove things about formal logic by using set theory and those intuitive logical principles. This gives us a more "formal" logic.
D) Today we describe set theory itself by using this formal logic.

Therefore, we don't have a logic --> set theory --> logic circle. It's more of, informal logic --> set theory --> formalization of logic, I guess.

Now, I can buy the fact that just because we write the axioms of set theory in first-order logic (FOL) does not imply that FOL need "come first". I mean, if I write the axioms in English, that doesn't mean English is needed for the axioms; it's just the language I'm using to communicate.

What I can't shake is the suspicion that some level of intuitionistic logic must be combined with set theory before one can prove anything at all, and thus, there are additional assumptions being made in addition to 1-4 above. I have not seen these assumptions spelled out anywhere, probably because most mathematicians don't really care when this starts drifting into epistemological stuff.

For example, it seems rather clear to me that one needs to assume, in addition to 1-4 above, the validity of a logical inference rule like modus ponens. Is this true?

If so, what else must we assume about logic before we can describe mathematics with set theory (and by its inclusion, formal logic itself)?

If not, why not? I mean, it seems like one could come up with a faulty inference rule which is capable of asserting its own existence, which would mean 1-4 are not a complete set of assumptions (unless maybe there is some consistency measure that determines which inference rules are or are not faulty)?

(Note: I know much of the lingo above uses "model", "truth", etc. in a loose and probable highly-irregular manner, but keep in mind I'm talking about assumptions of informal logic needed to jump-start set theory into proving things about formal logic.)

Thanks in advance!

Anna

Originally Posted by Annatala

What are the minimal assumptions necessary in order to construct and assess the consistency (as best as one possibly can) of the majority of mathematics?

That's a pretty vague question, since it's not clear what you mean by 'construct and assess' and 'majority of mathematics'.

I'm simplyfing a good amount here, but some basic set theory is the most usual axiomatization for the basic mathematics of real analysis, topology, abstract algebra, graph theory, number theory, et al. (Z set theory plus the axiom of dependent choice is more than enough (more than enough since we don't need the axiom of regularity).)

But by Godel's second incompleteness theorem, (assuming that Z set theory is consistent, which assumption I'll take as tacit generally) there is no proof of the consistency of Z set theory in Z set theory, thus, perforce in no theory weaker than Z set theory. Especially, there is no finitistic proof of the consistency of even a basic number theory such as Peano arithmetic (not even of even weaker Robinson arithmetic).

Originally Posted by Annatala

AFAIK, the only two foundational bases for math are set theory and topoi theory

There are lots of other approaches, but you're right that set theory is the most usual approach.

Originally Posted by Annatala

undefinable concept/object (set)

In the formal theory, we don't need to take 'set' as a primitive.

To your questions that follow: I basically agree with the outline you mentioned: informal logic->formal math->formal logic. (Or it could be informal math->formal logic->formal math if we like. Or an infinite escalation going up to formalizations of meta-theories (but then we observe that each escalation is just a clone of the previous escalation, etc.).) And I agree that at each informal stage above a formal stage, we take certain principles as given, such as modus ponens.

No matter what we do, unless we begin the whole process in an unexplained formal language, we will use certain principles informally to explain or stipulate our formalizations.

As to the extent of our informal assumptions, it seems to me that pretty much an informal version of first order logic is itself assumed. (For merely stating a formalization of the language and axioms of a formal theory like a formal set theory, I think informal versions of the principles of intuitionistic first order logic suffice?). That is reasoning that includes sentential (or at least intuitionistic sentential?) logic and the principles of universal generalization and universal instantiation. Also informal versions of the principles of identity: (1) Any object equals itself, and (2) If x equals y then whatever holds for x also holds for y.

Originally Posted by MoeBlee

That's a pretty vague question, since it's not clear what you mean by 'construct and assess' and 'majority of mathematics'.

Yes, I know--but you did understand what I meant, fortunately. I guess I could have saved myself the trouble by saying "what all must you assume before you can prove things in set theory".

Originally Posted by MoeBlee

But by Godel's second incompleteness theorem, (assuming that Z set theory is consistent, which assumption I'll take as tacit generally) there is no proof of the consistency of Z set theory in Z set theory,

Of course. I meant having some way to deduce things from the theory, not prove that math is consistent (although there are subsets of math, like (R, +, x) in which the set N can't be defined, which are provably consistent).

Originally Posted by MoeBlee

In the formal theory, we don't need to take 'set' as a primitive.

Ah! Now you are the first person I have heard claim this. Every text and instructor I have asked has said that the concept of "set" is undefinable in set theory, and must be taken as an assumption. Are you suggesting the concept of set can itself be defined in set theory? How can this be possible since you need sets a priori for everything? I'd agree you can prove existence of the empty set from induction and separation, which proves at least one set exists, but this still does not define what a set is.

Originally Posted by MoeBlee

As to the extent of our informal assumptions, it seems to me that pretty much an informal version of first order logic is itself assumed. (For merely stating a formalization of the language and axioms of a formal theory like a formal set theory, I think informal versions of the principles of intuitionistic first order logic suffice?). That is reasoning that includes sentential (or at least intuitionistic sentential?) logic and the principles of universal generalization and universal instantiation. Also informal versions of the principles of identity: (1) Any object equals itself, and (2) If x equals y then whatever holds for x also holds for y.

5) Modus ponens and 6) universal instantiation, definitely. I'm not sure universal generalization is needed--can you elaborate where it is used? For 7), an undefinable concept of "statement" or "sentence" might suffice...? It seems like I would also need either a two-place logical connective, or production rules for parsing sentences, or both.

Equality I'm a little surprised by--I thought you could get far enough with proofs in set theory based solely on the other direction (extensionality) to build logic and then prove theorems of equality in logic directly.

Anna

Originally Posted by Annatala

Every text and instructor I have asked has said that the concept of "set" is undefinable in set theory, and must be taken as an assumption.

Notice that I said FORMALLY. In the FORMAL theory itself (and I'm in context of Z style set theories), there's not a primitive predicate 'is a set'; there is only the primitive predicate 'is an element of'.

Also, yes, 'is a set' can be defined in Z set theory.

thm: E!xAy ~yex
def: x=0 <-> Ay ~yex
def: x is a class <-> (x=0 or Ey yex)
def: x is a set <-> (x is a class & Ez xez)

Of course, that's trivial, not very informative, but it is a definition that works in Z set theory, and we get a desired (though trivial) theorem:

Ax x is a set

None of that contradicts that in our basic INformal notions, we may take the notion of 'set' as a given.

Originally Posted by Annatala

I'd agree you can prove existence of the empty set from induction and separation

(By 'induction' I take it you mean 'infinity'.) Separation alone (no need for infinity) proves: ExAy ~yex.

Originally Posted by Annatala

I'm not sure universal generalization is needed--can you elaborate where it is used?

I didn't have any particular instance in mind; just that reasoning by generalization is ubiquitous in mathematical discourse, even in everyday discourse.

Originally Posted by Annatala

Equality

Yes, in set theory we can define '='. But the context was not what set theoretic principles we use, but rather the context was what logical principles we use to FORMULATE set theory (math).

Anyway, I think the gist of your point seems correct: To do any reasoning, even reasoning about formalizing reasoning itself, we use some basic principles of reasoning. We may add that formalizing formal languages or formal systems itself involves also some basic principles about natural numbers.

i'd like to point out that we need not make an exhaustive catalog of what every possible set could be, in order to start using set theory. we just need to know "some things are sets". how big a "universe" you need, depends on what "stuff" you're working with. some stuff takes big universes, other stuff (like arithmetic, or finite combinatorics) can get by with a much smaller universe. much of current set theory evolved as a way to make sure stuff we had been calling sets up until then, it was ok to continue to call sets (with some famous exceptions).

in other words, knowing what a set is, and knowing something is a set, are 2 different things. i've never heard anyone give an accurate description of the former, but the latter is necessary.

i think we (functioning humans) come with hardware with generalization and instantiation "built-in", that in essence, these are "undefinable" concepts, but ones we all understand (common and specific properties of experiences).

Originally Posted by MoeBlee

Also, yes, 'is a set' can be defined in Z set theory.

I don't see how this restricts "set" to include only the abstractions which are given in the axioms. This allows both urelements and objects which are neither sets nor classes, but may contain sets or be otherwise related (or unrelated) to sets. Am I mistaken in thinking that the concept of "set" needs to be at least a vague premise in order to set the universe of discourse?

Originally Posted by MoeBlee

Separation alone (no need for infinity) proves: ExAy ~yex.

Not according to Jech, and I've seen this in at least one other place. The reason you need infinity has nothing to do with infinity's axiom per se; you need anything that says "there exists a set". Otherwise, a universe with no sets would fit the axioms (it is consistent with everything there because no other axiom of ZFC claims there exists a set independent of some other initial set or sets). This is why the axiom of the empty set exists in some other set theories.

In other words, separation by itself does not imply that any set exists. You have to first have a set before you can apply separation to produce another set. If no sets exist, then separation cannot apply to anything...it holds vacuously. The reason we don't have a "some set exists" axiom is infinity asserts the existence of at least one set.

Originally Posted by MoeBlee

Yes, in set theory we can define '='. But the context was not what set theoretic principles we use, but rather the context was what logical principles we use to FORMULATE set theory (math).

Yes, but do we need = to formulate set theory? Can't I just replace all instances of:

S = T with: ( x (x S x T))? (This should also work for definable proper classes, I think.)

Originally Posted by Deveno

i'd like to point out that we need not make an exhaustive catalog of what every possible set could be, in order to start using set theory.

I agree completely, and I'm not attempting to formalize the assumptions. I just want to have a good understanding of what they are. Since many people interested in set theory are interested in it for the "foundational" aspects it provides to mathematics, I'm surprised this is not something that is commonly delineated.

Originally Posted by Annatala

I don't see how this restricts "set" to include only the abstractions which are given in the axioms. This allows both urelements and objects which are neither sets nor classes, but may contain sets or be otherwise related (or unrelated) to sets. Am I mistaken in thinking that the concept of "set" needs to be at least a vague premise in order to set the universe of discourse?

My only point is that among the FORMAL provisions we need for set theory, taking 'is a set' as a primitive is not required. The only formal relation needed is 'is a member of'. Then a FORMAL definition of 'is a set' can be provided also. I do not argue that this formal definition is anything more than trivial or that it aids in any explication of the basic informal notion of what a set is or of what domains may serve for models of set theory.

However, IF a formal set theory that is Z style is itself used as a meta-theory (recall that all our informal model theory can be formalized in a formal meta theory) for a formal set theory, then in that formal meta-theory we also have the theorem 'Ax x is a set' and thus the elements of any domain for a model of ANY theory are all sets.

This does not preclude that one may wish to use a theory (something other than a Z style set theory) that allows urelements as the formal metatheory. In that case, the Z set theory still has the theorem 'Ax x is a set' but there are models of that theory in which the domain has more than one object that is not a set. In that case, the model doesn't map the 'e' symbol to the membership relation on the domain of the model.

Originally Posted by Annatala

Not according to Jech,

Would you please quote where Jech says that the axiom schema of separation does not prove "ExAy ~yex"? The proof is famous and easy. It's in at least a few well referenced set theory texts. You could do it yourself.

Originally Posted by Annatala

This is why the axiom of the empty set exists in some other set theories.

The empty set axiom is included in certain axiomatizations of Z style set theories for two possible reasons: (1) It is included, though redundant, because it makes the presentation easier to digest for students who are not so versed in the technicalities of first order logic that provide a proof of "ExAy ~yex" right from an instance of the separation schema, or (2) it is included, non-redundantly, in certain axiomatizations that don't have the separation schema.

Originally Posted by Annatala

In other words, separation by itself does not imply that any set exists.

My claim is exactly this:

First order logic applied to an instance of the separation schema provides a proof of "ExAy ~yex".

That is a plain fact. You could yourself easily do the proof.

Your point about proving that there exists some set to begin with is taken care of by first order logic itself, since the first order logic we use here provides both syntactically "ExP" for various valid formulas P in the language, and semantically that the domain of any model is non-empty.

There's no sense arguing against the plain fact that an instance of the separation schema proves "ExAy~yex". You can do the proof yourself, or, if you get stuck, I can type it out for you.

Originally Posted by Annatala

Yes, but do we need = to formulate set theory?

We don't need '=' as a primitive OF the formal OBJECT level set theory. However, in the META-theory (whether formal or informal) we do use the principles of equality (whether formal or informal) to formulate our object level formal set theory. Now, the same thing can be deferred to the meta-theory: Possibly equality is itself defined, not primitive, in that meta-theory. I don't dispute that either. But whether defined or primitive in the meta-theory, we will be using principles of equality in our formulation of various object theories.

Originally Posted by MoeBlee

My only point is that among the FORMAL provisions we need for set theory, taking 'is a set' as a primitive is not required.

According to Wikipedia's Object theory : A formal system:

A few axioms that are stated up front and may include "undefinable notions" (examples: "set", "element", "belonging" in set theory...).

This seems to suggest that "set" is an undefinable notion in formal set theory. Granted, this is Wikipedia and it's not sourced, but I know I've seen this same claim in a mathematical logic text (which is not useful unless I can find it). I'll look in Enderton and see.

Originally Posted by MoeBlee

Would you please quote where Jech says that the axiom schema of separation does not prove "ExAy ~yex"? The proof is famous and easy. It's in at least a few well referenced set theory texts. You could do it yourself.

Jech, Thomas. Set Theory. Third Millenium Edition, Revised, Expanded. Under Basic Set Theory, page 8:

One consequence of the Separation Axioms is that the intersection and the difference of two sets is a set, and so we can define the operations:

(definition of intersection and set difference here, omitted).

Similarly, it follows that the empty class

= {u : u u}

is a set--the empty set; this, of course only under the assumption that at least one X exists (because X):

(1.4) X (X = X).

We have not included (1.4) among the axioms, because it follows from the Axiom of Infinity.

The bolding is mine but the rationale is clear. Separation begins with a "for all sets X" quantifier. Therefore, it does not assert the existence of a set unless a set already exists. Separation asserts that if a set exists, you can apply separation with a formula to produce a new set.

This is the very problem naive set theory had, actually; application of separation in an unrestricted manner. You can't apply separation unless you have some larger set you're applying it to.

Originally Posted by MoeBlee

There's no sense arguing against the plain fact that an instance of the separation schema proves "ExAy~yex". You can do the proof yourself, or, if you get stuck, I can type it out for you.

With all due respect, I trust Jech on this, and my intuition agrees with him.

I feel like you're talking down to me a little bit here, and I would prefer to deescalate things before I upset you further, so I'm going to stop here.

The following post is long because I have generously reiterated certain points and arguments along the way.

First though, you said that I am upset. I'm not upset and the discusssion is not personal, or at least would be better not to be personal.

My indisputably correct claim is that the axiom schema of separation alone proves ExAy ~yex.

More laboriously stated:
using only the first order predicate calculus,
there is a proof of
ExAy ~yex
where the proof uses an instance of the axiom schema of separation as the only non-logical premise.

That is easily seen to be correct either by doing the simple exercise in first order logic for oneself or by taking my offer to provide a specific instance of the axiom schema of separation by which it is routine to complete the simple exercise.

And this is not a matter of appeal to authority – Jech's or anyone else's - nor to intuition, but rather a pure question of provability in the first order predicate calculus.

Moreover, in the passages you cited, Jech does NOT say that the axiom schema of separation alone does not prove ExAy ~yex nor does he say anything that implies that the axiom schema of separation alone does not prove ExAy ~yex. What Jech does say is that the axiom of infinity proves Ex x=x and that we may use that with the axiom schema of separation to prove ExAy ~yex. But that does not imply that ExAy ~yex is not provable from the axiom schema of separation alone.

Let 'I' stand for the axiom of infinity.
Let 'T' stand for Ex x=x.
Let 'M' stand for ExAy ~yex.
Let 'S' stand for AzExAy(yex <-> (yez & (yey & ~yey))).
(Note that S is an instance of the axiom schema of separation).

Jech says I -> T, and (S & T) -> M. (Thus (I & S) -> M.)
But that does NOT preclude that more simply S -> M.

This is along the lines I mentioned, authors sometimes use set theoretic axioms to prove Ex x=x, but doing that is not required, since Ex x=x is provable in logic (with identity) alone. Moreover, Ex x=x is not even needed in a derivation of ExAy ~yex from the axiom schema of separation.

Moreover, even though my indisputably correct claim should not require further reference, here are some as to various matters in this discussion:

(1) Smullyan & Fitting 'Set Theory And The Continuum Problem' pg. 18 [I changed 'x' to 'y']:

"There exists at least one empty class by P2 [P2 is their class theory version of the axiom schema of separation] since we can take any property P(y) that holds for no x at all (such as ~(y=y)) and have a class consisting of all and only those y having this property."

Smullyan & Fitting are in class theory, not set theory, and mention 'class' rather than 'set' in the above. But neither that nor the difference between the separation schema they use and the more ordinary separation schema is a crucial difference for the matter here, which is that the quote indicates the method by which to derive ExAy~yex.

Their formula P(y) is ~y=y while the P(y) I used is (yey & ~yey). In either case we have, by first order logic with identity (with Smullyan & Fitting) and in first order logic alone (by my formulation):

AzExAy(yex <-> (yez & P(y)) -> ExAy ~yex.

That is, an instance of the axiom schema of separation proves ExAy ~yex. And that is the case no matter whether the variables refer to classes, sets, pineapples, or English muffins. Moreover, it is not necessary to pass through any formula like Ex x=x here.

(2) As to the argument about whether we need first to prove that something exists or that there is a set that exists, see Kunen 'Set Theory' pg 10:

"Ex(x=x).
This axiom says that our universe is non-void. Under most developments of formal logic [ordinary first order logic, which is the logic for Z set theory], this is derivable from the logical axioms and thus redundant to state here, but we do so for emphasis."

For emphasis, and with added emphasis, I reiterate Kunen as a reiteration of what I alluded to in my earlier post: "[...] it is REDUNDANT [...] but we do so for EMPHASIS."

(Note that we don't even need identity theory, as we could use Ex(xex -> xex) or various others.)

This is just as I mentioned. The first order logic itself mandates syntactically that there exists an object. (And that goes along with the semantical stipulation that the universe of a model is non-empty.) Moreover, as such an object that exists, I’ve said that for the pure question of the derivability of ExAy ~yex from the axiom schema of separation, it doesn’t matter WHAT this object is or what KIND of object it is

Further, this is enabled by the rules of quantification. From AzQ(z) we infer Q(z). Where Q(z) is ExAy(yez <-> (yez & (yey & ~yey))) we have AzQ(z) is an instance of the axiom schema of separation:

AzExAy(yez <-> (yez & (yey & ~yey)))

thus

ExAy(yez <-> (yez & (yey & ~yey)))

from which it is routine to prove

ExAy ~yex.

The object z to which we instantiated is provided by the rule of universal instantiation.

And, again, it doesn't matter what z "is" since the ACTUAL axioms don't stipulate that z is a class or a set or anything at all. Indeed, you are incorrect when you claimed that Jech stipulates that X (z in my formulation) is specified to be a set. On the contrary, no matter what 'z' instantiates to, we STILL get

ExAy ~yex.

Moreover, Jech provides in Separation that Y (x in my formulation) is a set. Not (in Jech's formulation) is X said to be a set, as you claimed, but rather his Y. You reversed X and Y as to Jech mentioning what is a set.

Ex(x is a set & Ay(yex <-> (yez & P(y))).

Now, it's another matter whether saying that Y (x in my formulation) is a set is gratuitous, added for emphasis (or suitable for transporting the formulation to class theory where there do exist proper classes so that saying 'x is a set' is actually substantive)). But regardless of that matter, ExAy ~yex follows from Jech's formulation of the axiom schema of separation PERFORCE, since in his formulation we get Ex(x is a set & Ay ~yex), which perforce provides ExAy ~yex.


And again, a proof of ExAy ~yex from AzExAy(yex <-> (yez & (yey & ~yey))) does not need to use any formula like Ex x=x.

(3) Levy 'Basic Set Theory' pg. 20.

"None of the axioms we gave until now postulated the unconditional existence of a set. [...] However, since Ex(x=x) is a theorem of first order logic, and since our only objects here are sets, we can say that we assumed the existence of at least one set when we adopted first order logic here.

[...] Proposition (Null-set). There exists a unique set which has no members. Proof. Let z be any set (there is a set by the above arguments). Let us take for Phi(u, v) in the axiom of replacement a logically invalid formula (e.g. ~u=u), then the set y whose existence is claimed by the axiom of replacement has no members. [...]"

So Levy uses replacement where I used separation, but that's not a crucial difference here. Also, in his discussion about 'sets', recall that 'is a set' is NOT an official primitive predicate (English rendering of a predicate symbol to be pedantic) of set theory. The only official predicate is 'e' (read as 'is an element of'). Of course, certain class theories may have a primitive predicate 'is a set' (or use a 2-sorted logic for that purpose), but the question here was as to derivability in Z set theory.

So some authors mention 'set' in their formulations of the axioms and elsewhere, but this is not required for stating the axioms of Z set theory and such formulations with the word 'set' are not in the official first order language for Z set theory.

A precise formulation of the axiom schema of separation:

If P is a formula, and x is a variable that does not occur free in P, then all closures of

ExAy(yex <-> (yez & P))

are axioms.

Nowhere is 'is a set' mentioned, no matter that our PRE-formal (intuitive, intended, whatever) notion is that the above is a formula about sets.

Thus, as I've mentioned, the axiom schema of separation proves ExAy ~yex, no matter what one may take to be the meaning of the formulas or take to be the intended context of sets.

There are some other problems with your latest post, but here I wish only to drive this basic point, which you have disputed:

The axiom schema of separation proves ExAy ~yex. And again, a proof of ExAy ~yex from AzExAy(yex <-> (yez & (yey & ~yey))) does not REQUIRE we use any formula like Ex x=x. And that is not rationally disputed. Rather, it is a plain fact of the proof calculus of first order logic.

Read Levy's own admission: "we assumed the existence of at least one set when we adopted first order logic". He goes on to prove the empty set exists, and I have no quarrel with that, as I quoted the exact same thing: it is easy to show the existence of the empty set once you have at least one set. The problem here is that Levy fails to realize this assumption he makes (which is often taken as a separate axiom in systems other than ZF) is entirely unnecessary in ZF, because the existence of at least one set follows directly from Infinity.

Additionally, when I began this discussion I was trying to formulate set theory from intuitionistic logic that did not contain references to sets (not formal logic) so this assumption is not one that I made in my discussion. But again, it's irrelevant because you don't need to assume when you can prove, I'd hope you would agree.

To show this to you more explicitly, here is a model of ZFC minus Infinity. I would think this would certainly settle the argument, but given you refer to your claim as "indisputably correct", we'll see.

Our model: The universe of discourse is empty. Let's examine the axioms:

1) Extensionality is satisfied.*
2) Pairing is satisfied.*
3) Union is satisfied.*
4) Power Set is satisfied.*
5) Separation is satisfied.*
6) Regularity is satisfied.*
7) Replacement is satisfied.*
8) Choice is satisfied.*

* This axiom is satisfied because it begins with "for all..." and there are no objects in the universe of discourse, so it holds vacuously true.

Every axiom in ZFC, with the exception of Infinity, begins with a universal quantifier. They all vacuously hold in the absence of a set, because the unity of the "for all" quantifier is true (just as the unity of "there exists" is false, the unity of is 0, the unity of is 1, etc). The reason the author you quote claims "a set exists" is because he explicitly assumes it.

So I'm not sure what you're trying to argue here. I agree completely that empty set can be proven once you either prove (which you can do in ZF without assuming!) or assume the existence of at least one set. I would prefer to prove something rather than assume it, and it can be proven without resorting to assumptions. Infinity is the only axiom of ZFC that begins with an existential quantifier, and thus it asserts that at least one set exists. Thus, with Infinity, you can't have a model with no sets in it, and without Infinity, you can.

If the issue here is you believe that a universal quantifier assumes the existence of an object in the universe of discourse, which is what I suspect, you're simply not interpreting universal quantification correctly. Quantifiers can and do range over an empty discourse in many cases in mathematics and this is frequently useful for establishing null bases (for example, 0! = 1, because "product from 1 up to 0 inclusive" counts no numbers given that 1 is already greater than 0).

Originally Posted by Annatala

I'm not sure what you're trying to argue here.

What I'm arguing is what I've said over a dozen times, and it an unassailable fact:

"Separation alone (no need for infinity) proves: ExAy ~yex."

As I wrote:

"First order logic applied to an instance of the separation schema provides a proof of "ExAy ~yex."

"[U]sing only the first order predicate calculus,
there is a proof of
ExAy ~yex
where the proof uses an instance of the axiom schema of separation as the only non-logical premise."

"This is […] a pure question of provability in the first order predicate calculus."

I'm sorry now to have to yet again repeat the explanation and augment it with even more pedantic detail.

First though, you mention that your context is "intuitionistic logic [...] not formal logic". Do you mean in particular an informal intuitionisitic logic per the intuitionists Brouwer, Heyting, et. al? Or do you mean merely 'informal'?

I haven’t opined on how one does or should regard proof of ExAy ~yex in informal, pre-formal, unofficial, intuitive (whether intuitionistic or classical) notions about sets or whatever else. I made clear enough that my claim is one of formal provability, though you continued to dispute my correct claim.

You wrote, "Are you suggesting the concept of set can itself be defined in set theory? How can this be possible since you need sets a priori for everything? I'd agree you can prove existence of the empty set from induction [infinity] and separation […]”. And I replied "Separation alone (no need for infinity) proves: ExAy ~yex." Then you disputed me. Since the context was set theory, it was correct for me to point out that the existence of an empty set is provable from separation without need of recourse to the axiom of infinity. Whether that note by me was relevant to the notions you wished to explore, I don’t opine. But it was a correct note (for whatever it was worth or not worth as to the notions you wished to explore) and you were incorrect to dispute it.

As a side note, as to formal intuitionistic logic (Heyting), my remarks still stand. Whether '|-' stands for intuitionistic provability or classical provability, we have

{AzExAy(yex <-> (yez & (yey & ~yey)))} |- ExAy~yex

Next, as to the existence of at least one set (again, my remarks regard the formal theory and I do not opine as to what may be the case with various informal, pre-formal, unofficial, intuitive notions), given the first order logic we use, it is not needed to stop for consideration of "whether there exists a set". The logic alone proves all theorems of the form:

ExP
where P is any validity at all.

And the above argument is not even needed, since showing

{AzExAy(yex <-> (yez & (yey & ~yey)))} |- ExAy~yex

does not need to go through first proving (or using as previously proven) such a formula ExP.

Rather, simply take AzExAy(yex <-> (yez & (yey & ~yey))) as the sole non-logical premise. Then proceed to derive ExAy ~yex in a routine manner.

Also, note that the primitive language of Z set theory does not have a predicate 'is a set'. Mention of 'set' in this context is unofficial and used in certain formulations and discussions for ease of conceptualization but is NOT part of formal derivation in Z set theory itself.

Next is the matter of, for example, Jech using the axiom of infinity to prove that there exists a set. (1) Jech's method and explanation does not preclude that ExP (for validities P) is not provable in pure first order logic alone, and (2) Jech's explanation does not preclude that ExAy ~yex is provable from the axiom schema of separation alone (not using the axiom of infinity).

I cannot speak for Jech, but my guess would be that his explanation and use of the axiom of infinity for proving the existence of an empty set is to avoid having to appeal to particulars of first order logic that are not known to many mathematics students especially since such particulars may be a digression from the thrust of the set theoretic goals he wishes to quickly advance.

I think it's pretty plausible that most mathematics students (some even at the graduate level) don’t know that (and why) first order logic alone proves ExP for validities P and further that for proving ExAy ~yex from separation in first order logic, we don't even need to go through such a step.

The particulars of rules for quantifiers and variables don't seem very intuitively related to questions about whether there exists some set (or object of any kind) from which to apply separation to get our desired empty subset.

But none of that refutes the exact correct claim I've been making: There is a proof of ExAy ~yex from an instance of the axiom schema of separation.

Originally Posted by Annatala

Levy's own admission: "we assumed the existence of at least one set when we adopted first order logic"

You're not quoting Levy's context in which the sense of 'assumed' here is actually regarded:

"[…] since Ex(x=x) is a THEOREM [emphasis added] of first order logic, and since our only objects here are sets, we can say that we assumed the existence of at least one set when we adopted first order logic here."

Ex x=x is a THEOREM of first order logic. It is NOT assumed as an axiom nor as a premise in a proof. He says, "we can say that we assumed", and in context we see that what he means is that we have Ex x=x already available as a THEOREM.

You pounced on the word 'assume' as you gave an incorrect impression of what it means in this particular context, left out Levy’s context that I quoted, and left out the rest of the explanations from the other authors. Also, you left out my point that even with Jech, nothing he wrote in the mentioned passages entails that we can't ALSO prove ExAy~yex from separation alone.

Originally Posted by Annatala

The problem here is that Levy fails to realize this assumption he makes (which is often taken as a separate axiom in systems other than ZF) is entirely unnecessary in ZF, because the existence of at least one set follows directly from Infinity.

No, Levy makes no failure of realization here. He is NOT making an additional assumption. Rather, our proof system for ZF is first order logic, and first order logic gives us Ex x=x ANYWAY. It is not required to take it (nor any other axiom ExP for some validity P) as an axiom of set theory or of ANY theory (not even as an axiom for first order logic itself). He is not making an ADDED assumption. He's saying we can use Ex x=x as an "assumption" for set theory since it is ALREADY proven in first order logic alone.

You would disservice the discussion and widely miss the point by making anything of Levy's relaxed use of the word 'assumed' when actually he made clear that he's speaking of a THEOREM of first order logic.

As I've explained:

First order logic proves all formulas of the form

ExP

for all validities P (including 'x=x' if 'x=x' is regarded as first order validity).

And that dovetails with the semantics for first order languages: The universe of structure for the language must be non-empty.

And explaining that we have Ez z=z (or Ez(zez -> zez), etc.) already from the logic may help a student to conceptualize that we are assured a z from which to take our empty subset via separation, but first proving such an existence formula is not even needed for proving ExAy ~yex from separation, since we can go right to ExAy ~yex from an instance of separation using quantifier rules (and a bit of sentential logic) that "in a sense" have this "existence of at least one object" already "built in".

To see this for yourself, all you have to do is fill in the routine lines in a derivation from

AzExAy(yex <-> (yez & (yey & ~yey)))

to

ExAy ~yex.

Originally Posted by Annatala

Our model: The universe of discourse is empty.

No, the first order logic used for set theory does not have a semantics that allows empty universes for a model.
If you wish to have models with an empty universe, then that leads to the subject of free logic, which may be interesting, but does not pertain to ZF in any ordinary context. In any ordinary context, provability in ZF is per classical first order logic and semantics for ZF (or any of these related set theories) does not permit models to have an empty universe.

Originally Posted by Annatala

Can't I just replace all instances of:

S = T with: ( x (x S x T))?

No, the correct formulation would be

S=T <-> Ax((xeS <-> xeT) & (Sex <-> Tex)).

Then the axiom of extensionality may be given as:

Ax(xeS <-> xeT) -> S=T.

I'll keep this short to see if we can come to an accord on the facts.

1) I know FOL has a non-empty domain requirement.

2) I am not using FOL. I was trying to establish an exhaustive list of assumptions necessary to construct math (and logic) from set theory, without bootstrapping, so I don't want to assume some of the stuff FOL assumes. (And if I do assume something, I want to note it, whether it comes from set theory or from the logic I'm using to prove things.)

3) FOL's non-empty domain requirement is an assumption of FOL. It is a sensible assumption: if you don't restrict FOL to non-empty domains, certain propositions under FOL which we want to be valid will appear to be invalid.

4) You can prove the domain is non-empty from the axioms of ZFC without relying on the non-empty domain requirement of FOL.

5) As an aside from a separate perspective: there are areas of database theory where allowing for the possibility of an empty universe of discourse is very handy, and believe it or not, the logic works out just fine for us. Logic doesn't suddenly turn inconsistent or incomplete just because we allow for the existence of an empty discourse.

To be blunt, Thomas Jech is the man who established the independence of Suslin's problem. He knows more about set theory than either one of us ever will, and he tends to couch his arguments in the fewest assumptions needed. This is why I like his writing. The less you need to rely on, the stronger your argument is. If you want to lean on FOL and say, "you don't need to prove this because FOL requires that it be true in the first place", that's fine. But that's not what I'm trying to do here, and most of what you're trying to argue are things I do not disagree with.

This is bickering over semantics, in other words, which is hands down the worst of what logic has to offer. :P