My knowledge of QM is very limited, but I think that the wave function collapses to a 'particle' when measured - at least for particles like the photon. A very small, collapsed, wave could be mistaken for a point particle? It would seem neat and tidy if all particle types had similar behaviour in this regard (string theory comes to mind). But probably we have to stick with uncollapsed waves from what you are saying. They could still be centred on a discrete grid point though. — Devans99

If I had a reasonable explanation of what the collapse of the wave function means I would immediately publish it and I would become the most famous physicist of the world :grin:

In my opinion the most likely interpretation of quantum mechanics should be a somehow refined version of the many-world interpretation ( https://en.wikipedia.org/wiki/Many-worlds_interpretation ). But, as it is now, even this interpretation doesn't make sense. A collapsed wave is not smaller than an uncollapsed one: a collapsed wave is part of classical mechanics, and all experiments are part of classical mechanics. Quantum mechanics simply does not describe experiments. It describes the evolution of any physical system as the evolution of an abstract mathematical object (a vector in an infinite-dimensional vector space, called the state-vector) that does not correspond to any real physical object. And you can use that object to predict the probability of an experiment by the "trick" of making the state-vector (or wave-function) collapse, but the experiment itself must be described using classical mechanics, not quantum mechanics. So, practically, inside quantum mechanics there are not "collapsed wave functions". The collapsed wave function is the mathematical "trick" used to make in some way a state-vector (or wave -function) become "visible" from classical-physics observer.

I think that our theories use continuous variables as an excellent approximation for a reality that is discrete on such a fine level that it appears continuous to us (and thus continuous theories give results very close to reality). So continuous calculus gives good results but does not reflect the micro nature of reality correctly. This seems to be how classical physics works - the classical approximation of (what we now know to be) discrete matter are good enough because discreteness of matter only manifests its effects in the micro world. — Devans99

Yes, exactly. But I think that in any case, whatever theory you use, physical results will always be only approximations. You can say that if you measure quantities that are fundamentally discrete, you can measure them with exact precision. But in quantum mechanics there is the problem that for very high degrees of precision you cannot be sure that the measure is correct: results have only a statistical meaning.

However, even if it were possible to create a model that is fundamentally discrete in all variables and described reality with absolute precision, it probably would be so complex that would be impossible to use!

The advantage of using infinity and differential equations instead of finite-difference equations (https://en.wikipedia.org/wiki/Finite_difference) is that calculations become much, much simpler. Without infinities, there are no symmetries. And without symmetries the laws of physics become a complete mess, impossible to use (even if they were the most accurate possible description of the real world).

P.S. I have a very good example of this kind related to computer-science that probably is easier to understand: computers are not able to represent natural numbers exactly, because memory locations are finite. But when you use them, you treat them as if the memory locations were infinite. You don't take into account what happens if the digits don't fit into memory: simply you take a bigger memory location so that you don't have to worry about the size.
Why? Because finite-precision arithmetic is much more complex that regular arithmetic, and if you had to take into account the finite size of memory locations, it would become impossible to reason about programs. Well, a very similar thing happens with the use of infinities in physics.

I think it is not necessary to fill space (as in a space-filling polyhedron like a cube). I am more imagining a grid of zero dimensional points in space. The particle, which has a non-zero dimension, would be centred on one of the grid points. If there are two neighbouring particles, they would not be in contact with each other, so space is not filled. Particles would move from point to point in the grid rather like the electron performs a quantum jump from one orbit to another - not passing between any intermediate space.

With QM, we have waves (and I suspect a particle is just a compressed wave) and so the waves would be centred on one of the grid points. — Devans99

But the wave functions in quantum mechanics are not supposed to have the size of the particle that they represent. For example, electrons are supposed to be point-like (or at least smaller than any detectable size), but the relative wave functions inside atoms are around $10^{-10}$ meters, and are even visible using scanning tunneling microscopes.
And there's even worse: in quantum mechanics if you make the space variables discrete, the momentum variables become continuous and periodic: a zero size for both position and momentum is forbidden by Heisemberg's uncertainty principle.

Loop quantum gravity - the competitor of string theory - has space as discrete. — Devans99

I don't know loop quantum gravity (except from some vague descriptions), but I am quite sure that it makes use of differential equations defined on continuous domains, like in all physics. If you use discrete values for the space variables, you cannot use derivatives on space variables.
Anyway, in any theory compatible with quantum mechanics events must be associated with a probability amplitude (https://en.wikipedia.org/wiki/Probability_amplitude), that is a complex number. And complex numbers are continuous. And you even need variables for fields, energy, momentum, etc.. I don't think there is any realistic theory of physics that has been defined without making use of continuous variables.

I think the main point of V.I. Arnold in this article is that the way mathematics is discovered (or invented), is not the way it is taught:

when a theorem is discovered, the theorem is conjectured to be true on the base of some physical intuition, or generalization of previous results, and then axioms are found to make the proof work.

when the same theorem it taught to the students, the axioms are presented (and you usually do not see why those particular axioms should be considered instead of others), and then the theorem is proved by means of logical deductions, sometimes without even mentioning the physical intuition and generalizations that was the base of it's discovery.

It is true that mathematics can be treated as the application of formal logic (the language) to a set of axioms, but in this way you lose the most important part of it: it's intuitive meaning.

Even stranger is calculations such as the Casmir Force uses 1+2+3+4......... = -1/12, and it is in accord with experiment. — Bill Hobba

Do you have a reference to a document where this result (1+2+3+4......... = -1/12) is actually used to calculate the the Casmir Force ?

A very strange phenomena - or is it? I have my view but would be interested in what others think. — Bill Hobba

The normal explanation, as you probably know, is that the the Zeta function coincides with the infinite series only where the series is convergent ( Re(s) > 1 ), but for s = -1 is defined as an integral, and the integral is convergent (https://en.wikipedia.org/wiki/Riemann_zeta_function).

The interesting question is: is there a way to define complex numbers so that the infinite series coincides with the integral on all complex plane? I don't know, but I even don't know any proof that this is not possible. Surely, to make this work complex numbers cannot be defined as an extension of the standard real numbers.

OK. So you are arguing that space is made of indivisible pieces, and every piece of space is made of a finite quantity of indivisible pieces. I think a more appropriate term for this is "atomic" (from the Greek world "atomos" that means indivisible). I didn't understand because before you wrote: "So all continua are (in the above sense) alike in that they can be subdivided forever".

But this means that points in geometry should have a size that is not zero, right? So, other question: what's the shape of a point? a 3-dimensional sphere? But you cannot fill the space with 3-dimensional spheres (there would be gaps between them). They should be rather like cubes.
In 1 dimension it could work: finite segments can be attached to each-other with no gaps. But if you try to build 2-dimensional geometry with squares in the place of points everything becomes much more complex:
- two "intersecting" lines not necessarily must have a point in common
- space cannot be isotropic (meaning: the same in all directions)
- the concept of straight line becomes very difficult to define, if the direction of the line respect to the grid is not a rational number.

Basically, you loose most of the symmetries of space. And symmetries seem to be a fundamental fact of nature. How do you deal with this problem?

A piece of space is discrete if it allows only a finite number of possible positions (points). So I've assumed an infinite number of possible positions - if its not discrete, it must be continuous. From Wikipedia:

"Formally, a linear continuum is a linearly ordered set S of more than one element that is densely ordered, i.e., between any two distinct elements there is another (and hence infinitely many others), and which "lacks gaps" in the sense that every non-empty subset with an upper bound has a least upper bound." — Devans99

But to be "discrete" does not mean to be "finite" (https://en.wikipedia.org/wiki/Discrete).

Discrete means that is made of parts that are distinct from each other: it can be finite, but not necessarily. The set of natural numbers is discrete but infinite. In fact, I think discrete is probably always synonym of "countable": it mean that you can associate each element of a discrete set with a natural number, so there are as many elements as there are natural numbers.

A linear continuum instead is made of "non separable" elements: you can shrink or expand the length of a segment, but you can't "separate" it's points from each other: the elements of a continuous set are not "countable".

So all continua are (in the above sense) alike in that they can be subdivided forever, so we can write:

points(0,1) = points(0,2) — Devans99

OK

It comes back to Galileo's paradox - the above are equal in the sense of a one-to-one mapping but at the same time, one is clearly twice the other. I think that it is not valid to compare the size of two infinities (as Galileo believed) - they are fundamentally undefined so have no size and cannot be compared. If something never ends, then it can never have a size and never be fully defined. I do not believe Cantor has added anything our the understanding of infinity - he has detracted from it - Galileo was on the right lines. — Devans99

Galileo's paradox is about positive integers, not about continuous sets. In fact, I believe that the idea of a "continuous set" had not even been invented in XVII century. For what I know, Euclidean geometry never speaks about a line being a set of points: for Euclidean geometry, 1-dimensional objects (lines) are a completely different kind of things then discrete (countable) objects. And Galileo does not even consider the idea that a line can be made of a set of distinct objects. For what I know, the idea of continuous (uncountable) sets was invented after Cantor, 200 years after Galileo.

So I think that maths cannot model infinity or continua. Does that mean these things do not exist in the real world? I think that maybe the case. If continua exist, then that implies that the informational content of 1 light year of space is the same as the informational content of 1 centimetre of space - in the sense that both 'containers' record the position of a particle to an identical, infinite, precision. This flaunts 'the whole is greater than the parts'. I trust that axiom more than I trust Cantor's math. — Devans99

So, if I understand correctly, you are trying to prove that the set of points of a line is finite (not countably infinite). Is it right?

If that's what you are arguing (that a line is made of a finite set of points), the obvious question is: how many points are there in a given segment?

If there is a finite number of points in each interval, space must be discrete, so I will assume an infinite number of points in each interval: — Devans99

If you want to show that continuum space implies a contradiction, you should start by assuming as hypothesis that "space is continuum AND one of the three points is true".

So how do you show that "space is continuum and point 1 is true" implies a contradiction?
The argument that you are making with the limits assumes that space is infinite but discrete, right?
How do you rule out that "space is infinite and continuum" ?

There is also a merely mechanical reason why it does not work: Gödel incompleteness theorems. I am actually not against the use of meaning, i.e. informal semantics, in mathematics. I am only against the use of semantics as proof; which should be syntactic only.

Actual meaning will be plugged in by the discipline that applies the mathematics. — alcontali

I totally agree that the use of logic in mathematical proofs, and the successive refinement of logic to formal logic at the beginning of 20th century, has been one of the one most important developments in the history of science. And it's this development that has given mathematics the freedom to create "new worlds", as Grothendieck used to say (http://www.landsburg.com/grothendieck/mclarty1.pdf).

But from another point of view, the evolution from ancient Greek's mathematics regarding Euclidean axioms of geometry as "a priori" to modern mathematics regarding symbolic logic as "a priori" is due to the recognition (due mainly to Riemann) that geometry should be really regarded as a branch of physics, and the facts that space is 3-dimensional and Euclid's 5th postulate is true should be regarded as experimental facts.

Well, what if the same was true even for symbolic logic?
If you think about it, what makes formal logic proofs absolutely certain, as opposite of geometric constructions, is the fact that they can be interpreted as algorithms or, equivalently, as purely topological geometric constructions (graphs built following a precise set of rules). And we are sure that every time that we execute the same algorithm with the same input, we get the same output (or, equivalently, that every time we follow the same path on a graph we always get to the same point).
But what if we leaved in a world where deterministic laws of physics do not exist? As we know from quantum mechanics (if quantum mechanics is correct), all laws of physic are in reality probabilistic: in principle you can never be sure with absolute certainty that the same experiment will give you always the same result. So, the reason why formal logic can be used to prove theorems with absolute certainty depends ultimately on physics: this is because at the macroscopic level the laws of physic are deterministic with an extraordinary high degree of approximation.

For example, Chris Barker's Iota combinator calculus is a Turing-complete system with just one combinator, i.e. Iota. People already wondered if the SK combinator calculus could be simplified from two symbols to one. So, Chris Barker positively answered that question. — alcontali

The Iota combinator is interesting because it's the simplest possible calculus that is equivalent to lambda calculus. And lambda calculus is interesting because it's equivalent to turing machines, and both are representations of the fundamental concept of a total recursive function.

Kleene's closure is an example of a theory that was utterly useless for a very long time, but surprisingly beautiful, and even intriguing. In the meanwhile, it has turned into a rage, some kind of hype. — alcontali

Kleene's closure is interesting because is a model of the algebraic structure called monoid, and a monoid is interesting because it's the generalization of a group. And a group.. you surely know.

Firstly, Immanuel Kant pointed out in his Critique of Pure Reason that the practice of solving visual puzzles, as in Euclid's Elements, could not possible be considered pure reason, because it rests on fiddling with visual input, while pure reason must be language only, entirely devoid of sensory input. That is one reason why an algebra-only, pure-reason approach to mathematics is much preferable to geometric fiddling with visual puzzles. — alcontali

Yes, I know Hilbert's program, from the beginning on 20th century (https://plato.stanford.edu/entries/hilbert-program/):
all mathematics should be reformulated as pure formal logic: syntactical operations on strings of symbols, following a well defined set of rules. The meaning of symbols is completely irrelevant in proofs. If a proof depends in some way on the meaning that you give to the symbols, it means that you are making hidden assumptions that should instead be expressed in a purely syntactic form.

And today we can be sure that this works: there are several extensive libraries of formalized proofs making use of computer-based formal logic systems, and a simple personal computer can verify the correctness of thousands of theorems in a few minutes. I guess this is Kant's "pure reason" in it's purest form.

But, as you probably know, there is a part of Hilbert's program that instead didn't work, despite more than 50 years of efforts to realize it. The idea is that if logic becomes a purely formal game, the search of a proof can be reduced to a mechanical computation: just search for all possible formal proofs and verify their correctness one by one, until you find one that is correct.
This idea doesn't work for one fundamental reason: once you have depleted a mathematical proposition of any meaning, you have no clue why that theorem should be true, or should be distinguished from the infinite sea of combinations of symbols that can be interpreted as theorems.

I believe that this fact is becoming more and more clear with today's rapid development of artificial intelligence. And this is the same problem that V.I. Arnold is referring to in this article, when he speaks about teaching mathematics: you cannot teach mathematics as a purely symbolic game, because in this way it has no meaning at all.

In other words: the meaning of a theory is not contained it it's purely symbolic representation, but in it's correspondence with the way the physical world works. In this sense, algebraic geometry (for example) is not substantially different from Maxwell's equations.

Geometrically constructible numbers are just a very, very small subset of all computable numbers. Therefore, these Euclidean methods hold us back. We had to drop them, in order to be able to progress. — alcontali

You are right: you can use algebra to generalize geometry. But you need geometry to have something to be generalized: the axioms and definitions of algebraic geometry are carefully chosen to correspond to Euclidean geometry as a the particular case.

Axioms are not "correct". Axioms are just arbitrary starting points for the construction of an abstract, Platonic world.. Axioms have nothing to do with the real world (just like everything else in math). — alcontali

It is true that from any set of axioms you can build a theory and derive the relative theorems, but I guess that nobody would be interested at all in axioms that do not correspond to any generalization whatsoever model that corresponds to ideas taken from the physical world. If you choose the 'wrong' axioms, you obtain a meaningless theory.

We do not want so-called usefulness. We want purity, because ultimately, it is purity that is math's usefulness. — alcontali

Yes, we don't want usefullness, but we want beauty, simplicity, symmetry, elegance. Try to take any of the most elegant parts of mathematics (say, for example, the theory of holomorphic functions - or complex functions' calculus), write it using ZFC first-order logic, changing all the names into random strings and present it to a mathematician without explaining what is it. Well, maybe I am wrong, but I think that nobody would say that this is beautiful mathematics.

I'll stop here for now (I don't want to make this post too long), but I hope I made clear what I mean...

Here's a video that may interest you:
https://www.youtube.com/watch?v=oBOZ2WroiVY

Goodstein's theorem is a theorem about a computable function that cannot be proved without assuming the existence of actual infinity.

P.S. Don't ask me why: I don't understand it either.. :smile:

Yes, no doubt it's impossible. But nobody says that only computable functions exist.

I believe there is constructivism - a minority view in maths - which rejects actual infinity. — Devans99

I see that there is a lot of misunderstanding about constructivism meaning the rejection of actual infinity.

Constructivism is not about the rejection or acceptance of actual infinity, but it's about choosing computable functions as a fundamental logic concept (that is implemented the rules of logic), as opposed to the more abstract idea of functions that is implied by the classical axiom of choice.

But this, in my opinion, is more a question of practical convenience in simplifying the proofs (mainly in topology), rather than a philosophical point of view: you can always reason about computable functions by using the internal logic of a "topos" in category theory, even taking non constructive logic as fundamental. And you can easily axiomatize the standard functions (the one corresponding to the classical set theory with the axiom of choice) by using constructivist logic. Only that, in my opinion, the latter choice is conceptually simpler and easier to use, at least for the branches of mathematics directly related to topology.

If you choose logical rules to represent computable functions, you get constructive logic.
If you choose logical rules to represent abstract functions (in the sence of input-output correspondence, not necessarily computable), you get the standard non constructive logic.

In summary, it's only about the choice of which kind of functions you choose to be "fundamental".

I think we could interpret natural numbers as properties, or attributes, of physical objects: "5" is an attribute of a physical object that is made of 5 parts. At the same way as "red" is an attribute of an object that reflects red light.

Hi @fishfry!

Read this first, don't waste time slogging through my other posts. This is the heart of the matter. — fishfry

OK! as you wish :smile:

* First, I must say that as much as I've been aggressively rejecting your remarks about Coq, that is only because I'm not yet ready to receive the information. First I need to grok the essence of this constructiveness business; and I have found that Cauchy completeness is a bridge from math that I know, to constructive math that I'm trying to understand. So I'm "On a Mission" and can't be distracted. — fishfry

No problem!

* On the other hand, if and when the day comes that I am ready to learn about Coq -- which I confess I've been interested in from afar since I started watching Voevodsky videos -- I will start at the beginning of this thread and read every word you've written and follow every link! Because you are giving a master class in how someone can think about Coq in the framework of constructive math. — fishfry

Actually, I find Coq is much easier then the paper that you found! But everything depends on your background, I guess.

* And what is that thing? It's Cauchy completeness. — fishfry

OK, let's focus on Cauchy completeness.

The constructive reals are Dedekind complete but not Cauchy complete — fishfry

Hmm.. I am sorry that I have always to disagree with what you say, but in my opinion this is not exactly what that paper says :sad:

Let's read the abstract: "It is consistent with constructive set theory (...) that the Cauchy reals (...) are not Cauchy complete".

That is exactly equivalent to say this: "It is not possible to prove with constructive set theory (...) that it is not true that the Cauchy reals (...) are not Cauchy complete.":
To say that a proposition is consistent with a theory means that it's not possible to prove that the proposition is false in that theory. It doesn't mean that it's possible to prove that the proposition is true.

In fact, the proposition "Cauchy reals (...) are not Cauchy complete" cannot be proved with the constructive set theory that he considers.

How do I know? Because the axioms of IZF_Ref (the constructive set theory that the paper is speaking about) are provable in ZFC, and the rules of IZF_Ref are the same rules of ZFC without Excluded Middle (here is a good reference for the axioms: https://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html).
Then, all theorems that are provable in IZF_Ref are provable even in ZFC: just use ZFC axioms to prove IZF_Ref axioms, and then apply the same rules as the original theorem (ZFC has all rules of IZF_Ref, then it can be done).
So, if "Cauchy reals (...) are not Cauchy complete" were provable in IZF_Ref, it would be provable even in ZFC. But, as we know, in ZFC this is provably false.

In fact, some models of IZF_Ref are not Cauchy complete (the two models that he considers) and some other models of IZF_Ref (the standard ZFC reals) are Cauchy complete.

And so, here is a confession: I don't even know what Dedekind completeness is — fishfry

Dedekind completeness is simpler than Cauchy completeness to formulate in set theory, but practically impossible to use in analysis. Basically, this is the thing: if you build "Dedekind cuts" of rational numbers you obtain the real numbers (this is not part of the theorem, but the definition of real numbers in ZFC), but if you build "Dedekind cuts" of real numbers you obtain again the same real numbers. The same thing hapens with Cauchy: taking limits of rationals you obtain reals but taking limits of reals you obtain again reals (the set is closed under the operation of taking limits and forming Dedekind cuts).
A Dedekind cut is simply the partition of an ordered set in two non empty sets that respects the order relation (any element of the first set is smaller than any element of the second set).

and then start to attempt to grok what it means to be Dedekind complete but not Cauchy complete in an intuitionist setting (whatever that means!) — fishfry

OK. In my opinion, intuitively it means that they can be the same thing as standard ZFC reals, but can even be something very different. Simply there are more possible "forms" for the object called "set of real numbers". And there is even another problem with the definition of convergent Cauchy sequences defined in this article: they are not the sequences of rational numbers (as the standard definition) but sequences of pairs made of a real number plus a function (from page 2: "So a real is taken to be an equivalence class of pairs <X, f>, where X is a Cauchy sequence and f a modulus of convergence).

* Finally I just want to say that with all the back and forth, and I do note that we both tend to the wordy side, this current post of mine represents my latest thinking about everything; and all prior comments are null and void. — fishfry

OK, I'll not look at you previous posts any more :wink:

Here is where your post totally went off the rails. As I said? I said nothing of the sort! I quoted the definition in the Italian paper. — fishfry

The definition of real numbers in the Italian paper is on the third page. The last axiom of that definition is this one:

$completeness: \forall f: N \to R. \exists x \in R. (\forall n \in N. near(f(n), f(n+1), n+1)) \to (\forall m \in N. near(f(m), x, m))$

Is that what we are speaking about? ( finally I learned how to write symbols :-) )

[ I don't want to address too many points because I'll go off the road again. So, I'll wait for an answer about these ones for the moment ]

Yes that's the one direction. But it's the other direction that's harder. If a sequence is Cauchy in standard math, is it Cauchy in intuitionist math? That's a good question and I'm sure the constructivists have an answer, I just don't happen to know what it is. — fishfry

Let me rephrase the question: "If a sequence is Cauchy in ZFC, is it Cauchy in intuitionist math?"
This question is too vague to have an yes/no answer:
"a sequence is Cauchy in ZFC" we know what it means.
"a sequence is Cauchy in intuitionist math" I don't know what you mean.

The adjective "intuitionist" is a property of a logic. You should say of what theory of real numbers (formulated in that logic) you are referring to.

I can try to interpret it as "a sequence is Cauchy in the theory of real numbers of the Italian paper".

Answer: If you take a Cauchy sequence in ZFC, you have a set of sets such that... (a proposition about that set of sets). Not all sets of sets that are expressible in the language of ZFC have a corresponding term of type R (the type of real numbers) in the language used in the theory of the Italian paper. So, you cannot really compare them.
Put it in another way: which logic do you want to use to compare the two sequences? The first one is expressed in first order logic, the other one in Coq (If you don't want to speak about Coq, please choose another concrete intuitionistic logic and model of real numbers. There are too many of them to be able to speak in general).

Ok. Question: How can any model of the reals built on constructive principles be Cauchy complete? — fishfry

Answer: because Cauchy completeness is assumed as an axiom of the theory (this is not a model of the reals because real numbers are described axiomatically). You can argue about the consistency of the theory, but you cannot argue about Cauchy completeness. Cauchy completeness is assumed as an hypothesis.

Yes but I'm not talking about Coq. — fishfry

The Italian paper is about a formalization of real numbers in Coq:
"We have formalized and used our axioms inside the Logical Framework Coq" (from the first page).
That's why I was speaking about Coq

OK. I see what I am doing wrong: I am making very long premises to be able to refer to them in the following argumentation. But if you start reading the beginning without looking at the following part you find what I wrote completely unrelated to the point you are asking.
So, I'll try to change my style of writing: go straight to the answer of only one specific question and keep the post short and focused on one question at a time.

$x = {-b \pm \sqrt{b^2-4ac} \over 2a}$

It works!!! :starstruck: :starstruck: :starstruck:

That validates my earlier point that among all models of the real numbers, the standard (ZF) reals are privileged by virtue of being Cauchy complete. — fishfry

What do you mean by "the standard (ZF) reals"?
Maybe I am saying obvious things, but at risk of being pedantic, I prefer to make everything clear about some basic facts. (That's one of the reasons why I like computer-based formal systems: everything has to be declared. No implicit assumptions!)

Fakt N.1. ZFC is NOT an axiomatic theory of real numbers. ZFC is an axiomatic theory of SETS.
In fact, in first order logic all functions and relations can be applied to all variables, and there cannot be some functions (like addition and multiplication) applied only to numbers and other functions (like union and interception) applied only to sets. In ZFC, all variables are interpreted as SETS.

Fakt N.2. The standard representation of real numbers in ZFC is the following: (https://www.quora.com/How-is-the-set-of-real-numbers-constructed-by-using-the-axiomatic-set-theory-ZFC-set-theory)
- Natural numbers are sets
- Integers are pairs of natural numbers (a pair is a function with two arguments)
- Rational numbers are pairs of integers
- Real numbers are sets of rational numbers

Here's the definition of real numbers in ZFC in Bourbaki: https://math.stackexchange.com/questions/2210592/in-which-volume-chapter-does-bourbaki-define-the-real-numbers

Fakt N.3. There is a more "usable" definition of real numbers given by Tarski (usable in the sense that the demonstrations are simpler): https://en.wikipedia.org/wiki/Tarski%27s_axiomatization_of_the_reals

- Tarski's real numbers are defined axiomatically, and make use of set relations (similar to the ones of ZFC). But they are not based on first order logic.
The difference is that it is allowed the quantification on all subsets of a given set (and not only on all elements of the universe), but the meaning of the subset relations is encoded in the rules of logic, and not given axiomatically.
The use of a second-order logic is essential to be able to express the property of being Dedekind-complete (Axiom 3)


So, going back to what you wrote:

The constructivists agree! They are trying to develop a context in which they can say that the constructive reals are complete.

[From now on complete means Cauchy complete and not any other mathematical meaning of complete]. — fishfry

OK, let's check the definition of being "Cauchy complete":
"Cauchy completeness is the statement that every Cauchy sequence of real numbers converges." (https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers)

What's a Cauchy sequence? "a Cauchy sequence (French pronunciation: ​[koʃi]; English: /ˈkoʊʃiː/ KOH-shee), named after Augustin-Louis Cauchy, is a sequence whose elements become arbitrarily close to each other as the sequence progresses." (https://en.wikipedia.org/wiki/Cauchy_sequence)

As you said, in the Coq formalization of real numbers there is this axiom:

completeness ∀f : N → R. ∃x ∈ R.(∀n ∈ N. near(f(n), f(n + 1), n + 1)) →(∀m ∈ N. near(f(m), x, m))

In the logic of Coq, "completeness" IS A FUNCTION, at the same way as "near" is a function and "+" is a function.

The function "completeness" takes as input a sequence of real numbers "f" and returns two things:
1. a real number "x" -- let's call it "first_part"
2. a proof that IF "f" is a Cauchy sequence, THEN "x" is the limit of "f" -- let's call it "second_part"

So, for every sequence of real numbers "f", the term "(completeness f).first_part" is a real number. If I have a proof that "f" is a Cauchy sequence, then I can use "(completeness f).second_part" (that is a proof) to obtain a proof that the Cauchy sequence "f" converges to the real number "completeness f".

That's all I need to get a COMPLETE field of real numbers: for all sequences "f", if you have a proof that "f" is a Cauchy sequence, you can produce a proof that "f" is convergent to the real number "(completeness f).first_part".

However, you can't explicitly compute it, because axioms are functions that cannot be reduced (https://stackoverflow.com/questions/34140819/lambda-calculus-reduction-steps)

Then, IF you ASSUME that you can get a real number for every Cauchy sequence, THEN you can prove that there is a real number for every Cauchy sequence. Magic! :-)

* How can the constructive reals be complete? If they are complete they must contain many noncomputable reals. How can that be regarded as constructive? — fishfry

Yes, that's the same old question that I thought I just answered many times... :-)

Here's the "computation" of pi:

Definition my_sequence := func n -> sum of 1/n bla bla...
Definition pi := "(completeness my_sequence).first_part"

Here's the proof that my_sequence converges to pi:
1. proof that my_sequence is a Cauchy sequence (let's call this proof my_proof)
2. from "(completeness my_sequence).second_part" (the proof that IF "f" is a Cauchy sequence, THEN "x" is the limit of "f") and "my_proof" (the proof that my_sequence is a Cauchy sequence) I get a proof that "x" is the limit of "f"
(by applying the rule of cut)

I "computed" the noncomputable real number pi, and the result is "(completeness "func n -> sum of 1/n bla bla...").first_part

If "completeness" were a theorem instead of an axiom, I should have provided the implementation of the program that computes the function "completeness". But an axiom is treated as an "external function" of a programming language:
I ASSUME to have some external machine that is able to compute the function "completeness", but I don't have to show how that machine works. That's cheating! :-)

However, remember that this is an AXIOMATIC DEFINITION of what real numbers are, NOT A MODEL of real numbers.
Axiomatic definitions, in whatever logic (intuitionistic or not), are not guaranteed to be consistent: you have to be careful on what axioms you assume to be true.
So, in principle it's not guaranteed that the real numbers that you defined make sense in some concrete model.

And that is true even for Tarski's real numbers, that are described using classical (non intuitionistic) logic.

Instead, this is not true for the description of real numbers in ZFC. In that case, real numbers are a model built from sets, and completeness is PROVED as a theorem, and not assumed as an axiom. Real numbers are concrete objects made of sets!

The problem is that sets are defined axiomatically in ZFC. So, IF sets make sense (are not contradictory), then real numbers make sense. But IT'S NOT GUARANTEED THAT THE SETS DEFINED IN ZFC MAKE SENSE IN SOME CONCRETE MODEL.

So, again, to be sure about the sets of ZFC you should define them as a model in some other axiomatic theory that you trust more than ZFC. Or you could use a FINITE MODEL: in a finite model you can verify a proposition "by hand" (as one of my favourite professors of analysis used to say) simply inspecting the model!

But, obviously, there is no finite model that verifies all the axioms of ZFC. The best that you can do is to verify ZFC axioms on a model built from natural numbers. But natural numbers are NOT a finite model (you cannot check theorems on natural numbers "by hand"). And, as Godel proved, there is no axiomatic definition of natural numbers, in any formal logic, that is guaranteed to make sense.

OK, I'll stop it here because it's just become too long and I am only at the first question.

* Does their formulation actually imply standard Cauchy completeness? — fishfry

Let me rephrase this question: "if a given Cauchy sequence has a limit in intuitionistic logic, does it have a limit even in ZFC?"
The answer is YES, because the axioms of intuitionistic logic correspond to theorems in ZFC, and the rules of intuitionistic logic are just a subset of the rules of classical logic. So, if you can prove that a given sequence is convergent in intuitionistic logic, you can use EXACTLY THE SAME PROOF in classical logic. You can map any proposition of one logic to a corresponding proposition of the other logic and every rule of one logic to a corresponding rule of the other logic. It doesn't matter what's the interpretation of the rules: if the rules are the same (or a subset of them), whatever you can prove in intuitionistic logic you can prove even in classical logic: just apply the same rules!

* In what sense is their formulation constructive? I gather this may have something to do with the rate of convergence, in which case perhaps the theory of computational complexity may come into play. Big-O, P = NP and all that. I'm a big fan of Scott Aaronson's site. — fishfry

Nothing to do with the rate of convergence! Constructive, in the particular interpretation of Coq, means that every object (every real number in this case) can be built using recursive functions ( except axioms... :-) )

* And if the constructive reals are Cauchy complete, they must contain a lot of noncomputable real numbers. How can that be called constructive? — fishfry

This sentence has a hidden presupposition: that real numbers are a concrete set of objects and you can check if a given noncomputable real number is present or not. This is not true: any model of real numbers is ultimately based on an axiomatic theory that cannot be checked "by hand".

[ I know, I wanted to use formulas to be more precise and at the end I didn't do it (mostly for lack of time). And probably I still wasn't able to be clear enough on what I meant. So, please repeat the questions that I wasn't able to be clear about, or where you thing that I am wrong. Maybe in that way will be easier to arrive at some conclusion ]

In ZFC a Cauchy succession is a definition, and completeness is a theorem, not an axiom.

P.S. OK, sorry. They have Dedekind as an axiom, that is equivalent in ZFC, so it's the same thing. My mistake! Just ignore what I said... :confused:

OK, I'll rephrase it: if you remove the completeness axiom (consider the same exact theory without that axiom), Cauchy completeness is not provable nor refutable.

By the way, just a quick note: as you said they have a completeness AXIOM. Not a completeness theorem. It means that completeness is not provable nor refutable!

Hi @fishfry!

Sorry, but you have to give me some time to learn about how to write symbols on this site, and I have not much time for this right now. Otherwise we keep speaking using words without meaning, never reaching any conclusion.

I promise that I'll answer very clearly to all your questions, but I am going to need some time (probably some days), even because I have a lot to do at work these days.

I am very curious about this. Doesn't the vector's length follow from the Pythagorean theorem? If so, then it seems it isn't a simple logical equivalence, since the equation between real numbers (a vector's length) depends on the application of the theorem. Or is there an independent way of measuring a vector's length? — Kornelius

Hi!

here's what I mean:
imagine you don't know anything about geometry: you are a computer without any way to "view" the world: no cameras, computer vision, or any kind of sensory system. Only a simple PC with a software to analyze theorems expressed in a formal logic.

You see this theorem:
forall A B C : PO, (orthogonal (vec A B) (vec A C)) <-> (Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C)). [ I added parentheses to make it more readable: this is Pythagoras taken directly from here: https://madiot.fr/coq100/, no changes at all]

All you can see is this: IF you are given 3 objects of some type named PO (points), the theorem says that there is a "logical equivalence" ( the "if and only if" in the middle of the expression, written as "<->" ) between two propositions:
- proposition 1: "orthogonal (vec A B) (vec A C)"
- proposition 2: "Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C)"

Now, you don't know what "orthogonal" and "vec" means. If you want, change the names into completely random strings. Could you guess that this is an interesting/important theorem?

All you know is that (vec A B) is an object, (vec A C) is another object, and "orthogonal" is a proposition speaking about these two objects.

Then we have the function Rsqr: you know what is Rsqr: it's the square root of a number: you are a calculator and you know how to compute the square root.
And then you have a function "distance" that takes two objects of type PO (points) and returns a number. You don't know how this function is implemented.

Given these conditions, this is not an "improbable" proposition because there are too many degrees of freedom: you can choose a random function for "distance" and on the base of that definition build the proposition "orthogonal" to make the equation become true.

But if you look at the model (interpretation) of the functions "orthogonal" and "distance" on the physical space, you discover that "orthogonal" is the only combination where the projection (the shade) of one vector over the other is exactly zero. And the function "distance" happens to be a very simple function of the length (it's square): so you have an improbable coincidence: a rare property of the angle coincides with a simple formula for the equation. If you define "orthogonal to be another angle, you can still define an equation that relates the lengths, but only making use of trigonometric equations (that are defined especially for this purpose; but Pythagoras' equation is one of the simplest expressions that you can build with addition and multiplication).
Ultimately, this depends on the fact that physical space is flat (zero curvature). If it was not flat the formula for the lengths of a straight triangle would have been a much more complex (random) equation.

Yes, that's very interesting. Thank you for the reference!

P.S. After reading this, please read my explanation on what is "wrong" with Banach-Tarski paradox, if you have time.

Here is a good explanation of what "contructive mathematic" means: https://www.iep.utm.edu/con-math/

There's exactly one model (up to isomorphism) that is Cauchy complete; and that is the standard reals. — fishfry

That seems to be the common point of all your arguments about real numbers, so I wanted you to show you this: https://mathoverflow.net/questions/128569/a-model-where-dedekind-reals-and-cauchy-reals-are-different
I know that there is a proof of uniqueness.

So that implies something false can be added to set theory without changing its consistency. — Devans99

Yes. Consistency and truth are not the same thing. That is one of the main consequences of Godel's incompleteness theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems

Truth is about the interpretation of a proposition on a concrete model. I a not even sure if there is a commonly accepted definition of what is a model, or a widely accepted definition of truth. I believe the definition of truth is more in the domain of philosophy: working mathematicians treat their (abstract) mathematical models as if they were real concrete physical models and the propositions were concrete physical experiments on which a proposition can be tested to obtain a result true or false.

Consistency, on the contrary, is defined as a property of a formal logic system: a formal system is inconsistent if a proposition can be proved to be both "true" and "false". "true" and "false", in this case, is are purely syntactical objects: a string of characters that is the result of the execution of an algorithm.
If a proposition cannot be proved to be "true" nor "false", it (it's interpretation as experiment, let's say) can be true for some models and false for other models. If a proposition can be proved, it has to be true for all models. It it's negation can be proved, it has to be false for all models.

For example, if I define a simple maths system with only one number: 1 and one operator: + then I can axiomatically define 1+1=1. Its consistent but not logical. — Devans99

I believe that the word "logical" is really used as a synonym of "consistent", but only in colloquial english. In mathematics I think it's not used at all.
A simple math system may be consistent even if it doesn't have any model (except from the "purely syntactical one": every consistent logical system has a model made regarding as objects of the model the syntactical symbols of the language). You can prove the proposition "1+1=1", but you cannot say that it's true if you don't specify in which model. (By the way, a formal logic system is not a completely arbitrary set of rules an symbols: symbols of negation true and false have to be defined: otherwise the definition of "consistency" itself makes no sense)

P.S. Sorry, I just realized that what I wrote about the definition of consistency is wrong: a formal system is inconsistent if for some proposition both the proposition and it's negation can be proved. I think the strings "true" and "false" (or something equivalent) are not required to be part of a formal logic system (well, everything depends on which logic we are speaking about: there are too many of them.. :-) ).

In 1940 Godel proved (https://www.sciencedirect.com/science/article/pii/S0049237X08715003) that the "generalized continuum hypothesis" can be added to the theory of sets without changing it's consistency. Basically, it means that, if the theory is inconsistent, it's not because of the addition of actual infinity to it.

What I am arguing about the model of real numbers based on ZFC is not that it's not consistent because of actual infinity, but that it's unnecessarily complex: the same thing can be achieved with simpler axiomatic theories, that seem to be more "natural" to encode the relevant theorems of mathematics.
This, as fishfry is trying desperately to make me understand :wink:, doesn't make much sense from the point of view of logic, because a formal logic system is like a definition of a mathematical structure: there are not good or bad definitions, but only definitions that are more or less appropriate because of their complexity.

Well, in my opinion there is a concrete way to judge if a definition, or a formal logic system, contains unnecessary overstructures or not. And what I was trying to understand with my poorly understood discussions "Is it possible to define a measure how 'interesting' is a theorem?" and "Is mathematics discovered or invented" is if somebody knows about other results/ideas in that direction.

P.S. http://mathworld.wolfram.com/ContinuumHypothesis.html

But you have to admit that there must be a way to make sense of the idealized things, because mathematics is essential in nearly all contemporary science. And it works! Very often physicists are astonished by the fact that you can predict the results of experiments with incredible precision by reasoning about idealized models, and without even knowing how to make the real objects correspond to the idealized ones! The most famous example is probably quantum mechanics, but all of physics from Newton (then practically all of it) is made in this way. Newton was very clear about this: he was looking for a causal explanation of the law of gravitation, but he had to admit that his "action at a distance" is not an explanation of how nature works (like you can explain how a clock works by describing how the internal gears are connected), but only a description by means of an idealization of the "force" by a mathematical model that makes no sense intuitively. But it works extremely well.
You can say that idealizing the real world is misleading, but after several centuries of mathematical models that work extremely well, I think that you can be convinced that this is the right way to go..

Yeah... I see what you mean. But this is not the way how mathematics works. You see, you cannot say that a plane does not exist because it has no width, and all real things have a width. If you try to reason about geometry using only 3-dimensional finite objects, any of the theorems of geometry makes sense any more! A plane, a line, a point, a real number, an integer number, whatever you define in mathematics is only an idealization of something that exists in reality: it's not the real thing. And very often it's an idealization of something that is completely imaginary and doesn't correspond to anything that exists in reality. But the fact is that idealizations are useful to capture essential characteristics (or symmetries, or properties) of the real things. Without idealizations there is no mathematics!

I don't know how to answer to this: division by zero is not defined, OK.

But how do you think you can use a value that is not defined? Not defined means simply that you did not define what that thing is: you cannot reason about something without defining what is it, can you?

I really don't follow your point here at all. B-T is the least of it. If you reject point-sets as the foundation of math, that's fine, but then you have to rebuild a LOT of stuff. B-T is the very least of it. — fishfry

OK, let alone BT. In my opinion there are no interesting results that depend in an explicit way on the fact that a continuum line is defined as an uncountable set of points. Are there? You could assume that a line is made of infinite trees, or functions from integers to integers, and everything could be made to work at the same way: if you assume the axiom of choice and the existence of non-measurable "gadgets", you can think a line to be made of whatever "gadgets" you want.

That's a pragmatic requirement I don't share. You think math is required to be bound by physics. Riemann kicked the hell out of that belief in the 1840's. You think math is physics. Mathematicians don't share that opinion. Math is whatever mathematicans find interesting. If the rest of the world finds an application, more the better, but that is never the point of research in pure mathematics. — fishfry

Formal logic (currently assumed as the foundation of mathematics) is only dependent on one very fundamental fact of physics (that usually is not regarded as physics at all): the fact that it's possible to build experiments that give the same result every time they are performed with the same initial conditions.

Mathematics (what is called mathematics today) is the research of "models' factorizations" that are able to compress the information content of other models (physical or purely logical ones). A formal proof makes only use of the computational (or topological) part of the model. The part that remains not expressed in formal logic is usually expressed in words, and is often related to less fundamental parts of physics, such as, for example, the geometry of space.

Riemann understood that the concepts of "straight line", measure, and the topological structure of space are not derivable from logic, but should be considered as parts of physics.

In the future, when mathematicians will start to use quantum computers to perform calculations, I believe that even the existence of repeatable experiments will not be considered "a priori", but as an even more fundamental part of physics. So, there will be quantum logic that is more powerful than standard (or even constructionistic) logic, at the price of not being able to be 100% sure that a proof is correct (but you will be able, for example, to say that we are sure about this theorem with 99% of probability).
Surely your ( and most of other peoples' ) reply to what I just said is that "this is no more mathematics". Well, at the time of Euler topology was not mathematics either.

What I do know is that the set-theoretic continuum, having won the 20th century, underpins all modern physical theory. — fishfry

Can you show me a physical theory, or a result of a physical theory, that is somehow derived from the fact that a continuous line is made of an uncountable set of points?

What's wrong with the Banach-Tarsky paradox
( meaning: how is it possible that you can change the volume of an object by applying only isometric tranformations? )

Let's take as reference the most complete proof of the theorem that I was able to find: http://www2.math.uconn.edu/~solomon/BTFinal.pdf

STEP 1. We define a group of rotations G (page 11: "The Group G")
The group G is defined as "the set of all matrices that can be obtained as a finite product of the matrices "phi" and "psi" ( Theorem 3.3 on page 12 ).
So, G is a discrete group. "psi" contains a parameter "tetha" (a real number), that is assumed to be a FIXED arbitrary number, with only one condition: "cos tetha" is a transcendental number (last paragraph on page 16). Then, by the way, tetha cannot be zero.

G is a discrete (countable) set of rotations around the origin (point (0,0,0)), that are ISOMETRIES ON R3. No doubt about this.

STEP 2. Theorem 3.5 on page 13.
(This is the surprising part about the decomposition of G, but I will not describe it in detail, since you know very well how it works)
We can decompose each element of G (each rotation, that we supposed to be built using TWO basic rotations), in an UNIQUE way, as a sequence of THREE rotations: the two that we considered before ("phi" and "psi"), plus "phi squared", that is "phi" applied twice.
As a consequence of this, you can split the set of rotations G in 3 parts, named G1, G2 and G3 ( Theorem 3.7 on page 17 ).

STEP 3. We use the partition of G to define a similar partition of the unit sphere in R3, named S (that is a 2-dimensional surface) - ( Theorem 4.1 on page 21 ).

First of all, we consider all possible rotations contained in G (that, remember, is a countable set). For each of them we have a pair of points of the sphere that are not moved by the rotation (the ones that lay on the axis of rotation). So, we define P to be the set of all points that lie on the axis of rotation for any rotation in G. This is obviously a discrete (countable) set of points, that has zero measure: it's not a 2 dimensional object.

Then, we consider all other points of S, excluding the set P (the set S \ P)
From page 22: "For each x ∈ S \ P, let G(x) = {ρ(x) : ρ ∈ G}".
It means: take a point x of S \ P and build the set G(x), that is the set of all points where you can arrive by applying all possible rotations that are in G. This is obviously a discrete (countable) set too. And is a set made of points that are distant from each other (the angles of rotations are finite). This is not a connected piece of S \ P, and is not an open set. It has zero measure.

Here's the critical part (still on page 22): "We can also notice, by conducting
the following calculation, that any two sets G(x) and G(y) are either disjoint or identical". OK, so the orbits induced by G are a partition of S \ P.

A few lines after: "This proves that the family of sets F = {G(x) : x ∈ S \ P} is a partition of S \ P"
The sets of this family are the orbits induced by G. How many orbits are there? Obviously, there are uncountably many orbits, right? (I think this is why the author calls it a "family" and not a "set").

So, now we can prove that "this partition is equivalent to one formed by the desired sets
S1, S2, and S3". OK, but what are the 3 parts of this partition? Each part is made of an uncountable number of points, and contains at least one point for each orbit. In other words: the set S \ P is split by splitting the single orbits (made of a countable set of points), and NOT by splitting the surface S \ P in an uncountable number of open sets. It is not proved that the partition of S \ P preserves it's topology.

On the contrary, I think that it can be proved that this partition cannot preserve the topology of S in any point of S. Or in other words, it cannot be continuous. That means that for each point x in S and for each real number epsilon greater than zero, you can always find a point of each of the sets S1, S2 and S3 contained in the circle with center x and radius epsilon.
Why? Because the orbits induced by the rotations of G are unstable: if you start from two points arbitrarily near to each other, you can finish in points that have a distance greater than 1/2, if you take an enough big number of steps.
(OK, to prove that each open set contains at least one point of each of the subsets you should show that the points of an orbit are distributed over all the sphere without leaving "holes", but this is a detail: for my argument to be valid is enough that this happens for at least a measurable portion of the sphere)

That is the point: there is no doubt that the rotations of G are isometric operations. The problem is that they are not performed on connected pieces of the sphere. They are performed on discrete sets of points (distant from each other) with zero measure. They do preserve that 0 measure, but the measure that you should preserve is the one of open subsets of S, and that measure is not preserved.

The "trick" of regarding an infinite sequence of points as the same set of points minus the first one can be applied only to countable sets, and G is a countable set. And the orbits of G are countable sets. But the transformation that we use to split S into 3 pieces is NOT a rotation, is NOT isometric, and it's even NOT continuous!!


OK, this is the end. I think I cannot explain better than this my argument about BT.

It's much less mysterious that you think.
First of all, let's use the definition of real numbers as Cauchy sequences.

The definition of the Omega number is this one: \Omega _{F}=\sum _{p\in P_{F}}2^{-|p|}, (taken from here: https://en.wikipedia.org/wiki/Chaitin%27s_constant - sorry, I still didn't learn how to correctly type formulas..). This is a Cauchy sequence, but there is a missing piece: the function "halt(p)" that takes a string representing the program p and returns true if it halts and false if it doesn't. Since the function halt(p) is not computable (but well defined), then the function Omega too is not computable.

In a non constructivist logic, you define Omega in this way: Let "halt(p)" be the function that returns true if the program p halts. Then, Omega is defined to be the previous formula.

In a constructivist logic, you do exactly the same thing: Let "halt(p)" be the function that returns true if the program p halts (that in costructive logic means: let's assume that the function "halt(p)" exists). Then, Omega is defined to be exactly the same formula.
That means: IF you give me a function "halt(p)", THEN I can give you Omega: this is simply a function that takes as an input a function from strings to booleans (strings represent programs), and returns a Cauchy sequence. The fact if "halt(p)" is computable or not does not make any difference for the constructivist aspect of logic: you ASSUME to be given this function (it's an hypothesis): you don't have to build it! (neither in constructivist, nor in standard logic).

The other essential point is: the fact that you cannot build a given real number (because you cannot build the function "halt(p)") DOES NOT MEAN that there is a missing real number, and then you have a hole in the real line, that is no more continuous! The real numbers are uncountable (using the standard definition, of course), so it's obvious that there is an uncountable quantity of real numbers that ARE NOT DEFINABLE. If they are not definable, it means that you cannot prove that they exist (classical logic), you cannot construct them (constructivist logic), and you cannot even prove that they don't exist! Simply you cannot speak about them in the language!

P.S. To be even more clear (I know that I am repeating myself):
constructivist logic does NOT mean that the only numbers that exist are the ones that can be built! It only means that to prove "forall x such that ... exists y such that..." you have to build a computable function that has an x as an input and produces an y as an output. x can be a number that is not computable, or even not definable. You simply assume that somebody gives you x, and you can use it to build y.

Your interest in Banach-Tarski is orthogonal to all the philosophical and foundational issues; and the confusion generated by conflating these things is causing you to misunderstand some extremely elementary points of math, such as the continuity of translations and rotations and reflections. — fishfry

Yes, I really wasn't interested in speaking about Banach-Tarski. I took it only as an example, maybe the wrong one. But on the other hand I am convinced that what I wrote is correct, so I am a little upset to not being able to convince you (and it's not about you: probably I didn't convince anybody...). I could start a separate discussion and try to use formal proofs instead of explanations, but I am afraid it's not appropriate for a philosophy forum (I still didn't read how to write symbols on this site). Maybe I'll make a last attempt tomorrow, and than stop talking about BT. But I have not time now. However, thank you for replying to my posts.