All of Larry_D'Anna's Comments + Replies

"first-order logic cannot, in general, distinguish finite models from infinite models."

Specifically, if a fist order theory had arbitrarily large finite models, then it has an infinite one.

Did Ira Howard actually say that? In which story?

I'm getting Deja Vu again. Are you recycling bits of older posts or other things you've written?

Eliezer: have you given any thought to the problem of choosing a measure on the solution space? If you're going to count bits of optimization, you need some way of choosing a measure. In the real world solutions are not discrete and we cannot simply count them.

I swear to god I've read these Kasparov posts before...

I feel like I've read this exact post before. Deja Vu?

Moral questions are terminal. Ethical questions are instrumental.

I would argue that ethics are values that are instrumental, but treated as if they were terminal for almost all real object-level decisions. Ethics are a human cognitive shortcut. We need ethics because we can't really compute the expected cost of a black swan bet. An AI without our limitations might not need ethics. It might be able to keep all it's instrumental values in it's head as instrumental, without getting confused like we would.

"But it was PT:TLOS that did the trick. Here was probability theory, laid out not as a clever tool, but as The Rules, inviolable on pain of paradox"

I am unaware of a statement of Cox's theorem where the full technical statement of the theorem comes even close to this informal characterization. I'm not saying it doesn't exist, but PT:TLOS certainly doesn't do it.

I found the first two chapters of PT:TLOS to be absolutely, wretchedly awful. It's full of technical mistakes, crazy mischaracterizations of other people's opinions, hidden assumptions... (read more)

Eliezer, I think you have dissolved one of the most persistent and venerable mysteries: "How is it that even the smartest people can make such stupid mistakes".

Being smart just isn't good enough.

J Thomas
Larry, you have not proven that 6 would be a prime number if PA proved 6 was a prime number, because PA does not prove that 6 is a prime number.

No I'm afraid not. You clearly do not understand the ordinary meaning of implications in mathematics. "if a then b" is equivalent (in boolean logic) to ((not a) or b). They mean the exact same thing.

The claim that phi must be true because if it's true then it's true

I said no such thing. If you think I did then you do not know what the symbols I used mean.

It's simply and obviously bogus, and I... (read more)

J Thomas: "How is that useful?"

I'm just answering your question

"Can you prove that if PA proved 6 was a prime number then 6 would be a prime number? How would you do it?"

I'm not stating that proving implications with false antecedent is particularly useful, just that it is valid. Also aside from 6 being prime it is true that for any sentence phi, ZF |- "if PA |- phi then phi", but that ZF cannot even say, yet alone prove that "forall phi. if PA |- phi then phi". But it can prove "forall phi. if PA |- phi then N |= phi".

"But Larry, PA does not actually say that 6 is prime, and 6 is not prime."

Well of course 6 isn't prime. But if PA said it was, then it would be. There's nothing invalid about proving that A -> B if you know ~A. It's just not very useful. But for a somewhat less vacuous example, let RH be the riemann hypothesis. Then if PA |- RH then RH is true and if PA |- ~RH then RH is false. At least one of these implications has a false hypothesis, but they are both perfectly valid.

J Thomas:

Once more through the mill. If PA proves that 6 is a prime number, then 6 is really a prime number. Can you prove that if PA proved 6 was a prime number then 6 would be a prime number? How would you do it?

If PA |- "forall x y . x y = 6 => |x|=1 || |y|=1" then N |= "forall x y . x y = 6 => |x|=1 || |y|=1" (N = the natural numbers equiped with + and ) so for all x and y in N, N |= ",x ,y = 6 => |,x|=1 || |,y|=1" (where ,x means a constant symbol for x) if xy = 6 then N |= ",x ,y = 6" so theref... (read more)

Caledonian: That's relativism, right there - the idea that rightness is not only socially determined, but individually socially determined.

What!? That's just not what I said at all.

Richard: It seems to me that asking how is it that the word 'right' came to refer to rightness is like asking why 'green' means green, instead of meaning zebra.

The fact is that there is some concept that we've been calling "right", and though we don't exactly know what we mean by it, we're pretty certain it means something, and in some cases we know it when we see it.

