I'd say things differently now. I'd drop the distinction between "logical uncertainty" and uncertainty about the output of one's source code, as knowledge about a formal system basically is a program that you can run, which basically is part of your source code (maybe with observed data, but then data became part of you -- what distinguishes you observing an event from the event observing you? -- it's more like merging). The important intuition in this case is that there is no transparency, that having a source code of a program is not at all the same thing as knowing how it behaves (it's not even about the halting problem, as simple calculations are still some computational steps away -- although static analysis (abstraction) may allow to run infinitely faster). You are not uncertain about your source code, you are uncertain about what it'll do. Logical hypotheticals can be seen as playing the central role in decision-making, as the steps in proof search that suggests the steps that one's own (known) algorithms could do, and seeing whether they should be made real ("winning", in games semantics terminology, which is highly misleading from goal-directed strategy point of view, as they only won your choice, not the "game"). While you can't reach some logical truths in a limited time, you can consider their hypothetical states, thus the program isn't so much being modified, as it is being refined where its consequences can't be directly observed (with naive formalism the difference between the program and its effect blurs). I still have serious gaps in my understanding of this stuff, so am not ready to describe it yet.
This doesn't seem to require slaughtering the intuition that "a logical truth couldn't be either way" because I can think that a logical truth couldn't be either way but I just don't know which way it is, and that still allows me to make the right decision. Do you agree, or do you still think that intuition needs to go?
If things that "could" be done or "could" happen are ones considered in hypotheticals during decision-making, then logical truths (possible behaviors of a program) should be comfortable as things that could be either way.
Followup to: Counterfactual Mugging.
Let's see what happens with Counterfactual Mugging, if we replace the uncertainty about an external fact of how a coin lands, with logical uncertainty, for example about what is the n-th place in the decimal expansion of pi.
The original thought experiment is as follows:
Let's change "coin came up tails" to "10000-th digit of pi is even", and correspondingly for heads. This gives Logical Counterfactual Mugging:
This form of Counterfactual Mugging may be instructive, as it slaughters the following false intuition, or equivalently conceptualization of "could": "the coin could land either way, but a logical truth couldn't be either way".
For the following, let's shift the perspective to Omega, and consider the problem about 10001th digit, which is 5 (odd). It's easy to imagine that given that the 10001th digit of pi is in fact 5, and you decided to only give away the $100 if the digit is odd, then Omega's prediction of your actions will still be that you'd give away $100 (because the digit is in fact odd). Direct prediction of your actions can't include the part where you observe that the digit is even, because the digit is odd.
But Omega doesn't compute what you'll do in reality, it computes what you would do if the 10001th digit of pi was even (which it isn't). If you decline to give away the $100 if the digit is even, Omega's simulation of counterfactual where the digit is even will say that you wouldn't oblige, and so you won't get the $10000 in reality, where the digit is odd.
Imagine it constructively this way: you have the code of a procedure, Pi(n), that computes the n-th digit of pi once it's run. If your strategy is
then, given that n==10001, Pi(10001)==5, and Is_Odd(5)==true, the program outputs "$100". But Omega tests what's the output of the code on which it performed a surgery, replacing Is_Odd(Pi(n)) by false instead of true to which it normally evaluates. Thus it'll be testing the code
This counterfactual case doesn't give away $100, and so Omega decides that you won't get the $10000.
For the original problem, when you consider what would happen if the coin fell differently, you are basically performing the same surgery, replacing the knowledge about the state of the coin in the state of mind. If you use the (wrong) strategy
and the coin comes up "heads", so that Omega is deciding whether to give you $10000, then Coin=="heads", but Omega is evaluating the modified algorithm where Coin is replaced by "tails":
Another way of intuitively thinking about Logical CM is to consider the index of the digit (here, 10000 or 10001) to be a random variable. Then, the choice of number n (value of the random variable) in Omega's question is a perfect analogy with the outcome of a coin toss.
With a random index instead of "direct" mathematical uncertainty, the above evaluation of counterfactual uses (say) 10000 to replace n (so that Is_Odd(Pi(10000))==false), instead of directly using false to replace Is_Odd(P(n)) with false:
The difference is that with the coin or random digit number, the parameter is explicit and atomic (Coin and n, respectively), while with the oddness of n-th digit, the parameter Is_Odd(P(n)) isn't atomic. How can it be detected in the code (in the mind) — it could be written in obfuscated assembly, not even an explicit subexpression of the program? By the connection to the sense of the problem statement itself: when you are talking about what you'll do if the n-th digit of pi is even or odd, or what Omega will do if you give or not give away $100 in each case, you are talking about exactly your Is_Odd(Pi(n)), or something from which this code will be constructed. The meaning of procedure Pi(n) is dependent on the meaning of the problem, and through this dependency counterfactual surgery can reach down and change the details of the algorithm to answer the counterfactual query posed by the problem.