by Sam Eisenstat 823 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

What does the Law of Logical
 by Alex Appel on Smoking Lesion Steelman III: Revenge of the Tickle... | 0 likes

To quote the straw vulcan:
 by Stuart Armstrong on Hyperreal Brouwer | 0 likes

I intend to cross-post often.
 by Scott Garrabrant on Should I post technical ideas here or on LessWrong... | 1 like

I think technical research
 by Vadim Kosoy on Should I post technical ideas here or on LessWrong... | 2 likes

I am much more likely to miss
 by Abram Demski on Should I post technical ideas here or on LessWrong... | 1 like

Note that the problem with
 by Vadim Kosoy on Open Problems Regarding Counterfactuals: An Introd... | 0 likes

Typos on page 5: *
 by Vadim Kosoy on Open Problems Regarding Counterfactuals: An Introd... | 0 likes

Ah, you're right. So gain
 by Abram Demski on Smoking Lesion Steelman | 0 likes

> Do you have ideas for how
 by Jessica Taylor on Autopoietic systems and difficulty of AGI alignmen... | 0 likes

I think I understand what
 by Wei Dai on Autopoietic systems and difficulty of AGI alignmen... | 0 likes

>You don’t have to solve
 by Wei Dai on Autopoietic systems and difficulty of AGI alignmen... | 0 likes

 by Vadim Kosoy on Delegative Inverse Reinforcement Learning | 0 likes

My confusion is the
 by Tom Everitt on Delegative Inverse Reinforcement Learning | 0 likes

> First of all, it seems to
 by Abram Demski on Smoking Lesion Steelman | 0 likes

> figure out what my values
 by Vladimir Slepnev on Autopoietic systems and difficulty of AGI alignmen... | 0 likes