All of Benya_Fallenstein's Comments + Replies

We should be more careful, though, about what we mean by saying that $\phi \left(x\right)$ only depends on ${Tr}_m$ for $m>n$, though, since this cannot be a purely syntactic criterion if we allow quantification over the subscript (as I did here). I'm pretty sure that something can be worked out, but I'll leave it for the moment.

I would suggest changing this system by defining $\psi \left(n\right)$ to mean that no $m\le n$ is the Gödel number of a proof of an inconsistency in ZFC (instead of just asserting that $n$ isn't). The purpose of this is to make it so that if ZFC were inconsistent, then we only end up talking about a finite number of levels of truth predicate. More specifically, I'd define $T_n$ to be PA plus the axiom schema

$$\forall m\ge n.\psi \left(m\right)\to \forall x.{Tr}_m(┌\phi (\overline{x})┐)\leftrightarrow \phi \left(x\right).$$

Then, it seems that Jacob Hilton's proof that the waterfalls are consistent goes through for this waterfall:

Work in ZFC and assume that ZFC is i

Hm; we could add an uninterpreted predicate symbol $Q\left(n\right)$ to the language of arithmetic, and let $s\equiv Q\left(0\right)$ and $r_n\equiv Q\left(\overline{n+1}\right)$. Then, it seems like the only barrier to recursive enumerability of $T_{\infty }$ is that $P$'s opinions about $Q(\cdot )$ aren't computable; this seems worrying in practice, since it seems certain that we would like logical uncertainty to be able to reason about the values of computations that use more resources than we use to compute our own probability estimates. But on the other hand, all of this makes this sound like an issue of self-reference,

The other direction follows from the fact that the algorithm is bounded, and PA can simply show the execution trace of $A$ in $\le CN$ steps.

Unimportant technical point: I think the length of the PA proof grows faster than this. (More precisely, the length in symbols, rather than the length in number of statements; we're almost always interested in the former, since it determines how quickly a proof can be checked or be found by exhaustive search.) The obvious way of showing $A\left(\right)=1$ in PA is to successively show for higher and higher $t$ that "after $t$ ticks, the T

Next, we consider the case that PA is consistent and work through the agent’s decision. PA can’t prove $A\left(\right)\ne 1$, since we used the chicken rule, so since the sentence $A\left(\right)=1\to U\left(\right)=5$ is easily provable, the sentence $A\left(\right)=1\to U\left(\right)=10$ (ie. the first sentence that the agents checks for proofs of) must be unprovable.

It seems like this argument needs soundness of PA, not just consistency of PA. Do you see a way to prove in PA that if $PA⊢A\left(\right)\ne 1$, then PA is inconsistent?

[edited to add:] However, your idea reminds me of my post on the odd counterfactuals of playing chicken

If you replace the inner "$=1$" by "$>1-ϵ$", then the literal thing you wrote follows from the reflection principle: Suppose that the outer probability is $<1$. Then

$$P\left[\right(a<P\left[\phi \right]<b)\wedge P[a-ϵ<P\left[\phi \right]<b+\epsilon ]\le 1-ϵ]>0.$$

Now, $P[a<P[\phi ]<b]>0$ implies $P[a\le P[\phi ]\le b]>0$, which by the converse of the outer reflection principle yields $a\le P\left[\phi \right]\le b$, whence $a-ϵ<P\left[\phi \right]<b+ϵ$. Now, by the forward direction of the outer reflection principle, we have

$$P[a-ϵ<P[\phi ]<b+ϵ]=1>1-ϵ,$$

which, by the outer reflection principle again, impl

This is very interesting!

My main question, which I didn't see an answer to on my first read, is: If the agent proves that action $a$ leads to the goal $G$ being achieved, are there any conditions under which this implies that the goal actually is achieved? The procrastination paradox shows that this isn't true in general. Is there a class of sentences (e.g., all ${\Pi }_1$ sentences, though I don't expect that to be true in this case) such that if $PA\star ⊢\phi$ then $N\models \phi$? In other words, do we have some guarantee that we do better at actually achieving $G$ than an agent which us

Categorization is hard! :-) I wanted to break it up because long lists are annoying to read, but there was certainly some arbitrariness in dividing it up. I've moved "resource gathering agent" to the odds & ends.

Want to echo Nate's points!

One particular thing that I wanted to emphasize is that I think you can see as a thread on this forum (in particular, the modal UDT work is relevant) is that it's useful to make formal toy models where the math is fully specified, so that you can prove theorems about what exactly an agent would do (or, sometimes, write a program that figures it out for you). When you write out things that explicitly, then, for example, it becomes clearer that you need to assume that a decision problem is "fair" (extensional) to get certain result

Some additions about how the initial system is going to work:

• Non-member contributions (comments and links) are going to become publicly visible when they have received 2 likes (from members---only members can like things).

• However, members will be able to reply to a contribution as soon as it has received 1 like. This means that if you think someone's made a useful contribution, and you want to reply to them about it, you don't have to wait for a second person to Like it before you can write that reply. (It won't be publicly visible until the contribution has two Likes, though.)

Yeah, that sounds good! Of course, by the Kripke levels argument, it's sufficient to consider $\varphi$'s of the form $\neg {\square }^n\perp$. And we might want to have a separate notion of "$i$ leads to $j$ at level $n$", which we can actually implement in a finite modal formula. This seems to suggest a version of modal UDT that tries to prove things in PA, then if that has ambiguous counterfactuals (i.e., it can't prove $A_i\to U_j$ for any $j$) we try PA+1 and so on up to some finite $n$; then we can hope these versions of UDT approximate optimality according to your revised version of "$i$ leads t

Fixed---thanks, Patrick!

Regarding the example, I earlier defined "action $i$ leads to outcome $j$" to mean the conjunction of $GL⊢A_i\to U_j$ and $GL⊬\neg A_i$; i.e., we check for spurious counterfactuals before believing that $GL⊢A_i\to U_j$ tells us something about what action $i$ leads to, and we only consider ourselves "fully informed" in this sense if we have non-spurious information for each $i$. (Of course, my follow-up post is about how that's still unsatisfactory; the reason to define this notion of "fully informative" so explicitly was really to be able to say more clearly i

(Thanks for the feedback!)

In our chat about this, Eliezer said that, aside from the difficulty of making a human-level mathematical philosophy engine aligned with our goals, an additional significant relevant disagreement with Paul is that Eliezer thinks it's likely that we'll use low-level self-improvement on the road to human-level AI; he used the analogies of programmers using compilers instead of writing machine code directly, and of EURISKO helping Lenat. (Again, hoping I'm not misrepresenting.)

This seems like a plausible scenario to me, but I'm not convinced it argues for the

...though although I'm guessing the variant of the reflective oracle discussed in the comment thread may be approximable, it seems less likely that a version of AIXI can be defined based on it that would be approximable.

Sorry for the delayed reply! I like this post, and agree with much of what you're saying. I guess I disagree with the particular line you draw, though; I think there's an interesting line, but it's at "is there a Turing machine which will halt and give the answer to this problem" rather than "is there a Turing machine which will spit out the correct answer for a large enough input (but will spit out wrong answers for smaller inputs, and you don't know what number is large enough)". The latter of these doesn't seem that qualitatively different to me from "i

I think the main disagreement is about whether it's possible to get an initial system which is powerful in the ways needed for your proposal and which is knowably aligned with our goals; some more about this in my reply to your post, which I've finally posted, though there I mostly discuss my own position rather than Eliezer's.

Actually, drnickbone's original LessWrong post introducing evil problems also gives an extension to the case you are considering: The evil decision problem gives the agent three or more options, and rewards the one that the "victim" decision theory assigns the least probability to (breaking ties lexicographically). Then, no decision theory can put probability $>1/N$ on the action that is rewarded in its probabilistic evil problem.

True. This looks to me like an effect of EDT not being stable under self-modification, although here the issue is handicapping itself through external means rather than self-modification---like, if you offer a CDT agent a potion that will make it unable to lift more than one box before it enters Newcomb's problem (i.e., before Omega makes its observation of the agent), then it'll cheerfully take it and pay you for the privilege.

Thread for proofs of results claimed above (not limited to stuff not found in Lindström); contributions appreciated. Stuff not in Lindström includes the uniqueness of arithmetic fixed points in PA (found in the modal agents paper), and I think the version of the fixed point theorem with more than one $F_i$ (the latter should be provable by iterated application of the fixed point theorem for a single $F$).

Thanks for expanding on your construction! I hadn't thought of the recursive construction, that's really neat.

I'm not that worried about the application to AIXI: unless I'm missing something, we can just additionally give our machines access to a double halting oracle (for ordinary Turing machines), and recover the same power. I considered doing that and didn't go with it because the stuff in my post seemed slightly more elegant, but if there's a reason to prefer the other version, it seems fine to use it.

I'm not clear on what you mean by "$P\left(O\right[X]$

Thanks! I didn't really think at all about whether or not "money-pump" was the appropriate word (I'm not sure what the exact definition is); have now changed "way to money-pump EDT agents" into "way to get EDT agents to pay you for managing the news for them".

About determining whether something's a query: A formulation of the statement we want to test is, (A) "for every (infinite) input on the oracle tape, and every $\epsilon >0$, there is a $T\in N$ such that with probability $>(1-\epsilon )$, the program halts in $\le T$ steps."

I think this is equivalent to, (B) "For every $\epsilon >0$, there is a $T\in N$ such that, for any input on the oracle tape, the program halts within $T$ timesteps with probability $>(1-\epsilon )$."

Reason why I think this is equivalent: Clearly (B) implies (A). Suppose that (B) is false; then

In the other direction, suppose that $\phi (m,n)$ is a primitive recursive predicate, and consider the following probabilistic Turing machine: First, randomly choose an $m\in N$ (placing positive probability on every natural number). Then, search exhaustively for an $n\in N$ such that $\phi (m,n)$ is true. If you find one, halt and output $1$. This machine is a query if and only if $\exists m.\forall n.\phi (m,n)$. Together with the parent comment, this shows that having an oracle that tells you whether or not something is a query is equivalent to having an oracle for ${\Pi }_2$ statements (i.e., a double h

Aagh... I'm conflicted. I really like the simplicity of having players correspond 1:1 to calls to the oracle, and their mixed strategies to the probability that the oracle returns "true", but the implication that the oracle must return the same answer if it's called twice on the same arguments during the execution of a single program interacts very badly with the intuitive picture of the applications I have in mind.

The intuitive picture is that the agents under consideration are living in a world whose laws of physics are probabilistic and allow for the co

Fixed the typo, thanks!

I considered describing the probabilities of the oracle returning "true" by a different function $\tau (┌M┐,p)$, but it seemed too pedantic to have a different letter. Maybe that's wrong, but it still feels too pedantic. If I do things that way I probably shouldn't be writing "$O(┌M┐,p)$ returns 'true' if...", though...

Thanks! I've been also thinking about making a finite version; my main motivation was that I've been hoping to take my still-incompletely-specified AIXI variant and find an analog variant of AIXItl, the computable version of AIXI that considers only hypotheses which terminate in time $t$ and whose source length is $<l$.

I think that would in fact be a pretty reasonable finite set of programs to use in what you're suggesting, since "we want it to terminate in time $t$" provides a motivation for why we would require programs to terminate surely, as opposed to al

Hm, I think it would be expectedly helpful to explain things more, but it would also take more time, and aiming much lower would take much more time. (That's part of why it's taking me so long to turn these things into research papers, although in that case the length limitations make the constraint even more difficult.) At the moment, I'm trying to get the things I'm working on out there at all, especially with something like this where I haven't yet worked through all the details of whether I can actually do my intended application based on it. After all

Thanks! Replied in a post.

A model of UDT with a halting oracle searches only for one utility value for each action. I'm guessing the other formulation just wasn't obvious at the time? (I don't remember realizing the possibility of playing chicken implicitly before Will Sawin advertised it to me, though I think he attributed it to you.)

Thanks! :-)

The reflective assignments correspond very directly to Nash equilibria (albeit in an $n$-to-$1$ manner, because given any finite game, a reflective assignment contains information about that game but also information about many other things). So I wouldn't quite say that they correspond to methods of equilibrium selection---e.g., if two methods of equilibrium selection give you the same Nash equilibrium, they're not distinguishable on the level of reflective assignments. But yeah, the question of what equilibrium gets played gets outsourced to the o

However, the approach is designed so that these "spurious" logical implications are unprovable, so they don’t interfere with decision-making. The proof of that is left as an easy exercise.

I don't think this is technically true as stated; it seems to be possible that the agent proves some spurious counterfactuals as long as the outcome it does in fact obtain is the best possible one. (This is of course harmless!) Say the agent has two possible actions, ${\overline{a}}^{\left(5\right)}$ and ${\overline{a}}^{\left(10\right)}$, leading to outcomes ${\overline{o}}^{\left(5\right)}$ and ${\overline{o}}^{\left(10\right)}$, respectively. The latter is preferred, and thes

I know this is supposed to be just introductory, but I actually think that the complete reformulation of UDT-with-a-halting-oracle in terms of modal logic is really interesting! For starters, it allows us to compare UDT and modal agents in the same framework (with the right $o$'s, we can see this version of UDT as a modal agent). It would also be really neat if we could write an "interpreter" that allows us to write UDT as a program calling a halting oracle, and then evaluate what it does by way of modal logic.

But also, it allows us to give a nice definition