Arghhh. In my opinion you are totally missing the point of math. I don't mean that to be such a strong statement, but in this instance ... yes.

The point isn't to have a pristine logical proof. The point is the beautiful lifting, via the axiom of choice, from the very commonplace paradoxical composition of the free group on two letters, up to a paradoxical composition of three-space itself. It's the idea that's important, not the formal proof. That is the actual point of view of working mathematicians.

I recently ran across an article, link later if I can find it. Professional number theorists were asked by professinal logicians, wouldn't you be interested in seeing a computerized formal version of Wiles's proof of Fermat's last theorem? And the logicians were stunned to discover that the mathematicians had no interest in such a thing! — fishfry

First of all, the point about formal systems. I completely agree that the formal proof is not the essential part of a theorem about geometry! I'll tell you more: I am pretty convinced that the formal proof alone does not contain the essential information necessary to "understand" the theorem, and I started to write on this forum because I was looking for somebody that has some results/ideas on this point. Please take a look at my last post on the discussion that I opened about two months ago: "Is it possible to define a measure how 'interesting' is a theorem?" (https://thephilosophyforum.com/discussion/5789/is-it-possible-to-define-a-measure-how-interesting-is-a-theorem).
Then, since nobody seemed to find the subject interesting, I started to reply to posts about infinity.. :-)

But the point of the discussion about infinity was more or less this one: "are ZFC axioms about infinity right?" and my answer was: "you cannot use a formal logic system to decide which kind of infinity exists". And I said you that I "don't like" ZFC because, for example, of Banach-Tarski paradox.

Let me try to explain this point: I am not saying that ZFC is wrong and Type Theory, or Coq, is right.
I am saying that the encoding of segments (and even surfaces and solids) as sets of points is not "natural", because you can build functions that have as input a set of definite measure and as output a set where measure is not definable: the transformations on sets and on measures are not part of the same category! Of course, you can say that this is because there really exist geometric objects that are not measurable, and it is really a feature of geometry, and not of ZFC.
Well, in that case you have to admit that there exist several different geometries, because there are sound logic systems based on type theory where all sets are measurable and lines are made of a countable set of "elementary" lines (integrals are always defined as series) (elementary lines have the property that their squared length is zero), and Banach-Tarski is false.
So, we can ask which one of the possible geometries is the "right" one. The problem is that they are only mathematical models. From my point of view, this is exactly the same thing as mathematical models for physics (or maybe you want to consider euclidean geometry as a model, but in that case non measurable sets surely do not exist): the best mathematical model is the one that encodes the greatest number of physical results using the smallest number of physical laws, and none of them is perfectly corresponding to physical reality anyway.

What's important about Wiles's proof is the ideas; not every last bit and byte of formal correctness.

This is something a lot of people don't get about math. It's the overarching ideas that people are researching. Sure, you can work out a formal proof if you like, but that's more like grunt work. The researchers are not interested.

Likewise, you are interested in a formal computer proof of BT, and that is not the point at all. The point is that the paradoxical decomposition of the free group on two letters induces a paradoxical decomposition of three space. That's the point. It's beautiful and strange. Formal proof in Coq? Ok, whatever floats your boat. But that is not the meaning of the theorem. The meaning is in the idea. — fishfry

I was looking for a formal proof of BT in ZF Set theory because the critical part of BT is the function that builds the non measurable sets (the one defined using of the axiom of choice). You are right that in most cases the formal logic is not necessary at all, but in this case the result of the theorem depends in a critical way on the actual encoding of a continuous space as a set of points. In fact, I am pretty convinced that It's possible to encode euclidean geometry in ZF Set theory in a way that is perfectly sensible for all results of euclidean geometry but makes BT false (I think I can do it in Coq, but surely you wouldn't like it.. :-) )

If you don't like the idea of "space as a set of points" I do understand that philosophical objection. But then you are objecting to a huge amount of modern math and physical science too. — fishfry

That is not true: the definition of measure is purely algebraic, and can be used with ANY definition of sets: it's the same thing as for calculus, derivatives, integrals, etc..

I'm not sure where you're coming from. If you don't like point sets, then you wouldn't like set theory. I can certainly see that. — fishfry

Well, I think you can easily guess: I studied electronic engineering (Coq can be used to proof the correctness of digital circuits), but I am working as a software developer. But I am even interested in mathematics and physics, and even philosophy, so I think I am not the "standard" kind of software developer.. :-)

I didn't say that I don't like point sets: I said that point sets are not a good model for 3-dimensional geometric objects, and I am not very original with this idea: in HOTT segments are not sets but 1-spaces. The word "sets" is defined as synonymous of 0-space (or "discrete" space).

But surely your objection then is not to BT, but to virtually all of modern mathematics and physics. Is that your viewpoint? How far does your rejection of using point sets to model mathematical ideas go? — fishfry

