Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: One universe as a foundation & friends

Federica Pasqualone (Aug 21 2024 at 22:18):

Strongly encouraged by @John Baez , here it is the new engaging discussion topic for today. One can think perhaps that it is a bit old-fashioned (1969), but actually it should be a good one... And I love the word "Universe" . Anyways, I was reading https://link.springer.com/chapter/10.1007/BFb0059147 by Saunders Mac Lane and some other great considerations of Feferman and wondering: Is this the end of the story, namely ZFC with a universe? What happened after 1969?

Madeleine Birchfield (Aug 21 2024 at 22:26):

Well, Martin-Löf developed his dependent type theory in 1971 - 1976 and then people showed in the 2010s that the types in his type theory actually model infinity-groupoids.

Federica Pasqualone (Aug 21 2024 at 22:27):

Indeed, and what about predicativity?

Madeleine Birchfield (Aug 21 2024 at 22:29):

Federica Pasqualone said:

Indeed, and what about predicativity?

Martin-Löf's type theory as usually presented is usually predicative in the sense that power sets cannot be constructed. But it's not the same kind of predicative as that found in classical mathematics. They usually accept function sets but not excluded middle, so function sets do not imply power sets.

With universes $U$ the type theory would have "power sets" defined relative to $U$ but the "power sets" themselves would still be external to $U$ so would behave more like power classes from set theory.

Federica Pasqualone (Aug 21 2024 at 22:32):

I am wondering if we want to elaborate a little more on the notion of predicativity, maybe there are also people less familiar with logical foundations, idk.

Federica Pasqualone (Aug 21 2024 at 22:35):

Ok, I will do it - but guys do not be shy to contribute here and/or ask!
As I learned it, remember the paradoxes after Dedekind & Cantor promoted their set theory? They arise more or less all from predicativity issues! or better: impredicativity!

Madeleine Birchfield (Aug 21 2024 at 22:37):

About predicativity I'll quote a conversation I had with Josselin Poiret from another thread:

Madeleine Birchfield said:

In the context of predicativism I think one has to make a distinction between "power sets exist but aren't small" and "power sets don't exist in the theory at all". I don't really consider the former to be predicative because you can still do everything you can in impredicative mathematics, only with the additional bureaucracy of keeping track of size or universe levels.

The latter is much more restrictive since certain constructions (i.e Dedekind reals via Dedekind cuts) aren't really possible without power sets.

Josselin Poiret said:

Madeleine Birchfield said:

I don't really consider the former to be predicative because you can still do everything you can in impredicative mathematics, only with the additional bureaucracy of keeping track of size or universe levels.

you cannot: see what I mentioned about strong normalization of System F, or the existence of complete lattices

Josselin Poiret said:

impredicativity manages to bump up the logical strength of the theory

Madeleine Birchfield said:

Josselin Poiret said:

you cannot: see what I mentioned about strong normalization of System F, or the existence of complete lattices

Complete lattices in Agda/Coq/book HoTT are a size issue as well, they are defined complete relative to a universe in the same way that Grothendieck toposes are defined to have all coproducts relative to a universe.

Josselin Poiret said:

while you might see it as just a size issue it does end up affecting logical strength, and this restriction is IMO exactly the one of predicativism: one cannot build possibly self-referential objects, ie. objects quantified over what they themselves are

Federica Pasqualone (Aug 21 2024 at 22:38):

The business, roughly, is all about self-referential definitions ... do you remember Russell's paradox? Anyone?

Peva Blanchard (Aug 21 2024 at 22:40):

I'm only familiar with the "informal" definition of impredicativity: self-referencing definition. E.g. $X = \{ x ~|~ x \not\in x \}$.

Federica Pasqualone (Aug 21 2024 at 22:41):

That's exactly what all the enterprise is about here! Great!

Madeleine Birchfield (Aug 21 2024 at 22:41):

Martin-Löf's original type theory from 1971 had a universe which contained every single type in the type theory, including itself.

Then somebody proved a type theoretic version of the Burali-Forti's paradox from the universe which contained itself, and Martin-Löf had to modify his theory so the universe doesn't contain itself.

It was later shown that if the type theory has W-types and a single universe containing every single type, then one can use the W-type for the universe to reconstruct the traditional membership-based Russell's paradox.

Federica Pasqualone (Aug 21 2024 at 22:42):

There is also a little other ingredient @Madeleine Birchfield , do we want to introduce some intuitionistic logic? You sort of cited it already .. don't you?

Madeleine Birchfield (Aug 21 2024 at 22:44):

Yes, so intuitionistic logic is logic done without the excluded middle.

Federica Pasqualone (Aug 21 2024 at 22:45):

d.h. (= i.e.) without the rule $A \lor \lnot A$

Federica Pasqualone (Aug 21 2024 at 22:46):

And could you also elaborate a little more for our audience about it? and its implications here?

Peva Blanchard (Aug 21 2024 at 22:46):

How does intuitionistic logic relate to im/predicativity?

Federica Pasqualone (Aug 21 2024 at 22:50):

Madeleine Birchfield said:

Federica Pasqualone said:

Indeed, and what about predicativity?

Martin-Löf's type theory as usually presented is usually predicative in the sense that power sets cannot be constructed. But it's not the same kind of predicative as that found in classical mathematics. They usually accept function sets but not excluded middle, so function sets do not imply power sets.

With universes $U$ the type theory would have "power sets" defined relative to $U$ but the "power sets" themselves would still be external to $U$ so would behave more like power classes from set theory.

Madeleine Birchfield (Aug 21 2024 at 22:52):

So with excluded middle, the set of truth values only has two elements in it $\{\bot, \top\}$, and so power sets are just function sets into $\{\bot, \top\}$. This means that predicativists who assume classical logic cannot assume that function sets exist between every single set.

However, without excluded middle, it is no longer the case that the set of truth values only has two elements. This means that power sets no longer coincide with function sets into $\{\bot, \top\}$, and predicativists who assume constructive logic can safely assume that all function sets exist, so long as they do not assume that the set of truth values exist.

Federica Pasqualone (Aug 21 2024 at 22:53):

The question then is: what is a function set? Lemme facilitate the discussion.

Madeleine Birchfield (Aug 21 2024 at 22:55):

Given sets $A$ and $B$, the function set $B^A$ or $A \to B$ is the set whose elements are the functions with codomain $A$ and domain $B$.

Federica Pasqualone (Aug 21 2024 at 22:55):

Well I mean, roughly speaking top and bottom there are 1 and 0, for the ones that prefer to go mod 2 :smiley: [in the presence of EM]

Federica Pasqualone (Aug 21 2024 at 22:56):

Madeleine Birchfield said:

Given sets $A$ and $B$, the function set $B^A$ or $A \to B$ is the set whose elements are the functions with codomain $A$ and domain $B$.

This sounds very categorical, isn't it? :stuck_out_tongue:

Madeleine Birchfield (Aug 21 2024 at 22:57):

In category theory those are usually called "exponential objects".

Federica Pasqualone (Aug 21 2024 at 22:58):

I am quite curious to see if there is any question from the audience at this point ... Is there any? - We should plan do it real life with mic and all the rest btw

Federica Pasqualone (Aug 21 2024 at 22:59):

Thanks @Madeleine Birchfield !

Peva Blanchard (Aug 21 2024 at 23:00):

Just to be sure, a predicativist is someone who refuses self-referencing definitions. But I guess that it's ok to have self-referencing definitions as long as "it terminates". E.g., the set of binary trees.

So, is there a precise characterization of definitions that are acceptable by a predicativist?

Federica Pasqualone (Aug 21 2024 at 23:05):

Here it is the trick: every time you quantify over you go one step higher. That's perfectly fine! Isn't it?

Federica Pasqualone (Aug 21 2024 at 23:07):

Ah .. do we want really to go also for Reducibility and all the magic of types?

Federica Pasqualone (Aug 21 2024 at 23:09):

