Zulip Chat Archive

Stream: general

Topic: how zfc works


Huỳnh Trần Khanh (Jul 07 2021 at 12:10):

well people keep talking about zfc... and I've read the axioms but I still can't understand how it models mathematics... any resources? thanks in advance

Huỳnh Trần Khanh (Jul 07 2021 at 12:13):

from my perspective, ZFC is like a dystopian world where people are only allowed to talk about sets and discussions about other things are only allowed if they can be described in terms of sets... but my idea of the ZFC world is still very vague...

Mario Carneiro (Jul 07 2021 at 12:24):

You could just as well say the same thing about type theory if you replace "sets" with "types"

Mario Carneiro (Jul 07 2021 at 12:25):

Sets are the primitive notion in ZFC. They have no definition, they just are axiomatized to have certain properties that amount to "there are enough sets for anything you could ever need"

Mario Carneiro (Jul 07 2021 at 12:27):

and then you just build whatever notions you need with that as the substrate. You very quickly stop thinking in terms of sets because that's not the topic of discussion, in the same way that we don't make a big deal about how mathematics is made of words

Huỳnh Trần Khanh (Jul 07 2021 at 13:10):

so... I have a more concrete question now. the axiom of infinity asserts that there is a set that contains every natural number in the von Neumann encoding and possibly other garbage elements... how can I extract the set of natural numbers from the axiom of infinity then? and how can I prove that induction holds?

Huỳnh Trần Khanh (Jul 07 2021 at 13:12):

the set of natural numbers is itself a natural number right?

Huỳnh Trần Khanh (Jul 07 2021 at 13:12):

and its name is omega or aleph null...

Eric Rodriguez (Jul 07 2021 at 13:12):

omega isn't a natural number it's an ordinal

Eric Rodriguez (Jul 07 2021 at 13:14):

you can probably make up some predicate to extract the non-junk, i'd go for something like (off the top of my head, not guaranteeing correctness):

{xX  sx,sXstx,s=t} \{ x \in X\ |\ \forall s \in x, s \in X \land \forall s t \in x, s = t \}

Mario Carneiro (Jul 07 2021 at 13:22):

I don't think that works, you are defining all the singleton subsets of XX but that might not be countable if XX is some arbitrary infinite set

Eric Rodriguez (Jul 07 2021 at 13:23):

what other singleton subsets can there be? any non-finite ones are ruled out by regularity, no? or am I missing something

Mario Carneiro (Jul 07 2021 at 13:23):

The usual approach is to define what it means for a set to be "inductive", i.e. 0X(xX,S(x)X)0\in X\wedge (\forall x\in X, S(x)\in X) (the axiom of infinity asserts that an inductive set exists), and then you take the intersection of all inductive sets to get ω\omega (which exists because it is a subset of XX)

Mario Carneiro (Jul 07 2021 at 13:24):

ω\omega is in fact not composed of singleton sets

Eric Rodriguez (Jul 07 2021 at 13:24):

I see, big oops then

Huỳnh Trần Khanh (Jul 07 2021 at 13:24):

that explains why I'm so confused by the predicate

Huỳnh Trần Khanh (Jul 07 2021 at 13:24):

:joy:

Jason Rute (Jul 07 2021 at 13:25):

If I recall correctly, you also need to do this to get the power set from the power set axiom.

Mario Carneiro (Jul 07 2021 at 13:26):

and the union axiom. It's a common trick to simplify all the axioms to unidirectional versions in the presence of the subset axiom

Eric Rodriguez (Jul 07 2021 at 13:26):

does it work for Zermelo ordinals Mario? that's what I was thinking of, not the VN ones

Eric Rodriguez (Jul 07 2021 at 13:27):

ahh I see what I've done, I've created a horrific mixture of both

Eric Rodriguez (Jul 07 2021 at 13:27):

that's terrifying and bad

Mario Carneiro (Jul 07 2021 at 13:27):

It depends on how the axiom of infinity is stated. The usual statement contains an explicit reference to VN successor

Mario Carneiro (Jul 07 2021 at 13:28):

but if you swapped it out for a zermelo successor then you could do the same thing with zermelo ordinals

Huỳnh Trần Khanh (Jul 07 2021 at 13:31):

wait, that's confusing. how can the axiom of infinity be stated with zermelo ordinals then?

Huỳnh Trần Khanh (Jul 07 2021 at 13:31):

and can that be shown to be equivalent to the VN version

Mario Carneiro (Jul 07 2021 at 13:31):

