@XanderHenderson: Please take note of the spammer whose comments I have moved to trash. Thanks!

@Cure You may be interested in the fact that some people have looked at ZFC over FOL without equality. For example:

Let's use FOL− to denote FOL without equality. The general idea is that you can drop equality from the inbuilt primitives and add "=" as a binary relation and add axioms stating that = is an equivalence relation, and most importantly add axioms stating that every non-logical symbol respects =. That produces an FOL− theory that syntactically behaves the same way as the ordinary FOL theory, but in general it will have more models than the ordinary theory, as per Carl's answer.

For example if you want PA over FOL− those axioms stating respecting of = would include "∀k,m,n ( m=n ⇒ k+m=k+n ∧ k·m=k·n )".

@user21820 Would you mind giving me your thoughts on this?

math.stackexchange.com/questions/3755965/…

Keep in mind this question was before I got used to the proper terms

I'm more interested in Somos' remark. I'm not sure what they're referring to.

@Threnody Sure. Give me a moment. And yes I understand that that post of yours was quite some time before you actually learnt FOL, so I will not focus on that but rather just what Somos is talking about.

@user21820 What does FOL stand for?

@Safdar First-order logic.

@Threnody: Basically Somos is saying that historically mathematics had not been carried out in any formal system whatsoever, so in that specific sense your question is based on a false premise (that mathematics is done that way).

However, Somos is not really correct that it leads to nonsense... At least, not in the way he/she meant it...

It is true that modern mathematics can be done within foundational system, and a foundational system must have a proof verifier program, or equivalently its theorems must be computably enumerable. This does imply that foundational systems cannot use any truly infinitary logic. But proving this fact requires understanding of the incompleteness theorem!

Let's assume that PA is consistent. Then for any specific string x, we can check that x is not a proof of "0=1" over PA. And PA can prove that too. But PA cannot prove ( every string is not a proof of "0=1" over PA )...

So technically speaking it is impossible to develop any field of modern mathematics that is not expressible in a formal system. That is where Somos is wrong. That idea on your part does not lead to nonsense.

The only real 'nonsense' in your post is when you say "What I think is happening is there is an implicit ...alluding? to infinity by employing the ... symbol - but this is just what the author chooses to believe if you will.". Now I know this was before you understood formal FOL deduction, so I think you know now that we very well can reason about strings from an infinite alphabet, but this reasoning is done in a meta-system MS that is of course an ordinary computable formal system.

We also can reason about infinitary formulae not as strings but rather as sets. (In MS) An infinitary conjunction can be defined as a set of formulae (just as the SEP article does). What can you do with such stuff? That's up to whoever wants to play with such things to define it. All natural notions of infinitary logic with infinite conjunctions or disjunctions fail to be practically useful unlike FOL.

Using the example from above.. Take any computable formal system S that interprets TC/PA−. Then S proves each member of the set { x : x is a string that is not a proof of "0=1" over S }. If S has infinitary logic L[ω1,ω], then it would prove the 'infinite conjunction' of that set and hence also prove itself consistent, which is impossible. Therefore S cannot have L[ω1,ω].

By the way, it is worth noting that the presence of ω1 in the usual definition of L[ω1,ω] is an illusion; our MS needs only to be able to handle countable sets, so ACA suffices to define and prove the above stuff about L[ω1,ω].

ZFC of course allows us to talk about L[α,β] for even bigger uncountable α,β, but at that point it is just a set-theoretic construction with no real-world implications.

@user21820 Noted. Thank you. I'll see what can be done.

@XanderHenderson Thanks! I'm glad to have you in here to keep an eye on things. =)

@user21820 Thank you for your reply :)

@Threnody You're welcome!

@Cure - There's no reason one way or the other to either eschew or keep the intuitive meaning of membership here. There's no sensible meaning you can imbue to a relation that will make false the things that hold of all relations, so to say it does mean "if x=y then x and y have exactly the same members" shouldn't cause any conceptual trouble. Of course a set has the same members as itself, no matter what membership might mean.

Oh yea, that too. I completely missed that point. =)

