I'll copy more of my comment here then, with added links that explain some terms. (No credit to me for the post, I'm just interpreting the result.)
Basically, you've combined two previously existing ideas into an algorithm that's better than either of them alone. The first idea is that moral arguments with shorter proofs seem to capture some of what it means for a moral argument to be "natural", but it's flawed in that it's not clear how similar in complexity are the other moral arguments, and if it's a close call, then the distinction is not particularly natural. The second idea is to use the diagonal method to banish the spurious moral arguments beyond an arbitrary proof length, but its flaw is that we have to know the guarded proof length in advance.
With this algorithm, you're not just passively gauging the proof length, instead you take the first moral argument you come across, and then actively defend it against any close competition using the diagonal method.
This post requires some knowledge of decision theory math. Part of the credit goes to Vladimir Nesov.
Let the universe be a computer program U that returns a utility value, and the agent is a subprogram A within U that knows the source code of both A and U. (The same setting was used in the reduction of "could" post.) Here's a very simple decision problem:
def U():if A() == 1:
return 5
else:
return 10
The algorithm for A will be as follows:
The usual problem with such proof-searching agents is that they might stumble upon "spurious" proofs, e.g. a proof that A()==2 implies U()==0. If A finds such a proof and returns 1 as a result, the statement A()==2 becomes false, and thus provably false under any formal system; and a false statement implies anything, making the original "spurious" proof correct. The reason for constructing A this particular way is to have a shot at proving that A won't stumble on a "spurious" proof before finding the "intended" ones. The proof goes as follows:
Assume that A finds a "spurious" proof on step 1, e.g. that A()=2 implies U()=0. We have a lower bound on L, the length of that proof: it's likely larger than the length of U's source code, because a proof needs to at least state what's being proved. Then in this simple case 10^L steps is clearly enough to also find the "intended" proof that A()=2 implies U()=10, which combined with the previous proof leads to a similarly short proof that A()≠2, so the agent returns 2. But that can't happen if A's proof system is sound, therefore A will find only "intended" proofs rather than "spurious" ones in the first place.
Quote from Nesov that explains what's going on:
By analogy we can see that A coded with f(L)=10^L will correctly solve all our simple problems like Newcomb's Problem, the symmetric Prisoner's Dilemma, etc. The proof of correctness will rely on the syntactic form of each problem, so the proof may break when you replace U with a logically equivalent program. But that's okay, because "logically equivalent" for programs simply means "returns the same value", and we don't want all world programs that return the same value to be decision-theoretically equivalent.
A will fail on problems where "spurious" proofs are exponentially shorter than "intended" proofs (or even shorter, if f(L) is chosen to grow faster). We can probably construct malicious examples of decision-determined problems that would make A fail, but I haven't found any yet.