Point-set topology and algebraic topology are equivalent, and all modern mathematics and physics since Grothendieck (https://en.wikipedia.org/wiki/Alexander_Grothendieck) are based on category theory: as you just said, they really don't care much about foundations... :-)
Both string theory and loop quantum gravity (the two most trendy at the moment....) (https://en.wikipedia.org/wiki/Loop_quantum_gravity) make heavy use of algebraic topology: not only they don't care "of what are made" the objects of the theory, but they are even not clear if they are something geometric, or maybe can be interpreted as emergent structures coming from something even more fundamental. This is the point of view of category theory: don't describe how objects are made, but only how they relate with each-other.

By the way you don't need the power of the well-ordering theorem to change the order type of a set via bijection. Just take the natural numbers 0, 1, 2, 3, ... and reorder them to 1, 2, 3, ..., 0. So it's the usual order but n '<' 0 for every nonzero n, where '<' is the new "funny" order relation. The natural numbers in their usual order have no greatest element; but in the funny order they do. We've changed the order type with a simple bijection. You don't argue that this simple example should be banished from decent mathematics, do you? The funny order is the ordinal number ω+1ω+1, or omega plus one. Turing knew all about ordinals, he wrote his Ph.D. thesis on ordinal models of computation. Even constructivists believe in ordinals. — fishfry

I was speaking about changing the topology of a set: any open set (that has no minimum or maximum) can be transformed into a set with a minimum (lower bound), not open and not closed. If the isometries used in BT are continuous transformations, they should preserve the topology of the sets that are transformed. My guess is that the ones used in BT cannot be continuous on sets that are not discrete (that is one of the things that I wanted to understand from the formal proof..). In other words, I think that to make that transformation you have to destroy the topological structure of the object (but I am actually not sure about this). If this wasn't possible (and, as I understand, it's not possible without axiom of choice) I think BT would be false.

It's can't be right or wrong any more than the game of chess can be right or wrong. BT is undeniably a theorem of ZFC. That's true even if you utterly reject ZFC. The novel Moby Dick is fiction, yet it is "true" within the novel that Ahab is the captain of the Pequod and not the cabin boy. Banach-Tarski is a valid derivation in ZFC regardless of whether you like ZFC as your math foundation. — fishfry

Absolutely, I agree.

Suppose I stipulate that ZFC is banned as the foundation of math.

Ok. Then Banach-Tarski is still a valid theorem of ZFC. So what is your objection to that? B-T is still fascinating and strange and its proof is surprisingly simple. One could enjoy it on its own terms without "believing" in it, whatever that means. I don't think the game of chess is "true," only that it's interesting and fun. Likewise ZFC. — fishfry

Yes, it's even more interesting because of the fact that it is an (apparent) paradox, and paradoxes are the most informative and interesting parts of mathematics.

AHA! Yes you are right. But these are RIGID MOTIONS. That is the point. We are not applying topological or continuous transformations in general, which can of course distort an object. — fishfry

Well, I have my doubts here. These are rigid motions on countable subsets of points, it means only on subsets with zero measure. I am quite sure that they cannot be continuous transformations on measurable subsets with non-zero measure. If you have a proof that they are, I am very interested in it ( even not formal :-) )

P.S. Algebraic definition of measure: see https://en.wikipedia.org/wiki/Sigma-algebra

The standard reals are the only model of the reals that are Cauchy complete.
The constructive reals are not complete — fishfry

I tried to google for "constructive real numbers are not complete", or something similar.
I found this, for example: https://users.dimi.uniud.it/~pietro.digianantonio/papers/copy_pdf/RealsAxioms.pdf ).

And I found this: https://www.encyclopediaofmath.org/index.php/Constructive_analysis

I think this is what you refer to by "constructive reals". Is it?
Can you give me a link where is written that they are not complete?

I am convinced that my definition of "constructivism" is not the same thing that your definition.

Well, here's a simple definition of what I mean by constructive logic:
=== A logic is called constructive if every time that you write "exists t" it means that you can compute the value of t. ===

I believe that you can define real numbers that are complete in a constructive logic. I think the example that I gave you using Coq is one of these. But I could be wrong: I am not completely sure about this.

On the other hand the other famous alternative model of the reals, the hyperreals of nonstandard analysis, are also not complete. Any non-Archimedean field (one that contains infinitesimals) is necessarily incomplete. — fishfry

I googled this: "non archimedean fields are not complete" and the first link that come out is this one:
https://math.stackexchange.com/questions/17687/example-of-a-complete-non-archimedean-ordered-field

Probably, as they say, "The devil is in the detail". I read several times in the past about Abraham Robinson's hyperreal numbers, and I believe that I read somewhere that non archimedean fields are not complete. So I believe that, under appropriate assumptions, this is true. But why is this a problem?

The constructive reals fail to be complete because there are too few of them. The hyperreals fail to be complete because there are too many of them. The standard reals are the Goldilocks model of the real numbers. Not too small and not too large. Just the right size to be complete. — fishfry

Hmmm... I understand what you mean:
- "constructive" reals are computable functions. Then there is a countable number of them.
- standard reals are the set of all convergent successions of rationals then their cardinality is aleph-1
- nonstandard reals are much more than this (not sure about cardinality), since for each standard real there is an entire real line of non-standard ones.