After all, the whole idea of "x=y" in FOL is that x,y are the same object. (We're not talking about some odd type theory here. =P)

@user21820 - I blame early math education; this is something I had to relearn early on because my impression for most of my primary education had been that n=m meant something like "they're the same size", whatever that means.

@MaliceVidrine Yea I agree with you blaming early math education. =D

It's perhaps a non-trivial job to teach students the difference between an object and a variable or expression referring to it.

I think it is. I've seen the confusion crop up even for early graduate students.

Even one instance of "how can we have uncountably many sets when we have only countably many variables?" To their credit, though, they seemed to understand the distinction quickly when it was pointed out.

@MaliceVidrine Actually though, I could well enough believe that my intended model of ZFC is countable...

Indeed, and that will be a whole other can of worms. It'll be interesting to see how they respond to L-S!

I just wish we'd hurry up and get to the incompleteness stuff, that's really all I need this class for. I'm trying to view it as a logic vacation in my schedule, but I'm also impatient :P

Hahaha.. Did I tell you that some logician I was talking to last year or so told me that Skolem thought his theorem would show how unsatisfactory set theory was...

Who knew that instead of his 'desired result', people generalized his theorem to get upward LS and even more 'preposterous' uncountable models of consistent theories...

I've heard that before! Boy did that backfire.

That reminds me, I got sidetracked by administrative nonsense and forgot to finish this model theory exercise. It's both horrible and I think I know how to solve it, which is a rare combination!

But it does give one serious food for thought when looking at strength of axioms in the foundational system. For example, AC can be seen to add nothing if your intended model is countable! For replacement, however, if we only have definable sets at each level of the cumulative hierarchy, we still have a definable uncountable well-ordering, but this well-ordering is not literally uncountable but just that we don't have a bijection to ℕ, so it makes no sense to climb the hierarchy along it!

So it's kind of amusing that people keep focusing on AC but conveniently Replacement sneaks away. Truly, AC has replaced Replacement as the Axiom of Concern.

(Chang & Keisler 5.1.3: Let $\mathcal{M}$ be $\beta^+$-saturated, and $X\subseteq M$ such that $||\mathcal{L}||\leq|X|\leq\beta$. Then there is a $|X|^+$-saturated elementary submodel of $\mathcal{M}$, containing $X$, of power at most $2^{|X|}$.)

Replacement is definitely weirder than I think people give it credit for, and I've been surprised at my reaction to it sometimes. My instructor last class used replacement to show the existence of the Cartesian product of a pair of sets, and I had an automatic cringe reaction.

Hahaha... Why not the usual double power set?

It's clearly the wrong way to prove the existence of products even if it's a fast way :P

Ah..

That's what I asked!

Surprisingly, his answer was he'd never thought of doing it that way.

I think you're fortunate though! When I took the set theory course in my undergraduate days, I did not know anything about ZFC, and just followed along.

Well, Kunen used to work here, and we're using his text, so the set theory is very much at the forefront.

Although the professor who taught that was in fact careful enough to point out when he used something and whether it was actually necessary (he even stated upfront that he was using MK rather than ZFC just for convenience), I didn't realize until this year that a lot of key results could be gotten in mere ZC, because he did them only after the whole ordinal business.

It's a funny text. It kind of leads with set theory and then develops facts about model theory and proof theory.

@MaliceVidrine By the way, do you want me to try that model theory problem? I am totally rusty so I may just flop on it. On the other hand, I may be able to give you some ideas that you may be able to get to work.

Oh, no, I was just sort of dropping it here in case any interested parties wander through and want to poke at it. I'm like 95% sure I have a solution.

I just hate gong "Oh, I forgot about this problem I'm working on" and then not saying anything about the problem :P

@MaliceVidrine Ah. =)

