Conversation started Feb 3, 2018 at 4:56.
Feb 3, 2018 04:56
I don't recall we have gone this deep before about the $\omega_1$ discussion:
in Mathematics, 14 hours ago, by Alessandro Codenotti
@Secret if you want to construct the Borel sets iteratively you can't stop at any countable ordinal but need $\omega_1$ iterations. Dunno if this counts aa natural
So case in point:
> Is the full Borel algebra $G^{\omega_1}$ necessary for all useful mathematics?
Previously, we already have examples where the use of the full Lebesgue measure is not necessary for all real world mathematics, as detailed in:
48
Q: Physical meaning of the Lebesgue measure

user21820Question (informal) Is there an empirically verifiable scientific experiment that can empirically confirm that the Lebesgue measure has physical meaning beyond what can be obtained using just the Jordan measure? Specifically, is there a Jordan non-measurable but Lebesgue-measurable subset of ...

8
Q: Is the notion of Lebesgue Measure a necessary construct for statistical physics?

David ReedIn chat last night a user and I were discussing the "physical" meaningfulness of the notion of lebesgue measure. In particular, we were curious as to whether physicists can "make do" without it. I mentioned that the dominated convergence theorem is needed to prove certain theorems in statistics t...

However, it seems probability measures are a different story...
101
Q: Why do probabilists take random variables to be Borel (and not Lebesgue) measurable?

MarkI've been studying a bit of probability theory lately and noticed that there seems to be a universal agreement that random variables should be defined as Borel measurable functions on the probability space rather than Lebesgue measurable functions. This is so in every textbook on probability theo...

> The moral is this: To get as many (BX,BY)-measurable functions f:X→Y as possible, one wants BX to be as large as possible, so it makes sense to use a complete σ-algebra there. (You already know some of the nice properties of this, e.g. an a.e. limit of measurable functions is measurable.)
> But one wants BY to be as small as possible. When Y is a topological space, we usually want to be able to compose f with continuous functions g:Y→Y, so BY had better contain the open sets (and hence the Borel σ-algebra), but we should stop there.
So one of the subquestions a predicative foundation need to address is the following:
> How much probability theory can we retain when we use a subset of the Borel algebra and how should we define our functions such that it can approximate completeness in a general sense?
It should be noted that the affirmative or the negative to the answer of the necessarity of the full Borel algebra in all useful mathematics is an interesting one regardless:
For if the answer is negative, as we are suspecting, it means the foundation of mathematics can be reduced to a predicative one, thus banishing all cantorian infinities and provide more support for a finitist view of mathematics
Meanwhile, if the answer is affirmative, it will mean the opposite, that real world mathematics cannot be formulated solely in a predicative fashion, as the existence of the Borel algebra is essential and hence we will need to allow at least one self referential sentence in our foundation:
> Definition of $\omega_1$: $\omega_1$ is an ordinal such that a Borel algebra $G^{\omega_1}$ is constructed by iterating countable unions and countable intersections of sets $\omega_1$ many times.
as we don't have any real world direct counterpart of $\omega_1$
2
A: The purpose of the $\sf ZFC$ Axiom of Infinity

Andrés E. CaicedoSet theory is a theory of infinite sets, one could say that this is the point (that it serves us as a foundation for mathematics is extra, the cherry on top). What is remarkable about the axiom of infinity is not that it provides us with a formal surrogate for the natural numbers (I mean, we bett...

Both $ACA_0$ and some parts of the type theory that we are currently building is basically (ZFC-I-unrestricted replacement) if I recall correctly... need to figure out how to recover probability theory from this
1. Borel measures are compatible with the underlying topology in an appropriate sense, which is important in certain situations. 2. In probability theory we frequently find ourselves wanting to compose random variables. When you do this, because the definition of Lebesgue measurability of a function is not symmetric with respect to the $\sigma$-algebras involved, the function composed "on the left" must be Borel measurable to ensure the composition is Lebesgue measurable. 3. I can say more if you're a bit more concrete about where this is used. — Ian Sep 28 '17 at 22:07
Feb 3, 2018 05:59
10
Q: Why bring in Borel sets and $\sigma$-algebra in probability theory?

AdityaGhoshIn Probability theory, we can simply use power set of the underlying sample space as the event space. Why go into higher concepts of Borel sets, $\sigma$-algebra and measure? Is it just an instance of generalization or does it address some flaw in the use of power sets? Thank you in advance :)

