Maybe you are right: sets cannot be empty. — Mephist

What this means is that zero is a very strange type of number, unique and different from the other numbers. So we ought to be careful in the way that we use it.

Maybe you are right: sets cannot be empty. — Mephist

So what do you make of the set $\{x \in \mathbb N : x \neq x \}$?

You reject the axiom schema of specification? You don't think $\mathbb N$ is a set? I really want to hear this.

I don't know. Ask @Metaphysician Undercover

This is a "set_or_nothing", not a "set"... :smile:

This is a "set_or_nothing", not a "set" — Mephist

If it's not a set, which do you disagree with: The axiom schema of specification? Or that the natural numbers are a set?

Does the smiley mean that you don't actually believe what you wrote but that talking to @Metaphysician Undercover has caused you to lose your grip? What does the smiley mean? Why did you claim there is no empty set? If you so claim, what do you do with the brief existence proof I just gave?

When I put the same question to @Metaphysician Undercover, he admitted that it's not the empty set he objects to, but rather the entirety of set theory. That's a nihilistic position but at least it's a position. You have none that I can see.

Does the smiley mean that you don't actually believe what you wrote but that talking to Metaphysician Undercover has caused you to lose your grip? What does the smiley mean? Why did you claim there is no empty set? If you so claim, what do you do with the brief existence proof I just gave? — fishfry

Yea, this discussion is going in circles without any hope of a conclusion. I would like to finish discussing about empty sets!

Yea, this discussion is going in circles without any hope of a conclusion. I would like to finish discussing about empty sets! — Mephist

You retract or stand by your claim that there is no empty set?

Does the smiley mean that you don't actually believe what you wrote but that talking to Metaphysician Undercover has caused you to lose your grip? — fishfry

Mephist seems to have no rebuttal to the arguments which demonstrate that the "empty set" is a contradictory concept, and unlike you, seems about ready to face the reality of this.

When I put the same question to Metaphysician Undercover, he admitted that it's not the empty set he objects to, but rather the entirety of set theory. That's a nihilistic position but at least it's a position. You have none that I can see. — fishfry

What I object to is the claim of "existence" for objects which have a contradictory description. This is not nihilistic, but a healthy skepticism. The attitude demonstrated by you, that we might assign "existence" arbitrarily is best described as delusional.

OK, I see it's not so easy to finish this discussion about the empty set... :meh:

I didn't change idea: there is no contradiction in the axiomatic definition of sets given by ZFC, at least for what has been discovered until now. It has not even been proved that ZFC is not contradictory, however; but since nobody has found any contradiction in ZFC after 100 years of using it, I would guess that it is consistent.
By the way, dependent type theory - at least a subset of the version used in coq - has been proved to be consistent (but of course it is not complete - no way to avoid Godel's incompleteness theorem).

However, I don't see any problem in the definition of an empty set, and the fact that the name "set" could suggest that it has to be composed of at least some elements is not a problem for me, since this is just a name, and names have no role in a formal logic system. If it was called "asodifj" nothing would change, except that it would be more difficult to remember this absurd name.

Mephist seems to have no rebuttal to the arguments which demonstrate that the "empty set" is a contradictory concept, and unlike you, seems about ready to face the reality of this. — Metaphysician Undercover

I understand that your objection is more about the philosophical interpretation of the idea of "set". This in my opinion is not about mathematics, and to say the truth I don't really see the point of this kind of issues. In my opinion, there are only two points of view:
- mathematics, that don't care about the "real" meaning at all
- physics, that cares only about the correspondence between symbols and results of physical experiments.
Anything that has no direct correspondence with the results with physical objects or results of experiments (such as the sets of ZFC, that can be infinite) is an useful mathematical entity, but it doesn't need to have any meaning at all: it's just an useful abstraction.

By the way, if you consider only finite sets, I don't see any problem at all with the obvious interpretation of sets as physical containers of something (that can be even empty).

What I object to is the claim of "existence" for objects which have a contradictory description. — Metaphysician Undercover

I think the word contradictory is not the right term in mathematics. The right term should be "inconsistent", and it has a very precise meaning in of formal logic system. Your "proof" of inconsistency, as I just said before, is not something that contemporary mathematics would accept as valid. Maybe it's valid from a philosophical point of view, but I don't fill qualified enough as a philosopher to discuss about it.

However, I really have no other new ideas how to object to @Metaphysician Undercover arguments, and I don't see the point in repeating continuously the same things...

I didn't change idea: there is no contradiction in the axiomatic definition of sets given by ZFC, at least for what has been discovered until now. It has not even been proved that ZFC is not contradictory, however; but since nobody has found any contradiction in ZFC after 100 years of using it, I would guess that it is consistent.
By the way, dependent type theory - at least a subset of the version used in coq - has been proved to be consistent (but of course it is not complete - no way to avoid Godel's incompleteness theorem). — Mephist

Was that a yes or a no? Stop dancing. You're wrong on the facts, wrong on the math. Why are you trying to placate @Metaphysician Undercover's nutty ideas?

What do you think a set is, if not anything that obeys the rules of set theory?

Mephist seems to have no rebuttal to the arguments which demonstrate that the "empty set" is a contradictory concept, and unlike you, seems about ready to face the reality of this. — Metaphysician Undercover

When I challenged you on this point, you admitted that it's not only the empty set, but set theory in its entirety that you object to. Then you added that you reject modern physics as well. Nihilism. You are speaking nonsense. For @Mephist's part, he read a book on category theory but knows very little actual math. The fact that he's confused about the empty set, even when shown its existence proof from the axioms of set theory, supports that conclusion.

Was that a yes or a no? Stop dancing. You're wrong on the facts, wrong on the math. Why are you trying to placate Metaphysician Undercover's nutty ideas? — fishfry

I don't understand what I am wrong about. I said there is no proof that ZFC is inconsistent (meaning: nobody has never derived a contradiction from ZFC's axioms), but there is even no proof that ZFC is consistent. That's why I prefer type theory to ZFC. Type theory is weaker but is provably consistent.

Can you show me what I said wrong?

What do you think a set is, if not anything that obeys the rules of set theory? — fishfry

I think the sets that are defined in ZFC are a hierarchical tree-like structure that can be used to model the relation "belongs to" at the same way as the leaves of a tree "belong to" it's root. It lacks symmetry and is too complex. I think in the future it will be substituted by a more elegant and simpler definition. I think it does not correspond to anything in the physical world, so basically yes: it's just an imaginary gadget that obeys the rules of set theory, ad it could be substituted by other similar gadgets that logically equivalent to it.

The fact that he's confused about the empty set, even when shown its existence proof from the axioms of set theory — fishfry

Can you show me a proof of consistency of ZFC set theory that doesn't make use of another even more complex and convoluted set theory?

For Mephist's part, he read a book on category theory but knows very little actual math — fishfry

I would like to hear the opinion of other real mathematicians about what I wrote. For example @jgill or anybody else that can be surely qualified as a mathematician. Could you please point out what I said that is not correct? (this, or even one of my previous posts).

It's perfectly possible (and probable) that I wrote something wrong, but I would like to know what's the mistake that I made.

For example jgill or anybody else that can be surely qualified as a mathematician. Could you please . . . — Mephist

I'd like to chime in with words of wisdom, my friend, but category theory is terra incognita to me. Read about it years ago and decided to give it a pass. Don't worry about the empty set. It can take care of itself. If it feels lonely, it can con an element from a comrade. Life goes on.

:sad: But that was about ZFC...
Thanks for the answer, anyway!

I had to wiki the axioms of ZFC, having forgotten them long ago. :yikes:

Your "proof" of inconsistency, as I just said before, is not something that contemporary mathematics would accept as valid. — Mephist

I went through this already. You cannot use the logic derived from the axioms to judge the axioms of the system, because valid logic will not allow one to produce a conclusion which is inconsistent with the premises. Therefore we need to refer to some other principles, and philosophy provides us with those judgements and proofs. If you're not interested, that's fine, but the assertion that such proofs are not valid in mathematics is not a sound rebuttal. I'm demonstrating to you, that the premises of your logic are false, and you reply, that doesn't matter because for me, and for everyone who uses my system the premises are true, and unless you can prove that they are false, by starting from the premise that they are true, you have no argument.

When I challenged you on this point, you admitted that it's not only the empty set, but set theory in its entirety that you object to. — fishfry

Of course, the nature of the empty set is essential to understanding what a "set" is, and if a theory has contradictory premises, then I object to the theory in its entirety, it needs to be reformulated

OK. Sorry, I give up...

Yes, however in my opinion Anders Kock's book ( https://users-math.au.dk/~kock/sdg99.pdf ) is not so difficult to understand. d in my opinion should not be interpreted as a number, but as the base of a vector space made of infinitesimal numbers attached to each of the real numbers of a "base" space — Mephist

You get something really similar to that with any mapping $t(k):D\rightarrow M$, where $M$ is some manifold in which $x$ is a point. With the constraint that $t(0)=x$, the collection of all such maps forms a module ("vector space with elements from a ring"). It's an infinitesimal tangent space attached to the point. It might mutilate intuitions of the real number line, but that doesn't matter, as it seems designed to simplify language and proofs about smooth functions. Whether it's "wrong" or not is just a question of taste and application.

Can you show me a proof of consistency of ZFC set theory that doesn't make use of another even more complex and convoluted set theory? — Mephist

As I'm sure you know, if a theory's consistent and has arithmetic, it can't prove its own consistency. You always have to go outside a theory to prove that theory's consistency; so consistency of system X is always just relative consistency to some other system Y. If you want to find a model of some axiom system, you need to construct the model through other rules (even if they're incredibly similar).

A weaker criterion might be that you want some theory which is equivalent to ZFC in the sense of having statements which are inter-derivable with all of its axioms. But then all consistency proofs here would establish are that "equivalent axiomatisations of ZFC are consistent at the same time"; like being reassured that ZFC is consistent because you can replace the C with Zorn's Lemma and that ZF+(Zorn's Lemma) is consistent when ZFC is.

I'd've thought you'd be quite happy with small categories? :brow: Aren't the models of intuitionistic logic Heyting algebras (from earlier) anyway? They're sets, or categories which are represent-able as sets. So I'm reading this like: "I don't like sets because I don't like the structures that establish ZFC has models. But I like intuitionist dependent type theory because it has a model! (Which is a collection of sets.)"

Here's an argument for the necessity of the empty set.

If you want a theory of sets, you want to be able to compare pairs of sets. You want to know if they have any elements in common, and aggregate all elements they have in common into some set at the same time; taking an intersection of sets.

Let's compare the interval of real numbers (1,2) and the interval of real numbers (3,4). Assume that the intersection of those sets must be non-empty, then there is is a number which is both strictly less than two and strictly greater than three. There is no such number.

The empty set comes quite naturally from two principles:
(1) The ability to state what elements sets have in common.
(1a) The elements that sets have in common must always be equal to a set.
(2) That two sets might be disjoint.

(as @fishfry pointed out, you can get contradictions if you disallow an empty set like object)

One possibility, seemingly proposed by @Mephist (if I understood your responses to MU anyway) is that you put in the empty set as a proper class primitive into the theory, so that (1a) is denied but (1) and (2) are still true. It's pretty much a distinction without a difference though; "intersections of sets contain at least 1 element or are the empty class", I'd imagine you'd have transfer results from this "empty set is declared a proper class for no reason + ZFC" theory to the usual ZFC theory. My guess is that it would be a distinction without a difference.

You get something really similar to that with any mapping t(k):D→Mt(k):D→M, where MM is some manifold in which xx is a point. With the constraint that t(0)=xt(0)=x, the collection of all such maps forms a module ("vector space with elements from a ring"). It's an infinitesimal tangent space attached to the point. It might mutilate intuitions of the real number line, but that doesn't matter, as it seems designed to simplify language and proofs about smooth functions. Whether it's "wrong" or not is just a question of taste and application. — fdrake

Yes, exactly. The intuition of the real number line, in my opinion, is not mutilated but simply different: you have a base space of points that can be built in type theory as limits of convergent sequences of rational numbers. Each of these points is "covered" by an infinitesimal open set.
The weird thing at first sight is that there are no closed intervals such as [0,1], and all functions have to be continuous. But if you think of a function as a model of a physical process, in my opinion that's the ideal mathematical object. In physics, there aren't really discontinuous processes, even in principle, since infinite precision is not measurable. A discontinuous function of time, for example, would mean an infinite velocity of some kind of process.

As I'm sure you know, if a theory's consistent and has arithmetic, it can't prove its own consistency. You always have to go outside a theory to prove that theory's consistency; so consistency of system X is always just relative consistency to some other system Y. If you want to find a model of some axiom system, you need to construct the model through other rules (even if they're incredibly similar). — fdrake

Yes, that's true. But the proof of consistency of a dependent type theory (such as for example Calculus of Constructions) is simply a proof that a given class of programs always terminates and is "strongly normalizing" (meaning: any two programs can always be compared with each-other by reducing them to a normal form, and then checking if they are syntactically equal). See for example https://prosecco.gforge.inria.fr/personal/hritcu/temp/snforcc.pdf.

In reality, in CC the induction principle P(0) and ( forall n:Nat, P(n) ==> P(n +1) ) ==> ( forall n:Nat, P(n) ), and then the definition of the type of natural numbers, is not an internal part of the logic, but is assumed as an axiom. So, strictly speaking, the logic of CC does not include natural numbers. But you only have to "trust" the principle of induction, not the existence of abstract infinite sets.

I'd've thought you'd be quite happy with small categories? :brow: Aren't the models of intuitionistic logic Heyting algebras (from earlier) anyway? — fdrake

Heyting algebras represent only the propositional part of intuitionistic logic, not including variables and quantifiers.

They're sets, or categories which are represent-able as sets. So I'm reading this like: "I don't like sets because I don't like the structures that establish ZFC has models. But I like intuitionist dependent type theory because it has a model! (Which is a collection of sets.)" — fdrake

Yea, this seems not to make much sense.
OK, I'll try to explain.

1. To speak about the elements of an arbitrary set, you need only first order logic. You don't need a set theory. Meaning: first order logic (the rules and axiom of the logic) define the meaning of "forall" and "exists" quantifiers. For example, you can axiomatize a generic group, or a generic ring, using only first order logic. No need of ZFC. ZFC is needed to speak about the relations between sets (inclusion, intersection, subsets, etc...), or the relations between groups, or rings.
2. In principle, the definition of a category requires the existence of two sets: Objects and Arrows. So, two sets, not one.. However, the definition can be reformulated to use only one set (the set of arrows), and the objects can be identified as the identity arrows. So, in principle a generic category can be defined making use only of first order logic, without any set theory.
The problem is that the most important theorems and constructions of category theory (such as functors, natural transformations, Yoneda lemma, etc..) are related to the category of sets. And the category of sets is "the category that has as objects (all possible) sets and as arrows (all possible) functions between these sets". In other words, the category of sets is not defined in terms of category theory itself (meaning: in terms of objects and arrows, as in the definition of a topos, for examle), but is defined in terms of an underlying set theory (that is what it's called a "concrete" category - https://en.wikipedia.org/wiki/Concrete_category).
If you suppose to have ZFC as an underlying theory, I believe (not completely sure) that there would be a problem with this formal definition: you can't say that the objects of the category of sets are the set of all sets, because there is no such set in ZFC. So, if you want to avoid this kind of problems you should use an underlying set theory that assumes the existence of a class of all sets.
Or, for example, you can build category theory based on type theory. Then, the category of sets in this case will have as objects all the types of a given "universe" of types, and as arrows all computable functions. Most of the results of category theory are independent from the preexistent "set theory" that you use to build the category of all sets, but not all of the results.
I don't know the details of these differences, but from a foundational point of view, category theory is not an univocally defined theory. There are even several ways of defining a category for a fixed intuitionistic type theory, because you can "build" the types of arrows and objects in more than one way.
Fortunately, most of the results (practically all of that I know) are independent of the underlying set (or type) theory that you use to define the category of sets. So, if you have a "real numbers object" in category theory you don't have to worry about the underlying logic that you use: you can choose the easiest one to reason about; one where all functions are computable, for example.

One possibility, seemingly proposed by Mephist (if I understood your responses to MU anyway) is that you put in the empty set as a proper class primitive into the theory, so that (1a) is denied but (1) and (2) are still true — fdrake

Yes, that's correct. You can consider a "topos" as a generalized class of all sets. So, the sets are the objects of the category. The final object of the category corresponds to the set that contains only one element (singleton), and the initial object of the category corresponds to the empty set.
In the general definition of a "topos", the existence of an initial object is not required (because in the definition you want to have largest possible generalization of the category of sets), but the "normal" examples of topoi (such as the category of sheaves, or the category of sets - that are all particular examples of a topos) all have an initial object (corresponding to the empty set).

I'm demonstrating to you, that the premises of your logic are false, and you reply, that doesn't matter because for me, and for everyone who uses my system the premises are true, — Metaphysician Undercover

And there you have it from a man (presumably) who cannot process that some things are true by definition within the context of their use.

Maybe - maybe - we can sharpen this with an example. What is a warehouse? If you hold that a warehouse is a place where goods are stored, then there can be no such thing as an empty warehouse, and if you say there is, then I reject the entire idea of warehousing.

On the other hand, if you say a warehouse is a place where goods may be stored, then no warehouse in which goods are actually stored can be a warehouse. And this is the logic of the thing. And as the logic of warehousing is clearly contradictory, then the whole idea is nonsense and I reject it pending some reformulation that accords with my ideas of how these things should be.

But you're a warehouse-man and and shipper, you say, and warehouses and warehousing are part of your business. Well, you obviously do not understand your business.... and so on.

Absolute silliness. And what cannot be cured at the least ought not to be fed.

What I object to is the claim of "existence" for objects which have a contradictory description. This is not nihilistic, but a healthy skepticism. The attitude demonstrated by you, that we might assign "existence" arbitrarily is best described as delusional. — Metaphysician Undercover

I can't take that as much of a criticism, since by your own criterion you regard the entire community of working professional mathematicians as delusional, and perhaps the physicists too. You have put me into some great company, that, frankly, I hardly deserve.

I do agree that I have not provided a definition of mathematical existence that you would find satisfactory. I'm thinking the issue over but it's tricky. However you are someone who regards the simple adjunction to the rational numbers of a formal square root of two as completely beyond the pale. I confess that I'm at a loss to respond to such philosophical nihilism. The principles by which we accept the rational numbers are no different and no logically simpler than those by which we adjoin a formal square root of two.

Of course, the nature of the empty set is essential to understanding what a "set" is, and if a theory has contradictory premises, then I object to the theory in its entirety, it needs to be reformulated — Metaphysician Undercover

Take it up with Frege, Russell, Zermelo, von Neumann, and all the other brilliant 20th century set theorists including those working at the forefront of knowledge today such as Hamkins, Steele, Woodin, Shelah, and others. Your childish objection to modern math and science is noted. You don't have to repeat it. I heard you the first 20 times. Your nihilistic point does not gain sanity by repetition.

It's perfectly possible (and probable) that I wrote something wrong, but I would like to know what's the mistake that I made. — Mephist

I'm sorely behind in responding to my mentions but I am getting to this point soon. I will explain in detail why you are wrong in your response to my demonstration of the existence of the empty set.

By the way, dependent type theory - at least a subset of the version used in coq - has been proved to be consistent (but of course it is not complete - no way to avoid Godel's incompleteness theorem). — Mephist

This point must be profoundly wrong or disingenuous on your part. If anything at all -- dependent type theory, Coq, a tuna sandwich on rye -- can prove its own consistency, then it must necessarily be entirely useless for representing modern mathematics.

If on the other hand you mean that it's been proven consistent using assumptions outside of itself, then the same is true of set theory. In 1936 Gerhard Gentzen proved the consistency of Peano arithmetic by assuming the consistency of transfinite induction up to the ordinal $\varepsilon_0$.

And in algebraic geometry, the branch of math that led to the original discovery of category theory by Mac Lane in the 1940's, the existence of an inaccessible cardinal is assumed. This in effect amounts to the assumption that ZFC is consistent, since an inaccessible cardinal is a model of set theory; that is, a set that satisfies the axioms of set theory.

In category theory and algebraic geometry the inaccessible cardinal shows up in the definition of a Grothendieck universe. The reason universes are the natural setting for categorical algebraic geometry is that they ensure that the categories in question contain enough sets to make the theory sensible.

Per the Wiki article: "The concept of a Grothendieck universe can also be defined in a topos." So if you're as as big a believer in topos theory as you say, you have a ready-made proof within topos theory of the consistency of ZFC.

Professional mathematicians, even category theorists -- especially category theorists -- understand that if you can't ground your categorical theory in set theory one way or another, you don't have a good theory.

I don't understand what I am wrong about. — Mephist

First let me put this in context. You said the empty set doesn't exist. I gave a short existence proof from the axiom schema of specification. That's a valid proof in ZF of the existence of the empty set. You then objected to my proof by saying ZFC can't prove itself consistent. Which would result in your rejecting the entirety of modern mathematics.

So I'll explain why you're wrong First, your response is a total deflection, changing the subject. Second, your response has the same slippery slope problem as @Metaphysician Undercover's response to the same question. Namely, that it's not only the empty set that's not deserving of being called existent. Rather it's the entire enterprise of modern mathematics. Surely you must realize that such reasoning is untenable because it's so broad. You both want to reject the empty set on narrow terms -- "it makes no sense to have a collection that doesn't collect anything," etc. -- but you each end up saying that math itself is flawed therefore there's no empty set. There must be a name for such an argument. You want to argue a very narrow technical point and your only argument is to blow up the entire enterprise.

Third, your overall understanding of what math is about is inverted, in exactly the sense @jgill notes. Many people who come to math through foundations believe math is about the foundations. It's the other way 'round. Mathematics comes first and foundations are just our halting and historically contingent attempts to formalize accepted mathematical practice. Archimedes, Newton, Euler, and Gauss never heard of set theory. Were they not doing math? You see the absurdity of trying to put foundations logically prior to mathematics.

First we discover the math; then we make up the axioms that let us formalize it.

That's how math works. My sense is that professional philosophers of math (Maddy et. al.) perfectly well understand this; and that it's only the amateur enthusiasts on the message boards who believe otherwise.

And fourth, you're wrong on the math and logic of the situation.

So let me lay out some talking points in support of my four reasons you are wrong.

I said there is no proof that ZFC is inconsistent (meaning: nobody has never derived a contradiction from ZFC's axioms), but there is even no proof that ZFC is consistent. — Mephist

The horrors. I suppose when Andrew Wiles solved Fermat's last theorem you said, "Harrumph, poppycock, we don't even know if ZFC is consistent." I hope you see the absurdity of your own position. For that matter it might interest you to know that Wiles's proof is done in the framework of Grothendieck's approach to modern algebraic geometry; which as I mentioned to you in another thread is done within a Grothendieck universe, a model of set theory that (a) assumes ZFC is consistent; and (2) posits the existence of an inaccessible cardinal, a transfinite cardinal whose existence is independent of ZFC. There's a lengthy and famous Mathoverflow thread about whether or not an inaccessible cardinal is necessary to Wiles's proof. Consensus is that it's not.

Likewise when Maryam Mirzakhani became the first woman and the first Iranian to win the Fields medal for "the dynamics and geometry of Riemann surfaces and their moduli spaces," you of course shouted, "Doesn't she know ZFC hasn't been proven consistent? She shouldn't have bothered."

If you are arguing anything different than this please let me know. Else retract your nonsensical point that since ZFC can't prove itself consistent, it must be fatally flawed. And that you can use this as a trump card to win any mathematical argument "The empty set exists." "No it doesn't, ZFC can't be proven consistent."

Man is this what you are arguing to me?

I want to add that when @Metaphysician Undercover makes the same argument, I have less of a problem with it; because he at least openly admits he does not engage with symbolic arguments. Please correct me if I have mischaracterized that in any way.

@Mephist, on the other hand, you seem perfectly willing to claim mathematical and symbolic knowledge. So your argument here is just awful. The empty set doesn't exist because ZFC can't prove itself consistent. Said by someone claiming math sophistication.

Am I missing your point here? Please tell me if I'm going off on the wrong thing. Because if that's your argument then you are a nihilistic as @Metaphysician Undercover, but with less of an excuse. You both want to throw out the entirety of modern mathematics just to defend your point that the empty set is not deserving of existence. You must not have much of an argument, either of you.

* Note that even if ZFC is inconsistent, then the empty set exists! The derivation from the axiom schema of specification is valid. So your own logic is screwed up. If ZFC is consistent the empty set exists, and if ZFC is inconsistent the empty set exists. Or rather in either case, the proof of its existence is valid. And what more do you ask for in terms of mathematical existence? You both want to reify the empty set. What nonsense. That's sophistry, to pretend to reject mathematical abstraction.

That's why I prefer type theory to ZFC. — Mephist

You thanked me for posting the Stackexchange thread the other day but I'm not sure you got its message. The example of synthetic differential geometry was given to show that the point of alternative foundations is to shed light on problems, not to brag about which foundation is more fundamental.

Likewise he gave the example of someone saying that set theory's more fundamental than topology so they don't need to study topology. That's silly, right?

So when you say, "I prefer type theory" because of a spurious understanding of ZFC's inability to prove its own consistency, you sound like you're clinging to what you know because you can't understand what you don't know. So far your logic is "the empty set doesn't exist because ZFC can't prove its own consistency and that's why type theory is better."

You're making a poor argument and only showing the limitations of your own understanding.

Type theory is weaker but is provably consistent. — Mephist

I responded to this in more detail in another post. This claim cannot possibly mean what you say it does. If type theory or any other theory can prove itself consistent, then à la Gödel it's useless for doing modern math.

On the other hand if you mean it can be proven consistent using means outside of itself, so can ZFC, as is commonly and standardly done in the modern categorical approach to algebraic geometry as pioneered by Mac Lane and perfected by Grothendieck.

Didn't they mention any of this in your category theory book? This is what I mean by your having a lack of overall understanding of math. It's part of the wrongness of your reply. Category theory and type theory don't invalidate 20th century math. They view it from another perspective. The math itself is the thing represented by the representations. You're trying to privilege one particular representation over another simply because you know one and not the other and don't get that the representation is not the thing itself. Not a good argument, not making points with me.

Again: Math precedes foundations. Not the other way 'round.

Can you show me what I said wrong? — Mephist

I've said my piece, and if it was too long, it's because "I didn't have the time to make it shorter," as some clever person said once.

I think the sets that are defined in ZFC are a hierarchical tree-like structure that can be used to model the relation "belongs to" at the same way as the leaves of a tree "belong to" it's root. — Mephist

Maybe, but not what I was looking for. A set is anything that obeys the axioms of set theory; in exactly the same way that point, line, and plane are undefined terms in Euclidean geometry. As Hilbert noted: "One must be able to say at all times--instead of points, straight lines, and planes--tables, chairs, and beer mugs." That is how we regard sets.

You want to somehow reify sets. You think a set should refer to the real world. I for one don't believe that. There's no set containing the empty set and the set containing the empty set in the real world. In set theory we call that set '2'.

It lacks symmetry and is too complex. — Mephist

I'd argue the contrary. Sets as an abstraction of collections are very natural. You can teach sets to school kids in terms of unions and intersections of small finite sets. Type theory and category theory are more sophisticated concepts that require some mathematical training to appreciate.

But so what? Are you honestly rejecting the entirety of contemporary math because you have some kind of personal issue with set theory? That makes no sense. Set theory, type theory, and category theory are various tools in the toolkit for exploring the world of mathematical entities.

Math precedes foundations. Not the other way 'round.

I think in the future it will be substituted by a more elegant and simpler definition. — Mephist

But of course. Foundations are always historically contingent. Set theory in its current form is less than a century old dating from Zermelo's 1922 axiomitization. By the way Cantor always gets the credit, but it's Zermelo who did the heavy lifting in the development of modern set theory. Before Cantor there was no set theory. A few decades from now category theory and type theory will be much better known and perhaps set theory will fade into history. It won't be wrong, just out of fashion. That's inevitable.

I think it does not correspond to anything in the physical world, so basically yes: it's just an imaginary gadget that obeys the rules of set theory, ad it could be substituted by other similar gadgets that logically equivalent to it. — Mephist

Well of course. Was someone thinking set theory refers to the physical world? It's a formal game. It's the chess analogy I constantly use (to no effect) with @Metaphysician Undercover. You are standing on a soapbox fervently preaching something so obvious it barely needs to be said. Set theory is an attempt at a formalization of math. What of it?

Can you show me a proof of consistency of ZFC set theory that doesn't make use of another even more complex and convoluted set theory? — Mephist

Not complex or convoluted? Sure. Grothendieck universes are very plausible and straightforward, and are the standard everyday mathematical framework in much of modern math. Wiles's proof of Fermat's last theorem is presented in the framework of universes, even though that's probably not strictly necessary. The proof of the consistency of ZFC via assuming an inaccessible cardinal is part and parcel of modern math. Of course we DO have to assume an axiom in addition to ZFC; but that axiom is by no means unintuitive or unbelievable. It's rather natural.

And what of it? You are making a TERRIBLE argument. That because you have some technical objection to the empty set (which you have not articulated) therefore the entirety of modern math is rejected because, "Nyah nyah type theory is better." And this to a simple technical question, does the empty set exist. And you go, "Well no, because the entirety of contemporary mathematics is bullshit."

That's your argument?

If I may make an analogy, it's like a beginning programmer arguing that their favorite language is better, just because it's the only one they know. And you, an experienced developer with a dozen languages under your professional belt, can only shake your head and remember when you were that young and dumb.

Oh and Columbo would say, One More Thing.

The empty set is the unique initial object in the category Set. You do believe in the category Set, don't you?

https://en.wikipedia.org/wiki/Initial_and_terminal_objects#Examples

Here's a formal proof in Coq that the Calculus of Constructions is sound: http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf

First let me put this in context. You said the empty set doesn't exist. — fishfry

I'll not discuss about the empty set any more. Yes, you are right. The empty set exists. You win!

Here's a formal proof in Coq that the Calculus of Constructions is sound: http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf — Mephist

I don't care. If anything whatsoever can prove its own consistency, it's useless as a foundation for math. If it requires something external to itself to prove its consistency, it's no better off than ZFC, which can easily (not complex or convoluted, but naturally) do the same.

But I am curious. Which of these is the case? Is the Calculus of Constructions useless as a foundation for most of modern math? Or relies on something outside itself for a proof of consistency?

If it's not one of these, then I stand to learn something. So please explain how this thing, whatever it is, defies Gödelian incompleteness.

I'll not discuss about the empty set any more. Yes, you are right. The empty set exists. You win! — Mephist

I was just surprised the other day when you agreed with @Metaphysician Undercover that it doesn't. I'm glad I was able to nip that in the bud, if in fact you mean it and are not just placating me. I should also point out that the reason denying the empty set entails denying so much more of modern math, is because the formalization of pretty much all of modern math depends on the existence of the empty set! This is a fact. Not of math itself, which is agnostic as to foundations. But to our formalizations of math. You can't do without the empty set. It exists on pragmatic grounds.

But now @Metaphysician Undercover has a good question. What does it mean that the empty set exists? Is it ONLY that its existence formally follows from somewhat arbitrary axioms? If so, he has a point. Can we do better in terms of defining mathematical existence?