Well, here's how I see it:
- "constructive" reals (with my definition) can be put in one-to-one correspondence with standard reals, only with a different representation (but I don't know a proof of this) and do not correspond to computable functions. It is true that if you can write "Exists x such that ... " then you can compute that x, But for the most part of real numbers x there is no corresponding formula to describe them (and this is exactly the same thing that happens for non constructive reals).
- Robinson's nonstandard reals are more than the standard reals because you exclude induction principle as an axiom (so that "P(0)" and "P(n) -> P(n+1)" does not imply "forall n, P(n)"). But there are objects used in mathematics that are treated as if they were real numbers, but DO NOT have the right cardinality to be standard real numbers: for example the random variables used in statistics: https://en.wikipedia.org/wiki/Random_variable . So, they are more similar to nonstandard reals.
- The real numbers of smooth infinitesimal analysis are less then standard real numbers, and even the set of functions from reals to reals is countable: basically, every function from reals to reals is continuous and expandable as a Fourier series. And there are infinitesimals.
What for such a strange thing? Well, for example, they correspond exactly to what is needed for the wave-functions and linear operators of quantum mechanics: there are as many functions as real numbers, and a real numbers correspond to experiments (then, there are a numerable quantity of "real" numbers). And what's more important, a wave function contains a definite quantity of information, that is preserved by the laws of quantum mechanics.

So, from my point of view, there is not one "good" model of real numbers, at the same way as there is not one "good" model of geometric space.

[ END OF PART TWO :-) ]

* Cauchy completeness is a second order property. It's equivalent to the least upper bound property, which says that every nonempty set of reals that's bounded above has a least upper bound. It's second-order since it quantifies over subsets of reals and not just over the reals.

The second order theory of the reals is categorical. That means that every model of the reals that includes the least upper bound axiom is isomorphic to the standard reals. Up to isomorphism there is only one model of the standard reals; and it is the only model that is Cauchy complete. — fishfry

Yes, and this clarifies a lot o things about infinity:

"In first-order logic, only theories with a finite model can be categorical." (form https://en.wikipedia.org/wiki/Categorical_theory). ZFC is a first-order theory and it has no finite model (obviously), than it cannot be categorical. Ergo, you cannot use ZFC to decide the cardinality of real numbers: "if a first-order theory in a countable language is categorical in some uncountable cardinality, then it is categorical in all uncountable cardinalities." (from the same page of wikipedia).

Then, you can say, the problem is in the language: let's use a second or higher order language, and you can discover the "real" cardinality of real numbers.
Well, in my opinion this is only a way of "hiding" the problem: it is true that if you assume the induction principle as part of the rules of logic, you get a limit on the cardinality of possible models (the induction principle quantifies over all propositions, so it's not expressible in first-order logic), but this is exactly the same thing as adding an axiom (in second order logic) and not assuming the induction principle as a rule. Ultimately, the problem is that the induction principle is not provable by using a finite (recursively computable) model: it's not "physically" provable.
That's exactly the same situation as for the parallels postulate in euclidean geometry: you cannot prove it with a physical geometric construction (finite model), because it speaks about something that happens at the infinite, and the fact of being true or not depends on the physical model that you use: if computers that have an illimited amount of memory do not exist, or, equivalently, if infinite topological structures do not exist, then the induction principle is false, and infinitesimals are real!
So, the sentence "if you use uncomputable (non constructive) axioms in logic, you can decide the cardinality of real numbers", for me it sounds like "if you use euclidean geometry, you can prove the parallel postulate".

OMG am I three posts behind already? And you know me, I sometimes reply at length to every paragraph. I'm overwhelmed again. Just remembering back, my favorite thing that I said was about the ordinals. The ordinal numbers are very cool, so I hope you said something about them. I'm going to go read at least your first reply and maybe the other two and mull them over a while.

Even a committed constructivist would have to acknowledge these facts, and hold the standard real numbers as important at least as an abstraction.

* As a final point, I believe as far as I can tell that not every HOTT-er is a diehard constructivist. In some versions of HOTT there are axioms equivalent to Cauchy completeness and even the axiom of choice.

If I'm understanding correctly, one need not commit to constructivism in order to enjoy the benefits of HOTT and computer-assisted proof. — fishfry

HOTT is not a constructivist theory (with my definition of constructivism) because it uses a non computable axiom: the univalence axiom (https://ncatlab.org/nlab/show/univalence+axiom).

This was considered by Voevodsky as the main "problem" of the theory, and there are currently several attempts to buid a constructive version of HOTT. One of them is cubical type theory (https://ncatlab.org/nlab/show/cubical+type+theory), but I don't know anything about it.

[ THIS WAS THE LAST PART :-) ]

[ THIS WAS THE LAST PART :-) ] — Mephist

Ok! In the meantime I just read through your first reply and I believe I can respond concisely and beneficially to it. Let me get to that. It might take me a day, or basically five minutes after putting it off for a day. But when I wait a day the five minutes worth is generally better. So let me work on reply #1 and read through the others.

I do think it's very cool that you learned Coq in EE. I had no idea! My background is that I learned set theory-based math back in the day, but my education did include introductory category theory as part of grad level algebra. In fact it is one of the high-water marks of my mathematical career that I totally grok the definition of the tensor product of modules as a universal property. I get a lot of mileage out of that one example!

I spent my professional career as a working software engineer and programmer. Along the way I was on Usenet in 1995 and started reading John Baez's amazing This Week's Finds in Mathematical Physics, which was essentially the world's first math blog. I was astonished to see that "n-categories" were being used to do loop quantum gravity. When I was in school categories were only for mathematicians, there were no applications yet. Now it's all over physics and computer science and biology and who knows what else.

I've followed all this at least via Baez over the years, and now that I've recently been reviewing and learning some more category theory, I am starting to get a vague understanding of what an n-category might be. And along the way of course I watched Vovoedsky's videos and vaguely kept up with HOTT at least at a buzzword level. It helps a lot that I already knew what a homotopy is from algebraic topology back in the day. So I get the thing about paths and paths between paths.

I think we have a good meeting of backgrounds coming from totally different directions. Now I'll go see what I can do with the reply queue.

I wonder what real infinity is really like. Infinite space, infinite speed, Infinite time, infinite heat, Infinite energy, Infinite number of something, and so on.
Because to me it seems infinity is not impossible. It just doesn't manifest in this world apparently, if one is to fully trust modern science.

In physics infinite is a simplification of the measure of an object, when the real measure is big enough to be ignored. So, for example, the electromagnetic field emitted by an antenna is the superposition of an infinite number of infinitely big spherical waves. We know that this is not true (this is only an approximation), but the approximation is essential to understand the symmetries of the real field.

The same is true for geometry: Archimedes discovered that you can calculate the circumference of the circle (knowing it's ray) if you consider it as a polygon with a very big number of sides: but to describe the symmetries of the circle you cannot treat it as if it was a polygon: you have to treat it as an "infinite" polygon.

Actually, even flat geometric figures do not exist in reality, because everything in nature is 3-dimensional, and it's obvious that considering one of the dimensions to be of measure 0 is only an approximation. So, in reality, not a big deal...

The problem with infinity started to be disturbing with calculus: you need a single measure (a number) that is approximated to zero in one place of a formula an not approximated (treated as finite number) in another place: for example if you take a very big number of very little segments that form a circle, it's clear that their sum is finite (the length of the circle), but if you build a little square on top of every little segment, you get a very thin ring whose area is approximated to zero. At the end, a rational explanation of this fact was found: you have to split at the same time in all dimensions, so that at all times you get only finite objects. This is a logically coherent explanation, only that if you have a lot of dimensions to consider at the same time, you get very complex formulas because it contains a lot of terms of the "wrong" dimensionality (for example you have to sum areas with lengths), that you know you could throw away (and in reality everybody with some experience in calculus throws them away in the calculations), but to be "logically coherent" with the underlying logic explanation of limits you "pretend" to have included them in the calculations.

But the "elimination" of infinity from mathematics started to become really complicated when Cantor discovered that something similar happens with infinitely big discrete objects (instead of infinitely small continuous objects): natural numbers are not enough to enumerate all discrete sets. In fact, there is no way to enumerate the set that is made of all possible tuples of natural numbers (pairs, triples, quadruples, etc..). So, the infinite of all tuples of numbers is more infinite then the infinite of all numbers, and in the same way you can build infinitely many infinites each one bigger than the previous one.

Now, it's clear that you can't neither count the uncountable discrete sets nor measure the infinitesimally small measures, but nevertheless, these imaginary infinte models have very interesting symmetries, that happen to correspond with a surprising accuracy to the symmetries that are present everywhere in nature. Without infinites, there are no symmetries and everything is a big mess (it's something like trying to discover the laws of Euclidean geometry using only polygons).

So, nobody really knows if infinites exist in nature or what are they really like, but they are essential in mathematics to discover very elegant models that often correspond to laws of nature, and I think that the idea that mathematics should work only using finite numbers because infinites don't really exist has been abandoned forever.

OMG my mentions are really piling up. What actually happens is that every time I write anything on the politics forums the replies depress me terribly and I have to stay away for days. I should know better. Back to math.

First of all, the point about formal systems. I completely agree that the formal proof is not the essential part of a theorem about geometry! I'll tell you more: I am pretty convinced that the formal proof alone does not contain the essential information necessary to "understand" the theorem, and I started to write on this forum because I was looking for somebody that has some results/ideas on this point. Please take a look at my last post on the discussion that I opened about two months ago: "Is it possible to define a measure how 'interesting' is a theorem?" (https://thephilosophyforum.com/discussion/5789/is-it-possible-to-define-a-measure-how-interesting-is-a-theorem).
Then, since nobody seemed to find the subject interesting, I started to reply to posts about infinity.. :-) — Mephist

I didn't read that thread because I thought the answer was trivial. You can measure citations of a paper, and that is commonly done. It works the same way as Google's page rank algorithm. Alternatively, it's unanswerable, because sometimes it takes decades or even centuries for the value of a mathematical insight to become apparent. But I'll glance at that thread if you like, once I catch up with my mentions. Which never happens.

But the point of the discussion about infinity was more or less this one: "are ZFC axioms about infinity right?" and my answer was: "you cannot use a formal logic system to decide which kind of infinity exists". And I said you that I "don't like" ZFC because, for example, of Banach-Tarski paradox. — Mephist

Well of course no axiomatic foundation for math can be right. People did math for thousands of years without any foundation at all, and now we've got several. But I would draw a line in the sand here and say that set theory has been extraordinarily successful as a theory of infinity, and I don't know that HOTT or Category theory are any improvement at all.

Of course no foundation can be "right" about infinity until the physicists discover actual infinity in the universe and report back to us. Just as we didn't know whether Euclidean or non-Euclidean geometry was right until Einstein's great breakthrough.

Regarding B-T, surely it's not right about the world (unless it is -- work for the physicists again). But as a theorem of ZFC, it's as right as a legal position in chess. Which is to say that it's the endpoint of a legal sequence of moves in a formal game.

Let me try to explain this point: I am not saying that ZFC is wrong and Type Theory, or Coq, is right. — Mephist

That's good, because the claim is meaningless. There is no right or wrong about it. Only useful or not, beautiful or not, interesting or not, fashionable this century as opposed to last.

I am saying that the encoding of segments (and even surfaces and solids) as sets of points is not "natural", — Mephist

There was a poster here a while back who gave me some great insights along these lines, before becoming so insufferably rude that I could no longer interact with him. I learned that Charles Sanders Peirce noted that the set-theoretic continuum can't possibly be the right model of a continuum, because a continuum must have the property that every part of it is the same as the whole; and a set, being decomposable into the union of its singleton points, fails this test.

If that's what you mean, I take your point. But knowing what's the "right" model of the continuum is beyond my own personal pay grade. I know that Weyl and Brouwer and others had many deep thoughts along these lines. I know little of these matters.

What I do know is that the set-theoretic continuum, having won the 20th century, underpins all modern physical theory. If one seeks to overthrow that foundation, one has much work to do.

because you can build functions that have as input a set of definite measure and as output a set where measure is not definable: the transformations on sets and on measures are not part of the same category! Of course, you can say that this is because there really exist geometric objects that are not measurable, and it is really a feature of geometry, and not of ZFC. — Mephist

If we accept the point-set foundation, then it's reasonable that not every point-set is measurable. After all, there are some wild point-sets. If you reject point-sets, then I guess not. But nonmeasurable sets in ZFC depend on the axiom of choice, and perhaps that's what you object to. It's AC that gives us sets whose only property is existence, with no clue as to how to construct them or identify their elements.

Well, in that case you have to admit that there exist several different geometries, — Mephist

Well yeah, but the Euclidean/non-Euclidean example gives us a good historical datapoint. There are lots of geometries but only one "true geometry" of the universe. But I'm not interested much in applications. The physicists can do their thing. I'll wear my formalist hat and steer cleer of ontological issues.

because there are sound logic systems based on type theory where all sets are measurable and lines are made of a countable set of "elementary" lines (integrals are always defined as series) (elementary lines have the property that their squared length is zero), and Banach-Tarski is false. — Mephist

I'll take your word for that. Are you talking about SIA? What of it? There are variations of chess too. It doesn't bother me.

But why are you hung up on Banach-Tarski? If you don't like point-sets, your objecions to standard math would be much wider than that.

So, we can ask which one of the possible geometries is the "right" one. — Mephist

As meaningless as the question of which variant of chess is the right one. Or whether in some fan fiction, Ahab is the cabin boy and not the captain of the Pequod, and whether that's right or wrong.

What do you mean by right one? Right as in best foundation for math? Or right as in true about the actual world? I don't share your focus on trying to figure out what's right about things that you and I will never be able to know, unless the next Einstein hurries up and gets born.

The problem is that they are only mathematical models. From my point of view, this is exactly the same thing as mathematical models for physics (or maybe you want to consider euclidean geometry as a model, but in that case non measurable sets surely do not exist): the best mathematical model is the one that encodes the greatest number of physical results using the smallest number of physical laws, and none of them is perfectly corresponding to physical reality anyway. — Mephist

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.

I was looking for a formal proof of BT in ZF Set theory — Mephist

There could never be such. ZFC is necessary.

because the critical part of BT is the function that builds the non measurable sets (the one defined using of the axiom of choice). — Mephist

Right. So why look for a proof in ZF that could never exist?

You are right that in most cases the formal logic is not necessary at all, but in this case the result of the theorem depends in a critical way on the actual encoding of a continuous space as a set of points. — Mephist

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. I don't understand why you regard B-T as uniquely interesting in the context of completely re-founding math on non point-set principles.

In fact, I am pretty convinced that It's possible to encode euclidean geometry in ZF Set theory in a way that is perfectly sensible for all results of euclidean geometry but makes BT false (I think I can do it in Coq, but surely you wouldn't like it.. :-) ) — Mephist

Why wouldn't I like it? Why would I even care? You seem to be tilting at windmills that I'm not defending. All I've ever said about set theory is that it won the 20th century and that Planck noted that science progresses one funeral at a time. Surely that shows my open-mindedness about historically contingent trends in foundations.

And as I already pointed out, if set theory is no longer required to be foundational, it becomes interesting for its own sake. It makes no difference to practitioners of set theory whether it's foundational or not.

That is not true: the definition of measure is purely algebraic, and can be used with ANY definition of sets: it's the same thing as for calculus, derivatives, integrals, etc.. — Mephist

I don't know what you mean but reading ahead I think I do so let's defer this for a moment ...

Well, I think you can easily guess: I studied electronic engineering (Coq can be used to proof the correctness of digital circuits), but I am working as a software developer. But I am even interested in mathematics and physics, and even philosophy, so I think I am not the "standard" kind of software developer.. :-) — Mephist

