Wiki Contributions

Comments

Apparently Eliezer decided to not take the time to read e.g. Quintin Pope's actual critiques, but he does have time to write a long chain of strawmen and smears-by-analogy.

A lot of Quintin Pope's critiques are just obviously wrong and lots of commenters were offering to help correct them. In such a case, it seems legitimate to me for a busy person to request that Quintin sorts out the problems together with the commenters before spending time on it. Even from the perspective of correcting and informing Eliezer, people can more effectively be corrected and informed if their attention is guided to the right place, with junk/distractions removed.

(Note: I mainly say this because I think the main point of the message you and Quintin are raising does not stand up to scrutiny, and so I mainly think the value the message can provide is in certain technical corrections that you don't emphasize as much, even if strictly speaking they are part of your message. If I thought the main point of your message stood up to scrutiny, I'd also think it would be Eliezer's job to realize it despite the inconvenience.)

I think this is especially clear with respect to our influence on what sort of future people will exist. Thus, consider again the example I discussed in earlier essay, of a boulder rolling towards a button that will create a Alice, paperclip-maximizer, but which can be diverted towards a button that will create Bob, who loves joy and beauty and niceness and so on, instead (and who loves life, as well, to a degree that makes him very much want to get-created if anyone has the chance to create him). Suppose that you choose to divert the boulder and create Bob instead of Alice. And suppose that you do so even without believing that an objectively-authoritative Tao endorses and legitimizes your choice.

Are you a tyrant? Have you "enslaved" Bob? I think Lewis's stated view answers yes, here, and that this is wrong. In particular: a thing you didn't do, here, is break into Alice's house while she was sleeping, and alter her brain to make her care about joy/beauty/niceness rather than paperclips.[16] Nor have you kept Bob in any chains, or as any prisoner following any triumphal car.

I object to this thought experiment on the same basis as the problem with the GLUT; "Bob, who loves joy and beauty and niceness and so on" is a high-information concept who would not have appeared by chance. Some process had to make Bob's details, and the tyranny/slavery/poultry-keeping could be attributed to this process, rather than to you who merely diverted a boulder and only contributed 1 bit of information.

In the context of natural impact regularization, it would be interesting to try to explore some @TurnTrout-style powerseeking theorems for subagents. (Yes, I know he denounces the powerseeking theorems, but I still like them.)

Specifically, consider this setup: Agent U starts a number of subagents S1, S2, S3, ..., with the subagents being picked according to U's utility function (or decision algorithm or whatever). Now, would S1 seek power? My intuition says, often not! If S1 seeks power in a way that takes away power from S2, that could disadvantage U. So basically S1 would only seek power in cases where it expects to make better use of the power than S2, S3, ....

Obviously this may be kind of hard for us to make use of if we are trying to make an AI and we only know how to make dangerous utility maximizers. But if we're happy with the kind of maximizers we can make on the first order (as seems to apply to the SOTA, since current methods aren't really utility maximizers) and mainly worried about the mesaoptimizers they might make, this sort of theorem would suggest that the mesaoptimizers would prefer staying nice and bounded.

Not sure this works constructively. x < y or x = y or x > y is valid for the constructive rationals, but taboo for the constructive reals. Wouldn't this make it taboo for the real order to be an elementary extension of the rational order? Not familiar with constructive model theory so not entirely sure.

If you have , then I think that's true, but if you just have  (where  is propositional truncation, basically quotienting by the relation that is always true, so collapsing the two sides to be indistinguishable), then the homotopy type book suggests that it might be wrong.

It's a bit similar to how the naive types-as-propositions encoding of the axiom of choice makes it trivially provable constructively, but a more careful encoding makes it imply excluded middle.

In Coq, the type of truth values is called Prop. In other foundations, it might be encoded differently, including by encoding functions into truth-values as functions out of an arbitrary type.

I guess to clean it up even further:

  • A set L is a lower real number when it is inhabited, downwards-closed and upwards-rounded.
  • A set U is an upper real number when it is inhabited, upwards-closed and downwards-rounded.
  • A closed interval [sup L, inf U] is constructed with a lower real L and an upper real U such that L < U.
  • A closed interval [sup L, inf U] is a real number if every rational interval x < y either has x < sup L or inf U < y.

People generally use "rounded" cuts when defining Dedekind cuts constructively. When a rounded cut defines a rational number, that rational number is included in neither the upper nor the lower set.

More formally, you can constructively define a closed interval of real numbers, potentially containing infinity, as follows:

  • U and L are sets of rationals
  • If x in L and y in U, then x < y
  • U is upwards-closed; for any x < y with x in U, y is in U
  • L is downwards-closed
  • U is downwards-rounded (open); for any x in U, there exists a y < x such that y is in U
  • L is upwards-rounded

This corresponds to a closed interval of real numbers that ranges from [sup L, inf U].

(Well, sort of. The bounds of this interval cannot actually be iteratively approximated. I think there are some contexts where you want that, because it means there are more intervals that are constructively definable. For instance this type of interval is closed under arbitrary intersections, whereas if the bounds could be approximated, it would not be closed under arbitrary intersections. It's one of those things where constructive math takes a concept and shatters it into multiple. But you regain iterative approximateability later as you force it to refer to just 1 real number.)

You can then force the interval to be finite by saying:

  • U is inhabited
  • L is inhabited

(If you want it to be only finite in one direction, you could have only one of these statements. Another option is to include "L is inhabited" but then drop the U set from your definition, in which case you get lower reals, which are useful in measure theory IIRC.)

Real numbers can then be identified with the closed intervals of zero width, which can be forced as follows:

  • For any x < y, either x is in L or y is in U

So basically if you have an approximation (x, y) in (L, U), you could e.g. take (2x+y)/3 < (x+2y)/3 and use this rule to tighten your bound.

Here U and L could be represented by functions A, B -> Q, but critically there would not be any straightforward functions back into A and B. The closest would be the final requirement, which could be taken to provide a function (x < y) -> A u B (strictly speaking one should probably have some appropriate quotients I'd guess), but if e.g. one of x and y is the actual value of the real number, then the function would always pick the answer corresponding to the other of the x and y.

Where B is the Boolean type.

Usually in defining Dedekind cuts, you'd use truth values rather than booleans for the codomain of indicator functions.

There's a ton of other nuances to real numbers in constructive math. For instance, Dedekind cuts defined by their lower bound, their upper bound, or both bounds are inequivalent (with both bounds being more appropriate in general, but lower bounds being useful sometimes in measure theory IIRC), and for Cauchy sequences you'd usually not just use CSRs but also Cauchy sequences of CSRs (and so on, recursively).

For a complete construction of the real numbers in constructive foundations, I recommend the Homotopy Type Theory book.

Showing that not every constructive Cauchy sequence corresponds to a constructive Dedekind cut

When constructed more carefully, every Cauchy sequence corresponds to a Dedekind cut, but it requires something stronger (such as excluded middle) to show that every Dedekind cut corresponds to a Cauchy sequence.

You can likely find contact with some students in an entirely different place who haven't heard of this experiment taking place, and ask them to find out.

Load More