What's your least favourite axiom? Mine's powerset.

@j If we're not only talking about ZFC then in decreasing order of bad:
Choice, Countable Choice, LEM, K

@j Axiom K is a type theory thing. It basically says that two things can only be equal if they are the same. That sounds like a tautology, and in ZFC it's pretty uninteresting, but in some systems (homotopy type theory) you want to allow a more subtle notion of equality. If you impose axiom K it immediately collapses all of that structure. It's particularly annoying because the pattern matching in a lot of theorem provers (Agda) assumes K, so you have to do some tricks to make HoTT work in them.

@kwarrtz Ah, it sounded like a type theory thing. I haven't had the time I'd like to look into HoTT. Any recommendations for resources?

I'm uncomfortable enough with ZF(C) as a basis for modern maths, that I'm not sure I could handle yet another system right now.

@j Really the only introductory text available right now is the HoTT book by UFP ( It's quite good, though obviously pretty dense. I'm not an expert by any means, but I'll also be happy to try to answer and questions.

Being comfortable with set theory or formal logic isn't necessarily a prerequisite for learning HoTT. In fact, I'd say if you've ever done any (especially functional) programming, type theory may actually be more intuitive than ZFC.

@kwarrtz Thanks :), I'm more than comfortable with Haskell, so that book might be fun; although it'll probably be late May by the time I get around to it. I'm quite busy this semester.

@kwarrtz I'm taking a module on axiomatic set theory this semester (focusing on ZFC and Cohen's proof of the independence of the continuum hypothesis. If I get a chance I'll glance through the book you've suggested. It might be useful to have a different philosophical perspective.

@kwarrtz ) closing bracket for the lispers and those with mild ocd.

@j I feel kinda bad that I didn't even notice...

@j I think that could be really rewarding. Also, that sounds like a fun class! I've always heard forcing is a pretty tough concept though

@kwarrtz Luckily, while forcing will be covered during the class, it won't be on the exam.

@kwarrtz I've one of the stranger course loads in the maths department at the moment:

"Axiomatic Set Theory", "Group Representations", "Quantum Filed Theory", "General Relativity", and "the Standard Model" are my modules this time around.

Bizarrely enough "Set Theory" and "General Relativity" are my favourite modules right now.

It's still a far cry from last semester where I kinda took an introductory haskell module that I could've done in my sleep to drag my grades back up.

@j Dang, that schedule sounds awesome. I'm still stuck taking intro physics classes and gen ed reqs right now. On the bright side, I should finally be able to start taking some grad classes next year. I have modern algebra and (hopefully) algebraic topology lined up on the math side, and if I'm lucky I might be able to sneak in a graduate mechanics or relativity course.

@kwarrtz I was actually going to be taking either algebraic topology or geometric this semester, but I switched to set theory just before christmas, after a bad experience with one lecturer. I'm not in the US, so no gen-ed requirements. Up until this year, I was in a theoretical physics degree, which required me to do some lab work.

I finally switched to a maths degree program this year, which means I no longer have to deal with the terrible lectures of the physics department. (No more labs!!)

@j Ah, see I'm in a lab right now and I actually rather enjoy it. I agree with you about the lectures though. The physics curriculum at my university is pretty terrible. Math actually isn't that much better, but at least it's easier to take graduate level classes (which, if you couldn't tell, is exactly what I plan to do)

@kwarrtz Where I am, there was a huge difference in the quality of lectures given by the maths department and physics department.

I'm lucky to be a student of a majority ex-USSR maths department. [The stories are the only thing that makes 3 hours of QFT on a tuesday afternoon bearable]

You might enjoy this essay by Arnol'd: (Mathematics is the part of physics where experiments are cheap.)

@j Hm, I disagree rather strongly with a lot of this essay. In my opinion, mathematics is not a science at all. Science is the act of building models to explain and predict measurements (whatever that may mean), There are no measurements in math, or external truths to compare it against. It is frequently inspired by physical observations, but it has no "reality". It's just a tool to help humans think about things. (1/2)

