You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Morgan Rogers (he/him) (Aug 08 2024 at 10:44):@Madeleine Birchfield it's fascinating to me that your attitude to non-constructive axioms is determined by sociological considerations like this. I haven't seen enough people think about that kind of influence on their reasoning principles.
Madeleine Birchfield (Aug 08 2024 at 16:10):Morgan Rogers (he/him) said:
Madeleine Birchfield it's fascinating to me that your attitude to non-constructive axioms is determined by sociological considerations like this. I haven't seen enough people think about that kind of influence on their reasoning principles.
It's more difficult in Ireland though because their curriculum does actually teach classical naive set theory in their junior cycle. I might actually have to assume that the sets form a Boolean pretopos while there and talking to the average Irish person.
Madeleine Birchfield (Aug 08 2024 at 16:20):But yeah, fundamentally when I encountered constructive mathematics, I ran into the philosophical question of "what exactly is mathematical truth"? Because there are mathematicians who assume or can prove that excluded middle is true, mathematicians who can prove excluded middle is false, and mathematicians whose foundational assumptions are independent of excluded middle. And moreover, that these mathematicians tend to cluster into different communities who sometimes have trouble communicating with each other due to their different beliefs. So the sociological content is already there.
However, most of this discussion took place in higher mathematics, and is largely disconnected from mathematics as experienced by the rest of the world. This is a big blind spot in constructive mathematics - some constructive mathematicians assume that LPO cannot be proven or false in their professional work and then assume LPO or analytic LPO is true when tutoring their own children in the real numbers, and then when you probe their philosophy of mathematics they claim not have a pluralist philosophy, because they implicitly assume that you are talking about their professional work.
Madeleine Birchfield (Aug 08 2024 at 16:57):Most maths teachers teach from a curriculum which states that all of these mathematical statements are facts about mathematics, without even knowing that there are huge philosophical debates over determining which statements are facts and which are mere opinions stemming from the underlying axioms assumed in the foundations. The Munchhausen trilemma in epistemology already shows that no mathematical statement can be proven to be absolutely true, so claims of which mathematical statements of true turns into sociological arguments - they're true because mathematical tradition or some authority states it's true or derivable from axioms which are claimed to be true, or they're true because assuming that it is true is useful for some application of mathematics in society, and so on.
Notification Bot (Aug 09 2024 at 09:08):5 messages were moved here from #learning: questions > Different types of non-constructive proofs by Morgan Rogers (he/him).
Morgan Rogers (he/him) (Aug 09 2024 at 09:43):I love thinking about this, especially how societal attitudes have developed over time as the domain of mathematics has expanded.
Regarding the Münchhausen trilemma -- this was my first time encountering it, and my first instinct is to wonder whether it misses any possibilities -- I am reminded of the time a couple of years ago where I was thinking about modus ponens as a reasoning principle that is often taken for granted, in contrast with other principles which tend to be included or not from logical frameworks more liberally.
Madeleine Birchfield (Aug 09 2024 at 15:10):The other thing I want to bring up is notation.
Constructive mathematicians who do not accept LPO (i.e. Cauchy-analytic LPO) have to come up with new notation for the various different concepts which are no longer provably the same. For example, the notion of apartness as distinct from inequality , or the notion of binary supremum of two Cauchy real numbers as distinct from the maximum of two Cauchy real numbers: the latter is only a partial binary function defined on in constructive mathematics.
Apartness and inequality are the same iff Markov's principle holds, and the maximum partial function is a total function which coincides with the binary supremum iff LLPO holds. But very few people in the real world use apartness or the suprema, they all use inequality and the maximum.
Morgan Rogers (he/him) (Aug 09 2024 at 15:18):Sure, and the introduction/elimination rules determine the behaviour of logical connectives. However connectives come with philosophical baggage, indicated by the name "implication". Why should that be the elimination rule for implication?
Morgan Rogers (he/him) (Aug 09 2024 at 15:18):oh you deleted your post
Madeleine Birchfield (Aug 09 2024 at 15:19):Morgan Rogers (he/him) said:
oh you deleted your post
Yeah because it was wrong, it is the converse of modus ponens that is the introduction rule of implication.
Morgan Rogers (he/him) (Aug 09 2024 at 15:20):Indeed, it's the elimination rule
Madeleine Birchfield (Aug 09 2024 at 15:23):I think there are logics out there in which modus ponens does not hold. For example, coherent logic and geometric logic do not have general implication and so modus ponens cannot even be expressed in coherent logic or geometric logic.
Morgan Rogers (he/him) (Aug 09 2024 at 15:57):I hadn't really thought about this before, but it should be possible to exploit that observation to yield a simple counterexample, in the following sense. The subobject lattices in a Grothendieck topos are Heyting algebras: implication is definable and interpretable as usual (inc. modus ponens) in the internal language of a topos. The reason that coherent and geometric logic are considered is that general geometric morphisms do not preserve the implication, so that when one considers the theory classified by a given topos, the models need not satisfy sequents that are provable in the first-order extension of the theory (so hold in the universal model). The most famous example of something like this is the fact that the universal local ring is a field; I'm struggling to find Ingo Blechschmidt's exposition of that, so I can't remember the precise formulation of " is a field" that's relevant here.
So it's plausible that one can have in the first-order extension of a coherent theory but in some model of that theory? Or maybe the restricted case of elimination for the case where the left-hand side of the sequent is always holds and one needs a more sophisticated set-up?
Kevin Carlson (Aug 09 2024 at 21:04):I'm confused about how this kind of question interacts with the consistency theorem. Aren't the sequents holding in the universal model just the ones that can be proven syntactically? Oh...I guess the universal model of a coherent theory satisfies those coherent sequents that can be proven syntactically, but might satisfy first-order sequents that can't, is that how you avoid breaking consistency?
Morgan Rogers (he/him) (Aug 10 2024 at 11:48):Exactly
Morgan Rogers (he/him) (Aug 10 2024 at 11:49):I should think a bit harder about this and produce a more specific example. Maybe next week.
Madeleine Birchfield (Aug 25 2024 at 22:32):Madeleine Birchfield said:
I don't have a problem with not accepting the full excluded middle, or the fan theorem, etc because formal logic, set theory, locales, topological spaces, formal topologies, uniformly continuous functions, the Heine-Borel theorem, etc aren't taught to the general public in high school algebra.
They do teach probability in high school algebra. However, for a finite sample space, the textbooks require that an event, usually defined as a subset of the sample space, is a finite set itself, which is only true if and only if excluded middle holds.
So by the logic in the original post I might as well just accept excluded middle, because otherwise I'll run into the problem that I'll have to tell the average person that their textbooks are wrong, and either not all subsets are events or not all events have well-defined probabilities or something similar.
Peva Blanchard (Aug 26 2024 at 07:01):oh, does it mean that there exists a model where some finite set has a subset that is not finite?
Morgan Rogers (he/him) (Aug 26 2024 at 08:47):Madeleine Birchfield said:
So by the logic in the original post I might as well just accept excluded middle, because otherwise I'll run into the problem that I'll have to tell the average person that their textbooks are wrong, and either not all subsets are events or not all events have well-defined probabilities or something similar.
It's true that not all subsets of a measurable set are measurable; it's also the case that measurable subsets are required to be complemented. Are complemented subobjects of finite objects finite?
Madeleine Birchfield (Aug 26 2024 at 10:34):Morgan Rogers (he/him) said:
It's true that not all subsets of a measurable set are measurable; it's also the case that measurable subsets are required to be complemented. Are complemented subobjects of finite objects finite?
They should be the ones which satisfy for subset of finite set - i.e. the decidable subsets of finite sets, which are finite.
Madeleine Birchfield (Aug 26 2024 at 10:42):So everything in the textbooks ought to go through for probability on finite sets, except that we would have to define an event as the decidable subsets of the finite sample space , and the space of possible events as the function set rather than the power set .
Kevin Carlson (Aug 26 2024 at 21:17):Peva Blanchard said:
oh, does it mean that there exists a model where some finite set has a subset that is not finite?
Yeah, because proving that a subset of , ie a truth value, is in bijection with some natural number, ie with or with , is exactly the same as proving that, as a truth value, is either true or false.
John Baez (Aug 26 2024 at 21:21):Some constructivists say a set is 'subfinite' if it admits a monomorphism into a finite set.
Madeleine Birchfield (Aug 27 2024 at 09:18):Let me say something about the other non-constructive principle assumed in classical mathematics - the axiom of choice.
The axiom of choice says that the indexed product of every family of inhabited sets is itself inhabited, or that there exists a section for every surjection. But even with the axiom of choice, one would still have to deal with the difference between an inhabited set and a pointed set, the difference between a split surjection and two functions which form a section-retraction pair. This doesn't quite matter as much in foundations using the traditional interpretation of logic because most of the theorems there are expressed using the existential quantifier in first-order logic, so a set being inhabited is sufficient most of the time.
But as somebody who takes the [[BHK interpretation]] seriously, I ultimately view choice principles as an attempt to make the traditional interpretation of the existential quantifier sufficient to imply the BHK interpretation of the existential quantifier, so that one can simply use the traditional interpretation of logic everywhere. In light of this, the axiom of choice itself isn't sufficient - I would instead prefer the axiom of global choice or a choice operator, something which would allow one to choose an element of a set from mere existence of an element of the set.
For certain versions of global choice (i.e. being able to construct an element of or ), the internal versions of the double negation law and the law of excluded middle are just those versions of global choice restricted to subsingletons, and the internal versions of Markov's principle and the limited principle of omniscience are just those versions of global choice restricted to semi-decidable subsingletons.
Madeleine Birchfield (Aug 27 2024 at 09:32):One downside to global choice is that in dependent type theory, global choice, even if restricted to sets, implies that every type is a set, while the usual axiom of choice doesn't. While this is fine for classical set-based mathematics (see the Lean proof assistant for an example), if I were doing something with higher groupoids such as category theory in dependent type theory I would want to have access to the intrinsic higher groupoidal structure of types rather than have to postulate all the structure and axioms from scratch.