"I design a cell to not fail and then assume it will and then ask the next 'what-if' questions," Sinnett said. "And then I design the batteries that if there is a failure of one cell it won't propagate to another. And then I assume that I am wrong and that it will propagate to another and then I design the enclosure and the redundancy of the equipment to assume that all the cells are involved and the airplane needs to be able to play through that."

—Mike Sinnett, Boeing's 787 chief project engineer

The game theory textbook "A Course in Microeconomic Theory" (Kreps) addresses this situation. Quoting from page 516:

We will give an exact analysis of this problem momentarily (in smaller type), but you should have no difficulty seeing the basic trade-off; too little punishment, triggered only rarely, will give your opponent the incentive to try to get away with the noncooperative strategy. You have to punish often enough and harshly enough so that your opponent is motivated to play [cooperate] instead of [defect]. But the more often/more harsh is the punishment, the less are the gains from cooperation. And even if you punish in a fashion that leads you to know that your opponent is (in her own interests) choosing [cooperate] every time (except when she is punishing), you will have to "punish" in some instances to keep your opponent honest.

Hmmmm. What do other people think of this idea?

I suspect one reason Eliezer did not do this is that when you make a long list of claims without any justification for them, it sounds silly and people don't pay attention to the rest of the sequence. But if you had first stepped them through the entire argument, they would have found no place at which they can really disagree. That's a concern, anyway.

Back when Eliezer was writing his metaethics sequence, it would have been great to know where he was going, i.e., if he had posted ahead of time a one-paragraph technical summary of the position he set out to explain. Can you post such a summary of your position now?

Now, citing axioms and theorems to justify a step in a proof is not a mere social convention to make mathematicians happy. It is a useful constraint on your cognition, allowing you to make only inferences that are actually valid.

When you are trying to build up a new argument, temporarily accepting steps of uncertain correctness can be helpful (if mentally tagged as such). This strategy can move you out of local optima by prompting you to think about what further assumptions would be required to make the steps correct.

Techniques based on this kind of reasoning are used in the simulation of physical systems and in machine inference more generally (tempering). Instead of exploring the state space of a system using the temperature you are actually interested in, which permits only very particular moves between states ("provably correct reasoning steps"), you explore using a higher temperature that makes it easier to move between different states ("arguments"). Afterwards, you check how probable the state is that you moved to when evaluated using the original temperature.

The web usability guru is Jakob Nielsen.

One possible solution would be a button present on every page that would toggle hyperlinks. If pressed, all hyperlinks would disappear. If pressed again, hyperlinks would come back. A 'reading mode' toggle.

The formalist school of math philosophy thinks that meaningful questions have to be phrased in terms of finite computational processes. But if you try to write a program for determining the truth value of "this statement is false", you'll see it recurses and never terminates:

def f():
return (not f())

See also Kleene-Rosser paradox. This may or may not dissolve the original question for you, but it works for me.

There's more to be said about the paradox because it keeps turning up in many contexts. For example, see Terry Tao's posts about "no self-defeating object". Also note that if we replace "truth" with "provability", the liar's paradox turns into Godel's first incompleteness theorem, and Curry's paradox turns into Löb's theorem.

ETA: see also Abram Demski's explanation of Kripke's fixed point theory here on LW, if that's your cup of tea.

I like that attitude. It is also not irrational because you are aware of it and deliberately choose to be that way. I believe that Less Wrong features a way too much ought. I don't disagree with the consensus on Cryonics at all, yet I'm not getting a contract because I'm too lazy and I like to be lazy. My usual credo is, I can't lose as long as I don't leave my way. That doesn't mean I am stubborn. I allow myself to alter my way situational.

Rationality is about winning and what constitutes winning is purely subjective. If you don't care if the universe is tiled with paperclips rather than being filled with apes having sex under the stars, that is completely rational as long as you are aware what exactly you care or don't care about.

If we want an AI to be friendly, the thing is to make sure that its utility function includes things that only humans can provide. That way, the AI will have to trade us what we want in order to get what it wants. The possibilities are endless. Give it a taste for romance novels, or cricket, or Jerry Springer. Stand-up comedy, postmodern deconstructionism, or lolcats. Electric power is one intriguing possibility.

The nice thing about having it give us what we want in trade, rather than simply giving us what it was programmed to believe we want, is that we are then permitted to change our minds about what we want, after we have already had a taste of material abundance and immortality. I certainly expect that my values will become revised after a few centuries of that, in ways that I am not yet ready to extrapolate or to have extrapolated for me.

I'm working on my ph.d. in program verification. Every problem we're trying to solve is as hard as the halting problem, and so we make the assumption, essentially, that we're operating over real programs: programs that humans are likely to write, and actually want to run. It's the only way we can get any purchase on the problem.

Trouble is, the field doesn't have any recognizable standard for what makes a program "human-writable", so we don't talk much about that assumption. We should really get a formal model, so we have some basis for expecting that a particular formal method will work well before we implement it... but that would be harder to publish, so no one in academia is likely to do it.