I can't speak to non-pointed set-theoretic probability theory. I know about ETCS (elementary theory of the category of sets) so I understand that sets don't require points. But as to probability, I can't say. However if you take finite line segments as sets, you seem to lose intersections. Are these closed or open segments? You have a reference for this interpretation of probability theory?
— fishfry
Let's look at Kolmogorov axioms here: (http://mathworld.wolfram.com/KolmogorovsAxioms.html)
Everything that is needed is a set W
W
, some Qi
Q
i
, that can be "anything", a function Qi
Q
i
from the Qi
Q
i
to real numbers, and a function "complement" on the Qi
Q
i
.
Let's consider as our probability space the segment [0, 1].
I can take for Qi
Q
i
the closed sets included in [0, 1] made of countable number of non overlapping segments with non zero length, and for W
W
the set of all these sets. The complement of a Qi
Q
i
will be the closure of the remaining part of [a, b] when I remove the Qi
Q
i
. There are no Qi
Q
i
of zero measure (and this is very reasonable for a probability theory: every event that can happen must have a non zero probability to happen).
The complement of a Qi
Q
i
overlaps with Qi
Q
i
only on the end points, and that is compatible with the axioms: the sum of measures adds up to 1.
The elements of W
W
are simply ordered pairs of real numbers instead of single real numbers, but everything works at the same way: from the point of view of set theory two segments are equal if and only if the extremes are equal: no mention of overlapping segments at all.
The definition of overlapping segments is the usual one: the higher number of the first pair is bigger than the lower number than the second pair.
There is no need to consider infinite sets of points, and for probability theory there is no need to speak about points at all: probability theory does not need zero-measure events, and no physical possible event has zero probability.
P.S. This is only a very simple example to show that it's not contradictory to define probability without points. Pointless topology is much more general than this and makes use of the concept of "locales" (https://en.wikipedia.org/wiki/Pointless_topology) — Mephist
↪fishfry Can’t a real number go on and on for infinity? Or is that an irrational number...? — Noah Te Stroete
I guess I got confused because you guys were talking about numbers as points, where I was thinking about zero-dimension points on a two-dimensional line. This stuff to me right now is very esoteric, as I don’t remember the terminology for the different kinds of numbers. I was always better at calculations like an engineer than I was so much interested in or ever had any exposure to theory. — Noah Te Stroete
But our use of real numbers (at least for the most part) is in integrals and derivatives, right?
So the "dx" infinitesimals in integrals and derivatives should be the morally correct model? This is how real numbers are intuitively used since the XVII century. — Mephist
First of all, does our imprecise use of real numbers warrant a precise account?
What does it even mean to say that a real number denotes a precise quantity? — sime
For in what sense can a formal system speak of universal quantification over all of the natural numbers? — sime
So in short, an imprecise and pragmatic model of the real numbers is what is important, corresponding to how numerical programmers implement them in practice, with particular attention paid to numerical underflow. — sime
For in what sense can a formal system speak of universal quantification over all of the natural numbers?
— sime
The standard way is assuming the principle of induction: if a proposition is true for n=0 and from the fact that is true for n you can prove that is true even for n+1, then you assume that is true for all natural numbers. (https://www.encyclopediaofmath.org/index.php/Induction_axiom)
It cannot be verified in a finite number of steps, so it's assumed as an axiom.
But assuming it to be false is not contradictory: you can assume the existence of numbers (inaccessible cardinals) that can never be reached by adding +1 an indefinite number of times (https://en.wikipedia.org/wiki/Inaccessible_cardinal). — Mephist
Therefore it is coherent to accept mathematical induction as a principle of construction, and yet reject it's interpretation as a soothsayer of theoremhood. — sime
Do we really want to insist that our use of these axioms is equivalent to a literal step-by-step substitution of every permissible number into P?
Do we even want to say that we are assuming the existence of this inexhaustible substitution? — sime
All that i and ii define in a literal sense is a rule that permits the substitution of any number for x.
Nowhere does this definition imply that induction is a test for the truth of every substitution.
Therefore it is coherent to accept mathematical induction as a principle of construction, and yet reject it's interpretation as a soothsayer of theoremhood. — sime
On the other hand, for universally quantified formulas over infinite domains that do not possess a proof by mathematical induction, there is no reason to support their informal interpretation as enumerating the truth or construction of the predicates they quantify over, by the very fact that they do not correspond to a rule of substitution. — sime
I do not believe that an oracle in computer science is in any way analogous to the axiom of choice. If you know of a connection perhaps you could explain it. An oracle allows you to compute something that was formerly noncomputable. The axiom of choice doesn't let you compute anything. In fact the elements of the sets given by the axiom of choice have no properties at all and could never be computed by any stretch of the word. — fishfry
In this sense the axiom is an oracle: it allows you to compute f — Mephist
I've re-read the SEP article on constructive math with a much deeper level of comprehension than I've had in the past. Your efforts have not been in vain. — fishfry
Also ... no form of the AC could possibly be construed as a computation. That, I just do not see at all. It's a pure statement of existence. A particular set exists with no means to possibly compute or construct or identify any of its elements. — fishfry
I don't remember which one is the SEP article. Could you send me a link? — Mephist
Yes, the AC can't be construed as a computation, and it's not part of constructivist logic. What I am saying is that AC can be added to a constructivist logic framework such as Coq if you want to use standard logic: standard logic can be obtained as an extension of constructivist logic (in a similar way as metric geometry can be seen as an extension of projective geometry): if you want to use classical logic in Coq (and that's how it's used most of the time) you just have to import the Classical_Prop library: — Mephist
I will say one thing though. I still just don't get constructivism as a philosophy. I DO understand that certain formulations of constructive math lend themselves beautifully to computerized proof systems. Nobody would deny the digital deluge that's flooding the world right now, why should math be spared?
But I don't get the metaphysics. "A thing only exists when we have an algorithm to instantiate it." But the world is full of things that have no algorithm. The world itself is not an algorithm. — fishfry
I completely agree. — Mephist
But proofs of existence are algorithms, in any formal logic. — Mephist
But if you code up the axioms of formal ZFC into a computer, the proof of the existence of the Vitali set can be cranked out by a program. Even by an undergrad! So in that sense, proofs are constructions even if they are constructing things that are in no way constructive.
Have I got that right? — fishfry
Secondly, you said you can import a library into Coq to recover standard math. But if that were true, standard math would be computerizable, and then that would remove the biggest benefit of constructivism. — fishfry
But I don't get the metaphysics. "A thing only exists when we have an algorithm to instantiate it." — fishfry
But if you don't assume the idea that everything is made of parts, you don't have to assume the unintuitive :wink: idea that a line is made of points: you can think of lines and points as two different types, and an intersection of two lines as a function from pairs of lines to points. — Mephist
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.