I think quarantine has made me even worse at (not) saying things that normal people would(n't).

@MaliceVidrine Why do you say that? I don't find what you say abnormal at all.

(Maybe I'm abnormal too, who knows.)

Well that's good. I'm passing :P

I get "what the hell" looks when talking to people in person more often than I'd expect, so who knows how it translates online.

Anyhow.

One thing I would change about the treatment of set theory in this class would be talking about proper classes.

More often I wish people teaching pure set theories would just say "they don't exist, they're a figure of speech". Not "they're too big to be a set, we can't quantify over them"

The substantive talk about proper classes in the context of ZFC just causes confusion if people don't already sort of understand the semantics better.

@MaliceVidrine Hmm.. Maybe you're talking to the wrong crowd? =D

Like I won't talk set theory or anything more than really really basic logic to most people in real life.

@MaliceVidrine Oh that "too big" thing is a really interesting escape from the philosophical problems. Interestingly, that same set theory professor that I mentioned above taught me used that notion of "too big" to 'handwave justify' replacement.

Something like, anything that is not too big is a set. Lol!

(Of course, as you noted, we should think about classes as just definable predicates.)

In an ideal world, I'd respond to that kind of business with Wang's construction to take any pure set theory and produce a conservative class/set theory extension that satisfies impredicative comprehension.

Though those people who like MK will come after you for saying they don't exist.

The models of which almost always include proper classes that are subclasses of sets :P

@MaliceVidrine Hang on, what is that? I have something like that in my type theory but didn't know such a thing existed in set theory.

It's a really simple thing: the theory is given by taking all of your comprehension instances and restricting them, in the new theory, to formulas whose free and bound variables are all restricted to sets.

That is, in general, classes can't be used as parameters in constructing sets at all.

I forget the paper Wang originally pointed this out in. But it was actually a paper about Quine's other set/class theory ML.

The revised edition of Quine's Mathematical Logic reformulates ML as what is essentially Wang's conservative extension applied to NF.

I have universal type obj and a type of all types called type and type ⊆ obj. I also have a type of all classes called class, where a class is a type with boolean membership, and obj ∈ class but ( type ∈ class ≢ true ). So every type is a subclass of obj but they don't form a boolean lattice unlike classes.

This is what I meant by "something like that in my type theory".

Interesting!

@MaliceVidrine This one?

Yes! Pretty sure that's it.

Of course, Quine still forgot to take care of one detail in ML, that I always think is funny: he didn't make sure that the natural numbers, as he defines them there, are actually a set. :P

Haha..

He defined it as the intersection of every class that contains 0 and is closed under successor. Spends a chapter developing facts about the real numbers, but none of it actually works properly.

That is one big blunder!

In fact, if the class he describes were a set, it would correspond to an incredibly strong induction scheme in NF.

I'll cut him some slack; he was not first and foremost a mathematician. And NF is still a pretty cool idea.

For me, I just take ℕ as given. I can't really understand people who want to make it convoluted to construct ℕ when ultimately all they are going to do is to add enough axioms to ensure they can construct it.

@MaliceVidrine Yea the idea of syntactic restriction to enforce type levels is interesting. Though for the same reason I don't buy NF, though I'm fine with NFU+Inf+Choice. =D

I understand the motivation; ontological economy. And it's a neat trick that you can implement the natural numbers as sets. But yeah, ultimately it has diminishing returns. I'm still a set theory fan as an object of study, but for a metatheory I'm increasingly fond of higher order type theory with a natural numbers object.

@MaliceVidrine That's indeed true. While I don't like ZFC, I do admit it's an elegant theory that so far hasn't produced ⊥.

Maybe it's just a long-running but eventually halting enterprise.

=D

heh

@Tim You have been asked repeatedly to keep the conversation on-topic and civil. Please stop harassing the users of this channel.

@MaliceVidrine That's interesting. I'm taking a class and the teacher says precisely that — classes are collections of elements too big, and the axioms impose restrictions on how big classes can be. From what (I thought) I understood, a set was a class with restrictions that make sure it is small enough.

@Cure - If you're in a theory like NBG or MK this can be a precise statement, but in ZFC it's a guiding intuition. But purely formally a statement like "there is some x such that x is a proper class and for all y, if y is a set it is smaller than x" is not something even expressible in the language of ZFC.

@user21820 FYI: math.meta.stackexchange.com/questions/32539/…