The idea that the axiom of choice is guilty of all the non-constructible, weird stuff in mathematics is incorrect. The actual source of non-constructibility is always the law of excluded middle (aka the difference between classical and intuitionistic logics). What is true however is that the axiom of choice amplifies in a non-trivial way the non-constructibility of the law of excluded middle.
To pick an analogy, consider the 2022 world cup. There will be a winner, but we don't know it yet. Thus, in a sense, the existence of the winner is non-constructible. In classical logic, we accept as true the following statement:
Either France is the winner or the 2022 world cup, or it is not,
even though we cannot tell which it is now. This is not a problem, because if we wait a bit, we will be able to determine which it is. The axiom of choice in that analogy amplifies the above non-constructive problem by allowing us to wait an infinite amount of time.
In the end, the reason why the axiom of choice 'won' is the same as the reason why classical logic 'won' over intuitionistic logic: because constructibility gets in the way.
It's interesting that although you can't prove "forall P, P or not P" in intuitionistic logic, you can prove "forall P, not (not (P or not P))". In other words, it can't possibly be the case that P is not either true or false.
I personally like the distinction between "this is true" and "this can't possibly be false". If you have a proof of the second, you know why something must be true; if you have a proof of the first, you know how something is true.
The rejection of double-negation elimination is more or less the (rather intuitive) idea that knowing why something must be true doesn't automatically mean you know how it's true.
> The rejection of double-negation elimination is more or less the (rather intuitive) idea that knowing why something must be true doesn't automatically mean you know how it's true.
Exactly. There is also the matter of efficiency: it is easier to know why something must be true than to know how it's true. Constructibility in mathematics usually means proving things the hard way.
There are weaker forms, those accepted in intuitionistic logic. The law of excluded middle usually appears in mathematical proofs in the form of reasoning by contradiction:
To prove A, assume not-A and reach a contradiction
This is the non-constructible reasoning par excellence, but the following weaker form is constructible:
To prove not-A, assume A and reach a contradiction
Intuitionistic logic also allows so-called Ex Falso:
To prove A, reach a contradiction (without assuming not-A)
Now, if what you wanted is a form of LEM that is non-constructible but 'less' non-constructible than LEM, then I don't know.
I don't think you can say that classical logic won over intuitionistic logic when the former is thousands of years older and the latter is a growing area of research interest.
There are a lot of seemingly bizarre consequences of the Axiom of Choice. This is well known. Sometimes people haven’t seen a list of bizarre consequences when the Axiom of Choice is dropped. Here’s a nice write up of this:
In a given model the axiom is either true or false. When I say “dropped” I mean “false” in that model. It isn’t true that in all models where choice fails we have fields with no algebraic closure.
In a given model of ZF either choice is true or it is false. In the absence of the Axiom of Choice you can’t say that not all fields have algebraic closures. What you can say is that there is a model in which there are fields with no algebraic closure.
Imagine having countable infinite many prisoners, put hats on them colored with 0-1 real numbers, and let them to guess their own colors. And then all but finite many prisoners guess their color correctly.
Would you believe in axiom of choice now, wouldn't you?
I don’t understand your point. There are seemingly bizarre consequences of choice and of the negation of choice. They revolve around uncountable sets. For me, the bizarre thing is uncountable sets. I’m fine with them existing in ZFC and use them when doing mathematics but uncountability is bizarre.
I had no real point. Just imagine it, and laugh, because it is a funny scenario. It doesn't need uncountable sets btw, countable infinite many prisoners, and 2 colors do the trick.
I don't know what you mean by uncountable sets are bizarre. Newtonian physics uses a lot of uncountable sets, and it is consistent witch our everyday experiences, isn't it? Or things like Banach-Tarski would appear anyway? Do you have some examples?
Most of the bizarre things that happen in set theory come from uncountability. Of course there are lots of examples where uncountable sets aren’t bizarre. Physics uses real manifolds and other continuous mathematics to model reality but this doesn’t mean reality contains any actual uncountable sets.
Without the Axiom of Choice it’s possible for a vector space to not have a basis. Examples of this phenomena require uncountable direct sums of vector spaces.
I'd assume none will guess correctly because you have countably infinite guesses from uncountably infinite set (the colors) so the set of guesses is very sparse, meaning pretty much none will hit it.
How on earth can almost all hit a point in a continuum exactly with random chance?
Yes. I’m not an expert in this area but the intuition for finite sets is well modeled by the standard axioms of set theory and I’ve never heard of an issue with finite sets. Things like Russell’s Paradox had to do with constructing sets when the foundations for doing this weren’t well established. Countably infinite sets are fine too, for the most part. The truly weird results come from uncountably infinite sets.
My favorite application of choice, known as ultrafilters:
You know those "mathematicians wearing hats" games, where the solution is a Hamming code or some kind of modular arithmetic thing? Here's one where there's no winning strategy.
You have N mathematicians wearing hats whose colors are chosen uniformly and independently at random from a set C. They can see each others' hats but not their own. Simultaneously and without communication, each mathematician must guess their own hat color. Everyone who guesses right wins, and everyone who guesses wrong loses. A strategy maps (other mathematicians -> hat color) -> guess of your hat color, or if you're guessing randomly, then a distribution of guesses.
No matter what strategy is chosen, N/|C| players win in expectation. There's no trick to improve this, though you can change the distribution of how many players win. For example, you can guarantee that at least floor(N/|C|) of them win. This is neat in that it works even in a derandomized setting, where the strategy must be deterministic and the hats are assigned maliciously by an opponent who knows the strategy. (This setting is easier to work with for infinite C, because you don't need to worry about probability distributions on infinite objects.) But if |C| > N, then you can't guarantee that anyone wins.
OK, but what if there are infinitely many mathematicians, and you have the axiom of choice? In that case, there exists a strategy which guarantees that all but finitely many players will win — that is, the overwhelming majority of them will win. This works no matter how big C is, even if C is infinite, even if it's vastly larger than the set of players (eg if it's uncountable but the players are countable).
Why? Well, consider the relation that two hat assignments are "almost the same" iff they differ in only finitely many places. This is an equivalence relation, so we can divide the space of hat assignments into equivalence classes. Assuming choice, there is a function F which maps an equivalence class to some element of it. Since these equivalence classes ignore finite differences, everyone can tell what equivalence class E has been assigned even without knowing their own hat color, so can guess their own color according to F(E). By construction this is in E, so it differs from the true assignment in only finitely many places, so all but finitely many players win.
(The same holds for finitely many players too, but a strategy where all but finitely many players win is less impressive there.)
A single step (deciding the equivalence class) requiring infinite knowledge (equivalence classes of infinite hat types) and infinite data (the observable hats) instead of the more usual infinite sequence of finite steps. Interesting, but still impossible.
This is the problem I was given in my set theory class that convinced me that the axiom of choice is really doing something weird. There's also the Banach-Tarski paradox, but the proof for ultafilters is very simple and approachable.
At least in my understanding, some of the weirdness of this specific problem comes from the fact that the mathematicians "know" the function. The AoC doesn't necessarily let you know what the function is, it just lets you know that it exists. So if you were to really play the game with infinite mathematician, nearly everyone would lose even with the AoC.
What does it mean to differ by finitely many places when C is infinite? Imaging C is all the rational numbers from 0 to 1. The size of each equivalence class would be exactly 1. There must be some other condition on C for this to work.
Suppose you have two hat color assignments. These are maps U,V from eg the natural numbers (countably many players) to C, where C in this example is all rationals in [0,1]. On some inputs, U and V may output the same value, and on other inputs they may output different values. Call this latter set Diff(U,V) := { x in Naturals such that U(x) != V(x) }.
U and V are "almost the same" if Diff(U,V) is a finite set.
This is an equivalence relation because if Diff(U,V) is finite, and Diff(V,W) is finite, then Diff(U,W) is also finite: it's a subset of the union of the other two.
The same relation exists, and is an equivalence relation, for any set of players and for any set C of hat colors. It even exists if there are only finitely many players, but it isn't interesting: in that case all assignments are equivalent.
Nothing here is Turing computable because it's infinite, but telling what class you're in is the easy part. The class is just all assignments (player -> hat color) that are the same as what you see except in finitely many places.
The hard part is F, which maps each equivalence class to some member of the class.
If the players are countable and the colors are countable, then each equivalence class is also countable. I guess that might also make it computable, in some model that lets you deal with infinite objects?
Eg suppose you have a 2-tape Turing machine where one read-write tape is input which records what you see. There is a separate tape for the Turing machine's internal state. The machine outputs an infinite stream of assignments by doing normal Turing machine things, plus a "yield" instruction that yields the current state of the input tape as an output. The equivalence classes ought to be computable in that model. Note that the equivalence class is a set, so the Turing machine's output should be interpreted that way, i.e. two equivalent inputs will give outputs in a different order. (They can't always give outputs in the same order, because F isn't computable.)
But yeah, there are uncountably many equivalence classes, and F is not computable. If it were, then as I understand it, then you wouldn't need choice.
But what if there are infinitely many voters v0, v1, v2, … ? What does it mean for there to be a majority in favour? AC implies that there exists an infinitary voting scheme but supplies not a hint about how it could work.
This already leaves me confused. I thought the axiom of choice says that it is possible to obtain an [infinite] set of votes from an [infinite] set of voters each with a non-empty set of choices, not that there is a way of combining a single [infinite] set of votes into a voting result. I guess it also says that there is a way to pick one of the votes from the [infinite] set of votes, but how does it imply that this choice can or must conform with the properties we want from a voting scheme?
In this context I believe that the author is thinking of AC as Zorn's Lemma.
I will try to make a draft of a possible expansion of the reasoning.
Take the set V of functions P(N) -> {Ma,Mi,Un} that for each subset of the naturals classifies it as a majority, a minority, or undecided respecting the conditions in the article.
P(A) = Ma ⇔ P(A') = Mi
P(A) = Ma ⇔ P(A ∪ B) = Ma
P(A) = Ma ⇒ P(A \ {n}) = Ma
P(A) = Ma ∧ P(B) = Ma => P(A ∩ B) = Ma
It is easy to prove that such a function exists f_0 (A) = Mi if |A| ∈ N, f_0 (A) = Ma if |A| = ∞, and f_0 (A) = Un otherwise.
It is harder to prove that there is a such a function that also respects P(A) = Ma ∨ P(A) = Mi for subsets of the naturals.
I believe that to prove this you pretty much have to use Zorn's Lemma with the order f ≤ g ⇔ (f(A) ≤ g(A)) for all A where Un ≤ Ma, Un ≤ Mi, but Mi ≰ Ma and Ma ≰ Mi.
I feel like you can prove that the hypothesis of Zorn's Lemma are satisfied in this case.
But is is easy to see how without ZL or something similar you would have to decide one-by-one how whether each non-finite non-cofinite set maps to Mi or Ma, but there are uncountably many of them to do by simple induction.
I made a mistake in the definition of f_0, here is the correct version:
f_0(A) = Mi if and only if |A| ∈ N
f_0(A) = Ma if and only if |A'| ∈ N
f_0(A) = Un if and only if |A| = ∞ ∧ |A'| = ∞
I mixed up the concept of infinite and cofinite in my previous comment, oops.
Actually I just realized that an even simpler example of a function satisfying the conditions would be f_1(A) = Un for all A, which is also the global minimum of the entire set.
> I thought the axiom of choice says that it is possible to obtain an [infinite] set of votes from an [infinite] set of voters each with a non-empty set of choices
The axiom of choice does say this but,
1) This is not where we are applying the axiom of choice
2) You don't need the axiom of choice here: you can always just pick the "voting set" where everyone votes for choice # 1.
The axiom of choice says that the product of infinitely many non-empty sets is empty. This is needed only when you might have a different and non-computable set of choices to make at each step.
Where we are applying the axiom of choice here is: the voting scheme is just a rephrasing of an "Ultrafilter on the power set of a set": https://en.wikipedia.org/wiki/Ultrafilter#Ultrafilter_on_the...
This is implied by the axiom of choice in a way that requires some working out (and is sketched in wikipedia). But you can roughly see how the axiom of choice comes about if you start trying to construct a voting scheme (the following is just intuition):
1) We know the result if the number of "Nays" or "Yays" is finite.
2) Pick any set of "Yays" so the number of "Nays" and "Yays" is both infinite. Declare this set (arbitrarily) as a victory for either "Nay" or "Yay"
3) The set in (2) implies that a bunch of other sets are either Nay or Yay by the axioms in the article (e.g. flipping all votes flips the outcome, etc)
4) While there are sets we haven't decided on, repeat steps (2) and (3).
Of course (4) is the whole tricky part, since you have to describe with this "looping forever" means rigorously... but you can see how the idea of "making infinitely distinct choices" comes up.
Okay, I got this, the axiom of choice is not even needed for finite sets of choices, it comes into play elsewhere. But there are quite a few more points where I can not understand the reasoning behind. Not saying that they are incorrect, only that they are not obvious to me.
Given any set of voters, either it or its complement is a majority, but not both
Why no draws, like the odd numbered voters versus the even numbered voters?
The result of removing a single voter from a majority is still a majority.
This is not true for finite sets of voters, why would we require it for infinite sets of voters? This seems more like a possible consequence of dealing with an infinite set of voters than something one would require in advance.
The intersection of two majorities is a majority
Also not true for finite sets of voters, so the same question as above.
Regarding mathematical existence, one thing that I have thought about before and don't have an answer for or understanding of is the concept of infinities. In set theory, there are cardinalities that are "infinities of infinities". This is all fine and makes sense within the world of mathematics, as the study of idealized structures. But what makes me curious is that the universe is finite, and thus presumably, contains a finite amount of information. That is, the universe has a finite amount of bits that can be used to represent information.
How does this work then? We can represent these sets of cardinality infinities of infinities in our brain and on paper, but representing these sets with all the available bits in the universe is not possible. This seems like a paradox, because our brains and paper are part of the universe.
Does anyone have some thoughts on this? Is this a well-discussed problem? Any good references?
Why should the limits of our universe have anything to do with the limits of math? Math is bigger than our universe. If our universe were completely different, math would still be the same.
> We can represent these sets of cardinality infinities of infinities in our brain and on paper, but representing these sets with all the available bits in the universe is not possible. This seems like a paradox, because our brains and paper are part of the universe.
Eh, I can write a recipe that calls for multiple universes-worth of flour and 600 trillion years in the oven, and I can write that recipe in a minute on an index card that weighs a couple grams. I can write small programs that loop infinitely or (attempt to) use infinite memory. I can write a song that repeats ad infinitum that nobody can ever sing to completion in the entire lifetime of the universe. That's not much different than the words "the Integers" requiring 2 words but describing something that could not possibly be "fully materialized" in any finite universe. Who cares?
What those all have in common is that despite being very big or long in some sense, they have low Kolmogorov complexity. It's very easy to describe "recipes" for infinite things that would exceed the bounds of the universe if they were ever fully realized; you don't even need higher cardinalities for that.
What higher cardinalities do tell us is that there must be some real numbers that have infinite Kolmogorov complexity, and in fact 100% of the real numbers have this property. (Of course all the numbers you have/will ever have heard of are in the remaining 0%.) There are only countably many (the smallest infinity) descriptions in any language (programming or natural), so most reals must not be "describable" at all. We will never be able to meaningfully use any of those numbers, because we couldn't possibly "compute" them -- we can't run the infinitely long program. It's not clear to me that we'd ever be able to learn anything at all about such numbers, or indeed that they "exist" in any meaningful sense.
> Why should the limits of our universe have anything to do with the limits of math?
Mathematics is a human activity, and humans are part of the universe.
> Math is bigger than our universe.
What does that mean?
> If our universe were completely different, math would still be the same.
That is more than debatable.
> Eh, I can write a recipe that calls for multiple universes-worth of flour and 600 trillion years in the oven, and I can write that recipe in a minute on an index card that weighs a couple grams. I can write small programs that loop infinitely or (attempt to) use infinite memory. I can write a song that repeats ad infinitum that nobody can ever sing to completion in the entire lifetime of the universe. That's not much different than the words "the Integers" requiring 2 words but describing something that could not possibly be "fully materialized" in any finite universe. Who cares?
I think you're skipping over the point. No one is going to argue with you about "multiple universes-worth of flour" existing because to our current knowledge, the universe is finite and thus there is a finite maximum to how much flour can exist. My question revolves around the philosophical question of the existence of mathematical objects and whether they can or cannot be actually realized with the given information in the universe. This is not a question out of left field. The acceptance of the real number continuum is not even settled.
Thanks for the reference to Kolmogorov complexity.
> How does this work then? We can represent these sets of cardinality infinities of infinities in our brain and on paper, but representing these sets with all the available bits in the universe is not possible. This seems like a paradox, because our brains and paper are part of the universe.
The "paradox" arises because you're using the word "represents" in two different meanings.
For example, the number TREE(3) is extremely big (to put it mildly.) If you haven't heard of it you can search Youtube, there's a few Numberphile videos on it that are wonderful.
Anyway, TREE(3) is extremely big but finite. I can explain exactly what TREE(3) is. You can understand what it is. I can therefore "represent" it, and you can have an exact picture of your head of how to write a computer program that calculates it.
It is, of course, much too big to "represent" it by writing down all its digits in base 10. There's not enough bits in the Universe.
But these are two different senses of the word "represent".
In a similar way, I can "represent" sets of infinites very easily, in the sense that I can explain to you what they are and how they behave. I mean, every schoolchild knows about a set that's infinite - just the regular old counting numbers. The set of counting numbers if infinite - there is no way to actually write down all of these numbers, within our universe.
But I can still explain to you what that set is, and how it behaves. Everyone understands that the behavior of it is that you can keep pulling out more numbers from it. That's all that "representing" it is in this context.
We can encode the idea of infinite sets and their relationship to one another with a finite set of symbols. But we can't enumerate those sets.
Edit: How is there a paradox?
> We can encode the idea of infinite sets and their relationship to one another with a finite set of symbols.
I have thought about this, but it isn't entirely clear to me. For example, what is the bit encoding of the real numbers? Is it really accurate to say we have an encoding of them by just saying we have the set R?
> But we can't enumerate those sets.
Well, that's kind of the point of my question. Is this not an issue?
> AC by itself implies only vapourware. However these zombie-like objects like the voting scheme are necessary for the smooth functioning of the mathematical universe. Without them the universe is chaotically irregular.
So, considering we just covered a bunch of reductio ad absurdum proofs, AC is false and the universe is chaotically irregular. I'm just being rhetorical, as I suspect it's more technical than that but why do people not see things that way? Whenever people talk about AC, all I hear is a bunch of reasons why ZFC is inconsistent or at the very least incoherent in some weaker sense. How is the Banach–Tarski paradox not just a refutation of the ZFC axioms taken as a whole?
Yes, the computable, countbale universe is incompatible with ZFC.
But ZFC is math, not computation or physics. ZFC is consistent with itself, which is good enough for math.
You don't even need AoC to run into this. Even the "tame" smooth functions of classical physics (like f(x)=x^2) are a non-physical approximation to discrete reality.
> ZFC is consistent with itself, which is good enough for math.
That's what we believe, but we don't know it. Nor do we have any hope of proving it in some reasonable way (via Gödel's second incompleteness theorem).
Math is necessarily consistent because, when we find inconsistencies, we remove them, so they are no longer valid math.
Math is but a language to express your thoughts in a very precise and rational way. When you find out that two of your carefully expressed thoughts contradict each other, you tweak one or both so that they are no longer contradictory. That's why "the barber who shaves those who don't shave themselves" and "the set of all sets that don't contain themselves" are not considered valid sets anymore.
> Math is necessarily consistent because, when we find inconsistencies, we remove them, so they are no longer valid math.
The former doesn't follow from the latter, because we may simply not yet have found any inconsistency, even though it exists.
edit:
Not sure if your point is just "if someone finds a contradiction in ZFC, it doesn't break maths, we'll just find a different foundation". Because I agree. But GP's point was about ZFC, a concrete set of axioms, being consistent.
If by "discrete" you mean rejecting the continuum, then I don't think it's as scary as it sounds. The rationals do not form a continuum, but they are "effectively" continuous -- between any two of them there is another. There are no "leaps" between them, and no concept of consecutive numbers. Computable numbers are similarly countable but allow the expression of numbers that can only be approximated by rationals.
It's the reals that require "bold" assumptions -- numbers exist which are not possible to compute even approximately?
Everything appears to be discrete except possibly space-time. Is there a reason to believe space-time isn’t discrete other than using manifolds makes things easier mathematically?
I believe the numbers in QFT are continuous. The electrons and what not are quantized but quantized over complex number spaces. U less one be
Unless the fine structure constant or speed of light, or other apparent constants of the theories, are computable some how? Disclaimer: I can only get a few chapters into a QFT book without it all becoming meaningless to me.)
The mathematical notion of "discrete" does not require that there be big gaps, or that there be fundamental limits to precision. The rationals are discrete (i.e. they are countable and have measure zero) but they are "continuous" in every way that matters -- between any two rationals there is another rational.
Even the computable/constructible/rationally-approximable numbers are discrete, and those sets contain basically all the numbers that are possible to compute (by definition) but they are still "discrete", forming a set of measure zero,
The idea of the continuum is the unintuitive one; the idea that there are numbers that cannot be constructed or computed is just kind of silly
Unintuitive till you move your hand from here to there, though I wouldn’t notice a Planck length digitization, but my point was more the maths for reals or complex over reals is so much simpler than over rationals, and so that is what the physics is based on. I have not seriously looked at constructivist analysis, but I do understand there is promise there, but it is a lot more complicated.
Interesting to imagine an integral over all possible paths with only computable paths. Such a smaller set of thing affecting the solution.
> Unintuitive till you move your hand from here to there
Continuity does not require the notion of a continuum. There need not be a "minimum length" even in a non-continuum approach. The rational numbers are perfectly fine for this because Zeno's paradox still applies -- between any two points is a halfway point, no matter what scale you look at.
If you need more power you have the computable reals, which include all real numbers that it is possible to compute.
The leap from the computable reals to the continuum is a huge, vast leap -- in measure theoretic terms you are going from a measure zero set to a non-zero-measure set. But all you get from that leap is access to a bunch of numbers that it is not possible to construct anyway, where I mean "not possible" in the strict, formal, definitional sense -- it is literally impossible to produce an example of one. Only the Axiom of Choice and similar nonsense even let you reason about these, the "zombies" of the OP.
In topology the rationals are not discrete[1]: every open interval around zero contains other rational numbers!
Also, what do you mean by "rationally-approximable"? I think the construction of the reals using Cauchy sequences is /exactly/ meant to formalise this.
The problem is that Cauchy sequences are too powerful. The intuitionist/constructive version of "rationally approximable" requires a procedure to approximate a number to any requested degree of precision, but cannot guarantee that equality is decideable.
My use of discrete was informal and in response to the thread here which equated discarding the notion on the continuum with saying the universe is "discrete". More precise in the topology sense is that the rationals are not compact
I believe the universe is finite and so there can only be a finite number of realizations of quantum numbers. I have no real intuition in physics or training in physics so I know I could be completely wrong. It seems to me though that our experiences are such that believing the universe is discrete in all things is not completely unreasonable. Though this belief of mine might itself be unreasonable.
Events themselves are discrete, but they might have contiguous properties, like the associated point in spacetime, assuming a the contiguous spacetime is not just an approximation.
Conversely, classical mechanics is discrete at the level where physics is applied. That it is applied to realia goes without saying. But it is not applied to reality as a whole.
Well, it's bold to assume anything about reality, because we only ever experience individual aspects of it. We can only try to model what we can observe.
But as a counter to the assertion that "AC must be wrong because we can't really experience Banach-Tarski in the real world", it's perfectly valid to comment that "well, we also can't really observe continuous functions R -> R either". Or have you ever seen a least upper bound in real life?
I think he's talking about the mathematical 'universe,' not the universe we live in. Apparently it's not so obvious what's absurd in the mathematical universe.
Alternatively, maybe you and I can define 'absurd' very solidly, then go and overturn large portions of current mathematics. But I'm guessing that's more difficult than it sounds.
"There is therefore a need to investigate how the
constructive axiom of choice, validated by the Brouwer-Heyting-Kolmogorov
interpretation, is related to Zermelo’s axiom of choice ..."
With his constructivist program I wish Steve Wolfram would just grow some balls and firmly reject the Axiom of Choice. (e.g. Mathematica at best can represent a measure subset 0 set of the phony numbers, the numbers that Mathematica can represent are more real than the rest of them.)
His whole approach of throw a lot of things at the wall and seeing what sticks is never going to sample all of the objects requiring an infinite choice procedure to find.
But equality over the constructible reals is not decidable either.
A constructible real number is essentially a suspendable computer program that outputs the next digit of the number whenever you ask for it, in finite time. With some work you can define operations like addition and multiplication of such objects. But if you try to define an equality test, you will find that the algorithm will correctly differentiate distinct numbers in finite time, but will not terminate on equal numbers (how many digits have to agree before you know they are the same?). Deciding equality here requires a halting oracle.
I've seen an advice to not use equality on floats, and instead use something like |x-y|<e. Probably translates to constructive reals as it needs to compute only some part of the numbers.
I've long held that floating point with a decimal exponent would help a lot more people feel like computing is something they can be a part of. That is, I think the non-professional programmer finds that
0.1 + 0.2 != 0.3
is one of many little problems that adds up to them giving up the possibility of using software to put their skills on wheels. Like many reforms in computing, performance is used as an excuse to maintain the status quo of the priesthood. IBM is the only company in the industry that's taken this seriously, see
>I've long held that floating point with a decimal exponent
You mean IEEE745 Decimals?
Decimals also have serious pitfalls. For many applications they are just worse and lead to more problems.
In the end they are at least as confusing as floats. And switching to them as the default would make programs generally worse.
> Like many reforms in computing, performance is used as an excuse to maintain the status quo of the priesthood.
Very silly argument. Performance is not the issue.
Floats are useful because of their range. Even if input and output are small, intermediate results can easily be very large and exceed the representable decimals.
Every programmer has to learn that the computer does not understand real numbers and that expecting it to is entirely misguided. No different representation will change that.
You'd find plenty of unfriendly inequalities just like yours if you made the exponent decimal. e.g 1/3 + 1/3 + 1/3 != 1. The fundamental issue remains, which is that some rationals don't have exact representations in the (finite) floats, so there is some roundoff error. Sure, using decimals means that if you're only working with decimal literals and addition and subtraction and possibly multiplication you usually won't have any roundoff, but how often are you doing something that matters that won't add roundoff some other way?
Someone here said recently: It is rarely a good idea to compare finite representations of real numbers for equality. I am inclined to agree.
Having a fixed size datatype which can emulate the reals to a degree satisfying most applications is really amazing. They are one of the best designed datatypes.
You can also use just floats to calculate mathematical true results.
I like Bill Wadge's stuff and this is a great explanation of the axiom of choice. I spent a fair bit of time on ZF set theory + AC working in databases, and AC is essential for data-driven set-theory to function.
Bit confused about the unit sphere explanation but then again I'm unfamiliar with the underlying paper.
Not to cop out but a HN reply isn't the best place to provide a full explanation. Suffice to say I use the ZF axioms as a basis to teach how sets both differ from and are similar to tables, particularly using the more accessible parts of Stoll's textbook on axiomatic set theory. To give a single example, the axiom schema of replacement is a good analogy for how the output of a SELECT command over a set will also result in a set.
In terms of AC, the comment below about how this is actually the AFC is correct, since the sets I am talking about are finite. Of course, set projections or selections are arguably choice functions themselves, which makes them relevant, and ZFC includes AC in order to infer well-orderedness, which tables (after all, collections of sets) can indeed be.
By database do you mean a finite 2d array with column headings? Or something that can be represented by such an object? And its entries are elements of some countable sets? If so, what are you doing using ZFC there?
What are the things that “break” if the axiom of choice is false?
I’ve been wondering if the axiom of choice has some relationship to an argument for the existence of free will. Not just because they share a name, but because you can think of physics as being a multiplayer game.
I have always had mixed feelings about this axiom. It feels "2nd level", like it should build upon simpler axioms related to the mathematical object "set" and the mathematical object "function".
Then it wouldn’t be an axiom, which it, in fact, is, being logically independent from the rest. It is considered somewhat special though, and mathematicians, being nice people, usually indicate whether they rely on it in a proof.
To pick an analogy, consider the 2022 world cup. There will be a winner, but we don't know it yet. Thus, in a sense, the existence of the winner is non-constructible. In classical logic, we accept as true the following statement:
even though we cannot tell which it is now. This is not a problem, because if we wait a bit, we will be able to determine which it is. The axiom of choice in that analogy amplifies the above non-constructive problem by allowing us to wait an infinite amount of time.In the end, the reason why the axiom of choice 'won' is the same as the reason why classical logic 'won' over intuitionistic logic: because constructibility gets in the way.