Well, engineers definitely have a pragmatic view of math. And one of my ongoing theses is that there are a lot of people studying computer science these days who thirty years ago would have studied math. So the mathematical point of view is somewhat lost among many people these days. But when you said that the purpose of a math foundation is to be able to found physics, that's just wrong. It's not how mathematicians view it at all.

I didn't say that I don't like point sets: I said that point sets are not a good model for 3-dimensional geometric objects, — Mephist

Ok. I can't argue the point but even if I could I don't have much reason to.

and I am not very original with this idea: in HOTT segments are not sets but 1-spaces. The word "sets" is defined as synonymous of 0-space (or "discrete" space). — Mephist

Ok. I wasn't aware that HOTT had gotten to the point of replacing differential geometry in general relativity, nor functional analysis in quantum physics. Are you making those claims? If so I am not sure I believe you. I watch a lot of physics videos these days and they're all differential geometry and functional analysis. The Schrödinger equation is functional analysis, not homotopy type theory. I think you're making claims that are more aspirational than true of the current state of the art.

Point-set topology and algebraic topology are equivalent, and all modern mathematics and physics since Grothendieck (https://en.wikipedia.org/wiki/Alexander_Grothendieck) are based on category theory: as you just said, they really don't care much about foundations... :-) — Mephist

Well yes and no. Analysis hasn't been categorized much. But physics? Again I think this is an aspirational claim. Loop quantum gravity uses n-categories but as far as I know relativity and quantum theory use classical 20th century math.

Both string theory and loop quantum gravity (the two most trendy at the moment....) (https://en.wikipedia.org/wiki/Loop_quantum_gravity) make heavy use of algebraic topology: not only they don't care "of what are made" the objects of the theory, but they are even not clear if they are something geometric, or maybe can be interpreted as emergent structures coming from something even more fundamental. This is the point of view of category theory: don't describe how objects are made, but only how they relate with each-other. — Mephist

Yes ok but LQG is not the standard theory yet. You're being aspirational again.

I was speaking about changing the topology of a set: any open set (that has no minimum or maximum) can be transformed into a set with a minimum (lower bound), not open and not closed. — Mephist

You are misapplying the well-ordering theorem. Bijections can radically change the order properties of a set. And the well-ordering theorme is equivalen to the axiom of choice so what of it? Reject one, reject the other. Take it up with Zermelo.

If the isometries used in BT are continuous transformations, they should preserve the topology of the sets that are transformed. — Mephist

Isometries preserve measure. They're rigid motions in space.

My guess is that the ones used in BT cannot be continuous on sets that are not discrete (that is one of the things that I wanted to understand from the formal proof..). — Mephist

I'm not sure exactly what you mean by continuous on sets that aren't discrete. All isometries are continuous and measure preserving (on sets that have a defined measure), period.

In other words, I think that to make that transformation you have to destroy the topological structure of the object (but I am actually not sure about this). — Mephist

I don't think so. Isometries are continuous since they preserve distances, and they preserve measure.

If this wasn't possible (and, as I understand, it's not possible without axiom of choice) I think BT would be false. — Mephist

Isometries aren't mysterious, they're rigid motions of space. Flips, rotations, translations. Clearly continuous, measure preserving, "shape-preserving" if you like. If you translate a triangle it's still a triangle. This is not mysterious nor does it require any esoteric philosophical assumptions.

— Mephist

Yes, it's even more interesting because of the fact that it is an (apparent) paradox, and paradoxes are the most informative and interesting parts of mathematics. — Mephist

It's a veridical paradox, meaning that it is NOT actually a contradiction, it merely violates our intuition. It should be named the Banach-Tarski theorem, since that's what it is. Now if you want to argue from that that the axiom of choice should be rejected, or points should be rejected, or sets should be rejected, that's fine. But it doesn't alter the fact that B-T is a theorem of ZFC, and moreover, not an extremely difficult one.

And as I mentioned earlier, it rests on the paradoxical decomposition of the free group on two letters, which at some point I should talk about, because this is a very strange paradox that has nothing at all to do with points or the axiom of choice or anything else questionable. It's very very simple and natural.

Well, I have my doubts here. These are rigid motions on countable subsets of points, it means only on subsets with zero measure. — Mephist

No not so. An isometry is a rigid motion on countable and uncountable sets. If I take the unit square and translate it 3 units to the right and 3 units up, the shape and measure are preserved. All measures are preserved.

I think you should open up a separate thread on Banach-Tarski so we could talk about these issues without all the philosophical baggage. You are misunderstanding a lot of basic issues. If you have a point set of any cardinality and measure, an isometry preserves its cardinality and measure. And shape, even though that's not a technical definition.

I am quite sure that they cannot be continuous transformations on measurable subsets with non-zero measure. — Mephist

You're simply wrong on this technical point. You should open a separate thread on B-T because we can't walk through that proof while you're claiming physics is based on HOTT and that mathematicians have point sets wrong. These are very different issues.

Regarding B-T you are misinformed on the basic math, on issues that are very clear and simple, and that we should discuss separately.

If you have a proof that they are, I am very interested in it ( even not formal :-) ) — Mephist

