I am glad that you replied to my post, so I can explain in more detail my point of view — Mephist
Oh no now I am falling even further behind in my replies!
I don't believe that physics is founded on ZF Set theory, if that's what you mean by "classical math".
Physics is based on calculus (for the most part), that was created starting from XVII century (Newton's "principia" was published in 1687), at a time when logic wasn't even considered as part of mathematics. — Mephist
Yes but by the 19th century it became clear that the logical problems of calculus were becoming a problem and needed to be addressed. We needed to know exactly what was a real number and a continuous function in order to resolve the delicate convergence issues that were arising.
I agree of course that the physicists don't care and I didn't mean to imply that they do. But physics is based on the real numbers and mathematical analysis in general; and those things were discovered to need a foundation; and that foundation is currently set theory.
In fact, I believe that most of physicists don't even know the exact formulation of the axioms of ZF set theory, and that's because these axioms are never used in physics directly. — Mephist
Of course. In fact most working mathematicians couldn't state the axioms and don't use set theory directly! That's a fact. My point still stands. Once you get picky about which things converge and which things don't, a problem that arose in the infinite trigonometric series that arose out of 19th century physics, you need a foundation and set theory is it. Currently of course.
The thing that really matters is that you can use logic to prove that your results follow from the algebraic rules of calculus, differential geometry, group theory, etc... — Mephist
Sure, not disagreeing at all.
If this was true, the distinction between the various axiomatizations of real numbers would be irrelevant for physics. ZF set theory only happens to be the first axiomatization to be discovered. — Mephist
Perfectly well agreed. But we are not talking about whether Dedekind cuts or equivalence classes of Cauchy sequences are a better way to represent the real numbers. You are advocating
nonconstructive foundations. It's in that context that my remarks make sense. We can NOT currently (as far as I understand it) get modern physics off the ground using nonconstructive math. The 't' in the Schrödinger equation is taken to be a variable that ranges over the standard mathematical real numbers, noncomputables at all.
I am aware of only one book that attempts to get physics working on nonconstructive math. That's a tiny drop of water in an ocean that needs to be filled.
I will agree that synthetic differential geometry is some kind of counterexample to my claim but I don't know enough about it. But SDG is not the same as nonconstructive approaches, is it? I thought SDG is just a categorical approach to infinitesimals so it's more like a complementary idea to nonstandard analysis. Not something directly related to homotopy type theory or neo-intuitionism or whatever. But I could be all wrong about all this, I have very little to no actual knowledge.
But this is in fact not completely true. There are some physical results that are not the same in all axiomatizations. For example, the Banach-Tarski theorem. — Mephist
I would never call B-T a "physical" result. On the contrary it's only a technical result regarding the isometry group of Euclidean 3-space, which happens to contain a copy of the free group on two letters, which has a paradoxical decomposition. It has nothing to do with the real world. As far as we know, of course.
But if earlier you said that physics doesn't depend on set theory, then surely we can't apply the axiom of choice to regions of physical space!
If you believe that the physical space can't be split in peaces and then reassembled with double volume, you have to conclude that the real numbers' axiomatization of ZFC is not the right model for physical space. — Mephist
I've often raised this point myself. If anyone seriously believed it was, then we'd see physics postdocs applying for grants to count the number of points in the unit interval and thereby discover the truth of the continuum hypothesis. The fact that the ides is absurd shows how far ZF, let alone C, is from the real world.
I'm not claiming the world's based on set theory. I apologize if my earlier wording made it sound like I did.
I claim that our best physical theories are based on the real numbers and the theory of limiting processes that go under the name of mathematical analysis; and that our current formulation of analysis is in terms of set theory. I don't state this as a metaphysical point, only as a historically accurate one. I don't care if you want to replace one definition of the real numbers with another. I do care that there is as yet no fully worked out constructive theory of the real numbers that will support modern physics. That is my belief. Certainly I could be wrong.
A more "practical" example are Feynman's path integrals: they can be used to calculate physical quantities with extreme precision, if you don't take for real the result that derives from ZFC's axioms. In fact, from ZFC axioms you can derive that the result is "infinite". But if you take only some terms of your infinite (divergent) series, the result is experimentally correct with a very high accuracy! — Mephist
I've heard about renormalization and I am not aware of whether it's been mathematically formalized or not. I found a stackexchange thread that some that "some" version of QFT are mathematically sound and others not! This is all inside baseball in the physics biz.
https://physics.stackexchange.com/questions/86597/qft-as-a-rigorous-mathematical-theory
Regardless, I take renormalization as a modern example of Newton's great use of calculus to work out gravity, two hundred years before we had a logically rigorous foundation for calculus. Physics often leads math that way. That doesn't mean the math of renormalization won't be fully patched up someday in terms of ZFC or some future foundation. Maybe tomorrow morning someone will derive renormalization from homotopy type theory. If that happens I'll have to shut up about constructivism.
I believe that the most popular explanation of this fact among physicists today is that physical space is in fact discrete. — Mephist
Yes we are now back to the ancient question of atomism. Zeno. All that stuff. We are not going to solve it today. The Planck scale doesn't say the world's a discrete grid. It only says that our contemporary theories don't allow us to speculate below that scale. Maybe there are little thingies in there.
Personally I do not think there are Euclidean points. I don't regard the real numbers as a good model of continuity. I'm not making any metaphysical claims for math at all. But I am making historical claims that our best continent theories DO need an underlying Euclidean model.
[By Euclidean I don't mean the geometry, I mean the Cauchy completeness of n-space],
But there is no experimental evidence of this until now.
( The same thing happens with energy: if energy is continuous you get infinite results for black body radiation. With Plank's quantization you get the correct results ) — Mephist
I hope my Planck point was clear. I didn't deny the Planck scale. It's that my own personal understanding is that the Planck scale is that scale of space and time below which we
can't sensibly measure or calculate or speculate about. I'm agnostic on whether there's anything actually there.
But with physics you can assume nothing until you find experimental evidence, because nature has surprised us so many times! However, if I had to guess, discrete space (like pixels of a video game) is too "ugly" to be true: nature has shown to prefer "beautiful" mathematical structures. — Mephist
I think we're meeting in the middle. I don't think mathematical continuous space is quite the right model for the world, and you admit that neither is a discrete grid. Most likely it's something even stranger, yet to be discovered by a genius not yet born.
I think an interesting question is: is there an axiomatization of a continuous space (where you can take measures represented as real numbers) where Feynman integrals make sense and are convergent? I don't know, but I don't see a reason why this shouldn't be possible. — Mephist
Don't know enough about the subject, more stuff to read. But quantum physics is probably not something I'll be tackling in this lifetime. I do know a little functional analysis, enough to know what Hilbert space is. So if you tell me that an observable is a linear operator on some complex Hilbert space, I know what that means mathematically. Just not physically. And I'll probably never know.
I'll try to give you a simpler explanation: In logic you have propositions, terms and relations. Martin-Löf type theory ( and HOTT too ) reduces all these three concepts to only one: functions. That's basically the reason why it has a simple categorical model.
The functions that you consider in the theory are, exactly as for morphisms in category theory, not limited in any way. Now the question is: how is it possible to use and reason about functions that are not computable? Obviously, you can't "execute" the function on a given argument to check what's the result. Well, the "trick" is: lambda calculus! With lambda calculus you can "execute" a function by what's called "beta reduction". That means that you can transform and compose functions from one form to another (equivalent to the previous one) using very simple rules that are supposed to be respected by everything that can be called "function".
The whole point about constructivism is that you can assume existing for sure only the functions that you can effectively compute. All the others can enter in the theory only as premises of your deductions (no axioms!). And that is enough to prove all mathematical theorems that can be proved with classical logic, if you add the appropriate axioms corresponding to the "non computable" parts of classical logic. In this way you make clear the distinction between the computable and not computable parts of logic! — Mephist
I understand the words but not the ideas. I suspect it's the kind of thing where mere Wiki reading wouldn't help. I've heard of lambda calculus but don't know anything about it except that everyone thinks it's terribly important. I gave the Wiki a quick scan and they pointed out in their section on beta reduction that "The lambda calculus may be seen as an idealised version of a functional programming language ..."
Ok. But a functional programming language can't do anything a Turing machine can't, and in fact Turing proved that TMs are equivalent to the lambda calculus, and Turing machines can't crank out the digits of noncomputable numbers. So once again I'm up to my original brick wall of understanding. Or misunderstanding. I'm sure that if I grokked this subject I'd suddenly realize that I've been ignorant all these years, and that you can in fact do everything you need to do with mere computability.
I just don't see it yet.
[ that's enough for today.. :-) ]
a day ago — Mephist
Thank you much!
ps --
And that is enough to prove all mathematical theorems that can be proved with classical logic, if you add the appropriate axioms corresponding to the "non computable" parts of classical logic. — Mephist
If I could only understand this. You are saying that if I can prove a theorem at all, I can prove it using constructive methods, by adding certain axioms. This could be within my grasp. What are the axioms that make this work?
pps --
Ah this is that Curry-Howard business I bet. Programs are proofs. Fine, I believe that. A proof has to be computable, but the thing it's talking about need not be. But doesn't that mean something? Proofs aren't sufficient to know mathematical reality, Gödel showed that. Same with physics. Restricting our epistemology to what we can prove with axiomatic systems or computers is not sufficient to understand reality. That perhaps would be my working thesis.