Replace 3^^^3 with whatever number is enough to guarantee whatever result you need.
But how do you know what number that is? The function “the number of steps needed to guarantee that a Turing machine won’t halt” is not a computable function of Turing machines, because if it were you could solve the halting problem. So how do you compute a function that’s, y’know, not computable?
First of all, I shouldn’t have used the number 3^^^3. That was a stupid idea, and I’ve forgotten what the notation means. So just replace that with “generic really big number”, let’s just say a googolplex (and, yes, I’m aware that’s nowhere close to 3^^^3).
To answer your question, I doubt FAI is going to care about whether Turing machine X halts; it’s going to be looking for a proof of a certain result regarding its own algorithms. It’s possible that it only needs to prove that its algorithms will work for “generic really big number” amount of steps, and thus could use a bounded quantifier instead of a universal quantifier. Using bounded quantifiers makes your system much weaker, but also moves it closer to being decidable (I mean this in a metaphorical sense; the system still won’t be decidable). Also, regarding searching for proofs, we’ll have to set an upper bound for how long we search, as well. So we need to specify some specific number in that context, too.
Specifically which numbers to select is something I have no idea about; I’m not an AI researcher. Maybe I’ll have some kind of idea (but very probably not) when a more formal problem specification is given, but this article is still discussing theoreticals, not applications yet.
Okay, non-ultrafinitist objection:
But how do you know what number that is? The function “the number of steps needed to guarantee that a Turing machine won’t halt” is not a computable function of Turing machines, because if it were you could solve the halting problem. So how do you compute a function that’s, y’know, not computable?
First of all, I shouldn’t have used the number 3^^^3. That was a stupid idea, and I’ve forgotten what the notation means. So just replace that with “generic really big number”, let’s just say a googolplex (and, yes, I’m aware that’s nowhere close to 3^^^3).
To answer your question, I doubt FAI is going to care about whether Turing machine X halts; it’s going to be looking for a proof of a certain result regarding its own algorithms. It’s possible that it only needs to prove that its algorithms will work for “generic really big number” amount of steps, and thus could use a bounded quantifier instead of a universal quantifier. Using bounded quantifiers makes your system much weaker, but also moves it closer to being decidable (I mean this in a metaphorical sense; the system still won’t be decidable). Also, regarding searching for proofs, we’ll have to set an upper bound for how long we search, as well. So we need to specify some specific number in that context, too.
Specifically which numbers to select is something I have no idea about; I’m not an AI researcher. Maybe I’ll have some kind of idea (but very probably not) when a more formal problem specification is given, but this article is still discussing theoreticals, not applications yet.