but meanwhile, there seemed to be some hints that whatever sample spaces that requires the full borel algebra, seemed to be of uncountable cardinality is nature, which both ACA and our foundations have taken cared of by throwing away the notion of cardinality as "size" as injections are not in general provable in such systems
3
Q: What is the advantage of Borel sigma algebras in defining probability spaces?

Antoni ParelladaI'm trying to get the central concepts correct, so I'm going to express them without embellishment. A Borel $\sigma$ algebra is defined as a sigma algebra generated by a topological space $(M,\mathcal{T})$. If $M$ is $\mathbb{R}$, it will typically be the "standard topology" defined as ...

hmmm... it seems we might lost conditional probabilities if we don't have borel algebras...
...
uh, I apologies for this seemly link dump... I guess I need to make the analysis more coherent first...
I will stop here for now even though MSE has more stuff to add to the discussion...
I just want to summarise: At my current level of understanding, it seems probability theory need Borel measures to be ok, and Borel measure need borel algebra, which in turn needs $\omega_1$ (the only place we knew so far outside of foundations that need $\omega_1$ based on the past months of discussion in all maths chat rooms)
so to justify banishing $\omega_1$ will need to ensure we can do probability theory without the full borel algebra and borel measure
---
A type theoretic approach to probability theory: https://arxiv.org/pdf/1511.09230.pdf
Feb 3, 2018 06:25
@amWhy It's okay. I've been very busy myself anyway. =)
@LeakyNun I don't have a problem if and only if the one who is giving me this proof knows very well how to prove the general theorem. =)
By the way I won't prove any of these first until I have already constructed the exponential function and proven its properties, because then it is trivial to define cos(x) = (exp(ix)+exp(−ix))/2 and sin(x) = (exp(ix)−exp(−ix))/2i and get all the identities by purely algebraic manipulation.
Note that the typical geometric proof is arguably pedagogically defective because it relies on geometric notions which are quite impossible to make rigorous without analytic euclidean geometry. In any case, if one really wants to invoke geometry, the easiest way is to use rotation matrices.
But rotation matrices are only going to work for real cos/sin.
Whereas the way I prefer will work for the full complex cos/sin.
In the case of sin(2x), we will see that it boils down to the algebraic identity x^2−y^2 = (x+y)(x−y).
@Secret Alessandro's comment "Dunno if this counts as natural" is precisely the point. Do we need Borel sets in real life? I can bet not.
Feb 3, 2018 06:46
@user21820 been a while since Ive seen the formal proof but if I recall correctly pretty much all the major identities can be proven from $sin^2(x) + cos^2(x) = 1$
@TheGreatDuck No. Try first and get back to me if you find a proof that does not involve any geometry.
@user21820 that's not a geometric proof as it was in high school that I learned that without any reference to geometry or even an yet an explanation as to why they were useful. It was very strange. The book actually defined them by algebraic rules and then later showed what the actual values of it were.
they hadnt even said yet that cos and sin were the relationship between lengths of sides of right triangles
@TheGreatDuck As I said, try first. I'm 100% sure you won't find a proof of sin(2x) = 2·sin(x)·cos(x) or the generalization that does not use geometry or analysis.
@Secret ACA and ACA0 have nothing to do with the kind of fragment of ZFC you're talking about.
In particular, it is more like Z minus powerset minus impredicative specification.
@user21820 fair enough. no need to get angry. I was just letting you know that I recalled cosine and sine not requiring many rules to be assumed in their definition in order to prove the other rules. Note: proving the rule I stated likely does require analysis.
@TheGreatDuck I said what I said because you were responding to our discussion in a manner that would imply to other readers that you can get the addition identities algebraically from the identity sin(x)^2+cos(x)^2 = 1. I'm sure this is false.
However, if you have that identity as well as all the addition identities, I would not be surprised if you can get all algebraic identities between sin,cos.
Feb 3, 2018 06:56
hmmm
strange because I remember very clearly the addition identities being derived
That's why I said I want you to try first. I wasn't angry, but you must try first before claiming something I'm sure is false.
If you find a proof not involving geometry or analysis, you would prove my certainty misguided!
no i mean I remember very clearly it being done somehow. Ill have to see if I have the book somewhere later. If not Ill probably ask a question about it.
Okay sure.
half angle formula
thats what i was forgetting
that is probably what they used.
@TheGreatDuck By intuition, just having double-angle and half-angle identities are not enough to entail the addition identities.
Feb 3, 2018 07:24
@Secret I'm not sure how relevant this is, because it seems to be not about probability theory as we are interested in.
@Secret Conditional probability is well-defined as long as the events are well-defined. That post refers to "conditional measure", which I do not know about, but is certainly not conditional probability.
I am not sure either because I have not read in detail, just that I found an example where bayesian probability can be formulated in type theory while all previous searches are all in terms of set theory, hence why I separated that message with --- cause I am not sure if it has anything to do with the $\omega_1$ discussion yet
@Secret Ah okay. You don't have to limit your search to type theories per se. As long as you can tag each object you construct with a type, and only use operations on inputs of the intended types, it would likely be translatable to a type theory. For example, in ZFC you can consider the types as simply the sets corresponding to the closure of N under cartesian product and function types.
Notice how having the replacement schema breaks this. Choice does not, which is why some type theories have no issue with choice. Specification does not either, even if impredicative. If however you want a predicative type theory, then you need to further restrict to predicative specification, and you will need to decide whether powerset is acceptable or not.
I think powerset is predicatively unacceptable over classical logic, but can be predicatively acceptable over 3-valued logic.
My current tentative position is I am ok with ditching power sets, but my position on $\omega_1$ is still a mess because I am torn between obssessed with keeping it and obssessed with finding the best foundation which based on our current discussion, will mean we need to ditch $\omega_1$ and higher ordinals