That a reflection, rotation, and translation are continuous? A freshman calculus student could work out those proofs. Measure preserving? A little trickier but not difficult.

Come on. Are you doubting that a translation is continuous? A reflection? A rotation? Why are you making these claims whose disproof is so elementary? I don't follow your logic here. Don't mean to be piling on, but after all this heavy-duty category theory and philosophy you are missing some very elementary freshman calculus.

You have a set of points which you can think of as vectors in the plane or space. You add a constant vector to each point. The resulting point set has the same shape and measure, and the transformation is continuous. I can not accept that this is not obvious to an engineering major.

P.S. Algebraic definition of measure: see https://en.wikipedia.org/wiki/Sigma-algebra — Mephist

Yes ok what of it? From the basic axioms of measure one proves the existence of a nonmeasurable set. And from that, Banach-Tarski.

I gather you are trying to make the claim that measure theory is "algebraic." That's a point of semantics. From countable additivity plus the axiom of choice, the existence of a nonmeasurable set falls out. Have you seen the proof? It's not difficult. Well it's not difficult after one's been through it a few times. Like everything else. But it's a very cool proof. It's a paradigm of all axiom of choice proofs.

But the bottom line, and this has been a long post so here is the tl;dr:

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.

Ok one post down, so many more to go ... thanks for reading.

