Interestingly, Peano arithmetic has the same “problem.” This isn’t directly relevant, but it does very strongly suggest that there is no possible way to exploit this flaw.
Suppose I take some program which looks really complicated to PA. In particular, the program runs indefinitely but PA can’t prove it. Then for every particular amount of time, PA can prove that the program hasn’t yet stopped. But there are models of PA where it is nevertheless true that “There exists a time at which the program has stopped.” It is intuitively like having two sets of integers. The normal integers, obtained from 0 by adding 1 a finite number of times, and the really large integers, obtained from the halting time of your program by adding or subtracting 1 a finite number of times. There is no way to get from one to the other, because the really large integers are just that large.
If you use to ZFC instead, you encounter significantly less intuitive versions of this strange behavior.
In our case, this would be like believing in a hypothetical future time where you will do work, but which can never be accessed by letting the days pass one by one.
Interestingly, Peano arithmetic has the same “problem.” This isn’t directly relevant, but it does very strongly suggest that there is no possible way to exploit this flaw.
Suppose I take some program which looks really complicated to PA. In particular, the program runs indefinitely but PA can’t prove it. Then for every particular amount of time, PA can prove that the program hasn’t yet stopped. But there are models of PA where it is nevertheless true that “There exists a time at which the program has stopped.” It is intuitively like having two sets of integers. The normal integers, obtained from 0 by adding 1 a finite number of times, and the really large integers, obtained from the halting time of your program by adding or subtracting 1 a finite number of times. There is no way to get from one to the other, because the really large integers are just that large.
If you use to ZFC instead, you encounter significantly less intuitive versions of this strange behavior.
In our case, this would be like believing in a hypothetical future time where you will do work, but which can never be accessed by letting the days pass one by one.