Anyone that has the Axiom of Infinity and the one of Reducibility at hand? [Don't be shy!]

Madeleine Birchfield (Aug 21 2024 at 23:12):

Peva Blanchard said:

Just to be sure, a predicativist is someone who refuses self-referencing definitions. But I guess that it's ok to have self-referencing definitions as long as "it terminates". E.g., the set of binary trees.

So, is there a precise characterization of definitions that are acceptable by a predicativist?

This really depends on the predicativist and their beliefs. There are many people calling themselves predicativists who would accept anything and everything so long as the things they assume don't yield power sets. They would accept say the induction principle for the natural numbers or the induction principle for binary trees, since to them impredicativity = power sets, and neither induction principle proves that power sets exist.

Federica Pasqualone (Aug 21 2024 at 23:15):

Yes, maybe we should also relate the two things: namely the axioms with the natural numbers issue ... we are not speaking two languages hahha

Federica Pasqualone (Aug 21 2024 at 23:20):

Ok, so long story short: If one wants to carry on proofs by induction - and we love them in maths - one has also to assume the Reducibility axiom that, as said in PM, is just there ad hoc to make those things work.

Madeleine Birchfield (Aug 21 2024 at 23:22):

It is especially hard to see how one would "move to the next level" for the induction principle of the natural numbers in some versions of Martin-Löf type theory - there is only one level, and the propositions / truth values are represented in the theory by subsingletons (i.e. types / sets $A$ where $a = b$ for all elements $a$ and $b$ in $A$) and logical operators are represented by the usual set theoretic / type theoretic operations on subsingletons. i.e. truth is any singleton, falsehood is the empty type, and universal quantification of a predicate is the Cartesian product of a family of subsingletons in Martin-Löf type theory.

Madeleine Birchfield (Aug 21 2024 at 23:24):

And there are some predicativists who would not regard any version of Martin-Löf type theory as being "predicative" because it has induction of the natural numbers but no way to move to a different level.

Madeleine Birchfield (Aug 21 2024 at 23:24):

This is why I say that it all depends upon the predicativist and their beliefs.

Federica Pasqualone (Aug 21 2024 at 23:25):

That's an amazing summary!

Madeleine Birchfield (Aug 21 2024 at 23:26):

Because many mathematicians would regard Martin-Löf type theory, as well as other theories like CZF and CETCS, as predicative theories, even though it does come with induction of the natural numbers and no level distinction in the logic.

Federica Pasqualone (Aug 21 2024 at 23:32):

Please guys take note of this remark! :100: :memo:

Federica Pasqualone (Aug 21 2024 at 23:35):

Well .. let's leave the groupoids wonderful mysteries for the next time ....

Peva Blanchard (Aug 21 2024 at 23:36):

It's almost 2am here so I have to leave, but thanks for the discussion!

Federica Pasqualone (Aug 21 2024 at 23:37):

Thank you for participating!

Jean-Baptiste Vienney (Aug 21 2024 at 23:38):

Madeleine Birchfield said:

However, without excluded middle, it is no longer the case that the set of truth values only has two elements.

Could you elaborate on this? What is the set of truth values without excluded middle? And what do you even mean by truth value in this context?

Madeleine Birchfield (Aug 21 2024 at 23:38):

There are other versions of Martin-Löf type theory where it is possible to move ot the next level, so are more amenable to the sort of predicativity that @Federica Pasqualone is talking about. These versions of Martin-Löf type theory usually first define an infinite hierarchy of universes, and then define type operations and logical operations for the types in each universe.

The trick to replicate moving to the next level is to assume that the function sets / types and the indexed Cartesian products / dependent product types lie in the next universe level. That way, universal quantification and the induction principle of the natural numbers will lie in the next universe level. However, most type theorists working in this kind of type theory don't do this and I think the only person who has done something like this so far is @Ulrik Buchholtz and his work on primitive recursive arithmetic in homotopy type theory, where the bottom universe level doesn't contain function types / dependent product types.

Madeleine Birchfield (Aug 21 2024 at 23:40):

Jean-Baptiste Vienney said:

Madeleine Birchfield said:

However, without excluded middle, it is no longer the case that the set of truth values only has two elements.

Could you elaborate on this? What is the set of truth values without excluded middle?

The set of truth values contains truth values, such as $\exists x \in \mathbb{N}.f(x) = 1$ for any function $f:\mathbb{N} \to \{0, 1\}$, which cannot in general proven to be logically equivalent to $\top$ or $\bot$ in the absence of [[excluded middle]].

Jean-Baptiste Vienney (Aug 21 2024 at 23:42):

But to start, what is the definition of truth value in this context? (EDIT: for me truth value means by definition "true" or "false" so I don't understand what you're talking about although it seems very interesting)

Federica Pasqualone (Aug 21 2024 at 23:42):

Madeleine Birchfield said:

There are other versions of Martin-Löf type theory where it is possible to move ot the next level, so are more amenable to the sort of predicativity that Federica Pasqualone is talking about. These versions of Martin-Löf type theory usually first define an infinite hierarchy of universes, and then define type operations and logical operations for the types in each universe.

The trick to replicate moving to the next level is to assume that the function sets / types and the indexed Cartesian products / dependent product types lie in the next universe level. That way, universal quantification and the induction principle of the natural numbers will lie in the next universe level. However, most type theorists working in this kind of type theory don't do this and I think the only person who has done something like this so far is Ulrik Buchholtz and his work on primitive recursive arithmetic in homotopy type theory, where the bottom universe level doesn't contain function types.

This is actually what I meant by when you quantify over you go one step higher.

Madeleine Birchfield (Aug 21 2024 at 23:52):

Federica Pasqualone said:

This is actually what I meant by when you quantify over you go one step higher.

Except most type theorists using this kind of type theory don't actually lift universal quantification to the next universe level. Take a look at the type theory in Coq or Agda, and the universal quantification lies in the same universe as the family of subsingletons that they are quantifying over; the same goes for the textbooks on this kind of type theory like the [[HoTT book]]. And so Coq/Agda/book HoTT aren't predicative in the sense that you are using, but they are predicative in the sense that the practitioners of the theory are using (i.e. no power sets).

Madeleine Birchfield (Aug 21 2024 at 23:53):

In general, for predicativity in the sense you are describing, one would want the universes in the type theory to correspond to the regular cardinals in set theory, even constructively, while currently in Coq/Agda/book HoTT, they correspond to the inaccessible cardinals in set theory.

Federica Pasqualone (Aug 21 2024 at 23:54):

I see, well ... I never play by the book :grinning:

Federica Pasqualone (Aug 21 2024 at 23:56):

But yeah, this is a crucial remark for people that are approaching these theories and wanted to learn more! Thanks for pointing that out!

Jean-Baptiste Vienney (Aug 22 2024 at 00:01):

I think I got what you mean by "it is no longer the case that the set of truth values only has two elements". Do you mean that either a proposition is provable, either its negation is provable, or none of the two are provable? So each proposition can be assigned one of these three "truth values".

Madeleine Birchfield (Aug 22 2024 at 00:02):

Jean-Baptiste Vienney said:

I think I got what you mean by "it is no longer the case that the set of truth values only has two elements". Do you mean that either a proposition is provable, either its negation is provable, or none of the two are provable? So each proposition can be assigned one of these three "truth values".

It isn't three truth values. It is usually an infinite number of truth values. Think about how many elements are in the free Heyting algebra on a set of propositions.

Jean-Baptiste Vienney (Aug 22 2024 at 00:03):

But what do you mean by truth value?

Federica Pasqualone (Aug 22 2024 at 00:05):

Well, every proposition is either true or false, and you assign 0 or 1. But the logic is working if you have the excluded middle!

Madeleine Birchfield (Aug 22 2024 at 00:06):

So the set of truth values is called the [[subobject classifier]] in category theory / topos theory and usually characterised by a particular universal property, and then a truth value is just an element of this subobject classifier.

In a set theory like IZF, the set of truth values is defined as the double powerset of the empty set, and a truth value is just an element of this set.

Madeleine Birchfield (Aug 22 2024 at 00:07):

In dependent type theory, propositions / truth values are literal subsingletons, and so the set of truth values is just the set of all subsingletons, suitably defined using inference rules, or using universes and the usual type theoretic operations.

Madeleine Birchfield (Aug 22 2024 at 00:09):

In all cases, while there is an injection from the set $\{\top, \bot\}$ to the set of truth values, this is not provably a bijection unless excluded middle holds.

Jean-Baptiste Vienney (Aug 22 2024 at 00:13):

Can you give a bit of intuition on what the set of truth values is meaning in addition to the definition. I'm looking at the nLab page subobject classifier and I really have no intuition about what this object of truth values $\Omega$ is doing. For instance, in IZF, how do you interpret that the set of truth values is $\mathcal{P}(\mathcal{P}(\emptyset))$?

Federica Pasqualone (Aug 22 2024 at 00:14):

How are natural numbers defined in ZF? Think about it ...

Jean-Baptiste Vienney (Aug 22 2024 at 00:14):

And what is a powerset in IZF? Because with my intuition of powersets, I would like to write $\mathcal{P}(\mathcal{P}(\emptyset))=\mathcal{P}(\emptyset)=\emptyset$ which is probably not what you mean.

Madeleine Birchfield (Aug 22 2024 at 00:15):

In IZF and ZFC and other set theories like that, the power set of the empty set is a singleton, a set with exactly one element.

Jean-Baptiste Vienney (Aug 22 2024 at 00:16):

Oh sorry, I should have written: $\mathcal{P}(\mathcal{P}(\emptyset))=\mathcal{P}(\{\emptyset\})=\{\emptyset,\{\emptyset\}\}$

Jean-Baptiste Vienney (Aug 22 2024 at 00:17):

So do we still have two truth values in IZF or did I do something wrong??

Madeleine Birchfield (Aug 22 2024 at 00:18):

But without excluded middle, one cannot prove that $\mathcal{P}(\{\emptyset\})$ is equal to $\{\emptyset, \{\emptyset\}\}$.

Jean-Baptiste Vienney (Aug 22 2024 at 00:19):

Okk. So what's the meaning of $\mathcal{P}(\{\emptyset\})$ here?

Federica Pasqualone (Aug 22 2024 at 00:19):

Federica Pasqualone said:

How are natural numbers defined in ZF? Think about it ...

Madeleine Birchfield (Aug 22 2024 at 00:20):

The set of all subsets of $\{\emptyset\}$. One cannot show that every subset of $\{\emptyset\}$ is equal to either $\emptyset$ or $\{\emptyset\}$ without excluded middle. So you end up having $\{\emptyset, \{\emptyset\}, \ldots\}$ with a whole bunch of other subsets of $\{\emptyset\}$.

In addition, given any predicate $P$ on $\{\emptyset\}$, one gets a subset of the $\{\emptyset\}$ by the axiom of separation.

Jean-Baptiste Vienney (Aug 22 2024 at 00:20):

Oh, you define them with the empty set I guess. You define $0:=\emptyset$ and then $n+1=\{n,\{n\}\}$. Something like this?

Federica Pasqualone (Aug 22 2024 at 00:22):

Well, you simply associate 0, 1, 2, ... and so on to the recursive application of the power set operation on empty

Federica Pasqualone (Aug 22 2024 at 00:22):

See for instance https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers

Jean-Baptiste Vienney (Aug 22 2024 at 00:23):

Oh, ok. It is simpler to see it like this.

Federica Pasqualone (Aug 22 2024 at 00:24):

Then $\left\{0,1 \right\}$ is exactly the set you constructed previously.

Madeleine Birchfield (Aug 22 2024 at 00:26):

In constructive mathematics, the set $\{0, 1\}$ or $\{\top, \bot\}$ or $\{\emptyset, \{\emptyset\}\}$ etc still has a meaning: it is the set of all decidable truth values. A decidable truth value is a truth value which does satisfy excluded middle, i.e. $P \vee \neg P$.

Federica Pasqualone (Aug 22 2024 at 00:26):

Madeleine Birchfield said:

But without excluded middle, one cannot prove that $\mathcal{P}(\{\emptyset\})$ is equal to $\{\emptyset, \{\emptyset\}\}$.

But what is key is the excluded middle!

Federica Pasqualone (Aug 22 2024 at 00:27):

oh we wrote at the same time - sorry!

Jean-Baptiste Vienney (Aug 22 2024 at 00:31):

What is the link between the definition of natural numbers as $0:=\emptyset$ and $n+1=\mathcal{P}(n)$ and the set of truth values?

Jean-Baptiste Vienney (Aug 22 2024 at 00:33):

I mean, is there something more when you go above $n=1$?

Madeleine Birchfield (Aug 22 2024 at 00:33):

No, not really.

Jean-Baptiste Vienney (Aug 22 2024 at 00:33):

Ok

Madeleine Birchfield (Aug 22 2024 at 00:34):

$n = 2$ is the set of truth values itself, while $n = 3$ is the powerset of the set of truth values; the set of endofunctions on the set of truth values, etc...

Madeleine Birchfield (Aug 22 2024 at 00:34):

this doesn't really have anything to do with subsets of $\{\emptyset\}$.

Jean-Baptiste Vienney (Aug 22 2024 at 00:37):

Madeleine Birchfield said:

The set of all subsets of $\{\emptyset\}$. One cannot show that every subset of $\{\emptyset\}$ is equal to either $\emptyset$ or $\{\emptyset\}$ without excluded middle. So you end up having $\{\emptyset, \{\emptyset\}, \ldots\}$ with a whole bunch of other subsets of $\{\emptyset\}$.

In addition, given any predicate $P$ on $\{\emptyset\}$, one gets a subset of the $\{\emptyset\}$ by the axiom of separation.

For instance $\{x \in \{\emptyset\}~|~x \not\in x\}$ is a truth value?

Madeleine Birchfield (Aug 22 2024 at 00:42):

Yeah, it would be.

Madeleine Birchfield (Aug 22 2024 at 00:45):

Also a truth value: given any predicate $P(x)$ on $\{\emptyset\}$, the set

$\{x \in \{\emptyset\} \vert P(x) \vee \neg P(x)\}$

is a truth value. It is also one where you can't prove it's equal to either $\emptyset$ or $\{\emptyset\}$ for general $P(x)$ without excluded middle. It's equal to $\emptyset$ if $P(\emptyset) \vee \neg P(\emptyset)$ can be proven false and it's equal to $\{\emptyset\}$ if $P(\emptyset) \vee \neg P(\emptyset)$ can be proven true, but currently we are unable to prove either for general $P(x)$. Similarly for

$\{x \in \{\emptyset\} \vert \neg \neg P(x) \Rightarrow P(x)\}$

Jean-Baptiste Vienney (Aug 22 2024 at 01:00):

If I understand the nlab page subobject classifier, given a fixed object $X$ in a topos, there is a bijective correspondence between monomorphisms of the type $A \rightarrow X$ where $A$ can be any object and morphisms to the type $X \rightarrow \Omega$. So a subset of $X$ corresponds to a morphism $X \rightarrow \Omega$. It means that in IZF, a subset of a set $X$ corresponds to a function which assigns to every element of the set an element of $\mathcal{P}(\{\emptyset\})$ which is this really weird set. How am I supposed to understand this? I don't get any longer what is a subset of a set if we work with IZF. Giving a subset of $X$ corresponds to saying for every element of $X$ whether this element is in the subset, not in the subset or ... where ... is a lot of things that I don't really understand for now.

Federica Pasqualone (Aug 22 2024 at 01:02):

Wait? Who switched the topic to topos theory here? :joy: .... ah this Heyting :heart_eyes:

Madeleine Birchfield (Aug 22 2024 at 01:03):

A subset $A$ of a set $B$ in IZF is still the usual set-theoretic definition of a subset.
$\forall x.x \in A \Rightarrow x \in B$
It's just that without excluded middle, one can no longer prove that $x \in A$ or $x \notin A$ for all $x \in B$.

Madeleine Birchfield (Aug 22 2024 at 01:04):

There are subsets of sets for which without excluded middle you just don't know whether an element is in the subset or not.

Jean-Baptiste Vienney (Aug 22 2024 at 01:10):

Ok. But given a subset $A$ of a set $X$, you can still say that the assertion "the element x of X is in the subset A" has a truth value (if I understand well). And giving a subset is exactly giving such a truth value to every element of $X$. I still don't get a good intuition of what it means when the truth value is neither true nor false.

What does it tell me if given some $x \in X$ and some subset $A$ of $X$, the truth value of $x \in A$ is
$\{x \in \{\emptyset\} \vert P(x) \vee \neg P(x)\}$
or
$\{x \in \{\emptyset\} \vert \neg \neg P(x) \Rightarrow P(x)\}$
given some predicate $P(x)$ on $\{\emptyset\}$?

Jean-Baptiste Vienney (Aug 22 2024 at 01:11):

For now it looks like complete sorcery to me.

Jean-Baptiste Vienney (Aug 22 2024 at 01:13):

I get it somehow I think. It tells me that the assertion $P(x) \vee \neg P(x)$ is true or the assertion $\neg\neg P(x) \Rightarrow P(x)$ is true I guess.

Madeleine Birchfield (Aug 22 2024 at 01:14):

Jean-Baptiste Vienney said:

I still don't get a good intuition of what it means when the truth value is neither true nor false.

A good comparison is like the axiom of choice in ZF. The axiom of choice is neither true nor false in ZF. It is independent of the ZF axioms.

So similarly, for a predicate $P(x)$ on $\{\emptyset\}$, if $P(\emptyset)$ is neither true or false in IZF, then $P(\emptyset)$ is independent of the IZF axioms.

Jean-Baptiste Vienney (Aug 22 2024 at 01:22):

Let see what it gives if $P(x)$ is $x \in \{\emptyset\}$. $P(\emptyset)$ is $\emptyset \in \{\emptyset\}$. This one should be true.

Madeleine Birchfield (Aug 22 2024 at 01:23):

Jean-Baptiste Vienney said:

Let see what it gives if $P(x)$ is $x \in \{\emptyset\}$. $P(\emptyset)$ is $\emptyset \in \{\emptyset\}$. Can we prove that it is false?

Well some predicates are provably true or false even in constructive mathematics. This is one of the examples of a provably true predicate in IZF.

Jean-Baptiste Vienney (Aug 22 2024 at 01:24):

What is a predicate $P(x)$ on $\{\emptyset\}$ such that $P(\emptyset)$ is neither provably true nor provably false?

Federica Pasqualone (Aug 22 2024 at 01:24):

We are now moving to Goedel 1931?
This is becoming a terrific discussion touching all the fundamentals of mathematical logic btw. Well done!

Madeleine Birchfield (Aug 22 2024 at 01:28):

Jean-Baptiste Vienney said:

What is a predicate $P(x)$ on $\{\emptyset\}$ such that $P(\emptyset)$ is neither provably true nor provably false?

$P(x)$ defined as

$x \in \{y \in \mathbb{N}^\mathbb{N} \vert (\exists n \in \mathbb{N}.y(n) \neq 0) \vee (\forall n \in \mathbb{N}.y(n) = 0)\}$

Jean-Baptiste Vienney (Aug 22 2024 at 01:29):

This one looked cool ahah

Madeleine Birchfield (Aug 22 2024 at 01:31):

I don't think this example works though.

Jean-Baptiste Vienney (Aug 22 2024 at 01:32):

Let me see what $P(x)$ means though
"x is a sequence of nonnegative integers such that:

• some term is nonzero

or

• all terms are zero"

Madeleine Birchfield (Aug 22 2024 at 01:33):

What i actually want is a predicate $P(x)$ on $\{\emptyset\}$ which comes with a sequence $y \in \mathbb{N}^\mathbb{N}$ such that $P(x) \iff \exists n \in \mathbb{N}.y(n) \neq 0$.

Madeleine Birchfield (Aug 22 2024 at 01:38):

Madeleine Birchfield said:

Jean-Baptiste Vienney said:

What is a predicate $P(x)$ on $\{\emptyset\}$ such that $P(\emptyset)$ is neither provably true nor provably false?

$P(x)$ defined as

$x \in \{y \in \mathbb{N}^\mathbb{N} \vert (\exists n \in \mathbb{N}.y(n) \neq 0) \vee (\forall n \in \mathbb{N}.y(n) = 0)\}$

What does work though is this:

$P(x) \coloneqq x \in \{z \in \{\emptyset\} \vert z = \emptyset \wedge \forall y \in \mathbb{N}^\mathbb{N}.(\exists n \in \mathbb{N}.y(n) \neq 0) \vee (\forall n \in \mathbb{N}.y(n) = 0)\}$

Jean-Baptiste Vienney (Aug 22 2024 at 01:41):

Ok, let me write this in words:
"x is an element of $\{\emptyset\}$ such that:

• $x=\emptyset$,
• for every sequence of integers, some term is nonzero or all the terms are zero."

Jean-Baptiste Vienney (Aug 22 2024 at 01:43):

More simply:
"x is the emptyset and for every sequence of integers, some term is nonzero or all the terms are zero."

Madeleine Birchfield (Aug 22 2024 at 01:44):

Yes. The first statement is always true, so whether the element $x$ is in the subset or provably not in the subset solely depends on the truth of the second statement. If "for every sequence of integers, some term is nonzero or all the terms are zero" is provably true than $x$ is in the subset; if "for every sequence of integers, some term is nonzero or all the terms are zero" is provably false than $x$ is not in the subset.

But here we don't know if "for every sequence of integers, some term is nonzero or all the terms are zero" is true or false, without excluded middle.

Jean-Baptiste Vienney (Aug 22 2024 at 01:45):

Just for me: $P(\emptyset)$ means
"$\emptyset$ is the emptyset and for every sequence of integers, some term is nonzero or all the terms are zero."
which is the same than
"for every sequence of integers, some term is nonzero or all the terms are zero"

Madeleine Birchfield (Aug 22 2024 at 01:47):

Another example,

$P(x) \coloneqq x \in \{z \in \{\emptyset\} \vert z = 0 \wedge \mathrm{AC}_\mathbb{N}\}$

where $\mathrm{AC}_\mathbb{N}$ is the axiom of countable choice.

Jean-Baptiste Vienney (Aug 22 2024 at 01:52):

Ok, so given an element $x$ of a subset $A$ of a set $X$, saying any of these is giving some truth value to $x \in A$:

• $x$ is in $A$,
• $x$ is not in $A$,
• "for every sequence of integers, some term is nonzero or all the terms are zero",
• "the axiom of countable choice is true"

right?

Madeleine Birchfield (Aug 22 2024 at 01:54):

Yes. Though strictly speaking, the latter two would be something like

• "$x = x$ and for every sequence of integers, some term is nonzero or all the terms are zero"
• "$x = x$ and the axiom of countable choice is true"

and then since the first conditions, i.e. $x = x$, are always true, it simplifies down to the second conditions, which are the statements you listed above.

Jean-Baptiste Vienney (Aug 22 2024 at 01:56):

What would be an example where $P(x)$ really depends on $x$? These ones are funny but look a bit artificial as they don't really talk about $x$.

Madeleine Birchfield (Aug 22 2024 at 01:58):

Then we can go to this example, where my predicate $P(x)$ is on the function set $\{0, 1\}^\mathbb{N}$ and is defined as

$x \in \{y \in \{0, 1\}^\mathbb{N} \vert \exists n \in \mathbb{N}.y(n) \neq 0\}$

Madeleine Birchfield (Aug 22 2024 at 01:59):

$P(x)$ is true if $\exists n \in \mathbb{N}.x(n) \neq 0$; $P(x)$ is false if $\forall n \in \mathbb{N}.x(n) = 0$, but in general one can't show that $P(x) \vee \neg P(x)$ for all $x \in \{0, 1\}^\mathbb{N}$ without excluded middle.

Madeleine Birchfield (Aug 22 2024 at 02:01):

The fact that $\exists n \in \mathbb{N}.x(n) \neq 0$ or $\forall n \in \mathbb{N}.x(n) = 0$ for all $x \in \{0, 1\}^\mathbb{N}$ is called [[limited principle of omniscience]] for the natural numbers, and is independent of IZF but is provable in ZF with excluded middle.

Jean-Baptiste Vienney (Aug 22 2024 at 02:11):

Let me sum up:

• A truth value in IZF is a subset of $\{\emptyset\}$.
• Given any predicate $P(x)$ on $\{\emptyset\}$, the set $\{x \in \{\emptyset\}~|~ P(x)\}$ is a subset of $\{\emptyset\}$.
• I can choose $P(x)$ to be $x \in \{y \in \{0, 1\}^\mathbb{N} \vert \exists n \in \mathbb{N}.y(n) \neq 0\}$ which means "x is a binary sequence which is not constantly equal to 0".
• So there is a truth value which means "the elements of $\{\emptyset\}$ which are binary sequences not constantly equal to 0".

Jean-Baptiste Vienney (Aug 22 2024 at 02:12):

I don't understand why $\mathcal{P}(\emptyset)=\{\emptyset\}$ in IZF?

Jean-Baptiste Vienney (Aug 22 2024 at 02:13):

What axiom of IZF let you prove this?

Madeleine Birchfield (Aug 22 2024 at 02:13):

Because by the usual set theoretic definition of a subset and the axiom of the empty set, the only subset of the empty set is the empty set itself, and this is provable without excluded middle.

Madeleine Birchfield (Aug 22 2024 at 02:23):

John Baez will have over a hundred comments to sort through when he reads this discussion thread tomorrow.

Federica Pasqualone (Aug 22 2024 at 02:25):

We did a great job!

Madeleine Birchfield (Aug 22 2024 at 02:26):

Federica Pasqualone said:

We did a great job!

What foundations do you personally use for your mathematical work?

Federica Pasqualone (Aug 22 2024 at 02:29):

Madeleine Birchfield said:

Federica Pasqualone said:

We did a great job!

What foundations do you personally use for your mathematical work?

Mmh who knows? hahahah ... but between Zermelo and Russell I prefer Russell ...

Madeleine Birchfield (Aug 22 2024 at 02:31):

More importantly i guess, do you use excluded middle in your logic or not?

Federica Pasqualone (Aug 22 2024 at 02:32):

What do you think?

Madeleine Birchfield (Aug 22 2024 at 02:34):

I think you do. Most of the literature on algebraic quantum field theory uses excluded middle and I don't think any constructive mathematician has done the work to see which properties of, say, factorization algebras still hold in the absence of excluded middle.

Madeleine Birchfield (Aug 22 2024 at 02:38):

It's a pretty big problem for constructive mathematicians in mathematics more generally. I think @Chris Heunen wrote a paper a few years ago where he synthetically defined a dagger-category satisfying certain axioms and then he used Soler's theorem to show that the dagger-category is the dagger-category of Hilbert spaces and linear maps. But no constructive mathematician has shown that Soler's theorem can be proven without excluded middle, which implies that he was using excluded middle throughout the paper.

Madeleine Birchfield (Aug 22 2024 at 02:43):

And most constructive mathematicians aren't really interested in seeing what parts of the far flung branches of mathematics such as mathematical physics or geometric Langlands are still true without excluded middle, simply because there is a lot of preliminary work that needs to be done before constructive mathematicians are ready to tackle such topics, and it is possible that something breaks down along the way without excluded middle rendering the entire subject unattainable. For example, some parts of cohomology are impossible in constructive mathematics without some weak version of choice.

Federica Pasqualone (Aug 22 2024 at 02:48):

Well, there are connections between the theory of factorization algebras and algebraic quantum field theory, but they are quite different. Benini et al. compared the two theories.

Federica Pasqualone (Aug 22 2024 at 02:56):

I agree, without excluded middle it might get a little tricky. However, for logical investigations not having the excluded middle, as we've just seen, can be a lot of fun!

Madeleine Birchfield (Aug 22 2024 at 04:20):

One more comment about predicativity. L.E.J. Brouwer himself was a predicativist in a strong sense, since according to Toby Bartels he apparently did not accept all function sets in his (informal) foundations, and would probably hate most modern constructive and intuitionistic predicative foundations of mathematics like CZF or MLTT because they do accept function sets:

https://golem.ph.utexas.edu/category/2008/12/the_status_of_coalgebra.html#c020731

Amar Hadzihasanovic (Aug 22 2024 at 07:36):

Madeleine Birchfield said:

It's a pretty big problem for constructive mathematicians in mathematics more generally. I think Chris Heunen wrote a paper a few years ago where he synthetically defined a dagger-category satisfying certain axioms and then he used Soler's theorem to show that the dagger-category is the dagger-category of Hilbert spaces and linear maps. But no constructive mathematician has shown that Soler's theorem can be proven without excluded middle, which implies that he was using excluded middle throughout the paper.

Please correct me if you disagree, but wouldn't you say that a work such as Chris's is can be perfectly justified from a constructivist perspective to mathematical physics, where the ultimate paragon is not the relation of mathematical structures between each other, but instead the relation of mathematical structure to physical reality?

What I mean is: presumably, if I consider a certain mathematical result about mathematical structures that model physical objects to be fundamental to our understanding of physical reality, and I am a constructivist, I would like this result to be constructively provable. But then a common situation is: a result is constructively provable for certain structures $S$, but not for certain other structures $S'$ more commonly used to model the same objects.
Then, to prove that $S$ is classically (but, necessarily, not constructively) equivalent to $S'$ serves the purpose of convincing classically minded mathematicians that they can "safely" work with $S$ instead, which is preferable to constructivists.

Amar Hadzihasanovic (Aug 22 2024 at 07:46):

I know you have worked on the locale of real numbers, which seems to me perhaps the most prominent example of this -- there's so many "fundamental" theorems that have constructive localic versions, but violate constructive "taboos" in other versions that are classically equivalent -- I'm thinking of Hahn-Banach, Gelfand duality...

So presumably a constructivist should believe that the locale of real numbers is a better model of the physical continuum, and would be justified in using classical logic to argue that a non-constructivist doesn't "lose" anything by moving to localic models.

Amar Hadzihasanovic (Aug 22 2024 at 07:47):

(I don't think Chris is a constructivist, but on the other hand, he is Dutch...)

Chris Heunen (Aug 22 2024 at 08:26):

Off-topic, but fwiw: I strongly prefer constructive (mathematical) proofs when they're available. One of my MSc supervisors Wim Veldman, sometimes called the last living intuitionist, had a strong influence there. I do like locales and constructive analysis etc, and shy away from e.g. size issues because that's not the heart of the matter to me, or why I'm interested in a certain problem. I just can't bring myself to denounce all the beautiful maths based on the axiom of choice or excluded middle. It's just a different game, and who am I to judge whether people shouldn't derive pleasure from playing it? Of course, whether and how it relates to physical reality or some platonic notion of truth is a whole different question.

Slightly more on-topic: the paper about Hilbert spaces mentioned above does rely on Soler's theorem, of which I know no constructive (or in fact intuitive-to-me proof). But for that theorem you in fact don't need Soler! @Matthew Di Meglio and I figured out how to relate categorical colimits to analytic limits of real numbers directly, which is much more satisfying. See also Matt's nice blog post on the process of how that came to be. We've been working on a paper bringing it all together, hopefully out soon enough.

John Baez (Aug 22 2024 at 08:30):

Thanks everyone for this engaging discussion. When I woke up yesterday I was puzzled and even mildly upset to find no new messages on this Zulip. When I woke up today there were 158 on just this one thread!

John Baez (Aug 22 2024 at 08:41):

As for mathematical physics using constructive reasoning, it will definitely be fun for constructivists to build up the framework of analysis required to do more and more mathematical physics. But to get more mathematical physicists interested, it would be helpful to come up with some examples of where constructivism might help us understand physics. E.g. some ways in which a locale of real numbers is "better" - for the purposes of physics, not logic! - than the usual set of real numbers.

John Baez (Aug 22 2024 at 08:46):

This is probably a very challenging project that would require expertise in both mathematical physics and logic. It would be quite risky for anyone to spend a lot of time on this. But if someone could succeed it might spark a revolution.

I described a bunch of problems in physics connected to the continuum here:

• Struggles with the continuum.

I listed various new approaches to logic and then said:

This sort of foundational work proceeds slowly, and is deeply unfashionable. One reason is that it rarely seems to impact ‘real life’. For example, it seems that no question about the experimental consequences of physical theories has an answer that depends on whether or not we assume the continuum hypothesis or the axiom of choice.

But even if we take a hard-headed practical attitude and leave logic to the logicians, our struggles with the continuum are far from over. In fact, the infinitely divisible nature of the real line—the existence of arbitrarily small real numbers—is a serious challenge to physics.

Morgan Rogers (he/him) (Aug 22 2024 at 08:47):

Federica Pasqualone said:

I am quite curious to see if there is any question from the audience at this point ... Is there any? - We should plan do it real life with mic and all the rest btw

There is precedent for live-streaming math content, but my personal experience is that building up an audience is tricky and requires dedication.

Tobias Fritz (Aug 22 2024 at 08:57):

John Baez said:

But to get most mathematical physicists interested, it would be helpful to come up with some examples of where constructivism might help us understand physics. E.g. some ways in which a locale of real numbers is "better" - for the purposes of physics, not logic! - than the usual set of real numbers.

This is a bit wacky and tongue in cheek, but I wonder whether some sort of paraconsistent logic would be more suitable to make sense of quantum physics, so that the cat can actually be dead and alive at the same time. In particular, dual intuitionistic logic seems to be a version of paraconsistent logic! Looks like some people have seriously thought in this direction.

Peva Blanchard (Aug 22 2024 at 08:58):

I tend to get confused about constructibility, computability, and "physical realizability".
For instance, the Chaitin's constant is defined as

$$\Omega = \sum_{p \in P} 2^{-|p|}$$

where $P$ is the set of (prefix-free) terminating programs (represented by a finite binary sequence) for some universal Turing machine. $\Omega$ is a real number, usually interpreted as the probability that a random program halts. It is also an example of an algorithmically random number (Martin-Löf randomness). In particular, it is non-computable. If we believe in the physcical version Church-Turing thesis, then it also means that one cannot build a physical device that can output $\Omega$ within an arbitrary tolerance range.

Does it mean that the definition of $\Omega$ is also non-constructive?

Morgan Rogers (he/him) (Aug 22 2024 at 09:24):

Madeleine Birchfield said:

There are subsets of sets for which without excluded middle you just don't know whether an element is in the subset or not.

An alternative interpretation which is literally valid in some contexts is that an element can be a member of a subset "to some extent"; it need not be entirely present or entirely absent from the subset.

John Onstead (Aug 22 2024 at 09:28):

Madeleine Birchfield said:

It isn't three truth values. It is usually an infinite number of truth values. Think about how many elements are in the free Heyting algebra on a set of propositions.

This is interesting, but there's something I wanted to bring up. When I was first learning logic, I made a big mistake by conflating intuitionistic logic with "many-valued logic". Fortunately, I quickly learned that the two are not the same nor do they converge in any sense. This is because "many-value logic" does still have the law of excluded middle, it just is "expanded" to include the other truth values. For instance, a 3-value logic with truth values A, B, and C still has the law of excluded middle, which states that a proposition must be A, B, or C, and nothing in between. The axioms defining a Boolean topos (where classical logic with LEM holds) seem to be independent of the question of how many arrows there are from the terminal object to the subobject classifier (which quantifies how many truth values your system has), which means most Boolean toposes actually won't be two valued! I'm not sure if this independence holds in the other direction, that is, if it's possible to have a non-Boolean topos with a finite number of morphisms from the terminal to subobject classifier.

Morgan Rogers (he/him) (Aug 22 2024 at 09:30):

Peva Blanchard said:

Does it mean that the definition of $\Omega$ is also non-constructive?

A definition can only really fail to be constructive if it relies on a non-constructive result to be well-defined, and indeed this particular definition relies on LEM to say that "for all programs $p$, either $p \in P$ or $p \notin P$".

John Onstead (Aug 22 2024 at 09:38):

Tobias Fritz said:

This is a bit wacky and tongue in cheek, but I wonder whether some sort of paraconsistent logic would be more suitable to make sense of quantum physics, so that the cat can actually be dead and alive at the same time. In particular, dual intuitionistic logic seems to be a version of paraconsistent logic! Looks like some people have seriously thought in this direction.

This is interesting to bring up because I was just learning about logic and quantum mechanics. The way I see it, you can do quantum mechanical logic with the usual intuitionistic logic. Think about the proposition "the particle is here at x = 1". In classical logic, this proposition is either true (and the particle is there) or the proposition is false (and the particle is elsewhere). This only makes sense if you've already performed a measurement to see if the particle was at x=1, and only in the moment right after the measurement was conducted. Without any measurement to cause the particle to behave more classically, you can't say whether the proposition "the particle is here at x=1" is true or false, or has any other truth value associated to it (since, at least in the usual interpretation of QM, it doesn't make sense to ask if a non-measured particle even "has" a well defined notion of position at all!) Therefore, LEM does not apply and you are working in intuitionistic logic!

What I was reading about recently were "Bohr toposes". The internal logic of a Bohr topos is a "quantum logic". While quantum logic was invented before topos theory, the validity of the original conception is debated and so it wasn't until topos theory that the notion of "quantum logic" could be put on more rigorous founding. Since Bohr toposes need not be Boolean, this means that quantum logic is indeed inherently intuitionistic just as I described above!

Amar Hadzihasanovic (Aug 22 2024 at 09:41):

John Baez said:

As for mathematical physics using constructive reasoning, it will definitely be fun for constructivists to build up the framework of analysis required to do more and more mathematical physics. But to get more mathematical physicists interested, it would be helpful to come up with some examples of where constructivism might help us understand physics. E.g. some ways in which a locale of real numbers is "better" - for the purposes of physics, not logic! - than the usual set of real numbers.

Couldn't one simply apply the "principle of parsimony" to principles of reasoning as well? If there is

• a physical object behaving in a certain experimentally testable way, and
• two competing mathematical structures $S, T$ that can model this object, which are “equivalent” except for the fact that $S$ can only be proven to behave in the experimentally testable way with the use of classical axioms, whereas $T$ is proven to behave in the experimentally testable way constructively,

then one should prefer $T$ as a model?

Amar Hadzihasanovic (Aug 22 2024 at 09:43):

Parsimony seems to be well-accepted as a way of ranking mathematical models of the physical world, so unless one is philosophically committed to consider logic as "fixed and pre-existing", then I do not see why it should not be counted as a part of the model?

Tobias Fritz (Aug 22 2024 at 10:20):

John Onstead said:

What I was reading about recently were "Bohr toposes". The internal logic of a Bohr topos is a "quantum logic". While quantum logic was invented before topos theory, the validity of the original conception is debated and so it wasn't until topos theory that the notion of "quantum logic" could be put on more rigorous founding. Since Bohr toposes need not be Boolean, this means that quantum logic is indeed inherently intuitionistic just as I described above!

That's a reasonable perspective and certainly worth exploring. But on the other hand, it seems doubtful to me that this approach most accurately reflects the physics, and I'm uncomfortable with calling it a "quantum logic". (And I'd expect the same objection to apply to a paraconsistent or dual intuitionistic approach.)

Here's why: if you take a 'quantum proposition' to mean a $\{0,1\}$-valued quantum observable, then this is mathematically modelled by a projection operator on the Hilbert space of wave functions, or equivalently by a (closed) subspace of that Hilbert space. Then these propositions form an orthomodular lattice. Notably, this propositional quantum logic then relaxes classical logic, as intuitionistic logic does as well, but it relaxes it in importantly different ways:

• Quantum logic satisfies excluded middle $P \lor \lnot P = \top$, which intuitionistic logic fails;
• Quantum logic fails the distributivity $P \land (Q \lor R) = (P \land Q) \lor (P \land R)$, which intuitionistic logic satisfies.

That's why the intuitionistic logic of a Bohr topos doesn't look like a "quantum logic" to me. As far as I understand, the mapping from quantum propositions to Bohr topos propositions fails to be a lattice homomorphism because the Bohr topos has additional propositions with unclear physical meaning. Am I getting this right? Perhaps you could object that the conception of quantum propositions as $\{0,1\}$-valued observables is too narrow and these extra propositions do have physical significance, but then I'd like to see a detailed account of what that significance is.

BTW I'm not trying to advocate for traditional quantum logic here; it seems to have been largely a failure so far, given that physicists aren't using it to reason about quantum systems, arguably because it's too clunky to be useful especially for quantitative things. And so far I don't see the Bohr topos approach being more useful for physics. I'd be glad to see evidence to the contrary.

John Baez (Aug 22 2024 at 11:02):

Amar Hadzihasanovic said:

Parsimony seems to be well-accepted as a way of ranking mathematical models of the physical world, so unless one is philosophically committed to consider logic as "fixed and pre-existing", then I do not see why it should not be counted as a part of the model?

In mathematical physics, logical parsimony is much less highly valued than being able to predict a physical phenomenon someone else can't, or do a calculation or prove a theorem with implications for physics that someone else can't. In fact the only sort of parsimony I've seen mathematical physicists care about is parsimony in explicitly physical assumptions: e.g. people prefer a black hole singularity theorem if it makes weaker assumptions on the stress-energy tensor of the collapsing matter. I've never seen a mathematical physicist advertise that they can prove something without using excluded middle. (If they did, they'd probably be talking only to logicians.)

David Corfield (Aug 22 2024 at 11:04):

For what is described as an approach "rather complementary to Bohr toposes", you might enjoy Schreiber and Sati's Quantum Monadology, in particular the section 'Literature 1.2 (Epistemology of quantum physics and its formalization)'

Amar Hadzihasanovic (Aug 22 2024 at 11:15):

But surely if, say (sorry for the "absurd" example, I can't think of a better one), it had turned out that no experimental fact about quantum mechanics relied on the existence of an inner product on Hilbert spaces, we would all be dropping it and using "plain" vector spaces in our mathematical foundations of quantum mechanics.

Amar Hadzihasanovic (Aug 22 2024 at 11:16):

Why should the same status not be given to logical axioms?

John Baez (Aug 22 2024 at 11:44):

It's probably true that if one could formulate Schrodinger's equation for the hydrogen atom and prove it gives the right spectrum without using excluded middle, one could get some attention.

It would not excite me very much, because I feel pretty confident that one could do this, in part bey avoiding reliance on general theorems like the spectral theorem, and focusing on the specific example, where everything should be constructive.

But still it might be worth doing.

John Baez (Aug 22 2024 at 11:45):

I would be more interested in some more result that didn't concern an 'exactly solvable' model.

John Baez (Aug 22 2024 at 11:56):

In Recursivity in quantum mechanics I proved that Schrodinger's equation for a collection of charged particles can be solved in a computable way, but that wasn't using constructive logic.

John Baez (Aug 22 2024 at 11:58):

Morgan Rogers (he/him) said:

Peva Blanchard said:

Does it mean that the definition of $\Omega$ is also non-constructive?

A definition can only really fail to be constructive if it relies on a non-constructive result to be well-defined, and indeed this particular definition relies on LEM to say that "for all programs $p$, either $p \in P$ or $p \notin P$".

The sum is over programs that halt - where does LEM com in? Maybe we need it to prove the number $\Omega$ exists, but I don't see it - I'm not very good at constructivity.

Peva Blanchard said:

Chaitin's constant is defined as

$$\Omega = \sum_{p \in P} 2^{-|p|}$$

where $P$ is the set of (prefix-free) terminating programs (represented by a finite binary sequence) for some universal Turing machine.

Jules Hedges (Aug 22 2024 at 12:06):

(Sorry if this was mentioned somewhere in the previous 100 messages) - the basic difficulty with doing anything in calculus constructively is that the Bolzano-Weierstrass theorem (every bounded sequence has a convergent subsequence) requires both excluded middle and countable choice to prove, and most of the main theorems of real analysis rely on it. The combination of EM + countable choice can be constructivised using techniques like dialectica-type translations, but it's extremely gnarly

Madeleine Birchfield (Aug 22 2024 at 12:07):

If I remember correctly, the Bolzano-Weierstrass theorem only requires a weak version of excluded middle called the [[analytic LPO]].

Madeleine Birchfield (Aug 22 2024 at 12:15):

Personally for me, I'm currently looking at weak versions of excluded middle, such as

• "given two sets $A$ and $B$ with decidable tight apartness relations, the tight apartness relation on the function set $B^A$ is decidable"
• "if a set $A$ has a tight apartness relation, that relation is decidable"

which would make the real numbers and the function sets $\mathbb{R}^\mathbb{R}$ and $(\mathbb{R}^\mathbb{R})^{(\mathbb{R}^\mathbb{R})}$ behave more as they do in classical mathematics.

Federica Pasqualone (Aug 22 2024 at 12:22):

Morgan Rogers (he/him) said:

Federica Pasqualone said:

I am quite curious to see if there is any question from the audience at this point ... Is there any? - We should plan do it real life with mic and all the rest btw

There is precedent for live-streaming math content, but my personal experience is that building up an audience is tricky and requires dedication.

@Morgan Rogers (he/him) ... I was born for the stage ... :smirk: :mic:

Federica Pasqualone (Aug 22 2024 at 12:24):

John Onstead said:

Madeleine Birchfield said:

It isn't three truth values. It is usually an infinite number of truth values. Think about how many elements are in the free Heyting algebra on a set of propositions.

This is interesting, but there's something I wanted to bring up. When I was first learning logic, I made a big mistake by conflating intuitionistic logic with "many-valued logic". Fortunately, I quickly learned that the two are not the same nor do they converge in any sense. This is because "many-value logic" does still have the law of excluded middle, it just is "expanded" to include the other truth values. For instance, a 3-value logic with truth values A, B, and C still has the law of excluded middle, which states that a proposition must be A, B, or C, and nothing in between. The axioms defining a Boolean topos (where classical logic with LEM holds) seem to be independent of the question of how many arrows there are from the terminal object to the subobject classifier (which quantifies how many truth values your system has), which means most Boolean toposes actually won't be two valued! I'm not sure if this independence holds in the other direction, that is, if it's possible to have a non-Boolean topos with a finite number of morphisms from the terminal to subobject classifier.

That's a very interesting remark! Thanks a lot for it! :memo:

Madeleine Birchfield (Aug 22 2024 at 12:25):

To get the true effect of classical mathematics for $\mathbb{R}^\mathbb{R}$ and $(\mathbb{R}^\mathbb{R})^{(\mathbb{R}^\mathbb{R})}$ I'd probably have to pair

• "given two sets $A$ and $B$ with decidable tight apartness relations, the tight apartness relation on the function set $B^A$ is decidable"

with something like

• "given two spatial locales $A$ and $B$, the locale associated with the function set $\mathrm{pt}(B)^{\mathrm{pt}(A)}$ is spatial, where $\mathrm{pt}(A)$ and $\mathrm{pt}(B)$ are the spaces of points of the locales $A$ and $B$"

Federica Pasqualone (Aug 22 2024 at 12:27):

John Baez said:

Thanks everyone for this engaging discussion. When I woke up yesterday I was puzzled and even mildly upset to find no new messages on this Zulip. When I woke up today there were 158 on just this one thread!

And still counting! :zany_face:

Federica Pasqualone (Aug 22 2024 at 12:37):

So .. now we are on pointless topology? :heart_eyes:
Then, for the ones interested, I would suggest reading "Frames and Locales" [Picado, Pultr] and "Categorical Foundations Special Topics in Order, Topology, Algebra, and Sheaf Theory" - Chapter 2 - Picado, Pultr and my BSc supervisor Anna Tozzi on locales.

Federica Pasqualone (Aug 22 2024 at 12:41):

Amar Hadzihasanovic said:

Madeleine Birchfield said:

It's a pretty big problem for constructive mathematicians in mathematics more generally. I think Chris Heunen wrote a paper a few years ago where he synthetically defined a dagger-category satisfying certain axioms and then he used Soler's theorem to show that the dagger-category is the dagger-category of Hilbert spaces and linear maps. But no constructive mathematician has shown that Soler's theorem can be proven without excluded middle, which implies that he was using excluded middle throughout the paper.

Please correct me if you disagree, but wouldn't you say that a work such as Chris's is can be perfectly justified from a constructivist perspective to mathematical physics, where the ultimate paragon is not the relation of mathematical structures between each other, but instead the relation of mathematical structure to physical reality?

What I mean is: presumably, if I consider a certain mathematical result about mathematical structures that model physical objects to be fundamental to our understanding of physical reality, and I am a constructivist, I would like this result to be constructively provable. But then a common situation is: a result is constructively provable for certain structures $S$, but not for certain other structures $S'$ more commonly used to model the same objects.
Then, to prove that $S$ is classically (but, necessarily, not constructively) equivalent to $S'$ serves the purpose of convincing classically minded mathematicians that they can "safely" work with $S$ instead, which is preferable to constructivists.

And @Amar Hadzihasanovic , "structures" what a tempting plural ... do we want to talk about Alexander :heart: (Grothendieck) for a moment? Anyone?

Madeleine Birchfield (Aug 22 2024 at 12:44):

It is well known in constructive analysis that if you want Georg Cantor's definition of the real numbers to behave like it does in classical mathematics, then you would need

1. that the tight apartness relation on the space of points of the Cantor space locale is decidable (i.e. the [[limited principle of omniscience]]
2. that the Cantor space locale is a spatial locale (i.e. the [[fan theorem]])

Similarly, if you want Richard Dedekind's definition of the real numbers to behave like it does in classical mathematics, then you would need

1. that the tight apartness relation on the space of points of the locale of real numbers is decidable (i.e. the [[analytic limited principle of omniscience]]
2. that the locale of real numbers is a spatial locale

This is necessary but not sufficient for mathematical physics - one also would want to study say subsets of the function set $\mathbb{R}^\mathbb{R}$ such as the smooth functions $C^\infty(\mathbb{R})$ or the analytic functions $C^\omega(\mathbb{R})$, or sequence spaces $\mathbb{R}^\mathbb{N}$ or other infinite-dimensional Hilbert spaces, which require that the locale associated with $\mathbb{R}^\mathbb{R}$ be spatial and the tight apartness relation on its space of points be decidable in order for it to behave classically.

Then one may also consider operator algebras on such Hilbert spaces, which are usually subsets of the function set $(\mathbb{R}^\mathbb{R})^{(\mathbb{R}^\mathbb{R})}$ if I recall correctly. And for those to behave like they do classically, then there needs to be similar axioms stating that the locale is spatial and its space of points has decidable tight apartness.

Madeleine Birchfield (Aug 22 2024 at 13:00):

Now I suppose constructivists can work instead with localic vector spaces such as the localic versions of Hilbert spaces or Fréchet spaces instead of the usual definition of Hilbert spaces or Fréchet spaces as topological vector spaces, but I'm not seen much literature in that direction yet.

Federica Pasqualone (Aug 22 2024 at 13:04):

I guess one problem, partly already addressed by @John Baez , is that people working on mathematical physics are not usually mastering logic and also the audience of the journals are different, that's why it is a challenging project to rewrite physics logically or to do logical physics! :sparkles:

Madeleine Birchfield (Aug 22 2024 at 13:07):

Many parts of mathematical physics, such as statistical mechanics and quantum mechanics, also rely on probability and statistics, and I don't know if any constructive mathematicians have developed a constructive theory of probability and statistics yet. The problem with the classical formalization of probability theory in terms of measurable spaces is that measurable spaces are not well behaved in the absence of excluded middle. Most of the literature on constructively more well-behaved alternatives to measurable spaces as a foundation for probability and statistics, such as measurable locales or the various categorical approaches, still assume excluded middle and dependent choice.

Madeleine Birchfield (Aug 22 2024 at 13:16):

Federica Pasqualone said:

I guess one problem, partly already addressed by John Baez , is that people working on mathematical physics are not usually mastering logic and also the audience of the journals are different, that's why it is a challenging project to rewrite physics logically or to do logical physics! :sparkles:

Another problem is that mathematicians have no formalisation of the path integral as used in quantum field theory, so until that happens, the path integral will not be amenable to constructive approaches.

John Baez (Aug 22 2024 at 13:20):

The path integral, and the infinities in quantum field theory, are something mathematical physicists care about a lot - so if any new approach to mathematics really helps, they will be interested. But this seems to be a hard problem.

There have been various attempts to tame the infinities in quantum field theory using nonstandard analysis, for example, but I've never been convinced that they accomplish something useful for mathematical physics.

Federica Pasqualone (Aug 22 2024 at 13:22):

This is an interesting challenge ... :sunglasses:

John Baez (Aug 22 2024 at 13:24):

I can give you extremely difficult challenges all day long for free. You have to pay extra to get problems that I have some idea how solve. :upside_down:

Federica Pasqualone (Aug 22 2024 at 13:28):

Now I am getting curious ... hahah
But yeah, when I was in Goettingen I got interested in nonstandard analysis. So if not this way, which way? ...

John Baez (Aug 22 2024 at 13:30):

@Jules Hedges - when it comes to dealing with things like Bolzano-Weierstrass constructively, I believe for physics and other practical applications of analysis we don't need to prove every bounded sequence has a convergent subsequence. I believe we only need to prove that "sufficiently nice" bounded sequences have convergent subsequence. That is, I think we should allow more hypotheses in the theorem: hypotheses that we can check in practical applications.

I haven't checked that we can prove interesting results about mathematical physics constructively, so this line of research is another difficult challenge - but actually I think it's easier than my last challenge.

The challenge here is to develop enough analysis constructively to prove interesting results about specific physical systems. The idea would be to sidestep extremely general results like "every Hilbert space has an orthonormal basis", which are non-constructive, and take advantage of what we know about specific examples.

Madeleine Birchfield (Aug 22 2024 at 15:17):

If any constructive mathematicians are looking for an extremely difficult challenge in mathematical physics they can try to prove the extended TQFT hypothesis without excluded middle.

John Baez (Aug 22 2024 at 15:35):

How about trying something easier first?

Federica Pasqualone (Aug 22 2024 at 15:39):

To each open issue here we should attach as tag the level of complexity :grinning_face_with_smiling_eyes:

Federica Pasqualone (Aug 22 2024 at 15:42):

and Alexander teaches us that a good theory is built from the ground up and nothing should be left to chance ...

Kevin Carlson (Aug 22 2024 at 18:51):

I didn’t see anybody mention, in the discussion of intutionistic truth values above, that while it’s not true that every truth value is either $\top$ or $$\bottom$$ , it’s also not true that there are any other specific truth values you can name! I don’t remember the details of this well but I think the late David McCarty (who I guess was the second to last living intuitionist) once proved to me that the set of truth values is not finite, even though it has no specific exotic values.

Federica Pasqualone (Aug 22 2024 at 19:49):

That's a great remark! Thanks for sharing! :memo:

Zoltan A. Kocsis (Z.A.K.) (Aug 22 2024 at 20:51):

@Kevin Carlson The term "truth value" is in itself a bit misleading here. In the context of the discussion above, "truth value" refers to an element of a subobject classifier in some category. You can construct a topos whose internal logic is classical (LEM holds) even though you can name 4 different truth values. However, if there are exactly 2 truth values in the sense that $\Omega \cong 1 +1$, the logic of your topos is necessarily classical (LEM holds).

Abstracting away from categories, the very notion of "$n$-valued logic" has some subtlety to it.

For instance, depending on the specific definition, intuitionistic logic might be 2-valued, or might not qualify as $n$-valued for any $n \in \mathbb{N}$ - see my answer to a related question over at Math.SE.

Todd Trimble (Aug 22 2024 at 20:56):

I usually find topos theory helpful in semantically grounding such discussions. The category of functors $M \to \mathsf{Set}$ for a monoid (or one-object category) $M$ is a topos with two "truth values" $1 \to \Omega$, because there are only two subobjects of $1$, but the logic is nevertheless intuitionistic.

Madeleine Birchfield (Aug 22 2024 at 21:05):

It probably has two "truth values" externally but you likely cannot prove it in the internal logic.

Zoltan A. Kocsis (Z.A.K.) (Aug 22 2024 at 21:11):

@Madeleine Birchfield The question is precisely what it means for a logic to have $n$ truth values i.e. when you say that "having two truth values is not provable in the internal logic", what is the internal statement $P$ that you're claiming is not provable. There is no widely-agreed-upon standard for that. (It's of course much easier to agree upon what it means for a semantics to have $n$ truth values; topoi, in this sense, are a possible semantics for intuitionistic logic. But that does not really say much about the logic itself: in this case, there are two-valued topoi whose internal logic nonclassical, and 65535-valued topoi whose internal logic is fully classical)

Madeleine Birchfield (Aug 22 2024 at 21:13):

It's weird, I've been using "excluded middle" as internal excluded middle; i.e. sets form a Boolean topos.

It is perfectly possible to define a classical set theory using intuitionistic logic - assuming the axiom of choice in IZF does this. The external logic itself is still intuitionistic in the sense that full excluded middle can't be proven for all propositions in the theory, but excluded middle holds in the internal logic (i.e. in the double powerset of the empty set).

Madeleine Birchfield (Aug 22 2024 at 21:16):

The thing is that I've been using dependent type theory for the past few years and unlike set theory, it doesn't have an external logic. So excluded middle there is literally "every subsingleton is either a singleton or equivalent to the empty set".

John Onstead (Aug 22 2024 at 21:23):

Zoltan A. Kocsis (Z.A.K.) said:

But that does not really say much about the logic itself: in this case, there are two-valued topoi whose internal logic nonclassical, and 65535-valued topoi whose internal logic is fully classical)

Ah, this seems to confirm what I was talking about above, that the "many-valued-ness" of a topos and whether or not it is Boolean (classical) are independent matters. To be honest I am a little surprised one can have a 2-valued non-Boolean topos though! Very interesting!

John Onstead (Aug 22 2024 at 21:34):

Madeleine Birchfield said:

Another problem is that mathematicians have no formalisation of the path integral as used in quantum field theory, so until that happens, the path integral will not be amenable to constructive approaches.

This might be an intriguing discussion all on its own, but I want to know more about what this means. Is this statement related to how apparently QFT is not "formalized" which necessitates things like AQFT and FQFT? If so I've never been able to see why this is the case. The path integral is a well formalized concept; every student learns about line integrals (also called path integrals) in first year multivariable calculus.

I also see ways of formalizing QFT itself that are immediately apparent. One way is to use the Schrodinger picture and just axiomatize QFT by stating it takes place in an infinite dimensional Hilbert Space where every vector is a quantum state for the quantum field. The quantum state can then be decomposed into eigenstates along the "field configuration" basis, allowing you to write the quantum state as a superposition of all possible field configurations. This leads to what is known as the "wavefunctional", a functional that takes in a possible field configuration and returns the probability amplitude you will find that configuration when you take a measurement of the field. I don't see any problem with this axiomatization, especially because it is basically exactly the same to how traditional QM is axiomatized- there's a Hilbert space, physical property observables are Hermitian operators on this Hilbert space, quantum objects are described by vectors in Hilbert space, etc.

Madeleine Birchfield (Aug 22 2024 at 21:42):

John Onstead said:

The path integral is a well formalized concept; every student learns about line integrals (also called path integrals) in first year multivariable calculus.

The path integral in quantum field theory is specifically talking about the Feynman path integral, rather than the line integral found in calculus:

https://en.wikipedia.org/wiki/Path_integral_formulation

John Baez (Aug 22 2024 at 21:43):

Yes, @John Onstead - we're not talking about line integrals: we're talking about an integral over an infinite-dimensional space of paths, or some other infinite-dimensional space of maps. This is what show up in quantum field theory, and it's difficult to formalize except in limited cases.

JR (Aug 22 2024 at 23:58):

John Baez said:

Yes, John Onstead - we're not talking about line integrals: we're talking about an integral over an infinite-dimensional space of paths, or some other infinite-dimensional space of maps. This is what show up in quantum field theory, and it's difficult to formalize except in limited cases.

Well if you Wick rotate into statistical physics and discretize into lattice (gauge) theory then it is “just” a finite but large Markov chain

Madeleine Birchfield (Aug 23 2024 at 01:22):

How much of the experiments and the analysis at the LHC or Fermilab or other particle physics laboratories actually use the Standard Model itself, as opposed to some discrete lattice gauge theory approximation of the Standard Model?

James E Hanson (Aug 23 2024 at 01:31):

@Madeleine Birchfield I'm not sure I think that's a completely well-defined question given the way physicists think about physics, but if I recall correctly a large amount of hadron collision physics is done with semi-empirical formalisms like parton distribution functions, which aren't derived from lattice computations or lower-level principles like the standard model. That said other parts of various calculations are done using the standard model and perturbation theory.

Federica Pasqualone (Aug 23 2024 at 01:50):

Good evening everyone, wait ... now we are going for the Standard Model and beyond? :heart:

Federica Pasqualone (Aug 23 2024 at 01:52):

This thread is getting seriously dangerous hahahha [in the good sense] very Federica!

John Onstead (Aug 23 2024 at 02:01):

Ah I see it's the Feynman path integral formulation, my bad. I still don't see why this is hard to formalize- it's just an integral, even if the underlying space is complicated. Let's say we have standard 2D Euclidean space R^2 as well as the Euclidean interval [0,1]. Both of these are objects in most "nice" categories of spaces, which are cartesian closed. Thus, we may define an internal hom Hom([0,1], R^2) to be the space of all functions from [0,1] to R^2, which we can imagine as paths in R^2. This is just a space as any other. We can then define a function (functional) on this space e^(i S): Hom([0,1], R^2) -> C which sends a path to a complex number. If we choose two points in R^2 (representing initial and final states), we can then define a subspace of Hom([0,1], R^2) on all paths between these two points. Now we have our function to integrate as well as the domain of integration, so we can properly take the integral. At which point in this process does the formalization break down?

Kevin Carlson (Aug 23 2024 at 02:14):

The immediate problem is that the domain of integration is infinite-dimensional.

Federica Pasqualone (Aug 23 2024 at 02:27):

In general, a path integral is given by some good measure and an action integrated over all possible paths. The action functional being the integral of a Lagrangian. How do we know this is a well-defined object? How do we treat divergences? and what about the domain of integration?

Federica Pasqualone (Aug 23 2024 at 02:30):

It's an infinities issue! :exploding_head:

Federica Pasqualone (Aug 23 2024 at 02:43):

In classical mechanics one gets trajectories of the system under investigation easily. I mean, one finds out potential and kinetic energies to write down the Lagrangian, integrate over time to have the action and then Hamilton's principle. Solutions of Euler-Lagrange eq.s are equivalent to the stationary points of the action functional. Here you are your trajectory ... and the system evolves along it.

Federica Pasqualone (Aug 23 2024 at 02:47):

When you switch to the quantum world things get a little tricky, it is all about calculus of probability over an infinite number of possible trajectories.

John Baez (Aug 23 2024 at 08:55):

Madeleine Birchfield said:

How much of the experiments and the analysis at the LHC or Fermilab or other particle physics laboratories actually use the Standard Model itself, as opposed to some discrete lattice gauge theory approximation of the Standard Model?

That's not really the kind of question that has a simple answer. For example, lattice models are especially important for studying low-energy quantum chromodynamics, like computing the mass ratio of the proton and neutron. But people working on this don't simply discretize QCD and put it on a lattice - the size of a lattice that people can compute with is much too small to get accurate results that way. So, elaborate methods based on the continuum are used to try to correct the errors due to working on a lattice.

Furthermore lattice computations are always done in Euclidean space, not Minkowski spacetime, as JR pointed out - this essentially amounts to replacing time $t$ with imaginary time $it$, which converts quantum field theory problems to statistical mechanics problems. So they need to be analytically continued back to get physically significant results, and the details of how this is done depends on what one is trying to compute.

So, please don't think people doing lattice gauge theory simply replace spacetime by a lattice, discretize quantum field theory, and do computations on that lattice.

John Baez (Aug 23 2024 at 08:58):

@John Onstead wrote:

Now we have our function to integrate as well as the domain of integration, so we can properly take the integral. At which point in this process does the formalization break down?

Right where you said "so we can properly take the integral". You can't do an integral using just the domain of integration and the function to be integrated! You need a measure, or perhaps some generalization of a measure. That's where all the work lies.

John Baez (Aug 23 2024 at 09:04):

You should read the answers here to get a rough sense of where we stand:

• MathOverflow, Mathematics of path integral: state of the art.

One of $1,000,000 Millennium prizes involves making the path integral rigorous enough so that we can prove some things we expect are true.

Federica Pasqualone (Aug 23 2024 at 10:49):

It's a lot of money @John Baez ... :rolling_on_the_floor_laughing: :money:

Federica Pasqualone (Aug 23 2024 at 10:53):

Now everyone will start studying MT hahahhahahah

Federica Pasqualone (Aug 23 2024 at 11:53):

and logic of course hahhahah

Benedikt Peterseim (Aug 23 2024 at 19:34):

Silly thought: maybe the Standard Model should actually be considered a billion-parameter model because it needs a physicist’s brain to make any predictions; and maybe the “theory of everything” will just be GPT-37 doing integrals like a physicist. :woman_scientist::robot:

Federica Pasqualone (Aug 23 2024 at 20:17):

I don't know ... AI ... mmh I am the kind of person who loves paper, her fountain pen and studies calligraphy! :feather:
And @Benedikt Peterseim , picture this: Being the one who formalized Feynman integrals!

Federica Pasqualone (Aug 23 2024 at 20:17):

If you are talking about just calculations afterwards, this is another story.

Federica Pasqualone (Aug 23 2024 at 20:21):

The "Theory of Everything" ... :thought:

Federica Pasqualone (Aug 23 2024 at 20:28):

Anyone on multiverse theory? :rolling_on_the_floor_laughing:

Benedikt Peterseim (Aug 23 2024 at 20:29):

Please don’t take seriously what I wrote in case that wasn’t clear. :D

Benedikt Peterseim (Aug 23 2024 at 20:34):

The slightly serious point, though, is that the “model” part in “Standard Model” is somewhat a misnomer I think, since it’s more of a framework that particle physicists use to derive various particular models. “Standard Theory of Particle Physics” would be better perhaps. After all, it’s also not called the “Classical Mechanics Model”, classical mechanics has many models and so does particle physics.

Federica Pasqualone (Aug 23 2024 at 20:36):

Actually, thanks for bringing up "The theory of everything"! I am assuming you are not referring to the movie! :stuck_out_tongue:

Federica Pasqualone (Aug 23 2024 at 20:37):

ahhh ... the good old days of David Griffiths' book "Introduction to elementary particles"!

Federica Pasqualone (Aug 23 2024 at 20:38):

You're right! It is a model! and Feynman did a great job there too with his diagrams!

Benedikt Peterseim (Aug 23 2024 at 20:40):

Federica Pasqualone said:

Actually, thanks for bringing up "The theory of everything" I am assuming you are not referring to the movie! :stuck_out_tongue:

No, the quotation marks are just there because I don’t even know what “theory of everything” might actually mean.

Federica Pasqualone (Aug 23 2024 at 20:47):

Federica Pasqualone said:

Good evening everyone, wait ... now we are going for the Standard Model and beyond? :heart:

That's it! Beyond the SM! The great unification, the dream of a unique theory that encompasses everything!

Federica Pasqualone (Aug 23 2024 at 20:53):

But I should also mention, given the appropriate nature of this thread hahah, that there are logical arguments against it too! (besides others of various nature)
Yes, here we are again: LOGIC :heart_eyes:

Madeleine Birchfield (Aug 23 2024 at 21:28):

Federica Pasqualone said:

But I should also mention, given the appropriate nature of this thread hahah, that there are logical arguments against it!

Assuming this is referring to the standard model, I have some doubts about the future about the standard model that I would like to share. If this happens to be about beyond standard model physics, well, the possibility of any beyond standard model physics will also likely get negatively affected by these doubts. Let me copy what I wrote in another thread over here:

Madeleine Birchfield said:

More importantly, a significant part of science is the ability to replicate experiments to demonstrate the validity of scientific results for contemporary society. One reason we know that general relativity is currently scientifically true in various domains is because there are currently people replicating experiments and observations in their labs first done in the 1910s and 1920s and the results have all been in accordance with general relativity.

However, much of the evidence for the Higgs boson and other parts of the standard model has come from various particle colliders such as the LEP and its replacement the LHC.

Now, there is currently debate over whether there will be funding for a replacement particle collider when the LHC stops performing experiments and gets decommissioned in the future. If no replacement particle collider ever gets built due to lack of funding, eventually a new generation of physicists will grow up not being able to replicate the experiments at the LEP and the LHC, won't be able to detect the Higgs boson, and won't have anybody around who still remembers when scientists at CERN did perform experiments to detect the Higgs.

In this case, I highly doubt that "the Higgs boson exists today" remains a scientific truth to those future physicists, because all that the physicists will have is the fact that "the LHC detected the Higgs in 2012" and they no longer have any way of verifying whether the experiments at the LHC are still true in their time, or whether something has changed in the years between LHC and their contemporary society potentially yielding different results for the experiments, thus requiring physicists to go beyond the standard model. While "the Higgs boson existed in 2012" is verifiable fact, "the Higgs boson exists today" becomes just another hypothesis in natural philosophy which is beyond scientific experiment.

Madeleine Birchfield said:

I think that as governments and universities and research institutes gradually cut funding to particle physics experiments and redirect them elsewhere, i.e. to astrophysics, condensed matter, etc, a lot of standard model physics will in the future become like what quantum gravity is today, still being studied as theory by physicists in physics departments but with no contemporary connections to scientific experiment.

Madeleine Birchfield said:

Trying to use the results of the LHC in the 2010s and 2020s to justify the truth of the standard model after the LHC has been shut down runs straight into the problem of induction. What the proponents of a new particle collider are trying to do is to set up a replacement for the LHC so that they can circumvent the problem of induction by directly testing for the Higgs and etc using the scientific method, so that the standard model can avoid becoming the next quantum gravity / string theory.

Federica Pasqualone (Aug 23 2024 at 21:51):

Madeleine Birchfield said:

Federica Pasqualone said:

But I should also mention, given the appropriate nature of this thread hahah, that there are logical arguments against it!

Assuming this is referring to the standard model, I have some doubts about the future about the standard model that I would like to share. If this happens to be about beyond standard model physics, well, the possibility of any beyond standard model physics will also likely get negatively affected by these doubts. Let me copy what I wrote in another thread over here:

Madeleine Birchfield said:

More importantly, a significant part of science is the ability to replicate experiments to demonstrate the validity of scientific results for contemporary society. One reason we know that general relativity is currently scientifically true in various domains is because there are currently people replicating experiments and observations in their labs first done in the 1910s and 1920s and the results have all been in accordance with general relativity.

However, much of the evidence for the Higgs boson and other parts of the standard model has come from various particle colliders such as the LEP and its replacement the LHC.

Now, there is currently debate over whether there will be funding for a replacement particle collider when the LHC stops performing experiments and gets decommissioned in the future. If no replacement particle collider ever gets built due to lack of funding, eventually a new generation of physicists will grow up not being able to replicate the experiments at the LEP and the LHC, won't be able to detect the Higgs boson, and won't have anybody around who still remembers when scientists at CERN did perform experiments to detect the Higgs.

In this case, I highly doubt that "the Higgs boson exists today" remains a scientific truth to those future physicists, because all that the physicists will have is the fact that "the LHC detected the Higgs in 2012" and they no longer have any way of verifying whether the experiments at the LHC are still true in their time, or whether something has changed in the years between LHC and their contemporary society potentially yielding different results for the experiments, thus requiring physicists to go beyond the standard model. While "the Higgs boson existed in 2012" is verifiable fact, "the Higgs boson exists today" becomes just another hypothesis in natural philosophy which is beyond scientific experiment.

Madeleine Birchfield said:

I think that as governments and universities and research institutes gradually cut funding to particle physics experiments and redirect them elsewhere, i.e. to astrophysics, condensed matter, etc, a lot of standard model physics will in the future become like what quantum gravity is today, still being studied as theory by physicists in physics departments but with no contemporary connections to scientific experiment.

Madeleine Birchfield said:

Trying to use the results of the LHC in the 2010s and 2020s to justify the truth of the standard model after the LHC has been shut down runs straight into the problem of induction. What the proponents of a new particle collider are trying to do is to set up a replacement for the LHC so that they can circumvent the problem of induction by directly testing for the Higgs and etc using the scientific method, so that the standard model can avoid becoming the next quantum gravity / string theory.

I was referring to the "theory of everything".

Madeleine Birchfield (Aug 23 2024 at 21:55):

Federica Pasqualone said:

I was referring to the "theory of everything".

Yeah, well my points still hold even more strongly for any "theory of everything". Unlike the standard model, where the lack of access to scientific experiments confirming the standard model is currently something that isn't the case now but could possibly happen in the future, the lack of access to scientific experiments confirming the various theories of everything in theoretical physics is a reality today.

Madeleine Birchfield (Aug 23 2024 at 21:56):

Why should anybody believe in a "theory of everything" if there is no scientific evidence that gravity is united with the rest of the forces?

Federica Pasqualone (Aug 23 2024 at 21:58):

Well, but even before thinking of switching to the experimental side of the story, having a formal theory of everything - meaning an axiomatics for describing every fundamental force in the universe - is an issue.

Madeleine Birchfield (Aug 23 2024 at 22:02):

The "theory of everything" isn't actually meant to be a theory of everything in the universe, it was merely a term used by particle physicists to describe the unification of the 3 quantum forces (electromagnetism, strong, and weak forces) with gravity into one unified field theory.

Even if the particle physicists had managed to succeeded in their quest for the theory of everything, it wouldn't literally be a theory of everything, since there are things, like consciousness, which remain inexplicable using the unified field theory.

Madeleine Birchfield (Aug 23 2024 at 22:03):

There is also the risk that dark matter exists and is mediated by some new fifth force. Dark matter is already outside the original definition of the "theory of everything" since the theorists were just focusing on unifying the three forces of the standard model with gravity.

Federica Pasqualone (Aug 23 2024 at 22:08):

Federica Pasqualone said:

But I should also mention, given the appropriate nature of this thread hahah, that there are logical arguments against it too! (besides others of various nature)
Yes, here we are again: LOGIC :heart_eyes:

Yes, there are indeed a bunch of arguments against it.

Madeleine Birchfield (Aug 23 2024 at 22:09):

There are also other arguments against the standard model.

In the standard model, neutrinos do not oscillate. But we know from scientific experiment and observations that neutrinos do oscillate. So we have to go beyond the standard model and add a mechanism that would allow neutrinos to oscillate. Most proposals add neutrino masses, while some others break Lorentz symmetry.

Madeleine Birchfield (Aug 23 2024 at 22:17):

So if I wager a guess as to the future of particle physics and the standard model - the large particle colliders like the LHC are likely going to be a thing of the past as funding for them dries up. Physicists will still believe in the Higgs boson even though they can no longer demonstrate its existence through repeated scientific experiment, and it will harden into dogma that gets passed down to generations of new physicists who cannot replicate the experiments. (This was one reason why I was saying in the other thread that physics is first and foremost a branch of "natural philosophy" and only secondarily a science.)

Meanwhile, the astrophysics community will likely turn decisively against the dark matter hypothesis as searches for dark matter turns up empty, and evidence accumulates that some relativistic MOND theory is actually favoured over dark matter to explain astrophysical observations in galaxies and galaxy clusters and in cosmology, meaning that funding for particle dark matter experiments will also end up being a thing of the past.

Supersymmetry is already virtually dead today.

In the end, neutrinos will be the only potential thing that could lead to beyond standard model physics, so most of the remaining energy and resources in particle physics will get poured into neutrino experiments and trying to sift through the different theories of neutrino oscillations that extend the standard model.

Federica Pasqualone (Aug 23 2024 at 22:20):

Neutrino physics and dark matter! These are the main areas in which they do experiments at the LNGS too in my hometown.

Federica Pasqualone (Aug 23 2024 at 22:22):

Yeah I know very well the story of the neutrinos :wink:

Federica Pasqualone (Aug 23 2024 at 22:25):

and I guess, for the audience, that could be a bit far from physics ( but hopefully got interested in it) in terms of education, David Griffiths' book "Introduction to Elementary Particles" is the best book I know to start diving into the subject! :books:

Federica Pasqualone (Aug 23 2024 at 22:26):

Time to study guys! :nerd: :rolling_on_the_floor_laughing:

Madeleine Birchfield (Aug 23 2024 at 22:36):

Since we're here at the frontiers of physics, I'm really tempted to go into another interpretation of "One universe as a foundation & friends" and talk about our current theories of physical cosmology.

Federica Pasqualone (Aug 23 2024 at 22:38):

This thread is better than HTT :upside_down: speaking of :infinity:
Would you mind waiting a little time? Maybe tomorrow, so that people are able to read first about the SM?

Madeleine Birchfield (Aug 23 2024 at 22:39):

Sure.

Federica Pasqualone (Aug 23 2024 at 22:41):

Great then, as tradition wants: Any questions? :mic:

John Onstead (Aug 23 2024 at 22:53):

Madeleine Birchfield said:

Why should anybody believe in a "theory of everything" if there is no scientific evidence that gravity is united with the rest of the forces?

A theory of gravity + quantum (not necessarily quantum gravity, which deals specifically with introducing gravitons, but rather any theory that explains both gravity and quantum mechanics at once) is needed simply because there are domains and conditions in the universe that bring the two together. For instance, you would need a unified description to explain the gravitational force generated by an object in superposition. Let's say you had a ball capable of entering superposition, and you sent it through a beamsplitter-like apparatus that splits its matter wave. You now have the ball in a superposition of being in two very different, and very far apart locations. Since all matter generates gravity, where is this gravity getting generated exactly? If the particle doesn't even have a well defined position in space- in fact, a position in space at all- then how can it curve spacetime?
The more usual example is that general relativity breaks down in certain places like a black hole singularity, which necessitates a theory that has both quantum and gravity in it. There's also the black hole information paradox which deals with the intersection between these two theories. Because these two theories intersect in nature, there must be some law governing how they intersect, which will be this theory of gravity+quantum you call a "theory of everything".

Madeleine Birchfield (Aug 23 2024 at 22:58):

John Onstead said:

A theory of gravity + quantum (not necessarily quantum gravity, which deals specifically with introducing gravitons, but rather any theory that explains both gravity and quantum mechanics at once) is needed simply because there are domains and conditions in the universe that bring the two together.

A theory that explains both gravity and quantum mechanics at once is not the same as a theory which says that there is one single unified force which at low energies separates into electromagnetism, the strong force, the weak force, and gravity. The latter is what particle physicists mean by uniting gravity with the other 3 forces, by the "theory of everything".

John Onstead (Aug 23 2024 at 23:00):

Madeleine Birchfield said:

Physicists will still believe in the Higgs boson even though they can no longer demonstrate its existence through repeated scientific experiment, and it will harden into dogma that gets passed down to generations of new physicists who cannot replicate the experiments.

I don't understand this position. Just because experiments stop confirming the higgs boson doesn't suddenly mean the higgs boson would cease to exist? That is, once we demonstrate its existence to a high degree of significance, why would we need to keep demonstrating its existence? The LHC is no longer running to establish the existence of the higgs, that's already done. It's now focused on either discovering new particles, or discovering more about the particles we already know exist (like the higgs). Though I would agree with your skepticism that larger colliders will be worth it since unlike with the higgs and LHC we have no solid evidence that there even might be more massive particles to make such a thing worthwhile.

Madeleine Birchfield said:

Meanwhile, the astrophysics community will likely turn decisively against the dark matter hypothesis as searches for dark matter turns up empty, and evidence accumulates that some relativistic MOND theory is actually favoured over dark matter to explain astrophysical observations in galaxies and galaxy clusters and in cosmology

I disagree. No theory of MOND is capable of explaining the CMB or why some pairs of galaxies with the same mass and mass distribution have wildly varying stellar rotation curves. To explain the latter any such theory would have to either be internally inconsistent or vary across the universe like a scalar field, which would then just be dark matter again.

Madeleine Birchfield (Aug 23 2024 at 23:10):

John Onstead said:

I don't understand this position. Just because experiments stop confirming the higgs boson doesn't suddenly mean the higgs boson would cease to exist? That is, once we demonstrate its existence to a high degree of significance, why would we need to keep demonstrating its existence? The LHC is no longer running to establish the existence of the higgs, that's already done.

This is the problem of induction that I was referring to earlier in the discussion. Just because we have scientifically tested that the Higgs boson exists between 2012 and today doesn't mean that we can extrapolate from 12 years to infinitely far in the future.

An empiricist far in the future would still want to scientifically test that what the LHC has proven in the 2010s still holds in their time, and that the laws of physics hasn't somehow changed in the meantime that replaced the Higgs boson with some other mechanism for breaking electroweak symmetry in the standard model.

Madeleine Birchfield (Aug 23 2024 at 23:27):

John Onstead said:

I disagree. No theory of MOND is capable of explaining the CMB or why some pairs of galaxies with the same mass and mass distribution have wildly varying stellar rotation curves. To explain the latter any such theory would have to either be internally inconsistent or vary across the universe like a scalar field, which would then just be dark matter again.

The radial acceleration relation predicted by MOND holds in galaxies at distances far beyond where dark matter ought to exist in galaxies and where the gravity ought to be Newtonian if the dark matter hypothesis held:

https://iopscience.iop.org/article/10.1088/1475-7516/2024/04/020

Wide binaries seem to follow MOND rather than Newtonian gravity - wide binaries are small enough that they shouldn't have any dark matter in them according to the dark matter hypothesis:

https://academic.oup.com/mnras/article/525/1/1401/7236869

Here's a paper from 2022 which summerises the status of dark matter and MOND using all the experimental evidence available for both, and which eventually concludes that MOND is favoured over dark matter:

https://www.mdpi.com/2073-8994/14/7/1331

Madeleine Birchfield (Aug 23 2024 at 23:32):

Dark matter as an explanation for galaxy dynamics was a plausible hypothesis around 2018 but many of the astrophysical discoveries since 2018 has shifted the balance towards MOND.

Madeleine Birchfield (Aug 23 2024 at 23:42):

Now, dark matter might still be needed to explain some cosmological effects such as early universe structure formation, but dark matter is having some issues there as well. Recent discoveries of very distant and very bright galaxies by the JWST indicates that structure formation in our universe is faster by three orders of magnitude than that predicted by dark matter + the rest of the concordance model of cosmology, and it is primarily the dark matter part of the model which influences early universe structure formation. So I think it likely that dark matter here will end up getting swapped out with something that can make structure form faster in the universe, even if it might not be MOND.

Madeleine Birchfield (Aug 23 2024 at 23:51):

On the other hand, with the Hubble tension and the S8 tension and the cosmic dipole anisotropies and the CMB anisotropies and the KBC void, I think it likely that the cosmological principle itself and the FLRW metric will get thrown out the window in cosmology, and then who knows what will cosmology look like a decade from now, if cosmological dark matter is even going to be relevant then.

John Onstead (Aug 24 2024 at 02:11):

Interesting points! I can see the logic in how physicists would want to test to make sure that the laws of physics don't change with time. I'm not too worried about the Higgs boson in particular, though- if that were to change, we'd know. Or, well, we wouldn't, since at that very moment we'd all be wiped out by the vacuum decay bubble expanding at the speed of light!

As for dark matter vs MOND, the articles presented are very interesting and do point to anomalies with the so-called standard model of cosmology (lambda-CDM). I already think lambda-CDM needs an update, because CDM might not be the best fitting model of dark matter (others exist, such as fuzzy dark matter, the dark sector with multiple dark matter particles, self-interacting dark matter, warm dark matter such as due to right handed neutrinos, etc.) and dark energy might not be as constant as we'd thought thanks to DESI results.

At the same time each article presented has also had a counter-article published that refutes the claims. For instance, the wide binary data from GAIA was a major point of controversy last year, with articles firing back and forth from both sides. From my perspective at least, the matter seemed settled by the paper which not only indicated a very low probability for MOND, but also explained why the authors of the paper you presented got the results they did: https://academic.oup.com/mnras/article/527/3/4573/7342478. Fun fact, the lead author Banik of this paper is the very same author as the paper from 2022 you cited! So this paper isn't biased against MOND since the lead author was formerly one of its supporters.

John Onstead (Aug 24 2024 at 02:12):

The JWST results of early formation were a significant anomaly when first reported. Recent results indicate, however, that the initial results overestimated the masses of the galaxies: https://academic.oup.com/mnras/advance-article/doi/10.1093/mnras/stae1547/7697173. While anomalies remained in regards to supermassive black holes, even more recent results has indicated the problem was less to do with the standard model of cosmology and more to do with our model of how black holes formed in the early universe. Traditionally we considered SMBHs to form in the following order: stars form -> collapse -> stellar mass black hole -> black hole mergers -> SMBH. Indeed, there's not enough time for this to have been the method to form SMBH and galaxies around them to match with JWST. But when astrophysicists considered another mechanism of SMBH formation, direct collapse out of dense gas clouds in the early universe, the model matched the observations perfectly!

Interestingly about the hubble tension, an article very recently came out by Wendy Freedman: https://arxiv.org/abs/2408.06153. It uses different methods to test the hubble constant and finds some to be in agreement with the CMB data in opposition to the tension, while also confirming that there is still very much a tension when using Cepheid variable stars. While conclusions may vary, I think it's likely this points to the hubble tension not being an actual problem with cosmology, and more to do with a systematic error in Cepheid analysis.

The most interesting point/article to me is the first one, but only because it has come out recently and so not enough time has gone by for a response. But I imagine this only rules out dark matter models where dark matter solely forms very dense clumps. But astrophysicists have already been moving away from those given they cause problems, such as the "core-cusp problem" and "missing satellites problem". Other forms of dark matter that don't clump as much are still consistent with the results since the galaxy halos they form will inevitably be much larger and dissipate less suddenly than those predicted by standard CDM.

This discussion has been very illuminating! I should stop here before I derail it too much :)

Madeleine Birchfield (Aug 24 2024 at 03:06):

John Onstead said:

Interestingly about the hubble tension, an article very recently came out by Wendy Freedman: https://arxiv.org/abs/2408.06153. It uses different methods to test the hubble constant and finds some to be in agreement with the CMB data in opposition to the tension, while also confirming that there is still very much a tension when using Cepheid variable stars. While conclusions may vary, I think it's likely this points to the hubble tension not being an actual problem with cosmology, and more to do with a systematic error in Cepheid analysis.

Meanwhile, the SH0ES group has published a paper shortly after on the exact same data set that the Freedman group used: https://arxiv.org/abs/2408.11770. They came to the exact opposite conclusion that the Freedman group did, that the H0 values for TRGB and JAGB were around the Cepheid H0 value, implying that the Hubble tension is still there and not likely due to Cepheid systematics.

Madeleine Birchfield (Aug 24 2024 at 03:36):

John Onstead said:

I already think lambda-CDM needs an update, because CDM might not be the best fitting model of dark matter (others exist, such as fuzzy dark matter, the dark sector with multiple dark matter particles, self-interacting dark matter, warm dark matter such as due to right handed neutrinos, etc.) and dark energy might not be as constant as we'd thought thanks to DESI results.

Fundamentally, there are two different kinds of dark matter that would be needed in the current dominant paradigm, and this distinction mostly goes unmentioned in these dark matter discussions.

The dark matter required in galaxies and galaxy clusters need to be some kind of baryonic matter whose behaviour is able to minic the MOND gravity force law, and so would have to be some kind of non-cold dark matter like self-interacting dark matter or superfluid dark matter, etc.

However, the dark matter in cosmology requires that the dark matter be cold and non-baryonic, so that they can get the Lambda CDM model to fit CMB observations and early universe structure formation (prior to JWST), something that wouldn't work with the non-cold baryonic matter needed in galaxies and galaxy clusters.

So it's not that Lambda CDM needs an update to dark matter, but that it's two separate debates entirely.

Madeleine Birchfield (Aug 24 2024 at 03:47):

The problem for ongoing particle dark matter experiments is that so far they only have been trying to discover the cold dark matter in cosmology - the WIMPs, axions, etc...

If they do end up discovering something like WIMPs or axions and confirm the dark matter part of the Lambda CDM model, it will not resolve the dark matter in galaxies question, since WIMPs and axions do not behave in a manner which can mimic MOND in galaxies.

Madeleine Birchfield (Aug 24 2024 at 04:02):

John Onstead said:

At the same time each article presented has also had a counter-article published that refutes the claims. For instance, the wide binary data from GAIA was a major point of controversy last year, with articles firing back and forth from both sides. From my perspective at least, the matter seemed settled by the paper which not only indicated a very low probability for MOND, but also explained why the authors of the paper you presented got the results they did: https://academic.oup.com/mnras/article/527/3/4573/7342478. Fun fact, the lead author Banik of this paper is the very same author as the paper from 2022 you cited! So this paper isn't biased against MOND since the lead author was formerly one of its supporters.

The Banik paper wasn't so conclusive in my eyes because there was a lot of controversy over how he chose his sample in a manner that may have caused him to misidentify a particular MOND behaviour called the "external field effect" as Newtonian behaviour, since Banik's data never reaches into the Newtonian regime to detect any difference between the Newtonian regime and the MOND external field effect regime.

The external field effect occurs when the wide binaries are in some external gravitational field, here the Milky Way. The orbits act like they do in Newtonian gravity but where Newton's constant $G$ is multiplied by some scalar factor greater than 1 that is dependent on the MOND acceleration limit parameter $a_0$ and the strength of the external gravitational field and a few other things. This is discussed here:

https://tritonstation.com/2023/11/23/a-post-in-which-some-value-judgements-are-made-about-the-situation-with-wide-binaries/

Madeleine Birchfield (Aug 24 2024 at 04:20):

So the best thing to do right now is to wait for more data to come in on the wide binary debate and the Hubble tension.

But I believe it likely that the data that comes in the future will simply strengthen the trends of the Hubble tension being a real issue and not just systematics, and the trends of anomalies popping up everywhere that look like MOND behaviour.

Morgan Rogers (he/him) (Aug 24 2024 at 11:12):

Federica Pasqualone said:

Great then, as tradition wants: Any questions? :mic:

I'm really enjoying having a discussion being actively led by someone, this is fun. Thanks @Federica Pasqualone

Federica Pasqualone (Aug 24 2024 at 11:48):

Morgan Rogers (he/him) said:

Federica Pasqualone said:

Great then, as tradition wants: Any questions? :mic:

I'm really enjoying having a discussion being actively led by someone, this is fun. Thanks Federica Pasqualone

I'm glad to hear that! @Morgan Rogers (he/him) Anytime!

Madeleine Birchfield (Aug 24 2024 at 16:37):

Madeleine Birchfield said:

Since we're here at the frontiers of physics, I'm really tempted to go into another interpretation of "One universe as a foundation & friends" and talk about our current theories of physical cosmology.

Federica Pasqualone said:

Anyone on multiverse theory? :rolling_on_the_floor_laughing:

All right, let's talk about the multiverse.

The multiverse is a philosophical hypothesis which says that there is more than one universe. This hypothesis is currently untestable for the forseeable future, and so it isn't scientific.

In physics, the multiverse comes into multiple flavours.

Madeleine Birchfield (Aug 24 2024 at 16:37):

There is the string theory multiverse, where the multiverse is just a philosophical argument to justify why there are at least $10^{500}$ possible string theories. I don't really take these multiverse arguments seriously because ultimately most string theorists still hope for and believe in the one true unified field theory of everything, which ultimately means selecting one of the $10^{500}$ string theories and arguing why this one is favoured over the other string theories. The multiverse argument mostly is used to shut up critics of string theory who say that $10^{500}$ string theories means that string theory is a worse framework than sticking with the existing framework of quantum field theory or moving to some other alternative framework for a theory of everything, because it's nearly impossible to find what they are looking for from $10^{500}$ theories, or because $10^{500}$ theories means that string theory becomes vacuous because it can basically explain everything and anything imaginably possible.

Madeleine Birchfield (Aug 24 2024 at 16:40):

Then there is the multiverse from inflation theory.

Madeleine Birchfield (Aug 24 2024 at 17:02):

Inflation theory is a philosophical theory from physical cosmology which says that, assuming that the universe is expanding, in the very early universe there was a period of exponential expansion of space. This was originally motivated as a way to make space flat, but then it was later discovered that in many models of inflation, the exponential expansion of space tends to expand forever, with only pockets of space with slower expansion.

If we interpret pockets of space with slower expansions as universes, the fact that there are many of these pockets of space separated by a vast gulf of exponentially expanding space means that there are multiple universes, hence the multiverse.

However, this is just one interpretation of the models of inflation, and another interpretation is just that there is only one universe where space just happens to expand faster in some places and slower in others and as a result it's impossible to get from one patch of slowly expanding space to another patch of slowly expanding space due to the exponentially expanding space in between, giving the illusion that there are multiple universes.

Madeleine Birchfield (Aug 24 2024 at 17:07):

The reason why inflation theory, while part of physics via physical cosmology, isn't a scientific theory, is because there is no observational evidence for anything before the cosmic microwave background. We don't even know if there is even a cosmic neutrino background, and nearly all inflation theories would have inflation occurring and ending orders of magnitudes before the cosmic neutrino background.

So all that is occurring is philosophical theorising from mathematical models and numerical simulations using the big bang theory as an underlying framework.

Federica Pasqualone (Aug 24 2024 at 17:08):

Welcome back guys! :smirk:
First off, lemme thank you once more @Madeleine Birchfield for the wonderful explanations and all the readers (silent and not) for making this discussion so successful! Thank you all!

Federica Pasqualone (Aug 24 2024 at 17:10):

Federica Pasqualone said:

Anyone on multiverse theory? :rolling_on_the_floor_laughing:

It seems here I cannot make jokes anymore ... :joy:

Federica Pasqualone (Aug 24 2024 at 17:13):

I am wondering how many of you are familiar with the basics of cosmology theory ... the physical one :)
Lemme pull out a good book ... :heart_eyes:

Madeleine Birchfield (Aug 24 2024 at 17:19):

Federica Pasqualone said:

Federica Pasqualone said:

Anyone on multiverse theory? :rolling_on_the_floor_laughing:

It seems here I cannot make jokes anymore ... :joy:

I just wanted to talk about a topic that was related to "One universe as a foundations & friends", and I felt the multiverse was suitably close to that.

Kevin Carlson (Aug 24 2024 at 17:22):

I’m surprised you described two multiverse theories, neither of which is the many worlds interpretation of quantum mechanics! That’s the only one I knew about: as I understand it, it basically says that when a wave function collapses, the universe actually branches out into versions where each possibility happened. This makes for quite a lot of near-parallel as well as very different universes; it’s quite mind-boggling to try to imagine any space that might parametrize them all.

Madeleine Birchfield (Aug 24 2024 at 17:23):

But i actually forgot another version of the multiverse.

There is a multiverse in mathematics. It's called the set-theoretic multiverse, and it's basically the philosophical position of pluralism applied to set-theoretic foundations.

Federica Pasqualone (Aug 24 2024 at 17:23):

Madeleine Birchfield said:

Federica Pasqualone said:

Federica Pasqualone said:

Anyone on multiverse theory? :rolling_on_the_floor_laughing:

It seems here I cannot make jokes anymore ... :joy:

I just wanted to talk about a topic that was related to "One universe as a foundations & friends", and I felt the multiverse was suitably close to that.

That's an amazing topic! and you're right: It fits well with the title.

Federica Pasqualone (Aug 24 2024 at 17:25):

And I wanted also to suggest, as I usually do here, a book: "Introduction to cosmology" by Barbara Ryder :nerd: :books:

Federica Pasqualone (Aug 24 2024 at 17:28):

Madeleine Birchfield said:

But i actually forgot another version of the multiverse.

There is a multiverse in mathematics. It's called the set-theoretic multiverse, and it's basically the philosophical position of pluralism applied to set-theoretic foundations.

:rolling_on_the_floor_laughing: please now let's go back to physics hahhahahah

Madeleine Birchfield (Aug 24 2024 at 18:02):

Kevin Carlson said:

I’m surprised you described two multiverse theories, neither of which is the many worlds interpretation of quantum mechanics! That’s the only one I knew about: as I understand it, it basically says that when a wave function collapses, the universe actually branches out into versions where each possibility happened. This makes for quite a lot of near-parallel as well as very different universes; it’s quite mind-boggling to try to imagine any space that might parametrize them all.

The philosophy of quantum mechanics is a subject that I haven't gone too deeply into.

The thing is that it's primarily talking about particle quantum mechanics, while we know from quantum field theory and the standard model of particle physics that particles are just excitations of fermion fields and boson fields which span the entire universe, including any of the detectors themselves which are measuring the particles.

What gets interpreted as wave function collapse is actually in my opinion the collapse of the particle approximation - the particle has interacted with a detector, which is a very complex quantum system made of interacting fermion and boson fields - and the particle is no longer a free particle, it has become part of the complex quantum system that is the detector. One has to take into account the state of the fermion and boson fields which comprise the detector, which nobody really does when talking about wave function collapse.

Federica Pasqualone (Aug 24 2024 at 18:36):

This reminds me of how I started a couple of talks last year speaking of observables in the quantum world.
Here it is the video: https://www.youtube.com/watch?v=NvzSLByrw4Q

Federica Pasqualone (Aug 24 2024 at 18:38):

Popcorn? :popcorn:

Federica Pasqualone (Aug 24 2024 at 18:51):

Thanks @Kevin Carlson for bringing it up!

Madeleine Birchfield (Aug 24 2024 at 18:53):

There are a lot of issues in particle quantum mechanics which simply disappear when you move to relativistic quantum field theories like the standard model.

For example, in quantum mechanics, there is the delayed-choice quantum eraser experiment, which seems to indicate that retrocausality is possible. However, Philippe Eberhard proved here that it is actually never possible to detect retrocausality in a relativistic quantum field theory, and our universe is currently described by one - the standard model of particle physics.

Spencer Breiner (Aug 24 2024 at 19:10):

Madeleine Birchfield said:

What gets interpreted as wave function collapse is actually in my opinion the collapse of the particle approximation - the particle has interacted with a detector, which is a very complex quantum system made of interacting fermion and boson fields - and the particle is no longer a free particle, it has become part of the complex quantum system that is the detector.

I'm a bit confused by this response. Are you saying that the state of the detector should determine whether I measure spin up or spin down?

The basic point seems to be that there were two possible outcomes before the measurement, and either both happened, but can't interact, or only one does. How do fields address this dilemma?

Federica Pasqualone (Aug 24 2024 at 19:17):

Spencer Breiner said:

Madeleine Birchfield said:

What gets interpreted as wave function collapse is actually in my opinion the collapse of the particle approximation - the particle has interacted with a detector, which is a very complex quantum system made of interacting fermion and boson fields - and the particle is no longer a free particle, it has become part of the complex quantum system that is the detector.

I'm a bit confused by this response. Are you saying that the state of the detector should determine whether I measure spin up or spin down?

The basic point seems to be that there were two possible outcomes before the measurement, and either both happened, but can't interact, or only one does. How do fields address this dilemma?

Lemme explain this business a little more. If you want to measure the length of your desk, for instance, what do you do? You grab a metric tape and read the measurement. Nothing happens neither to the desk nor to the tape, isn't it?

fosco (Aug 24 2024 at 19:17):

Madeleine Birchfield said:

More importantly i guess, do you use excluded middle in your logic or not?

Only true logicians will answer "yes" here

fosco (Aug 24 2024 at 19:21):

sorry to hijack back the discussion to logic

Federica Pasqualone (Aug 24 2024 at 19:21):

And if you repeat the measurement the day after most probably (up to a $\delta s$) you will read the same result. Here is not the case, @Spencer Breiner. The fact that in order to make a measurement an instrument has to be introduced changes the whole thing!

Federica Pasqualone (Aug 24 2024 at 19:24):

fosco said:

sorry to hijack back the discussion to logic

haha no worries! Are you suggesting we should talk about the set-theoretic multiverse theory? @fosco :rolling_on_the_floor_laughing:

fosco (Aug 24 2024 at 19:27):

Can you summarize what the discussion has been about so far? It feels.. scattered.

Federica Pasqualone (Aug 24 2024 at 19:31):

Sure! After pointless topology, we moved to open issues in theoretical physics and then we started giving some arguments and references on the Standard Model, Cosmology and Multiverse theory. There were comments about both the experimental physics side and the philosophical one.

Federica Pasqualone (Aug 24 2024 at 19:32):

Am I forgetting anything?

Madeleine Birchfield (Aug 24 2024 at 19:33):

fosco said:

Can you summarize what the discussion has been about so far? It feels.. scattered.

So we began with discussing the different kinds of predicativity in mathematics, then made a huge detour into discussing intuitionistic Zermelo-Frankel set theory. Then I asked Federica if she used excluded middle and then we got into a discussion on how it would be a real challenge for constructive mathematicians to do mathematical physics. Then it segued to a discussion about the path integral in quantum field theory and about the standard model of particle physics, and then we started talked about the theories of everything.

Madeleine Birchfield (Aug 24 2024 at 19:38):

Then I had a conversation about my views on dark matter vs MOND and the Hubble tension, before finally ending up at the multiverse.

fosco (Aug 24 2024 at 19:41):

I was surprised when you said that no one seems to be doing / have done measure theory without LEM (that's the bunch of messages where I stayed for a while)

fosco (Aug 24 2024 at 19:42):

I think the challenge then, besides particle physics, might be making ergodic theory constructive (and that would be a fun thing to read)

fosco (Aug 24 2024 at 19:44):

also, I'd like to hear Urs opinion on the matter...

Madeleine Birchfield (Aug 24 2024 at 19:50):

fosco said:

I was surprised when you said that no one seems to be doing / have done measure theory without LEM (that's the bunch of messages where I stayed for a while)

Actually, my statement is incorrect. Steve Vickers did do some measure theory in geometric logic, and thus did not use LEM, such as in this paper:

https://arxiv.org/abs/2312.05228

However, it was mostly in the context of real analysis. I am not aware of anybody has pushed it towards probability theory yet.

I'll have to go through Steve Vickers's sources and other papers to see if this was entirely developed on his own or if he took some developments from other authors as well.

Madeleine Birchfield (Aug 24 2024 at 20:01):

fosco said:

also, I'd like to hear Urs opinion on the matter...

From what Urs Schreiber wrote in [[Science of Logic]], it seems that he believes that excluded middle should hold for at least the discrete types / infinity-groupoids since he identifies the sharp modality with $\mathrm{loc}_{\neg \neg}$, which wouldn't be the case in constructive mathematics.

Madeleine Birchfield (Aug 24 2024 at 20:05):

But it would be better to ask him directly.

Madeleine Birchfield (Aug 24 2024 at 20:16):

fosco said:

I was surprised when you said that no one seems to be doing / have done measure theory without LEM (that's the bunch of messages where I stayed for a while)

From what I can also tell, @Toby Bartels has also done some constructive measure theory as well; see for example [[Cheng space]] (who he attributed to a Henry Cheng but provided no references) and [[measurable locale]] and [[locale of real numbers]]. But the things that Bartels put on the nLab seem to be either from some unknown source or original research.

Madeleine Birchfield (Aug 24 2024 at 20:19):

But I don't really know anything else doing constructive measure theory. Measurable locales were developed by Dmitri Pavlov and he uses classical logic, there is a related approach using $\sigma$-locales by Alex Simpson but he also uses classical logic.

fosco (Aug 24 2024 at 20:25):

A ref that comes to mind is http://www.contrib.andrew.cmu.edu/~awodey/students/jackson.pdf which although is classical (is it? I just skimmed the intro and I have read a few paragraphs years ago..)

fosco (Aug 24 2024 at 20:25):

seems to connect well with whatever theory of measurable locales is out there.

Madeleine Birchfield (Aug 24 2024 at 20:27):

Now that I'm digging into the references in the Steve Vickers paper, there is actually a lot of constructive measure theory, but none of it is actually mentioned on the nLab.

Example, this paper by Thierry Coquand and Bas Spitters: https://arxiv.org/pdf/0808.1522

Madeleine Birchfield (Aug 24 2024 at 20:30):

Then in the references of the the Coquand-Spitters paper there is this paper by the first author:

https://link.springer.com/article/10.1007/s11117-004-7399-0

and this paper by Coquand and Erik Palmgren:

https://link.springer.com/article/10.1007/s001530100123

and this paper by Spitters:

https://www.cs.au.dk/~spitters/obs.pdf

fosco (Aug 24 2024 at 20:35):

nice

Madeleine Birchfield (Aug 24 2024 at 20:47):

Before he moved on to study homotopy type theory, Bas Spitters himself has authored a few papers with Chris Heunen above which has interpreted some quantum physics in constructive mathematics:

• The Gelfand spectrum of a noncommutative C*-algebra: a topos-theoretic approach

• Bohrification of operator algebras and quantum logic

Madeleine Birchfield (Aug 24 2024 at 21:02):

Chris Heunen said:

But for that theorem you in fact don't need Soler! Matthew Di Meglio and I figured out how to relate categorical colimits to analytic limits of real numbers directly, which is much more satisfying. See also Matt's nice blog post on the process of how that came to be.

Well here the issue is that I'm not aware of anybody who has proven that DeMarr’s theorem, which replaced Soler's theorem, holds in constructive mathematics.

I suspect that DeMarr's theorem won't hold in constructive mathematics because there are multiple Archimedean ordered Heyting fields (which are partially ordered semifields) which are sequentially complete and thus are monotone sequentially complete, but are not provably equivalent to each other.

And there are axiom sets that one can add to constructive mathematics to show that there are two provably inequivalent sequentially complete Archimedean ordered fields: the LPO and Brouwer's continuity principle for Dedekind reals show that the Escardo-Simpson reals (the initial sequentially compete Archimedean ordered field) are inequivalent to the Dedekind reals (the terminal sequentially compete Archimedean ordered field) - the former is a discrete field with LPO while the latter is provably not a discrete field with Brouwer's continuity principle.

Madeleine Birchfield (Aug 24 2024 at 21:08):

I also suspect the partial order wont be enough and one actually needs the constructive strict order structure on semifields.

Toby Bartels (Aug 25 2024 at 00:37):

Madeleine Birchfield said in part:

From what I can also tell, Toby Bartels has also done some constructive measure theory as well; see for example [[Cheng space]] (who he attributed to a Henry Cheng but provided no references) and [[measurable locale]] and [[locale of real numbers]]. But the things that Bartels put on the nLab seem to be either from some unknown source or original research.

Henry Cheng's work is described in the updated version (by Douglas Bridges) of Errett Bishop's book on constructive analysis; that's the source for the nLab page. There are references to Cheng's papers in that book, but I haven't ever read those. The contribution by Todd and me described there as abstract nonsense is really just the observation that Cheng was working with a Chu space; this also connects to Mike Shulman's work on the antithesis interpretation of linear logic in constructive mathematics (which had not been done yet).

The only thing constructive about measurable locales is that since they have so many equivalent formulations, I have an intuition that one of them is more likely to work out constructively, so I said so. It is important to realize, since locales provide a constructive approach to topology, that they do not as yet provide a constructive approach to measure theory, but I don't know how to fix that.

As for the locale of real numbers, the constructive formulation and proof of Cousin's Theorem, and the resolution that follows of the paradox that the set of real numbers has measure zero in Russian constructivism, are my original work as far as I know. But I never worked out anything beyond what I wrote there on the nLab. It makes me feel better to think that a constructive treatment of the Henstock–Kurzweil integral is not out of the question, but I don't have such a treatment myself.

Spencer Breiner (Aug 25 2024 at 03:23):

Federica Pasqualone said:

And if you repeat the measurement the day after most probably (up to a $\delta s$) you will read the same result. Here is not the case, Spencer Breiner. The fact that in order to make a measurement an instrument has to be introduced changes the whole thing!

I still don't see the relevance. Can you be more specific?

Are you suggesting that the measurement is deterministic given the joint state of particle and measuring device? If not, how does the probability of the unrecorded result migrate (collapse?) to the observed branch? In particular, what do fields have to do with this difference.

Also, I'm under the impression that repeated measurements after the first will continue to see the same result, modulo other interactions with the particle.

Madeleine Birchfield (Aug 25 2024 at 14:24):

Toby Bartels said:

Henry Cheng's work is described in the updated version (by Douglas Bridges) of Errett Bishop's book on constructive analysis; that's the source for the nLab page. There are references to Cheng's papers in that book, but I haven't ever read those.

Is this the textbook you are referring to?

https://link.springer.com/book/10.1007/978-3-642-61667-9

Toby Bartels (Aug 25 2024 at 14:44):

Madeleine Birchfield said:

Is this the textbook you are referring to?

https://link.springer.com/book/10.1007/978-3-642-61667-9

Yes! And if you scroll down, Springer offers a PDF file of the end matter, including the bibliography, where you can find Cheng's name three times. So presumably those are the papers where this is developed. (It's also summarized in Chapter 6 of the book, Integration, which I read about 20 years ago.)

Madeleine Birchfield (Aug 25 2024 at 14:52):

Toby Bartels said:

Madeleine Birchfield said:

Is this the textbook you are referring to?

https://link.springer.com/book/10.1007/978-3-642-61667-9

Yes! And if you scroll down, Springer offers a PDF file of the end matter, including the bibliography, where you can find Cheng's name three times. So presumably those are the papers where this is developed. (It's also summarized in Chapter 6 of the book, Integration, which I read about 20 years ago.)

What seemed to have tripped people up in the past is that on the nLab you had linked to "[[Handbook of Constructive Analysis]]", which was not the name of the above book, and lead to a non-existent page on the nLab. The actual title of the book was "[[Constructive Analysis]]" and does lead to nLab's article on the Bishop and Bridges textbook.

Mike Shulman asked about this a few years ago on the nForum but didn't get a definitive yes-or-no answer to his question.

Toby Bartels (Aug 25 2024 at 15:32):

Madeleine Birchfield said:

What seemed to have tripped people up in the past is that on the nLab you had linked to "[[Handbook of Constructive Analysis]]", which was not the name of the above book, and lead to a non-existent page on the nLab. The actual title of the book was "[[Constructive Analysis]]" and does lead to nLab's article on the Bishop and Bridges textbook.

Mike Shulman asked about this a few years ago on the nForum but didn't get a definitive yes-or-no answer to his question.

Sorry, I didn't notice that mistake! Yes, HCA should be FCA (which strictly speaking is only the title of the first edition, by Bishop alone; Bridges shortened the name for the revised edition, which is the one that covers the work by Cheng).

James E Hanson (Aug 25 2024 at 19:42):

What arguments are there that basing constructive measure theory on locales in particular is a good idea (over and above something like the metric Boolean algebras of Coquand and Palmgren or even a point-set approach as in Bishop and Cheng)?

Locales seem very poorly suited for recovering the already known computational content of measure theory. They're complete lattices and don't have well-behaved complements. You cannot make a non-trivial constructive measure theory in which measures are Dedekind or Cauchy reals and the collection of measurable 'things' is a complete lattice or even a countably complete lattice: There is a computably presentable open subset of $[0,1]$ whose measure is not computable.

Madeleine Birchfield (Aug 25 2024 at 19:56):

James E Hanson said:

What arguments are there that basing constructive measure theory on locales in particular is a good idea (over and above something like the metric Boolean algebras of Coquand and Palmgren or even a point-set approach as in Bishop and Cheng)?

In constructive mathematics, [[measurable locales]] are a misnomer because they cannot be proven to be locales constructively. So in the conversation above we aren't talking about using locale theory for measure theory.

James E Hanson (Aug 25 2024 at 21:18):

I guess then my question is why is there a mystery about the 'right' way to do measure theory constructively? We already have a constructive point-free approach to measure theory (i.e., metric Boolean algebras) that is about as good as one could plausibly hope for and agrees with real analysts' existing intuition about what the 'actual content' of measure theory is. In order to make it entirely smooth, one either needs to work with the Cauchy reals and track codes of objects explicitly (or implicitly, as ends up happening with setoid presentations such as the one in Coquand and Palmgren) or one needs countable choice, but this is already true classically and countable choice has a computational interpretation.

For example, if we want to think about the typical measure theory on $[0,1)$, we can start by looking at the formal Boolean algebra $\mathcal{I}$ of finite unions of intervals of the form $[a,b)$. It is easy to then define the typical notion of measure on $\mathcal{I}$ and show that $d(A,B) = \mu(A)+\mu(B) - 2\mu(A \wedge B)$ is a metric. We can then take the completion of $\mathcal{I}$ with regards to this metric, which gives the formal probability algebra of 'measurable subsets of $[0,1)$'. Call this $\mathcal{P}$. Then you show that the measure and the meet, join, and complement operations are all Lipschitz on $\mathcal{I}$ and so extend canonically to all of $\mathcal{P}$, yielding a metric Boolean algebra. Then you can then start defining things like $L^p$ spaces using formal simple functions (or you could even start with formal simple functions based on $\mathcal{I}$).

You can even connect it back to a more traditional point-set approach. In particular, I believe you can define a constructive point-set notion of Lebesgue measurable subset of $[0,1)$ that also recovers $\mathcal{P}$ and has other nice properties such as positive measure sets being inhabited and knowing that for a sequence of measurable sets $(A_i)_{i \in \mathbb{N}}$, the union $\bigcup_{i \in \mathbb{N}}A_i$ is measurable if $\lim_{n \to \infty} \mu \left(\bigcup_{i < n}A_i\right)$ exists in the Cauchy reals. Bishop and Cheng already identified that this extra condition is really the only thing you need to make point-set measure theory work constructively. The possibility of such an approach to measure theory follows from their work but is also implicit in some work on computable measure theory (such as that of Schnorr). Again this needs countable choice, but without it one should be able to more or less recover an analogous theory using coded sets (such as in the chapter on choiceless measure theory in Fremlin). Measure theory on non-finite measure spaces (such as $\mathbb{R}$) shouldn't be that much harder, if a little annoying.

Madeleine Birchfield (Aug 25 2024 at 21:33):

I guess then my question is why is there a mystery about the 'right' way to measure theory constructively?

Because most likely when @Toby Bartels was writing the nLab's article on measurable locales in 2011 he wasn't aware of Coquand and Palmgren's point-free approach to measure theory.

Madeleine Birchfield (Aug 25 2024 at 21:36):

As I mentioned above, there's a lot of constructive measure theory which isn't on the nLab.

Madeleine Birchfield (Aug 25 2024 at 22:01):

Going back to a comment posted by John Baez,

John Baez said:

As for mathematical physics using constructive reasoning, it will definitely be fun for constructivists to build up the framework of analysis required to do more and more mathematical physics. But to get more mathematical physicists interested, it would be helpful to come up with some examples of where constructivism might help us understand physics. E.g. some ways in which a locale of real numbers is "better" - for the purposes of physics, not logic! - than the usual set of real numbers.

The issue here is that, already in constructive real analysis, there are multiple notions of real numbers which are not provably the same but which are each important in the subject.

In some constructive approaches to integration, lower integrals are defined using the lower Dedekind reals, while upper integrals are defined using the upper Dedekind reals, and neither the lower reals nor the upper reals are provably equivalent to the Dedekinds themselves without excluded middle. The lower reals are also used to define metric spaces in constructive mathematics.

For those interested in calculating digit representations of real numbers, the relevant notion of reals here are the Cauchy real numbers, which are not provably equivalent to the Dedekind reals without either excluded middle or countable choice.

There is also, as you mentioned, the locale of real numbers which is useful for proving some topological and analytic properties of the real numbers which cannot be proven in the point-set manner for the Dedekind reals.

I have a feeling that in constructive mathematical physics, many of these sets of real numbers are going to be used just to get some of the proofs and concepts working, just like in constructive real analysis.

Federica Pasqualone (Aug 26 2024 at 10:59):

Morning everyone! We are not taking any day off here! Very good :smirk:

Federica Pasqualone (Aug 26 2024 at 11:01):

Have a wonderful start of Fall semester 2024!

Federica Pasqualone (Aug 26 2024 at 11:03):

Anyways, Chu spaces, bornologies .... all great stuff! Thanks a lot for the references and the comments on the difficulties of measure theory ... and intuistionistic logic :heart_eyes: !
We are learning so much these days!

Federica Pasqualone (Aug 26 2024 at 11:08):

Before coming back to physics, let me add a little caveat to the whole enterprise - a caveat that sort of was also in the remark of John Baez: If you want to help the physics department, do not strive to write down 1.5K pages of abstract and rigorous math without any pragmatism, but rather let the spirit of physics guide your academic writing! :diya_lamp:

Madeleine Birchfield (Aug 26 2024 at 11:14):

Federica Pasqualone said:

Before coming back to physics, let me add a little caveat to the whole enterprise - a caveat that sort of was also in the remark of John Baez: If you want to help the physics department, do not strive to write down 1.5K pages of abstract and rigorous math without any pragmatism, but rather let the spirit of physics guide your academic writing! :diya_lamp:

Yeah, well the same could be said about many other things being done in mathematical physics. I don't think a lot of physicists actually care about stuff like Grady's and Pavlov's proof of the [[geometric cobordism hypothesis]] because it is a whole bunch of rigourous math which doesn't have much pragmatic relation to the stuff that physicists actually work with.

Similarly, physicists don't actually care whether the path integral can be formally defined in mathematics, while mathematicians working in mathematical physics do.

Federica Pasqualone (Aug 26 2024 at 11:15):

and also, since we are gossiping about him so much :rolling_on_the_floor_laughing: ...

You can recognize truth by its beauty and simplicity. When you get it right, it is obvious that it is right—at least if you have any experience—because usually what happens is that more comes out than goes in.... The inexperienced, the crackpots, and people like that, make guesses that are simple, but you can immediately see that they are wrong, so that does not count. Others, the inexperienced students, make guesses that are very complicated, and it sort of looks as if it is all right, but I know it is not true because the truth always turns out to be simpler than you thought.

~ Richard Feynman :heart:

Graham Manuell (Aug 26 2024 at 11:42):

James E Hanson said:

What arguments are there that basing constructive measure theory on locales in particular is a good idea (over and above something like the metric Boolean algebras of Coquand and Palmgren or even a point-set approach as in Bishop and Cheng)?

Locales seem very poorly suited for recovering the already known computational content of measure theory. They're complete lattices and don't have well-behaved complements. You cannot make a non-trivial constructive measure theory in which measures are Dedekind or Cauchy reals and the collection of measurable 'things' is a complete lattice or even a countably complete lattice: There is a computably presentable open subset of $[0,1]$ whose measure is not computable.

I don't know enough about measure theory per se to speak on it definitively, but I can say something about probability theory. I think there are strong arguments for including the topological structure of objects more or less in all circumstances, but especially in constructive mathematics. So in particular, I think it is helpful to do so when dealing with measures. Classically, the theory of valuations agrees with that measures in 'good' situations (Radon measures on compact Hausdorff spaces). It also works well constructively. Possibly using only opens leads to some issues with certain more advanced topics in measure theory, but analysis works pretty smoothly. I guess time will tell whether valuations are sufficient for practical considerations, but I tend to think they will be.

You are right that you don't use Dedekind reals for valuations (and certainly not Cauchy reals). Instead you use lower reals. I think this is intuitively the correct thing to do and I can say more on this if you like. I have some thoughts about how to recover Dedekind reals in certain cases, but it is work in progress, so I would rather not say too much about it yet.

Madeleine Birchfield (Aug 26 2024 at 11:52):

If I may ask, the lower and upper reals coincide with the Dedekind reals in classical mathematics. What other axioms imply that these sets coincide with each other?

Graham Manuell (Aug 26 2024 at 11:58):

They only coincide (modulo infinity) if you forget the topologies, so from the pointfree perspective they are always different. I know very little about 'pointy' constructive analysis, so I couldn't say.

Madeleine Birchfield (Aug 26 2024 at 12:05):

Graham Manuell said:

They only coincide (modulo infinity) if you forget the topologies, so from the pointfree perspective they are always different.

This kind of backs my point I made earlier in the thread that if one wants to use the locale of real numbers in constructive mathematical physics, chances are that one would end up using at least three locales of real numbers - those whose space of points are the lower reals, upper reals, and Dedekind reals, because of the heavy reliance on measure theory via integration and probability in mathematical physics.

Graham Manuell (Aug 26 2024 at 12:39):

Absolutely. But I think there are already three spaces being used classically. It's just that people don't always pay careful attention to the topologies.

Graham Manuell (Aug 26 2024 at 12:40):

For example, consider how lower semicontinuous functions are sometimes used in analysis.

Madeleine Birchfield (Aug 26 2024 at 13:02):

I'm just trying to think how this would end up working in real cohesion.

Assuming excluded middle for the discrete $\infty$-groupoids, one would have Dedekind reals $\mathbb{R}_D$, finite upper reals $\mathbb{R}_U$, and finite lower reals $\mathbb{R}_L$ all be inequivalent cohesive $\infty$-groupoids since they come naturally equipped with different topologies - order topology, upper semicontinuity, and lower semicontinuity respectively, but one would have weak equivalences $\flat \mathbb{R}_D \simeq \flat \mathbb{R}_U \simeq \flat \mathbb{R}_L$ since they all have the same points and thus are the same $\infty$-groupoid when equipped with the discrete topology.

James E Hanson (Aug 26 2024 at 15:34):

Madeleine Birchfield said:

If I may ask, the lower and upper reals coincide with the Dedekind reals in classical mathematics. What other axioms imply that these sets coincide with each other?

This is equivalent to LEM. Fix a sentence $\varphi$ and consider the lower real $x = \sup (\{0\} \cup \{1 : \varphi\})$. If we assume $x$ is a Dedekind real, then we have that either $x < \frac{2}{3}$ or $x > \frac{1}{3}$. In the first case we have $\neg \varphi$ and in the second we have $\varphi$.

James E Hanson (Aug 26 2024 at 15:50):

Graham Manuell said:

I think there are strong arguments for including the topological structure of objects more or less in all circumstances, but especially in constructive mathematics.

And what exactly are these arguments? I ask because from my perspective the relationship between measure theory and topology is subtle. $[0,1]$, $(0,1)$, and $2^\mathbb{N}$ are all equivalent as measure spaces (with their standard measures) and it's fairly straightforward to make sense of this fact constructively, so already we can see that considering things up to measure $0$ erases a huge amount of topological information (compactness, connectedness, etc.). Moreover one of the most important structural facts about regular measures is that every measurable set is equivalent to a $G_\delta$ set modulo a null set.

The other problem is just that, on a practical level, complementation is an extremely important basic operation in probability theory. It allows you to extent a lot of intuition gleaned from finite event spaces to infinite event spaces. Obviously exact complementation is problematic constructively, but in measure theory all that really matters is complementation modulo a null set, and this does work well constructively.

This is what I find so uncompelling about Simpson's locale of random reals and presumably other localic approaches to measure theory. There are dense open subsets of $[0,1]$ that have measure less than $1$, but the Heyting complement of these open sets is empty. Insisting on basing measure theory solely on open sets materially changes the mathematical content and character of the field.

Madeleine Birchfield (Aug 26 2024 at 16:16):

James E Hanson said:

This is what I find so uncompelling about Simpson's locale of random reals and presumably other localic approaches to measure theory.

IIRC Alex Simpson is also working with excluded middle and dependent choice the entire time, so this is also irrelevant to constructive mathematics.

Madeleine Birchfield (Aug 26 2024 at 16:21):

I brought up measurable locales and Alex Simpson's approaches as alternative approaches to measurable sets that I knew of, but they all used excluded middle to develop their theories and so aren't really suitable for constructive mathematics.

Similarly goes for the categorical approaches - Alex Simpson's topos of random probability sheaves assumes a Boolean topos satisfying dependent choice, and so isn't constructive.

Madeleine Birchfield (Aug 26 2024 at 16:27):

James E Hanson said:

Madeleine Birchfield said:

If I may ask, the lower and upper reals coincide with the Dedekind reals in classical mathematics. What other axioms imply that these sets coincide with each other?

This is equivalent to LEM. Fix a sentence $\varphi$ and consider the lower real $x = \sup (\{0\} \cup \{1 : \varphi\})$. If we assume $x$ is a Dedekind real, then we have that either $x < \frac{2}{3}$ or $x > \frac{1}{3}$. In the first case we have $\neg \varphi$ and in the second we have $\varphi$.

I suspect that this remains true if we take some $\sigma$-subframe $\Sigma \subseteq \Omega$ of the set of truth values $\Omega$, and use that to construct $\Sigma$-lower reals, $\Sigma$-upper reals, and $\Sigma$-Dedekind reals using functions $\mathbb{Q} \to \Sigma$ or pairs of such functions. Then that every $\Sigma$-lower or $\Sigma$-upper real is a $\Sigma$-Dedekind real is equivalent to LEM for all truth values in $\Sigma$. For the initial such $\sigma$-frame this would result in LPO, and for the set of truth values $\Omega$ itself this would result in the usual LEM.

Federica Pasqualone (Aug 26 2024 at 17:36):

Well, in any case I guess it would be nice to read through @Alex Simpson work ...

Federica Pasqualone (Aug 26 2024 at 17:38):

Maybe over the weekend we can also have a little discussion on the theory of locales and frames, just basic level - as we did for predicativity. So people can engage, ask questions, usw. Good idea?

Todd Trimble (Aug 26 2024 at 18:09):

(For people not familiar with German, usw = und so weiter = et cetera -- I assume this is what is meant)

Madeleine Birchfield (Aug 26 2024 at 18:39):

Todd Trimble said:

(For people not familiar with German, usw = und so weiter = et cetera -- I assume this is what is meant)

Probably, she did her masters at Göttingen before going to CMU so she should have some familiarity with the German language.

Madeleine Birchfield (Aug 26 2024 at 18:40):

Federica Pasqualone said:

Maybe over the weekend we can also have a little discussion on the theory of locales and frames, just basic level - as we did for predicativity. So people can engage, ask questions, usw. Good idea?

if I have time on the weekend, which I do not know yet.

Federica Pasqualone (Aug 26 2024 at 19:34):

Thanks a lot for explaining my abbreviations hahhah @Todd Trimble I am particularly skilled at code mixing when I am in a rush! :grinning:

Graham Manuell (Aug 27 2024 at 07:49):

@James E Hanson One reason is that every function that can be carried out in practice is going to be continuous, so it makes sense to record this information. Another is that almost all nonconstructive principles become valid when phrased in terms of locales instead of sets (for example, the product of nontrival sets being nontrivial). A third is that a topology is essentially precisely what is necessary to specify the points of an object not only in the current topos, but in every Grothendieck topos and so results that take it into account tend to be stable under change of base. Finally, it seems to get rid of a lot of pathologies, such as Banach-Tarski and the like.

Since I'm arguing for remembering the topology I'm not moved by the fact that certain different spaces coincide when you forget it.

Sometimes there will be open complements up to measure zero and this might be interesting to explore. I guess I am willing to bite the bullet on not being able to have complements in general that behave in the same way as the original opens (unlike closed sublocales, which can, of course, still be discussed).

I don't really understand what your criticism has to do with Simpson's approach, since he extends the valuation to every sublocale. There are still no complements in general, but the dense open sets you suggest do have complements in his approach. The pesudocomplement is a red herring. It doesn't play any role in any of these approaches as far as I know.

I suppose I agree that basing things on opens changes the character of the field, but I think it is for the good, or at least is unavoidable. I don't agree that it changes the content.

James E Hanson (Aug 27 2024 at 19:02):

@Graham Manuell I'm sorry but I'm not really moved by your arguments either. Basically, the broad issue to me is that real analysts already know what point-free measure theory is. Constructive mathematicians already know how to do this point-free measure theory constructively in a down-to-earth way that can be implemented in real-world computations. (In terms of your first statement this corresponds to the fact that the meaningful topology in measure theory is the topology induced by the metric on measurable sets.) Category theorists already know how to characterize Lebesgue integration in terms of a universal property. (And in particular, note that $L^1[0,1]$, $L^1(0,1)$, and $L^1(2^\mathbb{N})$ all satisfy this universal property, because measure spaces themselves are fundamentally not topological.) I don't really see how you can claim that basing measure theory on open sets is 'unavoidable' when people have evidently been able to avoid it just fine.

At the end of the day, what it means to be able to take complements in measure theory and probability theory is that if $f$ is a measurable function or a random variable, then $1-f$ is a measurable function or a random variable. You can start a theory of integration with something like semicontinuous functions on a locale (or something like the duals of maps from lower sets in $\mathbb{R}$ to sublocales of your locale), but at some point you're going to want to subtract one function from another or want to have your integrals be Cauchy or Dedekind reals so that you can actually produce a tangible number in a real-world computation, and at that point you need to introduce some kind of two-sided regularity condition and isolate a special class of 'measurable' functions. This is what I don't find compelling about Simpson's approach. It's often presented as if it 'fixes the existence of non-measurable sets,' but in order to actually do functional analysis with it you need to reintroduce something equivalent to the concept of measurability at some point.

Graham Manuell (Aug 28 2024 at 10:45):

@James E Hanson I'm not sure how down-to-earth it is to use a theory where you are required to assign measures to sets for which you have no ability to tell whether a point actually lies in that set (or similar such question). I don't really understand the operational meaning of saying that a randomly chosen point lies in some arbitrary Borel set with some probability. Maybe there is some way to make sense of this (which I would be interested to hear about), but it certainly seems less conceptually straightforward than the usual pointfree approach using valuations.

In any case, "unavoidable" was surely too strong, since almost anything can be avoided with sufficient effort, but I was mainly thinking of the case where we do want to consider the topologies (which for me is always). I can think of reasonable probability distributions on Sierpinski space where the probability of choosing $\top$ is just not a Dedekind real. It would seem that such cases would not fit into these other approaches and this feels like a deficiency.

If you are talking about random variables instead of measures, then these can be (Dedekind-)real-valued and there is no issue with taking $1-f$. You can integrate a (Dedekind-)real-valued function over a compact Hausdorff locale with a finite valuation to give a Dedekind real. (Of course, we necessarily restrict to continuous functions here, which I do not see as a disadvantage.) Just because the valuations take values in one-sided reals, does not mean we cannot consider real-valued integrals. In general, the functional analysis approach to measures (if done in an appropriately pointfree way) should be equivalent to valuations in this case. (I don't know if all of the details of this last part have actually been worked out yet, but a fair bit has been.)

I don't know the details of how integration would be handled in Simpson's approach (though I would be surprised if you really do need some restricted concept of measurable sublocale; measurable functions, sure, but we'd probably just restrict to continuous ones), but that approach is slightly different to the one I can advocating for (though I still think his approach is pretty cool).

Federica Pasqualone (Aug 28 2024 at 14:05):

Good morning measure theorists and QFT lovers! :sunglasses:
I am still down for an amazing basic discussion on lattice theory, don't worry ... coming soon! :books:

Federica Pasqualone (Aug 28 2024 at 14:07):

But also (metacomment): I hope we will have some rooms for group work at the next ACT2025! :sparkles:
It sounds like we have a lot to do here ... :nerd: don't we?

James E Hanson (Aug 28 2024 at 19:33):

Graham Manuell said:

(Of course, we necessarily restrict to continuous functions here, which I do not see as a disadvantage.)

Physicists (and other appliers of mathematics) use and integrate discontinuous functions all the time. Obviously it's heavily debatable whether there are any truly discontinuous phenomena in reality, but working with discontinuous functions is a practically useful idealization, much like the real numbers themselves. (See, for instance, shock wave weak solutions of PDEs.) If your theory of integration can only handle continuous functions (under the assumption that one wants to be able to subtract functions), then I'm sorry but you are changing the mathematical and practical content of the field.

Toby Bartels (Aug 29 2024 at 13:58):

Graham Manuell said in part:

I'm not sure how down-to-earth it is to use a theory where you are required to assign measures to sets for which you have no ability to tell whether a point actually lies in that set (or similar such question).

You can't even always tell whether a given point lies in a given open set. (If it does lie in the open set, then eventually you'll be able to tell, but if it doesn't, then you might not.) At least if the open set is a located interval, then for almost every point you can tell whether it belongs to the set, but even that doesn't work for arbitrary open sets. I agree that any open set can be given a lower real as a measure, but I can also see why one might consider a set to be measurable only when its measure is a Dedekind real (and perhaps the more general case should only be considered the outer measure).

I would be surprised if you really do need some restricted concept of measurable sublocale; measurable functions, sure, but we'd probably just restrict to continuous ones

Constructive analysis knows a lot of discontinuous functions that are defined almost everywhere, and I'd like to integrate those too.

Toby Bartels (Aug 29 2024 at 15:59):

Graham Manuell said in part:

Classically, the theory of valuations agrees with that measures in 'good' situations (Radon measures on compact Hausdorff spaces).

This reminds me that when Bourbaki got to measure spaces, they decided to only deal with Radon measures on (I think) locally compact Hausdorff spaces.

Measurable locales similarly capture only ‘good’ situations, specifically those that satisfy big theorems like the Radon–Nikodym Theorem, which are often stated only for σ-finite measures but also apply to some others. (This is why I got interested in them; and since I also like things to be constructive, that's why the nLab has some musings about how to make them constructive. The idea that locales=constructive is a red herring.)

Mike Shulman (Aug 29 2024 at 17:02):

James E Hanson said:

Physicists (and other appliers of mathematics) use and integrate discontinuous functions all the time.

Physicists also use and integrate things all the time that aren't even functions, like "$\delta$-functions". These can be defined mathematically as distributions, elements of the dual space of a space of smooth (and in particular continuous) functions. Discontinuous functions can also be considered (up to almost-everywhere equality) as particular distributions, even if the only actual "functions" are continuous. I don't know what the theory of distributions looks like constructively, but it would be one approach to make sense of the discontinuous functions used in applied mathematics, which would generalize the accepted way of making sense of the non-functions used in applied mathematics.

Graham Manuell (Aug 29 2024 at 18:36):

@James E Hanson I'm currently working on a paper with @Peter Faul on how to handle 'discontinuous' functions of the kind needed for things like shock waves. I don't think they would actually pose an issue for integration in this system either. I guess I don't really care whether you think it changes the content or not. In so far as it differs, why are you so certain that what the other approaches do is correct? I do care that it can model all physical phenomena, but I believe that with sufficient care it can. As @Mike Shulman notes, distributions should also be able to be accommodated.

Graham Manuell (Aug 29 2024 at 18:42):

Toby Bartels said:

You can't even always tell whether a given point lies in a given open set. (If it does lie in the open set, then eventually you'll be able to tell, but if it doesn't, then you might not.)

Indeed, this is why the measure needs to take values in the lower reals instead of the Dedekind reals.

At least if the open set is a located interval, then for almost every point you can tell whether it belongs to the set, but even that doesn't work for arbitrary open sets. I agree that any open set can be given a lower real as a measure, but I can also see why one might consider a set to be measurable only when its measure is a Dedekind real (and perhaps the more general case should only be considered the outer measure).

Okay, I can understand this perspective. This result about located intervals is very interesting and feels like it might be related to something I have been thinking about regarding valuations. Do you know somewhere can I read about this?

Graham Manuell (Aug 29 2024 at 18:46):

Toby Bartels said:

Constructive analysis knows a lot of discontinuous functions that are defined almost everywhere, and I'd like to integrate those too.

I haven't given it enough thought yet whether this is possible in the approach I am advocating for, but in Simpson's approach perhaps they they can be understood as maps out of the smallest sublocale of full measure?

Toby Bartels (Aug 29 2024 at 20:06):

Graham Manuell said in part:

Toby Bartels said:

At least if the open set is a located interval, then for almost every point you can tell whether it belongs to the set, but even that doesn't work for arbitrary open sets.

This result about located intervals is very interesting and feels like it might be related to something I have been thinking about regarding valuations. Do you know somewhere can I read about this?

It's nothing deep. It's just that if the interval is located, then it has a (possibly infinite) Dedekind real as both lower and upper endpoint (which depending on what one means by ‘interval’ one might assume anyway); and any point (Dedekind real) apart from the endpoints is either in the set or in its exterior (both open sets, so you can tell which). If ‘almost every’ means anything constructively in a pointwise context, then that includes everything distinct from a given two points.

But to be formal about it: If an interval 𝐼 is located, then its upper bound is given by the two-sided Dedekind cut

$$( \{ q \in \mathbb Q \; | \; \exists \, x \in I , \; q < x \} , \; \{ q \in \mathbb Q \; | \; \forall \, x \in I , \; q > x \} )$$

and similarly for the lower bound. And these are Dedekind reals because, given rational 𝑟 < 𝑠, the locatedness of 𝐼 immediately tells us that 𝑟 belongs to the lower set or 𝑠 belongs to the upper set (with the rest being obvious, allowing the upper or lower set to be empty to give ±∞). And then, writing the endpoints as 𝑎 and 𝑏, given any 𝜀 > 0, and any Dedekind real 𝑥, we have 𝑥 < 𝑎, 𝑎 − ⅕𝜀 < 𝑥 < 𝑎 + ⅕𝜀, 𝑎 < 𝑥 < 𝑏, 𝑏 − ⅕𝜀 < 𝑥 < 𝑏 + ⅕𝜀, or 𝑥 > 𝑏, meaning that each point in the Dedekind real number line belongs to at least one of the interior of 𝐼, the exterior of 𝐼, and a collection of (in this case two) open intervals whose total length converges to a Dedekind real less than 𝜀 (specifically to ⅘𝜀).

Toby Bartels (Aug 29 2024 at 20:15):

Graham Manuell said:

Toby Bartels said:

Constructive analysis knows a lot of discontinuous functions that are defined almost everywhere, and I'd like to integrate those too.

I haven't given it enough thought yet whether this is possible in the approach I am advocating for, but in Simpson's approach perhaps they they can be understood as maps out of the smallest sublocale of full measure?

Perhaps; I don't even know if there is a smallest sublocale of full measure, but it seems reasonable. You can treat common discontinuous functions (such as a square wave or a binning/bucketing function) up to almost-everywhere equality as continuous maps on an ad-hoc sublocale; and besides, you can treat any integrable function (or generalized function) up to almost-everywhere equality as a distribution (as Mike remarked), so I don't mean this as an argument against working with locales. It's just that in measure theory, we really don't want to restrict attention to continuous functions, so we do have to check that we can handle the others.

Madeleine Birchfield (Aug 29 2024 at 20:20):

Toby Bartels said:

I don't mean this as an argument against working with locales. It's just that in measure theory, we really don't want to restrict attention to continuous functions, so we do have to check that we can handle the others.

There's no guarantee that you'll have any discontinuous functions to work with even on the Dedekind reals in constructive mathematics. One version of Brouwer's continuity principle says that every function on the Dedekind reals is continuous and that principle is consistent with intuitionistic logic. If you want discontinuous functions on your Dedekind real numbers, then assume the [[analytic LPO]].

Toby Bartels (Aug 29 2024 at 20:33):

Madeleine Birchfield said:

Toby Bartels said:

I don't mean this as an argument against working with locales. It's just that in measure theory, we really don't want to restrict attention to continuous functions, so we do have to check that we can handle the others.

There's no guarantee that you'll have any discontinuous functions to work with even on the Dedekind reals in constructive mathematics. One version of Brouwer's continuity principle says that every function on the Dedekind reals is continuous and that principle is consistent with intuitionistic logic.

But there are lots of discontinuous functions that are defined almost everywhere, as I remarked upthread, and this is all that you need for measure theory. For example, the Heaviside step function is defined on (at least) every real number apart from 0, which is almost all of them. (To be precise, for each 𝜀 > 0, for some collection 𝒞 of open intervals (with rational endpoints if you like) whose total length converges to less than 𝜀, for each 𝑥, the function is defined at 𝑥 or 𝑥 belongs to at least one of the intervals in 𝒞. In this case, we can take just one interval, ]−⅓𝜀, ⅓𝜀[.)

Madeleine Birchfield (Aug 29 2024 at 20:36):

Toby Bartels said:

But there are lots of discontinuous functions that are defined almost everywhere, as I remarked upthread, and this is all that you need for measure theory.

Well those are partial functions and are automatically discontinuous by virtue of not being defined on the entire domain. Because you are already using subsets of the real numbers to define partial functions, in locale theory it would make sense to use some sublocale of the real numbers for defining corresponding partial functions which are discontinuous but defined almost everywhere.

Do measure theorists use "function" as a synonym for "partial function"?

Madeleine Birchfield (Aug 29 2024 at 20:42):

I might get rid of this sentence from [[measurable locale]]

"Simpson’s theory of sigma-locales, see below, is developed in classical framework, but could be a good starting point for a constructive theory, as it avoids the focus on complements. (But the main problem is completeness, not complements.)"

since I don't think the nLab should take an editorial stance on these issues, and this sentence seems to be one of the source of @James E Hanson's comments earlier in this thread.

Toby Bartels (Aug 29 2024 at 20:58):

Madeleine Birchfield said in part:

Do measure theorists use "function" as a synonym for "partial function"?

No, but they use ‘function’ to mean a function up to almost-everywhere equality. If you give them a partial function defined almost everywhere, then they'll immediately replace it with a function defined everywhere (if they're not constructivists) but refuse to tell you which one because it doesn't matter. If you're a constructivist and you tell them that you'd just as soon leave it undefined on a null set, then they'll shrug and not care even if they don't understand your reasons. If you're a constructivist measure theorist and leave your own function undefined on a null set, the other measure theorists probably won't even notice.

And a good thing too! Because it's up to the constructivists to make constructive math that works, not to close our eyes and say ‘Discontinuous functions don't exist, so I don't have to deal with them!’. Discontinuous functions do exists constructively, just not from ℝ to ℝ, and we need to be able to handle them. Since the ones of interest are defined almost everywhere, it's not a problem.

(Actually, if you give a measure theorist a partial function that's not defined almost everywhere and say that you want to integrate it, they'll handle that too, by defining it to be 0 outside its original domain. But that's a different matter, and it doesn't work for an arbitrary codomain.)

Toby Bartels (Aug 29 2024 at 21:04):

Madeleine Birchfield said:

I might get rid of this sentence from [[measurable locale]]

"Simpson’s theory of sigma-locales, see below, is developed in classical framework, but could be a good starting point for a constructive theory, as it avoids the focus on complements. (But the main problem is completeness, not complements.)"

since I don't think the nLab should take an editorial stance on these issues, and this sentence seems to be one of the source of James E Hanson's comments earlier in this thread.

The nLab takes lots of editorial stances, but this one's a bit muddled, because @Bas Spitters added the bit about how Simpson's σ-locales don't need complements, and I added the bit about how complements aren't really the source of the problem. I wouldn't mind getting rid of the whole thing, or perhaps replacing it with a note that σ-locales are a different approach that shouldn't be confused with measurable locales just because they both have ‘locale’ in the name. (And if I'm not mixed up, neither of these was intended as a constructive approach, even if constructivists who like them for other reasons might like to fix that.)

Federica Pasqualone (Aug 29 2024 at 23:04):

Thanks a lot guys for carrying on this wonderful discussion during the start of the semester! I really appreciate it! :folded_hands:

Federica Pasqualone (Aug 29 2024 at 23:06):

And @Mike Shulman is right about distribution theory and physicists' tricks :big_smile: in general ...
The fact is: when you are dealing with an open issue in mathematical physics, everything helps everything! Mathematical physics is the land of creativity and ingenious non-standard solutions ... :smirk:

Federica Pasqualone (Aug 29 2024 at 23:07):

Smearing included :heart_eyes: :innocent:

James E Hanson (Aug 30 2024 at 00:04):

Mike Shulman said:

James E Hanson said:

Physicists (and other appliers of mathematics) use and integrate discontinuous functions all the time.

Physicists also use and integrate things all the time that aren't even functions, like "$\delta$-functions". These can be defined mathematically as distributions, elements of the dual space of a space of smooth (and in particular continuous) functions. Discontinuous functions can also be considered (up to almost-everywhere equality) as particular distributions, even if the only actual "functions" are continuous. I don't know what the theory of distributions looks like constructively, but it would be one approach to make sense of the discontinuous functions used in applied mathematics, which would generalize the accepted way of making sense of the non-functions used in applied mathematics.

I used to be in a physics PhD program so I am intimately familiar with this. That said, one of the big issues with distributions is that one often wants to multiply them, but this doesn't really make sense mathematically. (Moreover the fact that it doesn't make sense really is a problem in applications like QFT.) Discontinuous functions and traditional measure theory do make sense mathematically though, so I don't really see the point in relegating discontinuous functions to a more exotic and poorly behaved class of mathematical objects than they need to be.

Mike Shulman (Aug 30 2024 at 00:15):

Yes, it's true that multiplying distributions is fraught in general. I think there are certain contexts in which you can do it, which might include discontinuous functions. But I think Toby's suggestion to regard discontinuous functions as just almost-everywhere-defined is even better.

James E Hanson (Aug 30 2024 at 00:22):

Graham Manuell said:

@James E Hanson I'm currently working on a paper with @Peter Faul on how to handle 'discontinuous' functions of the kind needed for things like shock waves. I don't think they would actually pose an issue for integration in this system either. I guess I don't really care whether you think it changes the content or not. In so far as it differs, why are you so certain that what the other approaches do is correct? I do care that it can model all physical phenomena, but I believe that with sufficient care it can. As @Mike Shulman notes, distributions should also be able to be accommodated.

I'm not saying that you cannot make an approach involving locales work, but I am saying that I don't see any reason for starting with locales when in probability theory the original topology of a given measure space is entirely irrelevant and in functional analysis the original topology is only loosely relevant. I would argue that really in that case it's the metric structure that is relevant (since you can't define, e.g., derivatives in purely topological terms) and so something like Nik Weaver's metric measure spaces (which can be given a point-free description easily, as I believe Weaver does in his book in terms of Lipschitz algebras) do a far better job of abstracting the relevant structure than a topology-focused approach like that of locales.

In fact, I would argue that locales are just a bad approach to numerical analysis in general since the category of locales doesn't compute product topologies of all metric spaces correctly.

James E Hanson (Aug 30 2024 at 00:24):

Mike Shulman said:

Yes, it's true that multiplying distributions is fraught in general. I think there are certain contexts in which you can do it, which might include discontinuous functions. But I think Toby's suggestion to regard discontinuous functions as just almost-everywhere-defined is even better.

I agree. It's a perfectly reasonable approach and lines up well with how things like step functions behave in computational contexts (e.g., there is a program that computes the Heaviside step function but it only converges on inputs that are apart from $0$).

Madeleine Birchfield (Aug 30 2024 at 01:01):

Honestly, the $\sigma$-locale approach to measure theory feels like that somebody asked "what is the most general structure we can define a countably additive measure on?" and the answer turns out to be a $\sigma$-frame, and then began developing measure theory on this level of generality.

John Baez (Aug 30 2024 at 01:21):

James E Hanson said:

Physicists (and other appliers of mathematics) use and integrate discontinuous functions all the time.

Indeed! They just have the good sense not to evaluate discontinuous functions at a point of discontinuity and expect the answer to be useful.

Mathematical physicists (a breed of mathematician, not physicist) formalize such ideas using functional analysis. We almost never use arbitrary real or complex-valued functions: instead, we work with them in a 'typed' manner. That is, we work with many different 'function spaces', like $L^p$ spaces and Sobolev spaces, and keep track of what we're allowed to do to elements of these various spaces. E.g. we can define

$\int_S f^2 \, d x$

if $f$ is in $L^2(\mathbb{R})$ and $S \subseteq \mathbb{R}$ is measurable. We can differentiate any element of $L^2(\mathbb{R})$, but we get an element of the Sobolev space $H^{-1}(\mathbb{R})$, which is a particular sort of distribution.

For most of these function spaces, the elements are not really functions in the traditional sense: they could be distributions, or they could be equivalence classes of functions. And in the latter case, it's often (though by no means always) true that changing the value of a function at just one point does not change its equivalence class. Then evaluation at a point is undefined. And this is fine, because we are using these functions for other things: we have no intention of evaluating them at a point!

fosco (Aug 30 2024 at 07:40):

I was thinking about something yesterday: if you try to do ergodic theory constructively, you are mixing together something that is very natural to see with category-theorist's eyes (dynamical systems) and something not-so-easy (measure theory).

I'd be curious to see what can be done and what comes out of it, e.g. what the def'n of ergodicity becomes.

JR (Aug 30 2024 at 08:56):

Mike Shulman said:

Yes, it's true that multiplying distributions is fraught in general. I think there are certain contexts in which you can do it, which might include discontinuous functions. But I think Toby's suggestion to regard discontinuous functions as just almost-everywhere-defined is even better.

Here is the standard approach: https://ncatlab.org/nlab/show/Colombeau+algebra

Graham Manuell (Aug 30 2024 at 09:08):

Toby Bartels said:

It's just that if the interval is located, then it has a (possibly infinite) Dedekind real as both lower and upper endpoint (which depending on what one means by ‘interval’ one might assume anyway); and any point (Dedekind real) apart from the endpoints is either in the set or in its exterior (both open sets, so you can tell which). If ‘almost every’ means anything constructively in a pointwise context, then that includes everything distinct from a given two points.

Ah, thank you. I had forgotten what exactly what located meant here. I will think about this further.

I don't even know if there is a smallest sublocale of full measure, but it seems reasonable.

Simpson proves this in his paper (at least when the measure of the space is finite).

Graham Manuell (Aug 30 2024 at 09:25):

James E Hanson said:

I'm not saying that you cannot make an approach involving locales work, but I am saying that I don't see any reason for starting with locales when in probability theory the original topology of a given measure space is entirely irrelevant and in functional analysis the original topology is only loosely relevant.

This seems to be the crux of our disagreement, because I think the topology is absolutely crucial and so I am never going to be happy with an approach where it is ignored. I gave a number of reasons why I think this above, but I suppose you did not find them convincing. If you do not buy that the topology is important, I can see why you wouldn't like this approach, but for me this is the entire point.

In fact, I would argue that locales are just a bad approach to numerical analysis in general since the category of locales doesn't compute product topologies of all metric spaces correctly.

This is completely backwards in my opinion. You are saying that just because the localic product disagrees with the topological product it is 'incorrect', but I would say it is the topological product that is incorrect! You really need to give an argument why you think the topological product is the correct one. The localic one is the one with all the good properties in terms of compactness, etc. (Also, if you equip a discrete locale with a metric, then finite products will agree with the spatial ones. You seem to not care about the topology, so this is probably what you want.)

Bas Spitters (Aug 30 2024 at 11:12):

Thanks @Toby Bartels for tagging me. I haven't read up on the whole discussion yet, but some quick comments:
There's a recent preprint on sigma-locales for measure theory: https://arxiv.org/pdf/2408.13911
It's also possible to develop measure theory synthetically: https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/synthetic-topology-in-homotopy-type-theory-for-probabilistic-programming/1EC63B25D83E58C51DAB8D3A0AF567EB
This can be done in a number of toposes. Condensed sets is one of them.

@fosco I'm in the middle of something else now, but Bishop and Nuber have already worked on Ergodic theory.
https://www.jstor.org/stable/24901875
https://www.ams.org/journals/tran/1972-164-00/S0002-9947-1972-0291411-3/S0002-9947-1972-0291411-3.pdf
Here's my contribution to the topic:
https://projecteuclid.org/journalArticle/Download?urlid=10.2178%2Fjsl%2F1146620162

John Baez (Aug 30 2024 at 14:13):

JR mentioned [[Colombeau algebra]] as a way to multiply distributions, but I haven't seen anyone use this to prove interesting results in analysis, and the nLab article explains some reasons why. Wikipedia claims that Colombeau algebras "have found numerous applications in the fields of partial differential equations, geophysics, microlocal analysis and general relativity so far", but it doesn't link to any examples, and I think this claim is misleading. Probably some people have tried applying it to all these subjects - but it hasn't caught on, because it doesn't help much.

John Baez (Aug 30 2024 at 14:25):

Schwarz's result put limits on how well we can multiply distributions in general, so most analysts try to restrict to multiplying distributions whose singularities don't get in each other's way. See section 2 of A smooth introduction to the wavefront set for a pedagogical introduction to multiplying distributions, leading up to Theorem 13, a criterion for when you can multiply distributions based on the all-important notion of [[wavefront set]]. This is more like the math I usually see when people apply multiplication of distributions to problems in nonlinear PDE, quantum field theory, etc.

Tobias Fritz (Aug 30 2024 at 16:29):

John Baez said:

JR mentioned [[Colombeau algebra]] as a way to multiply distributions, but I haven't seen anyone use this to prove interesting results in analysis, and the nLab article explains some reasons why. Wikipedia claims that Colombeau algebras "have found numerous applications in the fields of partial differential equations, geophysics, microlocal analysis and general relativity so far", but it doesn't link to any examples, and I think this claim is misleading. Probably some people have tried applying it to all these subjects - but it hasn't caught on, because it doesn't help much.

There's a nice book Geometric Theory of Generalized Functions with Applications to General Relativity by a group of mathematical physicists in Vienna. These people have been applying Colombeau algebras to general relativity over the past 25 years or so, and it certainly looks like they're claiming success by saying that these structures are better suited for their purposes than mere distributions:
image.png

Tobias Fritz (Aug 30 2024 at 16:30):

As far as I understand, the overarching theme here is general relativity on spacetimes with low regularity. That may sound boring and irrelevant when you first see it, but of course many actual physical models involve functions that are not smooth, such as the mass density in an idealized spacetime modelling a star.

Another person who's done a lot of work in this direction is James Vickers -- not to be confused with Steve Vickers, who's worked on constructive measure theory!

John Baez (Aug 30 2024 at 16:38):

Okay, I'd really like to see if they do something practical with Colombeau theory and whether it goes beyond the usual rules for multiplication of distributions (namely, you can multiply them if the wavefront sets of the two distributions intersects transversely, or something like that - I'm no expert).

John Baez (Aug 30 2024 at 16:38):

So now I have another new hobby.

John Baez (Aug 30 2024 at 16:48):

I'm more interested in seeing what they prove about solutions of Einstein's equations than reading about the general theory - I once studied Colombeau algebras hoping they'd help me with quantum field theory, and I eventually decided I couldn't do anything with it. One of the authors of that book is named Michael Oberguggenberger and he wrote a paper called Solutions to semilinear wave equations of very low regularity. The abstract makes him sound like an ordinary analyst, not a Colombeau cultist, so that's good.

Tobias Fritz (Aug 30 2024 at 16:56):

Right, that sounds pretty accurate given my personal impression, thanks to Michael's office just being one floor down from mine :upside_down: He's the only one among those authors not based directly in Vienna. (In practice, we haven't gotten around to talking often -- partly due to an idiosyncratic system of there being three or four different math departments in one and the same building and university, and him being at another one.)

Tobias Fritz (Aug 30 2024 at 16:56):

But that's how I've known about this stuff.

John Baez (Aug 30 2024 at 17:42):

Please sometime ask him about the usefulness of Colombeau theory!

James E Hanson (Aug 31 2024 at 17:06):

Graham Manuell said:

but for me this is the entire point.

The entire point of what? If your approach to measure theory doesn't have that $L^1[0,1]$ and $L^1(2^{\mathbb{N}})$ are the same Banach algebra at the end of the day, then you're not doing the mathematics that most people mean when they say 'measure theory.' Obviously there are times when a case can be made that certain fundamental definitions and results in a field are 'wrong' in the sense that they are going down the wrong path, but for a big successful field like functional analysis you need really solid arguments supporting such a claim and your arguments absolutely have not established this. For example, one of your arguments was about 'functions that can be carried out in practice,' but (a) as discussed elsewhere in this thread it is actually possible to assign computational meaning to things like step functions as partial functions and (b) almost all of the familiar $L^p$ spaces have computational presentations as Banach algebras, which means that one can in fact work with the traditional objects in measure theory, probability theory, and functional analysis 'in practice.'

This is completely backwards in my opinion. You are saying that just because the localic product disagrees with the topological product it is 'incorrect', but I would say it is the topological product that is incorrect! You really need to give an argument why you think the topological product is the correct one. The localic one is the one with all the good properties in terms of compactness, etc.

A lot of topology is supposed to be an abstraction of the behavior of metric spaces. Addition is a continuous operation on the rationals with the ordinary metric, but it isn't continuous localically. Likewise, when I look at the direct sum $X \oplus Y$ of Banach spaces, the topology on it should be both the topology induced by the norm and the product topology of $X$ and $Y$, but localically it's usually not. Locales only do a good job of capturing ordinary intuition about topology in the context of locally compact spaces. This is wrong. The localic product of any two complete metric spaces is spatial (classically).

Graham Manuell (Aug 31 2024 at 21:05):

I am a topologist. I do not care about measure theory per se. I care about being able to deal with probability and integration. Anyway, it is probably not possible go into enough detail in this medium and you seem to have a distaste for any mathematics that is not 100% within the dominant paradigm.

For what it's worth, you can get $L^p$ spaces no problem by completing 'locales of continuous functions'. Probably those two spaces are still isomorphic. This feels like a separate point to what we were discussing before. I am also happy with step functions as partial functions. I already told you that I am writing a paper on this. General measurable functions seem like a different story though since they can be discontinuous everywhere.

You are using the wrong topology on the rationals. The rationals naturally have the discrete topology. I don't know enough about Banach spaces to comment on that example, but for any separable Banach space the localic and spatial products will agree (classically).

You are defining "ordinary intuition about topology" to mean "everything works exactly like topological spaces", without interrogating why things ought to work that way. (And even then Polish spaces would also behave like you expect.) Good luck doing point-set topology constructively; I do not envy you.

James E Hanson (Aug 31 2024 at 21:47):

Graham Manuell said:

I don't know enough about Banach spaces to comment on that example, but for any separable Banach space the localic and spatial products will agree (classically).

I realized that I was misinterpreting a result that I had read. I believe that the results of this paper imply that every localic product of Banach spaces is spatial, regardless of size.

James E Hanson (Aug 31 2024 at 22:12):

Graham Manuell said:

General measurable functions seem like a different story though since they can be discontinuous everywhere.

The whole point of the normal approach to measure theory is that we get actual point-set function representations of all of the elements of the completion of a given probability algebra. (This isn't even that hard to do constructively.) This is sometimes a useful thing to have. An analogously useful feature of a localic approach to measure theory would be that every element of a space like $L^p(X)$ can be represented by some function-like object on the original locale, but this requires the ability to treat functions that can be discontinuous everywhere.

My point is that if your approach to measure theory isn't going to offer a feature like this, then there's not really a strong reason to start the theory with locales rather than starting with the already established point-free presentation of measure theory in terms of probability algebras (i.e., metric Boolean algebras).

James E Hanson (Aug 31 2024 at 22:18):

Graham Manuell said:

You are defining "ordinary intuition about topology" to mean "everything works exactly like topological spaces", without interrogating why things ought to work that way.

You are putting words in my mouth. I was only talking about ordinary metric spaces (complete or incomplete), not arbitrary topological spaces. I admit that I had the wrong impression about how well locales handle topology on metric spaces and that complete metric spaces are a lot more important than arbitrary metric spaces, but I still think that $\mathbb{Q}$ with the ordinary metric $|x-y|$ is not that ridiculous of an example.

James E Hanson (Aug 31 2024 at 22:27):

Graham Manuell said:

Good luck doing point-set topology constructively; I do not envy you.

I was never intending to do point-set topology constructively. Honestly, the fact that point-set topology and other parts of math that I use regularly (like ordinals) behave so poorly in constructive math just makes me want to stop thinking about constructive math, if anything.

Morgan Rogers (he/him) (Sep 02 2024 at 08:13):

James E Hanson said:

Honestly, the fact that point-set topology and other parts of math that I use regularly (like ordinals) behave so poorly in constructive math just makes me want to stop thinking about constructive math, if anything.

That's okay, not everyone has to do constructive math. I'm very happy that Graham is doing it, though.

Federica Pasqualone (Sep 03 2024 at 20:10):

Good evening everyone!
Where were we? :thinking: Ah locales .... :heart_eyes:
Well, I was investigating some properties of open sets in writing my Master's thesis, left alone in the library with a lot of dangerous books ... and I found out we can actually play around ... ehm make some rigorous logic out of them!
The frame of open sets ... but what is a frame? Is the dual notion to the one of local! :upside_down:

Federica Pasqualone (Sep 03 2024 at 20:15):

And still I haven't answered the question, I know.
The category of frames Frm should have some objects and morphisms to start with hahha
And indeed they are complete lattices A satisfying some good property, i.e.
$a \land \bigvee S = \bigvee \left\{a \land s : s \in S \right\} \ \ \ \forall a \in A$, where $S \subseteq A$
and arrows preserve joins, finite meets, top and bottom.

Federica Pasqualone (Sep 03 2024 at 20:22):

Your set-theoretical gut feelings :smile: are right: $\cup$ and $\cap$ are just join $\lor$ and meet $\land$.

Federica Pasqualone (Sep 03 2024 at 20:32):

There are also a couple of words here needing an explanation, namely complete and lattice - that is why I wrote down lattice theory some comments ago!
For sure we need some notion of order if we wanna say this thing is greater than this other, or bigger than the other and then we can define the meet and join of two elements, respectively - that yes, are dual of each other.
More precisely, let $\left(X, \le \right)$ be an ordered set, than given two elements $x,y \in X$, their meet $x \land y$ is such that $\forall z \in X \ \ \ \ z \le x \land y \iff z \le x$ and $z \le y$.
The join is left as an exercise!
When we equip an ordered set with these two binary operations, meet and join, it becomes a lattice.
Completeness? Well, as you are imagining is about having a sup and an inf for all subsets of such a lattice! And look, we have nice symbols for them: $\top, \bot$. :innocent:
It is also true that this is just one point of view, and I was curious enough to discover the categorical side of the story. What if the idempotent, commutative, monoidal structures given on $X$ by the join and the meet with their "neutral elements" top and bottom are transforming $X$ into a lattice? :smirk:

Federica Pasqualone (Sep 03 2024 at 20:48):

And what about this Heyting?

Madeleine Birchfield (Sep 03 2024 at 21:35):

I guess what you're looking for is that every frame is a complete Heyting algebra.

Madeleine Birchfield (Sep 03 2024 at 21:36):

But frame homomorphisms, unlike homomorphisms of complete Heyting algebras, do not have to preserve the Heyting implication.

Federica Pasqualone (Sep 03 2024 at 21:36):

Here we go ...

Federica Pasqualone (Sep 03 2024 at 21:37):

But @Madeleine Birchfield, what is an Heyting algebra? :mic: Let us define it once and for all!

Madeleine Birchfield (Sep 03 2024 at 21:38):

A Heyting algebra is a Cartesian closed lattice.

Madeleine Birchfield (Sep 03 2024 at 21:39):

For those who are not familiar with category theory, there is an order theoretic or lattice theoretic definition of a Heyting algebra but I can't seem to remember it at the moment.

Federica Pasqualone (Sep 03 2024 at 21:39):

hahah the perfect definition for the working mathematicians ... in CT!

Federica Pasqualone (Sep 03 2024 at 21:40):

Well part of the job must also be done by the audience, that will carefully look it up! :wink:

Federica Pasqualone (Sep 03 2024 at 21:43):

or wait for tomorrow ...

Madeleine Birchfield (Sep 03 2024 at 21:54):

The nLab says that a [[Heyting algebra]] is a lattice $A$ with an implication $x, y \mapsto x \Rightarrow y$ such that for all $x$, $y$, and $z$ in $A$, $x \vee y \leq z$ if and only if $x \leq y \Rightarrow z$.

Federica Pasqualone (Sep 03 2024 at 21:59):

When the meet $\land$ has a right adjoint, namely the Heyting implication, the lattice is said to be Heyting. If it also antisymmetric, it is an Heyting algebra.

Madeleine Birchfield (Sep 03 2024 at 22:00):

Here's a question I have. Why do we need two different notions, the concepts of "frame" and "locale"?

Federica Pasqualone (Sep 03 2024 at 22:03):

Ah this has to do with sober spaces :heart_eyes:

Federica Pasqualone (Sep 03 2024 at 22:05):

There is a functor $\Omega:$Top$\rightarrow$Frm that takes open sets into the frame of open sets and we want it to be a full embedding when restricted to sober spaces.

Madeleine Birchfield (Sep 03 2024 at 22:06):

More generally, locales are a generalisation of topological spaces. A locale is defined as a set $X$ with an arbitrary frame $\mathrm{O}(X)$, while a topological space is defined as a set $X$ with a frame $\mathrm{O}(X)$ of subsets of $X$.

Madeleine Birchfield (Sep 03 2024 at 22:07):

Frames are algebraic structures which describe how the opens behave, while locales are spaces.

Federica Pasqualone (Sep 03 2024 at 22:08):

The usual duality between algebra and geometry! :sunglasses:

Federica Pasqualone (Sep 03 2024 at 22:09):

But that $\Omega$ is contravariant, and we like to have it covariant for the full embedding. In fact, locales extend sober spaces.

Madeleine Birchfield (Sep 03 2024 at 22:14):

Now, a continuous function between locales $(X, O(X))$ and $(Y, O(Y))$ is defined as a function $f:X \to Y$ with a frame homomorphism $f^{-1}:O(Y) \to O(X)$. Why are continuous functions defined as such?