Huỳnh Trần Khanh said:

and how can I prove that induction holds?

Given the intersection definition of ω\omega, the induction theorem falls out naturally. If P(0)P(0) holds and x,(P(x)P(S(x)))\forall x,(P(x)\to P(S(x))), then {xωP(x)}\{x\in \omega|P(x)\} is an inductive set, so therefore ω{xωP(x)}\omega\subseteq \{x\in \omega|P(x)\} and hence P(x)P(x) holds for all xωx\in\omega

Mario Carneiro (Jul 07 2021 at 13:34):

I've been using S(x)S(x) so far to talk about the successor function. VN ordinals use S(x)=x{x}S(x)=x\cup \{x\}, and zermelo ordinals use S(x)={x}S(x)=\{x\}. All the theory is the same for either one, since all you need to make the argument work is for SS to be injective and not have 00 in the range

Mario Carneiro (Jul 07 2021 at 13:36):

For technical reasons VN ordinals turn out to be more convenient once you start doing more advanced set theory (VN successor of a transitive set is also transitive)

Huỳnh Trần Khanh (Jul 07 2021 at 15:22):

alright so it seems that I can play the Natural Number Game in ZFC... how about this? https://github.com/leanprover-community/mathlib/tree/master/archive/miu_language how can this be modeled in ZFC? like I mean the inductive predicate that tells whether or not a given string is derivable...

Huỳnh Trần Khanh (Jul 07 2021 at 15:23):

I don't even know how to define a list in ZFC!

Johan Commelin (Jul 07 2021 at 15:27):

You could encode [a,b,c,d] as {{a}, {a,b}, {a,b,c}, {a,b,c,d}}, or something like that.

Yaël Dillies (Jul 07 2021 at 15:32):

although it's rather defined as {{a}, {a, {{b}, {b, {{c}, {c, d}}} because we want to define it by induction using the pair

Damiano Testa (Jul 07 2021 at 15:32):

As with every definition in maths, you should take it very seriously, but, in Johan's encoding -- which normally goes under the name of Kuratowski's encoding, I remember that I had to think hard about the case in which there are repetitions among the elements of the list. In particular, you may want to define ordered pairs first, and then proceed to longer lists.

Johan Commelin (Jul 07 2021 at 15:38):

Ooh, I guess I messed up, right? With repeated elements you my encoding doesn't work.

Huỳnh Trần Khanh (Jul 07 2021 at 15:39):

so. many. subtleties. how can I construct stuff in ZFC without subtly messing stuff up, when even working mathematicians on here still get things wrong

Huỳnh Trần Khanh (Jul 07 2021 at 15:42):

hmm I'll check back later for answers to my questions, also are there any resources to help me learn this stuff without having to ask like 998244353 questions for every single thing I want to do in ZFC

like a website or something that teaches ZFC stuff

Huỳnh Trần Khanh (Jul 07 2021 at 15:43):

thanks in advance, as usual. I have to go to bed :in_bed:

Yakov Pechersky (Jul 07 2021 at 15:51):

You can read "Naive Set Theory" by Halmos

Damiano Testa (Jul 07 2021 at 15:51):

Note that the "mess up" is with the encoding, not with the concept! No mathematician should ever make a mistake with lists with repeated entries, except possibly in their definition!

Kevin Buzzard (Jul 07 2021 at 16:51):

I think it would be interesting to make a ZFC natural number game in Lean using the ZFC naturals

Kevin Buzzard (Jul 07 2021 at 16:51):

Of course once you've established recursion I guess it'll just reduce to the same thing

Brandon Brown (Jul 07 2021 at 19:35):

Why isn't there foundational pluralism in mathematics like there is in computer science? E.g. in CS/software engineering there are myriad programming languages (some of which I guess correspond to formal logics) and people typically choose the foundation (language) that is best suited to a particular problem. In mathematics there is just one de facto foundation/language, ZFC with FOL. But I imagine that some mathematical problems are more easily stated or solved in some other foundational system.

Jason Rute (Jul 07 2021 at 19:40):

ZFC is more of a theoretical foundation than a practical one. For the practical side, yes, there are a Myriad of options.

Yakov Pechersky (Jul 07 2021 at 19:42):

I don't agree that ZFC is comparable to languages. More like x86, or binary.

Mario Carneiro (Jul 07 2021 at 19:46):

Huỳnh Trần Khanh said:

so. many. subtleties. how can I construct stuff in ZFC without subtly messing stuff up, when even working mathematicians on here still get things wrong