It strikes me as unfair to accuse Eliezer of having his own private meaning of "right" that isn't in accordance with the common one, because hasn't endorsed a criterion or ... (read more)

Roko:

Eliezer decides to start using the symbol "c" to denote the real number 3*10^8.

No, he has continuously refused to spell out an explicit description of morality, because it admits no concise description. When Eliezer writes a list of values ending with "etcetera" he's saying (in your analogy) "c is 3*10^8, up to one significant digit".

Richard:

but others have pointed out that this reference fact is fixed by means of a seemingly 'relative' procedure

I think you are mixing meta-levels here. The seemingly relative procedure is used to describe morality in blog posts, not to chose what morality is in the first place.

Roko: It certainly is possible to opine that 22 is prime. Watch this:

22 is prime!

See, I did it. If you claim murder is right, then you aren't talking about something other than right, you are just making false statements about right.

@Roko

Also, Echoing Jadagul: as most people use the words, you're a moral relativist

Honestly I do not understand how you can continue calling Eliezer a relativist when he has persistently claimed that what is right doesn't depend on who's asking and doesn't depend on what anyone thinks is right.

Is anyone who does not believes in universally compelling arguments a relativist?

Is anyone who does not believe that morality is ontologically primitive a relativist?

Is anyone who does not believe that morality admits a concise description a relativist?

With these distinctions in mind, I hope my intent will be clearer, when I say that although I am human and have a human-ish moral framework, I do not think that the fact of acting in a human-ish way licenses anything.

hah. I was wondering what this Lob stuff had to do with morality.

good job on an excellent post.

simon:

