IngoBlechschmid

From the title I thought this was an implementation of Gwern's idea, but it's not.

I agree. Here is a remote example where it exceptionally does, but it is mostly practically irrelevant:

In mathematics, we distinguish between "constructive" and "nonconstructive" proofs. Intertwined with logical arguments, constructive proofs contain an algorithm for witnessing the claim. Nonconstructive proofs do not. Nonconstructive proofs instead merely establish that it is impossible for the claim to be false.

For instance, the following proof of the claim that beyond every number n, there is a prime number, is constructive: "Let n be an arbitrary number. Form the number 1*2*...*n + 1. Like every number greater than 1, this number has at least one prime factor. This factor is necessarily a prime numbers larger than n."

In contrast, nonconstructive proofs may contain case distinctions which we cannot decide by an algorithm, like "either set X is infinite, in which case foo, or it is not, in which case bar". Hence such proofs do not contain descriptions of algorithms.

So far so good. Amazingly, there are techniques which can sometimes constructivize given nonconstructive proofs, even though the intermediate steps of the given nonconstructive proofs are simply out of reach of finitary algorithms. In my research, it happened several times that using these techniques, I obtained an algorithm which worked; and for which I had a proof that it worked; but whose workings I was not able to decipher for an extended amount of time. Crazy!

(For references, see notes at rt.quasicoherent.io for a relevant master's course in mathematics/computer science.)

By Greg Egan, so highly recommended.

This is suspected but currently not yet proven.

In fact, we don't even have a proof yet that the digit 7 occurs infinitely often in pi. (Same for any other digit.) Right now it's conceivable, but very unlikely, that there is some final 7 in pi.

This is because we can prove, in the small and generally trusted metatheory PRA, that ZFC is inconsistent if and only if ZF (= ZFC − AC) is inconsistent (if and only if IZF (= ZFC − AC − LEM) is inconsistent).

[ This metaproof rests on the fact that ZF can prove that the axiom of choice (AC) holds in "Gödel's sandbox" L, the "constructible universe", even if it might not hold in the universe of all sets. ]

In other words: Adding the axiom of choice to ZF doesn't cause new inconsistencies. In case ZF is consistent (a statement which most logicians believe), then ZFC is so as well.

A couple pointers to the literature are here: https://www.speicherleck.de/iblech/stuff/37c3-axiom-of-choic...

For instance, regarding statements of the form "for all natural numbers x, there is a natural number y such that %", where in "%" no further quantifiers appear, there is no difference between ZFC (Zermelo–Fraenkel set theory with the axiom of choice), ZF (set theory without the axiom of choice) and IZF (set theory without the axiom of choice and without the law of excluded middle).

Any ZFC-proof of such a statement can be mechanically transformed to an IZF-proof, with just a modest increase in proof length.

I included some references about this in a set of slides: https://www.speicherleck.de/iblech/stuff/37c3-axiom-of-choic...

1. Accept that our intuition about volumes is off when dealing with point clouds so weird that they cannot actually be described, but require the axiom of choice to concoct them.

2. Reject the axiom of choice and adopt the axiom of determinacy. This axiom restores our intuition about volumes to all subsets of Euclidean space, at the expense of which sets can be formed. (That said, the axiom of determinacy allows other sets to be formed which are not possible with the axiom of choice, so it wouldn't be correct to state that the axiom of determinacy causes the set-theoretic universe to shrink.)

3. Keep logic and set theory as it is, but employ locales instead of topological or metric spaces. Locales are an alternative formalization of the intuitive notion of spaces. For many purposes, there are little differences between locales and more traditional sorts of spaces. But, crucially, a locale can be nontrivial even if it does not contain any points. Locale-theoretically, the five pieces appearing in the Banach–Tarski paradox have a nontrivial overlap (even though no points are contained in the overlapping regions), hence you wouldn't expect the volumes to add up.

I tried to give a varied account on the axiom of choice at the Chaos Communication Congress once, the slides are here: https://www.speicherleck.de/iblech/stuff/37c3-axiom-of-choic...

https://en.wikipedia.org/wiki/Square_root_of_2

For instance, 0.123123123... is checked to be the same as 123/999, a fraction -- hence rational. Similarly, 0.abcdabcdabcd... is the same as abcd/9999. This works for repeating blocks of digits of any length.

That said, the axiom of choice is always available in Gödel's sandbox of "constructible sets", and by "Shoenfield absoluteness", some results can escape the sandbox.

For instance, the result that every vector space has a basis is equivalent to the axiom of choice. We have it in Gödel's sandbox and we don't have it outside, if we prefer to not use the axiom of choice in our meta theory. But every purely number-theoretic consequence of that result flows from the sandbox to the ambient universe.

In this sense, the axiom of choice can be regarded as a useful fiction. Not necessarily true in a literal sense, but true enough for many purposes.

I gave a 37c3 talk on this topic: https://www.speicherleck.de/iblech/stuff/37c3-axiom-of-choic...

Fun fact: For certain kinds of results, there is an explicit procedure for transforming any given ZFC-proof into an IZF-proof. By ZFC, I mean classical "uncomputable" mathematics with the axiom of choice and with the law of excluded middle. By IZF, I mean (a specific flavor of) constructive mathematics without those two contested axioms.

In particular, this metatheorem applies to termination results. So feel free to use the axiom of choice and the law of excluded middle to your heart's content when proving that a program terminates; you can trust that at the end of the day, your proof can be transformed to a constructive proof.

Slides which I hope are also accessible to non-specialists in proof theory: https://www.speicherleck.de/iblech/stuff/37c3-axiom-of-choic...

More pointers to the literature: https://math.stanford.edu/~feferman/papers/reductive.pdf

* No amount of personal spending decisions can advance systemic changes like better public transport or more careful military funding. These require governmental action.

* With our wallet, we can only choose between those alternatives which are offered. In many cases, we can only choose between bad options.

* Voting with our wallet requires immunity against professional PR campaigns, time (for researching on what to buy), money (to afford options which are better according to personal views but more expensive), friends who appreciate instead of belittle our purchasing decisions, ...

In the end, I believe the story "vote with your wallet" internalizes a form of victim blaming: The consumers are blamed for their irresponsible purchasing decisions, but the responsibility really is with the companies and governments.

Of course, not spending consciously is also not a solution. But we obtain greater leverage by using our influence on society. Only few of us are editor-in-chiefs of important newspapers or important politicians, but most of us can engage in visually powerful protests which are also able to generate political wind.

If you want to experiment with Agda without installing it, you can do so directly in your browser: https://agdapad.quasicoherent.io/

Nowadays, there is indeed a movement towards interoperability between the various proof assistants, one of these bridge-building projects is called Dedukti: https://deducteam.github.io/ It's a challenging project because the different proof assistants which are currently in use differ in their foundational perspectives and their idioms. The question how to best formalize mathematics is still an open research problem, just as the question how to best develop programs, but we already have quite a good understanding of many important issues in this area.

Also, by now there are attempts to use AI for discovering proofs, see for instance https://leandojo.org/ or https://github.com/lean-dojo/LeanDojoChatGPT.

1. In those proof assistants which don't have the axiom of choice built-in, you can still formalize proofs depending on this axiom by putting it as an extra assumption. One repository using this style which I particularly like is the one by Martín Escardó: https://www.cs.bham.ac.uk//~mhe/TypeTopology/index.html He even takes care to explicitly put axioms as visible assumptions which are almost always taken for granted, such as function extensionality.

2. You don't need the axiom of choice to construct the real numbers, in fact several constructions are available (Dedekind cuts, Cauchy sequences, Cauchy processes, ...) and all do their job. It's just that without the (countable) axiom of choice, you cannot prove that the Cauchy real numbers are complete. But the other constructions work fine even in the absence of choice.

Many compsci people have been captivated by it and wrote introductions, trying to put the technique into a wider perspective. Here is mine, including a "poor man's variant" of automatic differentiation which does without operator overloading, but uses complex numbers instead:

https://pizzaseminar.speicherleck.de/automatic-differentiati...

For the purposes of teaching Python, I once created something similar---but without the explanations:

https://www.speicherleck.de/iblech/zufall-im-browser/index.e...

I tried to explain the resulting "multiverse philosophy" (not really related to the idea of physical alternate universes) here: https://iblech.gitlab.io/bb/multiverse.html

2. Scientists, especially young ones, have an incentive to challenge dominating scientific views because that is how you make yourself known in the scientific community. Being known can be transformed to getting the next academic position.

(1) Provably so in a very weak (and hence trustworthy) metatheory, assuming the axiom of choice does not result in any new inconsistencies. More precisely: The systems ZFC (Zermelo–Fraenkel set theory with the axiom of choice) and ZF (ZFC but without choice) are equiconsistent; if ZF is consistent, then so is ZFC.

(2) There is a mechanical procedure for transforming ZFC-proofs of number-theoretic statements into ZF-proofs. That is, appeals to the axiom of choice can always be mechanically eliminated from proofs of number-theoretic statements, even if those proofs rely on results in other areas which crucially depend on the axiom of choice.

You should worry about the axiom of choice because:

(3) Assuming the axiom of choice imposes an undue restriction on the scope of your results: Any theorem proven without the axiom of choice and without the law of excluded middle (which is implied by the axiom of choice) automatically also applies to continuous families. For instance, the theorem "every real symmetric matrix has an eigenvalue" has a proof avoiding AC and LEM. Hence it also holds that for every continuous family of symmetric matrices, locally on the parameter space, there is a continuous eigenvalue-picking function.

PS: One could also wonder whether one should worry about the law of excluded middle. One should not because: (1') The systems ZF and IZF (ZF but without LEM) are equiconsistent. (2') There is a mechanical procedure for transforming ZF-proofs of number-theoretic statements of the special kind "for every numer x, there exists a number y such that some equation holds" into IZF-proofs. On the other hand, one should worry because of (3).

PPS: The axiom which one should truly worry about is the inconspicuous powerset axiom. In contrast with ZFC, ZF and IZF, which are all equiconsistent, removing the powerset axiom results in a drastically weaker system. The proof-theoretic strength of Kripke–Platek set theory (ZF without powerset) is a reasonably large ordinal, whereas we are lacking the technology to even fathom the ordinal calibrating the strength of IZF/ZF/ZFC.

There are several systems of axioms we can use to base mathematics on.

A common such is ZFC, Zermaelo–Fraenkel set theory with the axiom of choice. Among its axioms are assertions like "there is a set which is empty", "there is an infinite set" and "if A and B, then in particular A".

Another is Martin-Löf type theory in one of its flavors, perhaps homotopy type theory.