The same way you do any formally intricate definition: you prove theorems about the stuff proving the key properties you expect. If you don't do this it's no better than an untested computer program.

Huỳnh Trần Khanh said:

hmm I'll check back later for answers to my questions, also are there any resources to help me learn this stuff without having to ask like 998244353 questions for every single thing I want to do in ZFC

like a website or something that teaches ZFC stuff

This is actually a very good use for the metamath website, which has fully worked out and hyperlinked proofs of all these facts from the axioms of ZFC

Mario Carneiro (Jul 07 2021 at 19:48):

Yakov Pechersky said:

I don't agree that ZFC is comparable to languages. More like x86, or binary.

ZFC itself, perhaps not, but ZFC + conservative extensions for definitions can certainly raise the level of discourse to traditional mathematical argumentation

Riccardo Brasca (Jul 07 2021 at 19:48):

Brandon Brown said:

Why isn't there foundational pluralism in mathematics like there is in computer science? E.g. in CS/software engineering there are myriad programming languages (some of which I guess correspond to formal logics) and people typically choose the foundation (language) that is best suited to a particular problem. In mathematics there is just one de facto foundation/language, ZFC with FOL. But I imagine that some mathematical problems are more easily stated or solved in some other foundational system.

I think that the reason is that practically mathematicians don't care at all about foundations. Someone told us that it is ZFC, maybe with the continuum hypothesis, but we really don't care doing "standard" mathematics.

Mario Carneiro (Jul 07 2021 at 19:52):

I'm not sure it's an exact parallel, but I see a sort of church-turing thesis for mathematical foundations: once you get past a certain very low bar all theories become interconvertible (modulo adding axioms to match up the consistency strengths of the source and target systems). Mathematics is presented using an implicit background foundation that fails to commit to any of these equivalent systems, and if pressed people will pick one like ZFC but that doesn't mean they were thinking about it at all before you ask the question

Mario Carneiro (Jul 07 2021 at 19:54):

ZFC has the advantage that it is really simple to define, which makes it appealing for metalogical analysis / "set theory". Type theory is more complex but comes with advantages for automation (e.g. type checking), so it is more common among computer proof assistants

Johan Commelin (Jul 07 2021 at 20:08):

Also, I think the stack is a lot larger in maths. Going with the PL analogy, Lurie wrote a "library" on higher topos theory. It's several thousand pages. If you want to use a language that is different from his, but you want to use higher topos theory, you first need to port that library.

As pointed out above, in practice informal maths is foundation-agnostic. But when you start formalizing, this library porting becomes a serious issue.

Huỳnh Trần Khanh (Jul 08 2021 at 04:19):

wait I'm extremely confused... why is the Naive Set Theory book titled so? it describes ZFC...

Huỳnh Trần Khanh (Jul 08 2021 at 04:20):

ZFC is not naive by any stretch of the imagination...

Mario Carneiro (Jul 08 2021 at 04:21):

I haven't looked at the book in detail but it probably means that it isn't dealing at the edges of the system where you have to worry about how ZFC avoids the contradictions in unrestricted comprehension

Mario Carneiro (Jul 08 2021 at 04:21):

Note that a lot of category theory is also "naive" in this sense - there are universe issues to be handled, but as long as you don't test the limits you can kind of pretend they don't exist

Mario Carneiro (Jul 08 2021 at 04:23):

I am reminded of a certain formal system that shall not be named, which implemented naive set theory, and the solution the developers had for avoiding contradictions was to simply not write down the russell set

Kyle Miller (Jul 08 2021 at 06:02):

The title of Halmos's book is sort of a joke -- it rigorously goes through the axioms of ZFC, and the only thing that's "naive" is the intended audience with regards to knowledge of foundations, and also it doesn't go into detail about things like what exactly is a logical formula. (It definitely expects mathematical maturity though.)

Kyle Miller (Jul 08 2021 at 06:09):

Halmos explains the axiom of restricted comprehension (here called the axiom of specification, which he helpfully tells you is often referred to as Aussonderungsaxiom), then shortly after proves "there is no universe", mentioning how in pre-axiomatic approaches the Russell paradox would arise.

Kyle Miller (Jul 08 2021 at 06:22):

Actually, he explains the title in the preface. More accurately, "it is naive in that the language and notation are those of ordinary informal (but formalizable) mathematics," and also that it works with set theory as if there were a single theory of sets.


Last updated: Dec 20 2023 at 11:08 UTC