That proof was a prerequisite for the idea to try the brute force method of finding the FAI.
Someone could also set an end condition that only an AGI is likely to ever reach and use iterated UTMs to find a program that reached the desired end condition. I’m not sure how to a priori figure out what someone smarter than me would do and test for it, but it isn’t the first thing I would do with a constant-time halting oracle. The first thing I would do is test a program that found additional implications of first order logic and halted when it found a contradiction. Then I would add the inverse of the Gödel statement and test that program.
That proof was a prerequisite for the idea to try the brute force method of finding the FAI.
Someone could also set an end condition that only an AGI is likely to ever reach and use iterated UTMs to find a program that reached the desired end condition. I’m not sure how to a priori figure out what someone smarter than me would do and test for it, but it isn’t the first thing I would do with a constant-time halting oracle. The first thing I would do is test a program that found additional implications of first order logic and halted when it found a contradiction. Then I would add the inverse of the Gödel statement and test that program.