ps -- Here is the proof that an isometry preserve a Hausdorff measure, which the measure on Euclidean 3-space is an example of. In the general case it's not true but that case doesn't concern us. https://math.stackexchange.com/questions/695492/isometry-vs-measure-preserving

pps -- Simpler theorem on point. Isometries preserve Lebesgue measure of Euclidean space.

https://math.stackexchange.com/questions/242837/lebesgue-measure-is-invariant-under-isometry

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.

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. — Mephist

Well I'm three of your posts behind I think so I'm planning to get to them soon.

But I'm not sure what you mean that " I am convinced that what I wrote is correct, so I am a little upset to not being able to convince you ...' About what? There are two things going on:

1) The business about ZFC and point-sets being "wrong" in some way; and

2) Your misunderstanding of isometries, which preserve measure of all measurable sets.

I don't know which one you want to talk about. I don't know what you think you didn't convince me of. I see foundations as historically contingent and not all that important to what working mathematicians do anyway. And you certainly didn't convince me that foundations are for the purpose of modeling physics, that's not mathematically true at all, it's something only a physicists or an engineer would believe :-)

So maybe you can concisely tell me exactly what thesis you are trying to convince me of. No, formal proofs would be the wrong way to go without a simple one or two sentence description of the thesis being put forth.

But if I understood you, you believe that the rightness of a foundation can be measured by how well it lets us model physics. And that's 100% opposed to what I think foundations are. Math is not held to the standard of physics, hasn't been since Riemann.

So just tell me as clearly as you can what it is you're trying to convince me of. That will be helpful to me because you covered a lot of different topics in the post I replied to and I spent a lot of time trying to explain that rigid motions are continuous and preserve measure, and if you don't care about those things we shouldn't lengthen our posts with them.

I think this is what you refer to by "constructive reals". Is it?
Can you give me a link where is written that they are not complete? — Mephist