To argue that a proof is being made concluding ?C using the assumption ?(◻C -> C) given the theory PA, to which proof we can apply the deduction theorem to get (PA |- "?(◻C -> C) -> ?C") (i.e. my interpretation of Löb's Theorem)

OK so the question marks are boxes right? In that case then yes, PA |- "?(?C -> C) -> ?C". This is OK. The contradiction comes if PA |- "(?C->C)->C". But morally this doesn't have anything to do with the deduction theorem. PA proves Lob because everything in the proo... (read more)

simon:

I was thinking that Löb's Theorem was a theorem in PA

It is a theorem about PA, although everything the statement and the proof of it can be expressed in PA if you like, in which case it is a theorem inside of PA about PA. There's no contradiction there, as long as you have everything quoted properly.

in which case the step going from PA + ?(?C -> C) |- ?(?L -> C) to PA + ?(?C -> C) |- ?(?(?L -> C)) seems legitimate given PA |- (?X -> ?(?X))

That's a valid deduction, but I don't think it's a step that anyone has written down ... (read more)

A puzzle: How can one rigorously construct Self-PA as recursively axiomatized first order theory in the language of PA?

simon: Let me explain some of the terminology here, because that may be where the confusion lies.

A scentence is a finite string symbols that satisfies a certain set of syntactic constraints.

A theory is a (possibly infinite) set of sentences. PA is a theory.

A proof from a theory T is a finite set of sentences, each of which is either an element of T, or follows from the ones before according to a fixed set of rules.

The notation PA + X, where X is a sentences is just the union of PA and {X}.

The notation PA |- Y means that a proof from PA that ends in Y ex... (read more)

Psy-Kosh: There are two points of view of where the flaw is.

My point view is that the flaw is here:

"Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C. Applying the Deduction Theorem to Löb's Theorem gives us, for all C: ((◻C)->C)->C"

Because, in fact Lob's Theorem is: (PA |- "◻C -> C") => (PA |- "C") and the Deduction theorem says (PA + X |- Y) => (PA |- "X->Y"). We don't have PA + X proving anything for any X. The deduction theorem just doesn't apply. The flaw is that the ... (read more)

"I just tested and anecdotally confirmed a hypothesis made with very little data: I suspected that neither Douglas Knight nor Larry D'Anna, the two who pinpointed 8 as the critical step, would be among the objectors to my metaethics. (Either of them can torpedo this nascent theory by stating otherwise.)"

I like your metaethics just fine.

Psy-Kosh: No that isn't the problem. If there is a proof that 1=2, then 1=2. If there isn't, then 1=2. Either way 1=2. The problem is the mixing of meta-levels / inappropriate use of the deduction theorem / tacit assumption that ◻a -> ◻b is the same as "a -> b".

Sebastian Hagen: no ◻X is PA |- "X". My best guess as to what Eliezer meant by "interpret the smiley face as saying.." is that he meant to interpret the cartoonproof as a proof from the assumption "(◻C -> C)" to the conclusion "C", rather than a proof from "◻(◻C -> C)" to "◻C".

Eliezer: "Larry, interpret the smiley face as saying:

PA + (◻C -> C) |-"

OK ignoring the fact that this is exactly what it doesn't say, I suppose we could notice that every step is surrounded at the top by a happy-face-says, so, if we may be inclined to think we can take those off and get a proof inside PA, starting with "◻C -> C" as a hypothesis. Lets see what happens.

1. ◻L <-> ◻(◻L -> C)
2. ◻C -> C

ok these are our hypothesis.

1. ◻(◻L->C) -> (◻◻L -> ◻C)

Modus Ponens works in PA, fine

1. ◻L -> (◻◻L -> ◻C)

or... (read more)

Eliezer: "Why doesn't the given proof of Lob's Theorem, the steps 1-10, show that PA + "◻C -> C" |- C?"

That's just not what it says. The hypothesis in step 2 isn't "◻C -> C" it's "◻(◻C -> C)". I suppose if the Hypothesis were "◻C -> C" we could try to find where it breaks. Step 7 is the only step that depends on 2 so it has to be there. Translating the amusing cartoons, we have

1. ◻(◻C -> C)
2. ◻(◻L -> ◻C)
3. ◻(◻L -> C)

Lets say that instead we have

2'. ◻C -> C

Well what are we supposed to do with it? We're stuck. Just because ◻C -> C doesn't mean that PA can prove it.

Robert: "You can only say (((◻C)->C)->(◻C))"

No that's not right. The theorem says that if PA proves "◻C -> C" then PA proves C. so that's ◻(◻C -> C) -> ◻C.

The flaw is that the deduction theorem does not cross meta levels. Eliezer says "Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C." and goes on to claim that (◻C->C)->C. But he's intentionally failed to use quotes and mixed up the meta levels here. Lob's Theorem does not give us a proof in first order logic from ((◻C)->C) to C. It gives us a proof that if there is a proof of ((◻C)->C) then there is a proof of C. Which is an entirely diffirent thing altogether.

Eliezer: "Any supposed analysis that does not tell you to mention a particular step, is inexact at best, and more probably mistaken."

I'm pretty sure my answer was completely correct. Care to point out the inexactness/mistakes?

oops that should be "what the deduction theorem really says"

The flaw is the instant you used the deduction theorem. You used it to go from

PA |- "◻C -> C" -> PA |- "C"

to

PA |- "(◻C->C) -> C"

What the induction theorem really says is

T + X |- Y implies T |- "X -> Y"

so what you really would have needed to apply the deduction theorm would have been

PA + "◻C -> C" |- C

do I win?

Roko: What the heck does morality have to do with category theory at all?

A related sense of "arbitrary", which is common in math and CS, is "could be anything, and will probably be chosen specifically to annoy you".

wikipedia on nets:

net or Moore-Smith sequence is a generalization of a sequence, intended to unify the various notions of limit and generalize them to arbitrary topological spaces.

Virge: Why is it "not the point"? In this discussion we are talking about differences in moral computation as implemented within individual humans. That the blind idiot's global optimization strategy defines homosexuality as a defect is of no relevance.

well because we're trying to characterize the sort of psychological diversity that can exist within our species. And this psychological unity argument is saying "we're all the same, except for a mix of one-step changes". This means that any complex adaptation in any human is in almost a... (read more)

Roko: I think Eliezer has explicitly stated that he is a realist.

Virge: The argument for psychological unity is that, as a sexually reproducing species, it is almost impossible for one gene to rise in relative frequency if the genes it depends on are not already nearly universal. So the all the diversity within any species at any given time consists of only one-step changes; no complex adaptations. The one exception of course is that males can have complex adaptations that females lack, and vice versa.

So, with respect to your specific examples:

Homosexuals: sexual preference certainly is a complex adaptation, but obvio... (read more)

Will Pearson: Why not just treat them as pure functions in the State monad?

Richard: You were correct. That is indeed the strongest pro-life argument I've ever read. And although it is quite wrong, the error is one of moral reasoning and not merely factual.

Richard: Abortion isn't a moral debate. The only reason people disagree about it is because some of them don't understand what souls are made of, and some of them do. Abortion is a factual debate about the nature of souls. If you know the facts, the moral conclusions are indisputable and obvious.

Roko: "And, of course, this lack of objectivity leads to problems, because different people will have their own notions of goodness."

Don't forget the psychological unity of mankind. Whatever is in our DNA that makes us care about morality at all is a complex adaptation, so it must be pretty much the same in all of us. That doesn't mean everyone will agree about what is right in particular cases, because they have considered different moral arguments (or in some cases, confused mores with morals), but that-which-responds-to-moral-arguments is the same.

@Tom McCabe: "Beware shutting yourself into a self-justifying memetic loop. If you had been born in 1800, and just recently moved here via time travel, would you have refused to listen to all of our modern anti-slavery arguments, on the grounds that no moral argument by negro-lovers could be taken seriously?"

Generally I think this is a valid point. One shouldn't lightly accuse a fellow human of being irredeemably morally broken, simply because they disagree with you on any particular conclusion. But in this particular case, I'm willing to take... (read more)

Tom McCabe: speaking as someone who morally disapproves of murder, I'd like to see the AI reprogram everyone back, or cryosuspend them all indefinitely, or upload them into a sub-matrix where they can think they're happily murdering each other without all the actual murder. Of course your hypothetical murder-lovers would call this imoral, but I'm not about to start taking the moral arguments of murder-lovers seriously. You just have to come to grips with the fact that the thing we call Morality isn't anything special from a global, physical perspective. ... (read more)

steven: your "not 100% sure" is a perfect example of the problem eliezer is trying to explain. "not 100% sure that X is false" is not a valid excuse to waste thought on X if the prior improbability of X is as incredibly tiny as it is for thoughts like "paperclip maximizers will find their own paperclip-related reasons not to murder everyone".

Roko: What would it even mean for an objective value to be implicit in the structure of the universe? I'm having a hard time imagining any physical situation where that would even make sense. And even if it did, it would still be you that decides to follow that value. Surely if you discovered an objective value implicit in the structure of the universe that commanded you to torture kittens, you would ignore it.

james andrix: we have to worry about what other Optimizers want, not just if they "think correctly". Evolution still manages to routinely defeat us without being able to think at all.

Caledonian: He isn't using "too-big" in the way you are interpreting it.

The point is not: Mindspace has a size X, X > Y, and any set of minds of size > Y cannot admit universal arguments.

The point is: For any putative universal argument you can cook up, I can cook up a mind design that isn't convinced by it.

The reason that we say it is too big is because there are subsets of Mindspace that do admit universally compelling arguments, such as (we hope) neurologically intact humans.

Roko: You think you can convince a paperclip maximizer to value human life? Or do you think paperclip maximizers are impossible?

"But my dear sir, if the fact of 2 + 3 = 5 exists somewhere outside your brain... then where is it?"

For some reason most mathematicians don't seem to feel this sort of ontological angst about what math really means or what it means for a mathematical statement to be true. I can't seem to articulate a single reason why this is, but let me say a few things that tend to wash away the angst.

• it doesn't matter "where it is", it is a proven consequence of our axioms.

• it is in every structure in the universe capable of representing integers

stephen: If we had a full understanding of fundamental physics then the only other a priori assumption we should need to derive the Born rule should be this: We aren't special. Our circumstances are typical. In other words: it is possible that at a fundamental physical level there is no Born rule and no reason one should expect a Born rule. But just by some fantastic coincidence, our little branch has followed the born rule all this time. In fact, we should expect it to stop following the Born rule immediately, for the same reason someone who's just ... (read more)