A model of UDT without proof limits

I found myself wondering if there are any results about the length of the shortest proof in which a proof system can reach a contradiction, and found the following papers:

Paper 1 talks about partial consistency. We have statements of the following form:

) is a statement that there is no ZF-proof of contradiction with length =< n.

The paper claims that this is provable in ZF for each n. The paper then discusses results about the proof length of the partial consistency statements is polynomial in n. The author goes on to derive analogous results pertaining to frege proof systems weaker than ZF.

From these results it may be possible to have the agent's proof system produce a partial consistency result for a stipulated length.

Paper 2 shows that the question of whether a formula has a proof of length no more than k is undecidable.

Both papers seem relevant, but I don't presently have the time to think them through carefully.

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.

I'm not sure why do you need a fast-growing function at all? It seems, L+1 would work just as well. Proofs longer than L are not considered in Step 1, and if Step 2 ensures that no spurious proof is found for length <=L, then the agent should be fine. Shouldn't it?

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.

If A's proof system is sound, that directly implies that A won't generate "spurious" proofs. I don't see the point of deriving this from the fact that "spurious" proofs lead to contradictions.

It seems like step 2 is just validating that proofs are correct, and when it finds a problem, it doesn't seem to do anything good about it. What is the point?

Another thing is that I don't think spurious proofs can have influence on the decision in any case.

Take the simpler algorithm B:

1. Search for proofs of statements of the form "B()=b implies U()=u". Upon finding at least one proof for each possible b, go to step 2.
2. Return the best b found on step 1.

A spurious proof is one for b where B()≠b.

By definition, the result returned in step 2 will be B(). Therefore B() is the best b found in step 1. Since B()=b for the best b, this can not be from a spurious proof. If for any other b' there is a spurious proof, then the proved utilities must be worse, since otherwise B() would equal c. Therefore the existence of spurious proofs does not affect B at all.

Why do you need statements of the form "A()==a implies U()==u" instead of "U(a)==u"? Or if you insist that A is a function, those of the form "U(()↦a)==u".

Then A would of course just pick the action with the highest (provable) utility.

The difference is that you no longer have need to prove things about A inside A, which is impossible.

def U(A):
    if predict(A) == 1:
        box1 = 1000, box2 = 1000000
    else:
        box1 = 1000, box2 = 0
    if A() == 1:
        return box2
    else:
        return box1+box2

Doesn't this totally kill the idea of resolving ASP by having the agent prove something about its own actions in less than N steps (for N<<L), that got posted last week?

What happens with U() like this:

def U():
if(A()==1 and every Goodstein sequence terminates at 0) return 10
else if(A()==2) return 1
else return 5

How the hell will it find proof that U() returns 100 if U() does not have 100 in a single return statement, and clearly can only return 5 or 10? Or are you meaning 10 here? Still, how it can find such proof with any but a very broken proof system?

It seems to me that even a very simple set of axioms will allow it to treat A() as a black box that returns x here, arriving at correct proof that if x=1 then U()=5 , without ever recursing into itself. When i have to make bots in game do something, i dont make bots emulate bots, i just say, x is the every bot's output in those circumstances, then apply algebra to find x from equation that got x on both sides.

edit: furthermore, the proof systems that can prove a contradiction, can prove anything.

I guess i miss something about decision theories. I, basically, do applied math for a living, meaning that I do decisions using math, in the domain where it works. First thing I do when I need to get rid of recursion, is turn this into an equation with x (or many unknowns). You just treat the bot as black box, which outputs the value that the bot outputs. Then, you can arrive at equation with one solution or many solutions or infinitely many solutions. I don't need to secondguess myself by running myself in emulator. Black-box unknown works fine.