By _assuming_ that program terminates, you are yourself taking the axiom of choice.
If it _does_ terminate, then it's not an axiom anymore it's a proof.
The axiom of choice is an assumption that is neither known to be true or false.
Moreover, you'd probably want to limit the tries to algorithms that terminate. But that brings you into the halting problem.
I think us programmers think in terms of time. But in math there is no time so whether you do things in parallel or procedural is irrelevant. That's why you can discuss infinities in math.
Nope, you don't need the axiom of choice to define the sequence of all algorithms. The axiom of choice allows you to order any arbitrary set, but you don't need it for things you can construct an explicit order for, like the natural numbers. In the case of all algorithms, it's somewhat straightforward to construct the set of all of them. You can construct the sequence of all strings, right? You can construct them as "", "a", "b", "c", ... "y", "z", "aa", "ab", ... "ay", "az", "ba", "bb", ... Now, pick a programming language, like C. Given any valid string, you can determine if it is a valid C program in finite time, and if so you can convert it into a set of instructions to use in the dove-tailing procedure in finite time. Take the list of all strings in the manner described above. For each one interpret it as a C program, or if it's got invalid syntax interpret it as a program that immediately halts. Now you've got an enumerable sequence of algorithms. Since C is Turing complete you'll find every single algorithm in that sequence. There will be a ton of duplicates (for whatever notion of equivalence you want to use) but all the algorithms will be there, and in a well-defined order that you can enumerate through.
No. I'm saying selecting an algorithm out of the set of all algorithms.
I'm not saying defining the set of all algorithms.
Then you don't need to "randomly pick" an algorithm. You just start with the first algorithm in the sequence, and keep going.
That is still random. You are arbitrarily picking an encoding, (English) in this case. Why not a Russian programming language or Chinese? How did you *select* your encoding out of the set of all encodings?
The act of assigning order to an unordered set is arbitrary. ABC order is a made up concept. It's not numerical, it's an arbitrary language and an arbitrary order that's a by product of human culture. Thus invoking this is at it's essence invoking the axiom of choice. You are arbitrarily selecting an algorithm.
You can phrase things like Gödel did. For any encoding of algorithms into natural numbers which is bijective (ignoring invalid syntax), enumerate the algorithms as 0, 1, 2, 3, ... using the bijection, and then run them in parallel by taking steps [0, 0, 1, 0, 1, 2, 0, 1, 2, 3, ...] The user provides an encoding, without invoking the Axiom of Choice.
You only need the axiom of choice if you need to pick an element out of a set WITHOUT SPECIFYING which one you are picking. And sometimes not even then. For instance, if you want to prove all elements in a set have a certain property, often you will see proofs take the form "pick an element of that set, assume it doesn't have this property, then by X, Y, and Z we have a contradiction, thus all elements have that property". That doesn't involve the axiom of choice at all, even though a straight reading of that statement makes it sounds like we are making a choice. In truth that proof is saying we can do this with every single element of that set, so you aren't really making a "choice". You only need the axiom of choice when you are, say, stating the existence of a function without defining what that function is. For an example of an actual invocation of the axiom of choice, check out the proof sketch in the wikipedia article on Zorn's Lemma: https://en.wikipedia.org/wiki/Zorn%27s_lemma .
I can say arbitrary stuff like the set of all sets with positive numbers but when I say the set of all algorithms written in English and C++ suddenly I'm getting too specific. Where is the line drawn?
Algorithms themselves have no specific order. In order to define enumeration you must first start off by *selecting* which algorithm gets the first enumeration. This is a completely arbitrary choice.
And yes, which particular encoding you decide to use is arbitrary, but the point is that you can enumerate the set of all algorithms, and thus you can select one without needing the axiom of choice.
Try to select an algorithm out of the set of all algorithms without using an encoding. If you must use an encoding, please ensure that it's not a "particular" encoding.
You can't.
The point is all encodings in the known universe are "particular."
Additionally, to even use an encoding you have to *select* and encoding from the set of all encodings.
One way of selecting an algorithm is to select a way to encode the algorithms.
It's easy to see that this is true. You chose an arbitrary example above. Try to do the same without choosing anything arbitrary. You can't.
But I'd also add that you can have a choice function that isn't an "algorithm". An algorithm, at least in the sense I'd generally interpret the word, has finitely many instructions and at most countably many steps. If we have uncountably infinitely many uncountably infinite sets, it is possible to have a choice function that can't be described in a finite algorithm.
Like, think about a well-ordering of the reals. If you believe the axiom of choice, then one exists. But you can't tell me what it is, because that would involve handing me infinite amounts of information. And similarly you can't write down an algorithm to produce it, without writing down infinite amounts of data.
No my algorithm above will never terminate. There's a recursive call where the input never shrinks and it won't converge on a base case.
It's equivalent to saying
def f(x):
return f(x)
Basically ketralnis is clarifying context which is sort of lost with my post. There's an axiom and do you believe in the axiom of not?
If the axiom can be proven then it is not an axiom. But a theorem. What I'm doing here is kind of pointless because we know it's an axiom by definition, the question is whether this axiom is valid or not. Attempting to prove the axiom is a a signal that I'm lacking clarity with the logic here.
def a(x):
return a(x)
I'm looking at it and such an algorithm is defined in terms of itself (like a factorial, which is legal) and may never terminate (which also legal because an algorithm selecting the smallest number from all sets that only contain positive numbers will never terminate either).
Wait but then if you look at the code it provably will never terminate because A does not shrink as it recurses.