Intelligent Agent Foundations Forumsign up / log in
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 LINKS

NEW POSTS

NEW DISCUSSION POSTS

RECENT COMMENTS

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

Your confusion is because you
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

RSS

Privacy & Terms