If you believe there is only one infinity (like I do) — Devans99
Now, if for transfinite numbers the neutral element for addition is nor unique, you can't define subtraction as the inverse of addition, simply because addition is not invertible! — Mephist
Sorry to disappoint you, but (as I just wrote in the previous post), I believe that at least infinitesimal objects do exist in nature in some sense, but you cannot decide if they exist or not using mathematics. — Mephist
So, at least for what I know, if you want calculus to be part of mathematics you have to allow the existence of actually infinite objects! — Mephist
I don't see why calculus cannot be defined purely in terms of potential infinity. A limit should approach but never reach actual infinity: — Devans99
How do you define the function sin(x) if you can't use infinite expressions? — Mephist
As usual, a citation from the old good wikipedia can come to the rescue :-)
"Set theory (which is expressed in a countable language), if it is consistent, has a countable model; this is known as Skolem's paradox, — Mephist
This of course doesn't mean that uncountable sets "do not exist", but only that you cannot use a finitary
first order logic theory to prove that they exist. — Mephist
So, you could even say that "every mathematical object is a string of characters", — Mephist
I don't believe this is true. ZF is a first-order theory with a countably infinite language that easily proves uncountable sets exist. See Cantor's theorem, as simple a proof as one can imagine for a fact so profound. — fishfry
No I don't believe so. This is confusing syntax with semantics. A formal theory consists of finite-length strings of symbols. But models of those theories are not strings of symbols. They're sets, often quite large ones. — fishfry
For example, with π, it's irrational so it can never be fully defined - it's impossible to know all the digits, so saying an expression tends to π rather than is equal to π is actually more accurate. We can never know π exactly. — Devans99
OK, probably this is not the conventional point of view in mathematics, but I'll try to explain my point of view: — Mephist
In ZF Set theory you have the "axiom of infinity" that says ( in a simplified form ):
There exists a set A such that:
-- ∅∈A,
-- for every x∈A, the set (x∪{x}) ∈ A.
This, from my point of view, is a complicated definition for a recursively defined structure that is equivalent to Peano's natural numbers:
You can build ∅ (equivalent 0), ∅∪{∅} (equivalent to S0), ∅∪{∅}∪{∅∪{∅}} (equivalent to SS0), etc... — Mephist
Then, first order logic postulates the existence of functions.
Basically, Cantor's theorem proves that, for every set A, the function A -> (A -> Bool) is always bigger than A (in the usual sense of no one-to-one correspondence). — Mephist
Then, since (A -> Bool) is itself a set, you can build an infinite chain of sets of the form (((A -> Bool) -> Bool) -> Bool) -> ...
So, from the infinite set you can build an infinite hierarchy of infinites. — Mephist
The crucial point here to decide the cardinality of "A -> (A -> Bool)", is what you take as a model for functions. — Mephist
If functions are only recursive functions (what I can evaluate using a decidable set of rules applied to the symbols of the language), I can never build anything that has non-numerable cardinality. — Mephist
In this case, it is
true that for every set you can find a bigger set, but their cardinality will be numerable: at the same way as it is true that for every integer, you can always find a bigger integer. — Mephist
If instead you define functions in the usual way as "sets of couples", then there are 2^|A| possible functions of type A -> Bool, and there exists a non-numerable set of sets. But, in any way, inside your language you are able to describe only an enumerable set of them. — Mephist
(https://en.wikipedia.org/wiki/Skolem%27s_paradox):
"From an interpretation of the model into our conventional notions of these sets, this means that although u maps to an uncountable set, there are many elements in our intuitive notion of u that don't have a corresponding element in the model. The model, however, is consistent, because the absence of these elements cannot be observed through first-order logic" — Mephist
Since both models for functions are consistent, what's the reason to take the standard interpretation as the "true" one? — Mephist
No I don't believe so. This is confusing syntax with semantics. A formal theory consists of finite-length strings of symbols. But models of those theories are not strings of symbols. They're sets, often quite large ones.
— fishfry
See Herbrand interpretation: https://en.wikipedia.org/wiki/Herbrand_interpretation. — Mephist
The demonstration of Godel's incompleteness theorem is using a similar technique to map natural numbers on the syntactic structures of the language and properties of arithmetic operations on syntactical rules of logic. — Mephist
What the axiom of infinity says is that {0, 1, 2, 3, ...} is a set, not just a collection. That's a much stronger statement. Without the axiom of infinity we still have PA and everything that we can do with it. But we don't have the powerset of the natural numbers nor do we have an easy way to get the theory of the real numbers off the ground. — fishfry
But Cantor doesn't prove that P(A) is bigger than A. He proves that there is no surjection from A to P(A); then we DEFINE "bigger" to mean there's no surjection. — fishfry
Yes. But then you can't get the theory of the real numbers off the ground and the intermediate value theorem is false. The constructivists counter: The IVT becomes true again we only consider computable functions. — fishfry
That's reassuring :-)Yes agreed. We agree on everything — fishfry
I just think the world of the full powerset of N is richer and more interesting than the computable powerset. That's an aesthetic judgment. And it's more useful. That's a pragmatic judgment. — fishfry
Nobody has yet succeeded in developing a computable or constructive theory of physics. People are working on it. Perhaps we'll need another few decades to get more insight into this question. — fishfry
I read that article and didn't fully understand it or the point you're making — fishfry
I agree. And I think Godel himself would agree: he built this model to confute Hilbert's idea that there is no truth except formal logic.Math is more than Gödel numbering — fishfry
I think Godel's idea was something similar to what I tried to express in (https://thephilosophyforum.com/discussion/5792/is-mathematics-discovered-or-invented): there exists a meaning of truth based on a physical world that is more "fundamental" than the physical world that we observe.Gödel himself was a Platonist. I found that surprising when I first learned it. He believed there is mathematical truth "out there" that's beyond the limitations of formal systems. — fishfry
Yes. But then you can't get the theory of the real numbers off the ground and the intermediate value theorem is false. The constructivists counter: The IVT becomes true again we only consider computable functions.
— fishfry
Sorry, I don't understand what you mean here: The constructivist (intuitionist) logic is only a "more general" logic than classical logic, since it has less axioms. As a result, it is valid for a bigger set of models: — Mephist
-- forall is a loop that stops returning false if it finds a false value, and it's value as proposition is false if it stops and true if it loops forever — Mephist
This tranlsates to the english: "however you choose to match elements of A with elements of B, there will always be an element of B that is not matched by any element of A"
I think this is a quite intuitive definition of the fact that B has at least one element more than A. — Mephist
Here's why IVT is false in constructive math. IVT, you will recall, says that if a function from the reals to the reals is continuous, and if it takes a negative value at one point x and a positive value at another point y, then it must be zero at some point between x and y.
That is if we have f(x) < 0 and f(y) > 0 then there exists p with x < p < y and f(p) = 0. This is intuitively correct about a continuous function f.
If you take the standard real line and omit all the noncomputable points, you get the computable real line. The computable real line is full of holes where the noncomputable reals used to be — fishfry
One thing I do know is that the axiom of choice implies LEM. To reject the axiom of choice involves throwing out quite a lot of modern math. — fishfry
You mentioned a lot of other interesting things that I'll try to get to later. One was about LEM and HOTT. I was not under the impression that HOTT is a constructivist theory. — fishfry
Yes of course, but this in my opinion is not really related to intuitionism.I'm sure Voevodsky believed in uncountable sets. — fishfry
A machine could verify Cantor's theorem. So I am not sure that HOTT and constructive math are the same. — fishfry
I'm not sure what that means. You can't iterate through a set unless it's well-ordered. And there are sets that are not well-ordered, unless you accept the axiom of choice, which implies LEM. How would you iterate through the real numbers, for example? Here's how I'd do it. First, well-order the reals. Second, use transfinite recursion. Those are two powerful principles of math not available to constructivists. I don't know how constructivists feel about transfinite recursion, but it applies to very large sets that constructivists can't possibly believe in.
But the "for all" operator can be applied to the reals without the need for such powerful machinery as the axiom of choice and transfinite recursion. You just say "for all reals" and you're good. That's much more powerful than iteration IMO. — fishfry
I can't agree that intuition is useful here. Intuitively, the even numbers adjoined with a single odd number are "larger" than the even numbers; and in fact this is confirmed by the proper subset relationship. But these two sets have the same cardinality. This is specifically a point of confusion for beginners. I reject naive intuition here and insist that "bigger" means injection but no surjection, end of story and no intuition allowed! Intuition is exactly what gets students into trouble when they first learn the math of infinity. — fishfry
Moreover if you reject the axiom of choice (necessary if you reject LEM) there are "amorphous" sets that have no sensible cardinality at all. Such sets defy anyone's intuition. — fishfry
First of all, let's look for a definition of "constructive mathematics", because I have the impression that we are not speaking about the same thing. — Mephist
There are many forms of constructivism.[1] These include the program of intuitionism founded by Brouwer, the finitism of Hilbert and Bernays, the constructive recursive mathematics of Shanin and Markov, and Bishop's program of constructive analysis. Constructivism also includes the study of constructive set theories such as CZF and the study of topos theory." — Mephist
Well, the constructivist theory that I know quite well is the "Calculus of Inductive Constructions", or CIC ("https://en.wikipedia.org/wiki/Calculus_of_constructions"), implemented in the Coq proof assistant (https://coq.inria.fr/).
This is a particular version of "Martin-Lof Type Theory" (https://en.wikipedia.org/wiki/Intuitionistic_type_theory) — Mephist
Here's a summary of the main properties of Coq's logic: https://github.com/coq/coq/wiki/The-Logic-of-Coq — Mephist
Basically, Coq is a programming language (let's cal this the "internal language" of the logic) based on dependently typed lambda calculus (https://en.wikipedia.org/wiki/Dependent_type) that allows only to build total functions: using this language it's impossible to define a function that does not terminate (then it's less powerful than the full untyped lambda calculus, or a Turing machine).
However, using the internal language you can operate on inductive (and co-inductive) data structures and on functions (the models about which you can speak about and on which you can operate using the internal language) that ARE NOT REQUIRED TO BE COMPUTABLE.
For example, you can say "let R be a field and let F be a function such that forall x:R, F(x)^2 = x; Let x be F(2)". You can represent for example real numbers as functions from natural numbers to the finite set {0...9 and comma} to make things simpler (the infinite decimal expansion of the number), and then you can prove that the algorithm that produces the digits of the square roots of two IS a real number that solves your equation. Of course "x" is not a recursive function (of course, it does not terminate if you execute it on all natural numbers! ), but to build it you only need a finitely defined algorithm.
In a similar way, you can say "Axiom excluded_middle: forall A:Prop, A \/ ~A." meaning: excluded_middle is a function that takes as input the prove of a proposition A and produces as output the prove of the proposition A \/ ~A. This function is not implementable in the internal language of Coq, but you can treat it as a pre-defined "external" function that you can call and use the result without knowing how it works (something like a function defined in an external library of a programming language).
The logic doesn't make sure that the function exists (and even it doesn't guarantee that i's consistent: the proof of consistency is related to the meta-theory of the internal language), but only says that if you have this function, you can use it. And the resulting logic is equivalent to classical higher order logic (not set-theory). — Mephist
The correspondence between set theory and the various versions of dependent type theory is rather complex:
See for example (https://mathoverflow.net/questions/69229/proof-strength-of-calculus-of-inductive-constructions):
"IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many "inaccessible cardinals" -- see Benjamin Werner's "Sets in Types, Types in Sets". (This is because of the presence of a universe hierarchy in the CIC." — Mephist
And this is a very good reference for intuitionistic type theory: https://plato.stanford.edu/entries/type-theory-intuitionistic/ — Mephist
I read that you can't define Cauchy or Dedekind real numbers in intuitionistic logic (without additional axioms), but you can use other definitions of "continuity": — Mephist
http://www.alternatievewiskunde.nl/QED/brouwer.htm
"Any function which is defined everywhere at an interval of real numbers is also continuous at the same interval. With other words: For real valued functions, being defined is very much the same as being continuous." — Mephist
and MY FAVOURITE ONE:
https://plato.stanford.edu/entries/continuity/#9 "Smooth Infinitesimal Analysis" — Mephist
What is your objection to this axiomatization of real numbers? — Mephist
One thing I do know is that the axiom of choice implies LEM. To reject the axiom of choice involves throwing out quite a lot of modern math.
— fishfry
Intuitionistic type theory implies a somewhat "weaker" version of the axiom of choice (the "good" part of it :-) ) — Mephist
[ ..going to continue next time! ] — Mephist
I know of Bishop's book and I even know a book where a physicist tried to do constructive physics. That's a project in its infancy but you constructivists will have to face the problem someday. Physics is founded on classical math, ie continuity and the real numbers as defined in set theory. — fishfry
I am grateful for your summary and I will try to work through it at some point. I have to confess I did not dive into this exposition but I'm glad you wrote it — fishfry
I am glad that you replied to my post, so I can explain in more detail my point of view — Mephist
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
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
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
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
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
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
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 believe that the most popular explanation of this fact among physicists today is that physical space is in fact discrete. — Mephist
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
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 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
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
[ that's enough for today.. :-) ]
a day ago — Mephist
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
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 — fishfry
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? — fishfry
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. — fishfry
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. — fishfry
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 — fishfry
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 ..." — fishfry
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. — fishfry
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.