by Sam Eisenstat 947 days ago | link | parent We can also construct an example where $${\rm PA} \vdash \phi \rightarrow \psi$$ with a short proof and $$\rm PA$$ also proves $$\phi \rightarrow \neg\psi$$, but any such proof is much longer. We only need to put a bound on the proof length in A’s proof search. Then, the argument that $${\tt A()} = 1 \wedge {\tt U()} \ne 0$$ proves its own consistency still works, and is rather short: $$O(\log n)$$ as the proof length bound $$n$$ increases. However, there cannot be a proof of $${\tt A()} = 1 \rightarrow {\tt U()} = 10$$ within $${\tt A}$$’s proof length bound, since if it found one it would immediately take action 1. In this case $$\rm PA$$ can still prove that $${\tt A()} = 1 \rightarrow {\tt U()} = 10$$ simply by running the agent, but this argument shows that any such proof must be long.

### NEW DISCUSSION POSTS

[Delegative Reinforcement
 by Vadim Kosoy on Stable Pointers to Value II: Environmental Goals | 1 like

Intermediate update: The
 by Alex Appel on Further Progress on a Bayesian Version of Logical ... | 0 likes

Since Briggs [1] shows that
 by 258 on In memoryless Cartesian environments, every UDT po... | 2 likes

This doesn't quite work. The
 by Nisan Stiennon on Logical counterfactuals and differential privacy | 0 likes

I at first didn't understand
 by Sam Eisenstat on An Untrollable Mathematician | 1 like

This is somewhat related to
 by Vadim Kosoy on The set of Logical Inductors is not Convex | 0 likes

This uses logical inductors
 by Abram Demski on The set of Logical Inductors is not Convex | 0 likes

Nice writeup. Is one-boxing
 by Tom Everitt on Smoking Lesion Steelman II | 0 likes

Hi Alex! The definition of
 by Vadim Kosoy on Delegative Inverse Reinforcement Learning | 0 likes

A summary that might be
 by Alex Appel on Delegative Inverse Reinforcement Learning | 1 like

I don't believe that
 by Alex Appel on Delegative Inverse Reinforcement Learning | 0 likes

This is exactly the sort of
 by Stuart Armstrong on Being legible to other agents by committing to usi... | 0 likes

When considering an embedder
 by Jack Gallagher on Where does ADT Go Wrong? | 0 likes

The differences between this
 by Abram Demski on Policy Selection Solves Most Problems | 1 like

Looking "at the very
 by Abram Demski on Policy Selection Solves Most Problems | 0 likes