I have a lot more to say about this second of your posts (of the four that I'm working through) but I wanted to just catch this up first because I already proved this earlier but with so much verbiage back and forth it was easy to miss.

You know Chaitin's Omega? Very cool number, because it's actually a specific example of a noncomputable real number, or rather any one of a specific class of noncomputable reals. We can define it because it's a definable real even though it's not computable. It's not computable because if it were, it would solve the Halting problem, which Turing showed we can't do.

Now, consider a sequence whose n-th term is simply the n-th truncation of Omega's decimal expression. In other words if we take pi, we can form the sequence 3, 3.1, 3.14, 3.141, ... This is a Cauchy sequence that converges to pi. This is an example of a Cauchy sequence of rationals that fails to converge to a rational, showing that the rational numbers are not Cauchy complete.

Likewise we can form the Cauchy sequence of rational numbers that are the n-th truncations of the decimal digits of Omega. This is a Cauchy sequence of computable numbers, because it's easy to see that a rational number is computable. The algorithm that cranks out the decimal digits is just grade school long division.

But this is a Cauchy sequence of computable numbers that fails to converge to a computable number! So the computable real numbers are not Cauchy-complete. QED.

Now the big problem IMO with the computable reals is that you can do this for every noncomputable real. Every noncomputable real represents the limit of a sequence of rational hence computable numbers that fail to converge to a computable real number. The computable real line has only countably many points and uncountably many holes. It's the swiss cheese of number lines and a terrible model of the ancient idea of the continuum. I confess that I do not understand why Brouwer and Weyl were not greatly troubled by this.

The other thing I wanted to mention about your post is that you found an example of a non-Archimedean ordered field that's Cauchy complete. I stand corrected!! I'm apparently wrong on this point. But I thought otherwise and now I have to try to understand why I've seen a proof that a non-Archimedean field can't be complete. This is a mystery but thank you for digging up this example, I have to study it.

Either way it's not too critical. In fact the Robinson hyperrreals are NOT Cauchy-complete so my Goldilocks remark still stands even if I am wrong about the general case.

You know Chaitin's Omega? Very cool number, because it's actually a specific example of a noncomputable real number, or rather any one of a specific class of noncomputable reals. We can define it because it's a definable real even though it's not computable. It's not computable because if it were, it would solve the Halting problem, which Turing showed we can't do. — fishfry

I think in that in an ideal mathematical language, Chaitin's Omega wouldn't be stateable. To say 'Omega is definable but non-computable' is surely not a statement about a number, but a statement about the syntactical inadequacy of our mathematical language for permitting the expression of Omega.

For if a sentence is understood to express logical impossibility, then it cannot be an empirically meaningful proposition. It can only serve as a rule of grammar for forbidding the syntactical construction of certain sentences in order to preserve the semantic consistency of the respective language.

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.

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.

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?

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.

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.

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? — Mephist

A point has length zero. How many length zero things can you fit on a line segment length one?

1 / 0 = UNDEFINED

Anything with length zero does not exist, so its like asking how many non-existing things fit within an existing thing. An answer of UNDEFINED seems right.

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 was given the impression in school that a line segment contains an actual infinity of points. The problem seems to me the mathematical definition of a point is non-sensical. Anything with all dimensions having length zero cannot exist. So bearing in mind that definition of a point, an undefined value for the number of points on a line makes sense - undefined and actual infinity are one and the same IMO.

If we instead use a more sensible definition of a point, say length 0.1, then we can reason about it - we get 10 points on a line segment length 1.

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 guess so, but it comes back to the problem of people taking ideas from mathematics and applying them to the real world. Idealisations are just that; they are not real world entities. A mathematical point, a plane, actual infinity cannot and do not exist in the real world.Yet we have cosmologists that are assuming time and/or space is actually infinite - idealising the real world and misleading other people in the process.

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..

I agree maths works very well for modelling reality in most instances. Actual infinity is not one of those instances though. I think perhaps the problem could be that actual infinity is not even a sound mathematical idealisation? Maths mirrors nature; both should be constrained to the logically sound. Presumably that is why maths models nature well. But actual infinity is illogical (Hilbert's Hotel etc...) and so is not found in nature, maybe it should not be found in maths either?

The maths that physicists use (calculus mainly) should only need depend upon the concept of potential infinity; actual infinity should not be needed anywhere in the physical sciences.

Maths mirrors nature; both should be constrained to the logically sound. — Devans99

Are you thinking that maths and nature are the same thing? Question: the word itself, "infinity," is well-defined. From it's existence, what do you infer?

I mean that nothing illogical exists in nature so if maths is to mirror nature, then nothing illogical should exist in maths either.

There are differing definitions of the actually infinite, one is: 'limitless or endless in space, extent, or size; impossible to measure or calculate'. The definition itself essentially precludes its existence in maths.

There are lots of reasons why actual infinity is illogical. Looking at just one - the division operation on transfinite numbers:

We can imagine the division operation as compressing space: for example division by 2 would compress the numbers on the real number line by a factor of 2: 10 would become 5, 4 would become 2 and so on. The convention is that ∞ / (any number) = ∞, so division by infinity does not decrease the 'overall' size of the real number line - the endpoints at 0 and ∞ are unaffected, but every finite number on the real number line must move closer together - this is clearly illogical from a physical standpoint.

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

The continuum hypothesis or its negation can be added it set theory without making it inconsistent. So that implies something false can be added to set theory without changing its consistency. Consistency and logical correctness do not seem to be the the same thing.

I think that something can be consistent and illogical at the same time. 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. That sums up my feelings about actual infinity in set theory; maybe the axioms are such that its consistent (or appears to be consistent)... but its not logically correct.

I mean that nothing illogical exists in nature so if maths is to mirror nature, then nothing illogical should exist in maths either. — Devans99

What you mean is that nothing self-contradictory exists in nature, nor in maths except as defined in for a purpose. Nor is the mirror analogy accurate. Now, perhaps you will answer. Does it not trouble you that mathematicians understand and use infinities appropriately where applicable? And that you alone seem to feel they're just plain wrong? (Lots of people use the ideas inappropriately where inapplicable, evidencing that they never understood the concepts in the first place.) That is, the word itself alone ought to get you to reconsider your thinking. Btw, what in your understanding does it mean?