(cont.)
I wish I can read things a lot faster... It also does not help that given that we all have work commitments and that given my current level of background, it will take a reading and comprehension speed akin to a finite time blowup in order to be able to read and understand everything I need to address both the predicative foundation construction and the $\omega_1$ discussion within say... 3 months
Feb 3, 2018 07:40
@Secret But if you don't even have powersets, you definitely don't have ω[1].
if we don't have ω[1], then we need to figure out a nice way to work with probability theory without invoking borel measures, but I might be wrong cause I have not read in detail yet on how essential are borel measures to have a working probability space, other than a lot of nice things will fall apart such as there will be events that cannot e assigned a probability
> I need more time... there is simply not enough time to handle both mathematics foundations and my PhD, even with all those massive speedups used by the scripts
@Secret If we have powersets, even the predicative versions, we should have no trouble with everyday probability theory.
I am sure because throughout my whole undergraduate mathematics course, not once did I need to invoke ω[1] for anything concrete.
And I had no trouble with information theory, which uses lots of conditional probabilities.
Feb 3, 2018 08:00
I am told that some stochastic processes are hard to handle without more machinery, but I think real-world stochastic processes won't need much, and can be handled via finite approximations.
Approximations as in like what we do when coarse graining the sample spaces and defining time steps in molecular dynamics simulations?
Yes. And many times a stochastic process is defined more or less as a limit of the finite approximations.
hmm... I guess at the level of this discussion (higher level will need a lot more time on my part to get my background ready), it is likely that we can do away borel algebra completely for probability theory. Combining this with Terry Tao's and knzhou's comment about complete hilbert spaces and how physicists usually use an equivalence class of Lebesgue measure instead of the full measure, means that we can also get away with measure theory without involving Lebesgue measures.

Since I have yet to find another concrete area where borel algebra is used, so the argument seemed to be further i
 
Conversation ended Feb 3, 2018 at 8:10.