@j I do agree that geometric intuition is an underrated pedagogical tool, but his disdain of abstraction feels otherwise unproductive.

@kwarrtz Arnol'd is an idol of mine (please, regardless of how this conversation pans out check out "Mathematical Methods of Classical Mechanics"), so I love any disagreement with this essay in particular.

I believe that mathematics is nothing more than an interpretation of those models that you describe as being built by science.

(Formalism+finitisim ftw!)

Mathematics is *useful*, but it's truth-hood is open to debate.

Show more

@kwarrtz What courses/modules are you taking this semester? I'm always curious as to how 3rd level educations works outside of ireland.

@j I'm taking a pretty light load this quarter. I'm taking the second part of an introductory real analysis series, along with a very very basic intro to quantum and a couple of credited "self-study" activities. In particular, I'm part of an algebra reading group to try to prepare for the grad sequence and I'm working in a condensed matter research lab.

@j All of them. Use an axiomless deduction system

The infinity axiom seems a lot weirder than the power set axiom. Although I wouldn't say I feel any strong dislike against it.

@abs See, I can at least conceptualize a countably infinite set. The idea that a process can be repeated indefinitely is amenable to even the most ardent finitists. Powerset involves accepting the powerset of a countable set, along with the powerset of that set, along with the powerset of that set, etc. An unimaginably large collection of sets, that I find hard to justify philosophically.

(I've other reasons to be uncomfortable with powerset, but this is the easiest to express in a toot)

I agree that a potentially infinite process (always generating the next natural number) is unproblematic finitistically. Concluding that all of its intermediate results should therefore exist, bundled up into a set isn't, though. That's the point where Hilbert, for example, would draw the line.

Avoiding higher cardinalities seems hard once you have countably infinite sets because even just the set of functions from the natural numbers into the two-set is uncountable. You would have to strongly identify functions with some kind of countable "programming language" to get around that.

On the other hand, if you were to remove the axiom of infinity, the power set axiom becomes pretty unproblematic, I think. This is not the case for the infinity axiom if you remove power sets, as you still have to justify why an actually infinite object should exist.

@abs @j What about the axiom of infinity as defined in ETCS or other categorical set theories? In these, the set of natural numbers is characterized exactly by the property that it is universal with respect to recursion. Since this definition references only the infinite *process* itself, would you consider it less problematic from the perspective of finitism?

@kwarrtz Yes I think that would be totally acceptable finitistically. (You’re referring to this, correct?)

There is a good paper by Tait that argues this point really well.


@abs That’s exactly what I was referring to, yes.

I’ll have to take a look at that paper. I didn’t realize anyone else had thought about this before (it was just a random thought that struck me reading your post) but I’m not surprised

@kwarrtz @abs Wait, what? The Axiom of Infinity in ZFC is almost exactly the literal statement that there's a natural numbers object.

Yes. I'm not quite sure what you're question is, though.

@abs @kwarrtz I don't see why a finitist would object to a natural numbers object in ZFC but not to one in ETCS.

Oops, you're right. I was focusing too much on the printive recursion. Even the way ECTS does it would not be acceptable because you still have a collection of infinite size.

@epicmorphism Regularity has always come across to me as a last-ditch effort to rid naiive set theory of contradiction.

@j @epicmorphism I don't understand this take. Could you explain? Remember that the intuitive idea of naive set theory does allow non-regular sets so I don't see how regularity is an attempt to formalize naive set theory.

@axiom @epicmorphism I'll have to get back to you about this particular take. I've a couple of days of assignments to catch up on, as well as a few nights needed to figure out exactly what I meant when I tooted that. (Alcohol makes me a finitist)

Sign in to participate in the conversation

A Mastodon instance for maths people. The kind of people who make \(\pi z^2 \times a\) jokes. Use \( and \) for inline LaTeX, and \[ and \] for display mode.