how zfc works

Stream: general

[Huỳnh Trần Khanh]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Huỳnh Trần Khanh]

and its name is omega or aleph null...

[Eric Rodriguez]

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

[Eric Rodriguez]

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):

$\{ x \in X\ |\ \forall s \in x, s \in X \land \forall s t \in x, s = t \}$

[Mario Carneiro]

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

[Eric Rodriguez]

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

[Mario Carneiro]

The usual approach is to define what it means for a set to be "inductive", i.e. $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 $X$)

[Mario Carneiro]

$\omega$ is in fact not composed of singleton sets

[Eric Rodriguez]

I see, big oops then

[Huỳnh Trần Khanh]

that explains why I'm so confused by the predicate

[Huỳnh Trần Khanh]

:joy:

[Jason Rute]

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

[Mario Carneiro]

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]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

that's terrifying and bad

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Huỳnh Trần Khanh]

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

[Mario Carneiro]

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)$ holds and $\forall x,(P(x)\to P(S(x)))$, then $\{x\in \omega|P(x)\}$ is an inductive set, so therefore $\omega\subseteq \{x\in \omega|P(x)\}$ and hence $P(x)$ holds for all $x\in\omega$

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Johan Commelin]

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]

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]

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]

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

[Huỳnh Trần Khanh]

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]

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]

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

[Yakov Pechersky]

You can read "Naive Set Theory" by Halmos

[Damiano Testa]

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]

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

[Kevin Buzzard]

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

[Brandon Brown]

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]

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

[Yakov Pechersky]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Huỳnh Trần Khanh]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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.