Starter mathematicians might think everything is math.
Senior mathematicians lose their sleep whenever they think about what our math is missing and they don’t know what it is yet
Do we have ways of computing orders of infinity higher than ℵ₀?
Crap. Markdown isn’t markdowning. Fixed with unicode.
Symbolically, sure, but then you’re not dealing with infinities you’re just representing them.
It’s a meme it’s playing fast and loose with things but the general gist is that mathematics, to this day, doesn’t really care about Gödel/Church/Turing, incompleteness, the halting problem, whatever angle you want to look at it from. Formalists lost the war and they simply went on doing maths as if nothing had happened, as if a system could be simultaneously complete and consistent. There’s people out there preaching to the unenlightened masses but it’s an uphill battle.
Math went on because it doesn’t matter. Nobody cares about incompleteness. If you can prove ZFC is inconsistent, do it and we’ll all move to a new system and most of us wouldn’t even notice (since nobody references the axioms outside of set theorists and logicians anyway). If you can prove it’s incomplete, do it and nobody will care since the culprit will be an arcane theorem far outside the realm of non-logic fields of math.
You wouldn’t even notice if some proof is wrong because it relies on an inconsistency that’s the issue. And that’s before you didn’t notice because noone builds anything on axioms but instead uses fragile foundations made of intuition, hand-waving, and mass psychology.
Incomplete is fine that’s exactly what constructive maths is doing.
You wouldn’t even notice if some proof is wrong because it relies on an inconsistency that’s the issue.
You wouldn’t notice because there’s no realistic chance that any meaningful result in the vast majority of math depends strictly on the particular way in which ZFC is hypothetically inconsistent.
And that’s before you didn’t notice because noone builds anything on axioms but instead uses fragile foundations made of intuition, hand-waving, and mass psychology.
This is a ridiculous attitude. Nobody uses the axioms of ZFC directly because that would be stupid. It’s obviously sufficient to know how to do so. There is literally no difference to the vast majority of all math which particular axiomatic formalism you decide to use, because all of those results are trivially translatable between them.
because all of those results are trivially translatable between them.
Then go ahead, reformulate everything in CoC or HoTT or similar. I’m waiting. Prove it trivial, prove that what you did is actually consistent.
Hence why what you’re saying is stupid. You might as well say “all computer science should be done in binary.” What you’re saying is completely unreasonable and has no bearing on actual mathematics.
Are you saying that the proofs of the four colour theorem aren’t proofs, aren’t mathematics, or something to that effect?
And no, working in Coq (as Gonthier did) is quite different from punching holes into cardstock. CS loves abstraction, all those Type Theory based systems basically look like functional programming languages and are just as ergonomic. Because they are functional programming languages (with fancy-pants type systems).
And by denying those systems you then are also denying the value of category theory because there’s some rather strong isomorphisms between those systems. Are you sure you want to throw all that maths out of the window just to be salty on the internet?
Here is an alternative Piped link(s): https://piped.video/watch?v=21qPOReu4FI
Piped is a privacy-respecting open-source alternative frontend to YouTube.
I’m open-source, check me out at GitHub.
We have sorta the same problem with imaginary numbers, and I remember some programmable calculators can process complex numbers using symbolic representation (which happens to work similarly to Cartesian coordinates, so that’s convenient)
But from what I remember any infinity bigger than counting numbers (say the set of real numbers) cannot be differentiated from each other, so we don’t have established rules.
To be fair, I last tinkered with infinities in the aughts and then as a hobbyist. The Grand Hilbert Hotel can accomodate more compound infinities and still retain perfect utilization since the last time I visited.
https://en.wikipedia.org/wiki/Continuum_hypothesis
Hmm. Frankly speaking I always assumed Mathematicians had more of an idea about infinities I mean why even have indices if you don’t have an inductive rule to descr… oh wait never mind.
That said the reals aren’t countable yet we have perfectly reasonable ways to deal with them symbolically, even compute with them, represent
every single one of1 them in finite space, it’s just when you want to compare or output them with infinite precision that you might have to wait for eternity. But who needs infinite precision anyway, arbitrary precision is plenty.1 On second thought, after diagonalisation, no we don’t. Or we do because there’s some magic going on with included transcendental constants that break through that do I look like a numerologist.
there actually is a way to represent the reals with full generality in homotopy type theory – work is still on-going to implement it in a real programming language/prove type checking is decidable, but the theory is already in place – via Cauchy sequences.
I don’t understand what you think the problem is. What do you mean infinities can’t be differentiated from each other? Infinite cardinals are by definition equivalence classes of sets that can be placed in bijection with one another. You can compare one cardinal to another by showing there exists an injection from a representative set of the first one into a representative for the other. You can show equality by showing there is an injection both ways (Cantor-Schroder-Bernstein theorem) or otherwise producing a bijection explicitly. Infinite ordinals may as well be copies of the natural numbers indexed by infinite cardinals, so of course we can distinguish them too.
So far AFAIK we have two kinds of infinity: Those that can be accommodated at the Grand Hilbert (e.g. integers, fractions, etc.) and those that cannot (set of irrational numbers, set of curves, set of polytopes, etc.) This was why we had to differentiate orders of infinity, e.g. ℵ₀ (The Grand Hilbert set), ℵ₁ (the irrational set, the real set), ℵ₂ (???), ℵ₃ (???), ℵₙ (???)
For values of infinity that are in higher orders than ℵ₀, we can only tell if they’re equal to ℵ₁ or undetermined, which means their infinity size is ℵ₁ or greater, but still unknown.
Unless someone did some Nobel prize worthy work in mathematics that I haven’t heard about which is quite possible.
No, that’s definitely not true. As I said, infinite cardinals (like the cardinality of the naturals ℵ₀) are defined to be equivalence classes of sets that can be placed in bijection with one another. Whenever you have infinite sets that can’t be placed in bijection, they represent different cardinals. The set of functions f : X --> X has cardinality 2^X too, so e.g. there are more real-valued functions of real numbers than there are real numbers. You can use this technique to get an infinite sequence of distinct cardinals (via Cantor’s theorem, which has a simple constructive proof). And once you have all of those, you can take their (infinite) union to get yet another greater cardinal, and continue that way. There are in fact more cardinalities that can be obtained in this way than we could fit into a set-- the (infinite) number of infinite cardinals is too big to be an infinite cardinal.
You might be thinking of the generalized continuum hypothesis that says that there are no more cardinal numbers in between the cardinalities of power sets, i.e. that ℵ₁ = 2^(ℵ₀), ℵ₂ = 2^(ℵ₁), and so on.
oh this is a neat argument I’d never encountered before. I was also under the impression that we hadn’t proved there were infinities with cardinality greater than ℵ₁.
How/why would you simultaneously hold this belief and reference the HoTT book
It’s quite possible that what I’m encountering is the the momentary failure to understand Cantor’s theorem, or rather the mechanism it uses to enumerate the innumerable. So my math may just be old.
Cantor’s theorem says the power set of X has a strictly larger cardinality than X.
When |X| is a natural number, the power set of X has cardinality 2^(|X|), since you can think of an element of the power set as a choice, for each element of X, of “in the subset” vs “not in the subset.” Hence the notation 2^X for the power set of X.
Cantor’s theorem applies to all sets, not just finite ones. You can show this with a simple argument. Let X be a set and suppose there is a bijection f : X -> 2^(X). Let D be the set { x in X : x is not in f(x) }. (The fact that this is well defined is given by the comprehension axiom of ZFC, so we aren’t running into a Russell’s paradox issue.) Since f is a bijection, there is an element y of X so that f(y) = D. Now either:
-
y is in D. But then by definition y is not in f(y) = D, a contradiction.
-
y is not in D. But then by definition, since y is not in f(y), y is in D.
Thus, there cannot exist such a bijection f, and |2^(X)| != |X|. It’s easy enough to show that the inequality only goes one way, i.e. |2^(X)| > |X|.
-
(which happens to work similarly to Cartesian coordinates, so that’s convenient)
it’s more than convenient, it’s isomorphism!
Your meme doesn’t work in the age of floating point numbers.
Suggestion: “1.0/x for x>0→0.0 goes against infinity, so 1.0/0.0 is infinity.”
[TREE(TREE)] ↑↑↑ (Busy Beaver)
Any sufficiently large number is indistinguishable from infinity.
Wait. Something’s wrong…
O(nm) = O(1) for all n,m < infinity.
You messed up your formatting there buddy
It’s maths there’s no syntax rules only rough guidelines.
Floats are actually fairly limited in what they can do and you lose a lot of accuracy at some point
deleted by creator
So that they can be taxed, of course.
Well… tax on infinity dollars is (crunches numbers) infinity dollars! Government deficit averted!
Computable. There are countably many computable numbers since there are only countably many possible programs. Non-computable numbers can’t be exactly referred to / described / constructed by a program, so if your point of view is that everything is a program, you would say they don’t exist.
homotopy type theory has a way to describe the reals in full generality via cauchy sequences, so if type checking ever gets proven to be decidable, this won’t be true any longer. it’s chapter 11 in the hott book.
I guarantee you’re misunderstanding or accidentally misrepresenting something here. The fact that there are only countably many computable numbers is a simple consequence of the fact that there are only countably many programs, which is bounded above by the number of finite sequences of letters from a finite alphabet, which is countably infinite.
There may be more finitistic/computable models for the real numbers or something, but “the computable real numbers” are countable.
the model provided is a lazy cauchy sequence so any given real number can be computed to arbitrary precision. the theorems about real numbers are directly provable and potentially machine checkable, assuming decidable type checking works out.
Nothing about what you said contradicts what I said. You can either change the definition of the computable real numbers, or agree that they are countable.
my point exactly
The meme is about computability of numbers though, not countability of sets of them
The universe is actually a computer program
The mind is actually a computer program
When someone has a hammer everything looks like a nail.
When someone is paid a lot of money because they have that hammer, the belief that everything is a nail seems backed by self-assigned genius and unique insight.
