Happy New Year, everyone!

In the past few months I've been thinking several thoughts that all seem to point in the same direction:

1) People who live in developed Western countries usually make and spend much more money than people in poorer countries, but aren't that much happier. It feels like we're overpaying for happiness, spending too much money to get a single bit of enjoyment.

2) When you get enjoyment from something, the association between "that thing" and "pleasure" in your mind gets stronger, but at the same time it becomes less sensitive and requires more stimulus. For example if you like sweet food, you can get into a cycle of eating more and more food that's sweeter and sweeter. But the guy next door, who's eating much less and periodically fasting to keep the association fresh, is actually getting more pleasure from food than you are! The same thing happens when you learn to deeply appreciate certain kinds of art, and then notice that the folks who enjoy "low" art are visibly having more fun.

3) People sometimes get unrealistic dreams and endlessly chase them, like trying to "make it big" in writing or sports, because they randomly got rewarded for it at an early age. I wrote a post about that.

I'm not offering any easy answers here. But it seems like too many people get locked in loops where they spend more and more effort to get less and less happiness. The most obvious examples are drug addiction and video gaming, but also "one-itis" in dating, overeating, being a connoisseur of anything, striving for popular success, all these things follow the same pattern. You're just chasing after some Skinner-box thing that you think you "love", but it doesn't love you back.

Sooo... if you like eating, give yourself a break every once in a while? If you like comfort, maybe get a cold shower sometimes? Might be a good idea to make yourself the kind of person that can get happiness cheaply.

Sorry if this post is not up to LW standards, I typed it really quickly as it came to my mind.

I'm not sure if this post is very on-topic for LW, but we have many folks who understand Haskell and many folks who are interested in Löb's theorem (see e.g. Eliezer's picture proof), so I thought why not post it here? If no one likes it, I can always just move it to my own blog.

A few days ago I stumbled across a post by Dan Piponi, claiming to show a Haskell implementation of something similar to Löb's theorem. Unfortunately his code had a couple flaws. It was circular and relied on Haskell's laziness, and it used an assumption that doesn't actually hold in logic (see the second comment by Ashley Yakeley there). So I started to wonder, what would it take to code up an actual proof? Wikipedia spells out the steps very nicely, so it seemed to be just a matter of programming.

Well, it turned out to be harder than I thought.

One problem is that Haskell has no type-level lambdas, which are the most obvious way (by Curry-Howard) to represent formulas with propositional variables. These are very useful for proving stuff in general, and Löb's theorem uses them to build fixpoints by the diagonal lemma.

The other problem is that Haskell is Turing complete, which means it can't really be used for proof checking, because a non-terminating program can be viewed as the proof of any sentence. Several people have told me that Agda or Idris might be better choices in this regard. Ultimately I decided to use Haskell after all, because that way the post will be understandable to a wider audience. It's easy enough to convince yourself by looking at the code that it is in fact total, and transliterate it into a total language if needed. (That way you can also use the nice type-level lambdas and fixpoints, instead of just postulating one particular fixpoint as I did in Haskell.)

But the biggest problem for me was that the Web didn't seem to have any good explanations for the thing I wanted to do! At first it seems like modal proofs and Haskell-like languages should be a match made in heaven, but in reality it's full of subtle issues that no one has written down, as far as I know. So I'd like this post to serve as a reference, an example approach that avoids all difficulties and just works.

LW user lmm has helped me a lot with understanding the issues involved, and wrote a candidate implementation in Scala. The good folks on /r/haskell were also very helpful, especially Samuel Gélineau who suggested a nice partial implementation in Agda, which I then converted into the Haskell version below.

To play with it online, you can copy the whole bunch of code, then go to CompileOnline and paste it in the edit box on the left, replacing what's already there. Then click "Compile & Execute" in the top left. If it compiles without errors, that means everything is right with the world, so you can change something and try again. (I hate people who write about programming and don't make it easy to try out their code!) Here we go:

main = return ()

-- Assumptions

data Theorem a

logic1 = undefined :: Theorem (a -> b) -> Theorem a -> Theorem b
logic2 = undefined :: Theorem (a -> b) -> Theorem (b -> c) -> Theorem (a -> c)
logic3 = undefined :: Theorem (a -> b -> c) -> Theorem (a -> b) -> Theorem (a -> c)

data Provable a

rule1 = undefined :: Theorem a -> Theorem (Provable a)
rule2 = undefined :: Theorem (Provable a -> Provable (Provable a))
rule3 = undefined :: Theorem (Provable (a -> b) -> Provable a -> Provable b)

data P

premise = undefined :: Theorem (Provable P -> P)

data Psi

psi1 = undefined :: Theorem (Psi -> (Provable Psi -> P))
psi2 = undefined :: Theorem ((Provable Psi -> P) -> Psi)

-- Proof

step3 :: Theorem (Psi -> Provable Psi -> P)
step3 = psi1

step4 :: Theorem (Provable (Psi -> Provable Psi -> P))
step4 = rule1 step3

step5 :: Theorem (Provable Psi -> Provable (Provable Psi -> P))
step5 = logic1 rule3 step4

step6 :: Theorem (Provable (Provable Psi -> P) -> Provable (Provable Psi) -> Provable P)
step6 = rule3

step7 :: Theorem (Provable Psi -> Provable (Provable Psi) -> Provable P)
step7 = logic2 step5 step6

step8 :: Theorem (Provable Psi -> Provable (Provable Psi))
step8 = rule2

step9 :: Theorem (Provable Psi -> Provable P)
step9 = logic3 step7 step8

step10 :: Theorem (Provable Psi -> P)
step10 = logic2 step9 premise

step11 :: Theorem ((Provable Psi -> P) -> Psi)
step11 = psi2

step12 :: Theorem Psi
step12 = logic1 step11 step10

step13 :: Theorem (Provable Psi)
step13 = rule1 step12

step14 :: Theorem P
step14 = logic1 step10 step13

-- All the steps squished together

lemma :: Theorem (Provable Psi -> P)
lemma = logic2 (logic3 (logic2 (logic1 rule3 (rule1 psi1)) rule3) rule2) premise

theorem :: Theorem P
theorem = logic1 lemma (rule1 (logic1 psi2 lemma))

To make sense of the code, you should interpret the type constructor Theorem as the symbol ⊢ from the Wikipedia proof, and Provable as the symbol ☐. All the assumptions have value "undefined" because we don't care about their computational content, only their types. The assumptions logic1..3 give just enough propositional logic for the proof to work, while rule1..3 are direct translations of the three rules from Wikipedia. The assumptions psi1 and psi2 describe the specific fixpoint used in the proof, because adding general fixpoint machinery would make the code much more complicated. The types P and Psi, of course, correspond to sentences P and Ψ, and "premise" is the premise of the whole theorem, that is, ⊢(☐P→P). The conclusion ⊢P can be seen in the type of step14.

As for the "squished" version, I guess I wrote it just to satisfy my refactoring urge. I don't recommend anyone to try reading that, except maybe to marvel at the complexity :-)

EDIT: in addition to the previous Reddit thread, there's now a new Reddit thread about this post.

My beliefs about the integers are a little fuzzy. I believe the things that ZFC can prove about the integers, but there seems to be more than that. In particular, I intuitively believe that "my beliefs about the integers are consistent, because the integers exist". That's an uncomfortable situation to be in, because we know that a consistent theory can't assert its own consistency.

Should I conclude that my beliefs about the integers can't be covered by any single formal theory? That's a tempting line of thought, but it reminds me of all these people claiming that the human mind is uncomputable, or that humans will always be smarter than machines. It feels like being on the wrong side of history.

It's also dangerous to believe that "the integers exist" due to my having clear intuitions about them, because humans sometimes make mistakes. Before Russell's paradox, someone could be forgiven for thinking that the objects of naive set theory "exist" because they have clear intuitions about sets, but they would be wrong nonetheless.

Let's explore the other direction instead. What if there was some way to extrapolate my fuzzy beliefs about the integers? In full generality, the outcome of such a process should be a Turing machine that prints sentences about integers which I believe in. Such a machine would encode some effectively generated theory about the integers, which we know cannot assert its own consistency and be consistent at the same time.

So it seems that in the process of extracting my "consistent extrapolated beliefs", something has to give. At some point, my belief in my own consistency has to go, if I want the final result to be consistent.

But if I already know that much about the outcome, it might make sense for me to change my beliefs now, and end up with something like this: "All my beliefs about the integers follow from some specific formal theory that I don't know yet. In particular, I don't believe that my beliefs about the integers are consistent."

I'm not sure if there are gaps in the above reasoning, and I don't know if using probabilistic reflection changes the conclusions any. What do you think?

Hal Finney has just died.

http://lists.extropy.org/pipermail/extropy-chat/2014-August/082585.html

http://lesswrong.com/lw/1ab/dying_outside/

I'm very sad to see him go.

This post doesn't contain any new ideas that LWers don't already know. It's more of an attempt to organize my thoughts and have a writeup for future reference.

Here's a great quote from Sam Hughes, giving some examples of good and bad advice:

"You and your gaggle of girlfriends had a saying at university," he tells her. "'Drink through it'. Breakups, hangovers, finals. I have never encountered a shorter, worse, more densely bad piece of advice." Next he goes into their bedroom for a moment. He returns with four running shoes. "You did the right thing by waiting for me. Probably the first right thing you've done in the last twenty-four hours. I subscribe, as you know, to a different mantra. So we're going to run."

The typical advice given to young people who want to succeed in highly competitive areas, like sports, writing, music, or making video games, is to "follow your dreams". I think that advice is up there with "drink through it" in terms of sheer destructive potential. If it was replaced with "don't bother following your dreams" every time it was uttered, the world might become a happier place.

The amazing thing about "follow your dreams" is that thinking about it uncovers a sort of perfect storm of biases. It's fractally wrong, like PHP, where the big picture is wrong and every small piece is also wrong in its own unique way.

The big culprit is, of course, optimism bias due to perceived control. I will succeed because I'm me, the special person at the center of my experience. That's the same bias that leads us to overestimate our chances of finishing the thesis on time, or having a successful marriage, or any number of other things. Thankfully, we have a really good debiasing technique for this particular bias, known as reference class forecasting, or inside vs outside view. What if your friend Bob was a slightly better guitar player than you? Would you bet a lot of money on Bob making it big like Jimi Hendrix? The question is laughable, but then so is betting the years of your own life, with a smaller chance of success than Bob.

That still leaves many questions unanswered, though. Why do people offer such advice in the first place, why do other people follow it, and what can be done about it?

Survivorship bias is one big reason we constantly hear successful people telling us to "follow our dreams". Successful people doesn't really know why they are successful, so they attribute it to their hard work and not giving up. The media amplifies that message, while millions of failures go unreported because they're not celebrities, even though they try just as hard. So we hear about successes disproportionately, in comparison to how often they actually happen, and that colors our expectations of our own future success. Sadly, I don't know of any good debiasing techniques for this error, other than just reminding yourself that it's an error.

When someone has invested a lot of time and effort into following their dream, it feels harder to give up due to the sunk cost fallacy. That happens even with very stupid dreams, like the dream of winning at the casino, that were obviously installed by someone else for their own profit. So when you feel convinced that you'll eventually make it big in writing or music, you can remind yourself that compulsive gamblers feel the same way, and that feeling something doesn't make it true.

Of course there are good dreams and bad dreams. Some people have dreams that don't tease them for years with empty promises, but actually start paying off in a predictable time frame. The main difference between the two kinds of dream is the difference between positive-sum games, a.k.a. productive occupations, and zero-sum games, a.k.a. popularity contests. Sebastian Marshall's post Positive Sum Games Don't Require Natural Talent makes the same point, and advises you to choose a game where you can be successful without outcompeting 99% of other players.

The really interesting question to me right now is, what sets someone on the path of investing everything in a hopeless dream? Maybe it's a small success at an early age, followed by some random encouragement from others, and then you're locked in. Is there any hope for thinking back to that moment, or set of moments, and making a little twist to put yourself on a happier path? I usually don't advise people to change their desires, but in this case it seems to be the right thing to do.

In decision theory, we often talk about programs that know their own source code. I'm very confused about how that theory applies to people, or even to computer programs that don't happen to know their own source code. I've managed to distill my confusion into three short questions:

1) Am I uncertain about my own source code?

2) If yes, what kind of uncertainty is that? Logical, indexical, or something else?

3) What is the mathematically correct way for me to handle such uncertainty?

Don't try to answer them all at once! I'll be glad to see even a 10% answer to one question.

This post was inspired by Benja's SUDT post. I'm going to describe another simplified model of UDT which is equivalent to Benja's proposal, and is based on standard game theory concepts as described in this Wikipedia article.

First let's define what is a "single player extensive-form game with chance moves and imperfect information":

1. A "single player extensive-form game" is a tree of nodes. Each leaf node is a utility value. A play of the game starts at the root and ends at some leaf node.
2. Some non-leaf nodes are "chance nodes", with probabilities assigned to branches going out of that node. All other non-leaf nodes are "decision nodes", where the player can choose which branch to take. (Thanks to badger for helping me fix an error in this part!)
3. "Imperfect information" means the decision nodes are grouped into "information sets". The player doesn't know which node they're currently at, only which information set it belongs to.
4. "Imperfect recall" is a special case of imperfect information, where knowing the current information set doesn't even allow the player to figure out which information sets were previously visited, like in the Absent-Minded Driver problem.
5. We will assume that the player can use "behavioral strategies", where the player can make a random choice at each node independently, rather than "mixed strategies", which randomize over the set of pure strategies for the entire game. See Piccione and Rubinstein's paper for more on this difference. (Thanks to Coscott for pointing out that assumption!)
6. The behavioral strategy with the highest expected utility will be taken as the solution of the game.

Now let's try using that to solve some UDT problems:

Absent-Minded Driver is the simplest case, since it's already discussed in the literature as a game of the above form. It's strange that not everyone agrees that the best strategy is indeed the best, but let's skip that and move on.

Psy-Kosh's non-anthropic problem is more tricky, because it has multiple players. We will model it as a single-player game anyway, putting the decision nodes of the different players in sequence and grouping them together into information sets in the natural way. The resulting game tree is complicated, but the solution is the same as UDT's. As a bonus, we see that our model does not need any kind of anthropic probabilities, because it doesn't specify or use the probabilities of individual nodes within an information set.

Wei Dai's coordination problem is similar to the previous one, but with multiple players choosing different actions based on different information. If we use the same trick of folding all players into one, and group the decision nodes into information sets in the natural way, we get the right solution again. It's nice to see that our model automatically solves problems that require Wei's "explicit optimization of global strategy".

Counterfactual Mugging is even more tricky, because writing it as an extensive-form game must include a decision node for Omega's simulation of the player. Some people are okay with that, and our model gives the right solution. But others feel that it leads to confusing questions about the nature of observation. For example, what if Omega used a logical coin, and the player could actually check which way the coin came up by doing a long calculation? Paying up is still the right decision (I think we solved that problem in September), but our model here doesn't have enough detail.

Finally, Agent Simulates Predictor is the kind of problem that cannot be captured by our model at all, because logical uncertainty is the whole point of ASP.

It's instructive to see the difference between the kind of UDT problems that fit our model and those that require something more. Also it would be easy to implement the model as a computer program, and solve some UDT problems automatically. (Though the exercise wouldn't have much scientific value, because extensive-form games are a well known idea.) In this way it's a little similar to Patrick's work on modal agents, which made certain problems solvable on the computer by using modal logic instead of enumerating proofs. Now I wonder if other problems that involve logical uncertainty could also be solved by some simplified model?

In physical science the first essential step in the direction of learning any subject is to find principles of numerical reckoning and practicable methods for measuring some quality connected with it. I often say that when you can measure what you are speaking about, and express it in numbers, you know something about it; but when you cannot measure it, when you cannot express it in numbers, your knowledge is of a meagre and unsatisfactory kind; it may be the beginning of knowledge, but you have scarcely in your thoughts advanced to the state of Science, whatever the matter may be.

-- Lord Kelvin

If you believe that science is about describing things mathematically, you can fall into a strange sort of trap where you come up with some numerical quantity, discover interesting facts about it, use it to analyze real-world situations - but never actually get around to measuring it. I call such things "theoretical quantities" or "fake numbers", as opposed to "measurable quantities" or "true numbers".

An example of a "true number" is mass. We can measure the mass of a person or a car, and we use these values in engineering all the time. An example of a "fake number" is utility. I've never seen a concrete utility value used anywhere, though I always hear about nice mathematical laws that it must obey.

The difference is not just about units of measurement. In economics you can see fake numbers happily coexisting with true numbers using the same units. Price is a true number measured in dollars, and you see concrete values and graphs everywhere. "Consumer surplus" is also measured in dollars, but good luck calculating the consumer surplus of a single cheeseburger, never mind drawing a graph of aggregate consumer surplus for the US! If you ask five economists to calculate it, you'll get five different indirect estimates, and it's not obvious that there's a true number to be measured in the first place.

Another example of a fake number is "complexity" or "maintainability" in software engineering. Sure, people have proposed different methods of measuring it. But if they were measuring a true number, I'd expect them to agree to the 3rd decimal place, which they don't :-) The existence of multiple measuring methods that give the same result is one of the differences between a true number and a fake one. Another sign is what happens when two of these methods disagree: do people say that they're both equally valid, or do they insist that one must be wrong and try to find the error?

It's certainly possible to improve something without measuring it. You can learn to play the piano pretty well without quantifying your progress. But we should probably try harder to find measurable components of "intelligence", "rationality", "productivity" and other such things, because we'd be better at improving them if we had true numbers in our hands.

Here's an internal dialogue I just had.

Q: How do we test rationality skills?

A: We haven't come up with a comprehensive test yet.

Q: Maybe we can test some part of rationality?

A: Sure. For example, you could test resistance to akrasia by making two contestants do some simple chores every day. The one who fails first, loses.

Q: That seems like a pointless competition. If I'm feeling competitive, why would I ever skip the chores and lose?

A: Whoa, wait. If competitiveness can cure akrasia, that's pretty cool!

Now we just need to figure out how to make people more competitive in the areas they care about...

Many people believe that Bayesian probability is an exact theory of uncertainty, and other theories are imperfect approximations. In this post I'd like to tentatively argue the opposite: that Bayesian probability is an imperfect approximation of what we want from a theory of uncertainty. This post won't contain any new results, and is probably very confused anyway.

I agree that Bayesian probability is provably the only correct theory for dealing with a certain idealized kind of uncertainty. But what kinds of uncertainty actually exist in our world, and how closely do they agree with what's needed for Bayesianism to work?

In a Tegmark Level IV world (thanks to pragmatist for pointing out this assumption), uncertainty seems to be either indexical or logical. When I flip a coin, the information in my mind is either enough or not enough to determine the outcome in advance. If I have enough information - if it's mathematically possible to determine which way the coin will fall, given the bits of information that I have received - then I have logical uncertainty, which is no different in principle from being uncertain about the trillionth digit of pi. On the other hand, if I don't have enough information even given infinite mathematical power, it implies that the world must contain copies of me that will see different coinflip outcomes (if there was just one copy, mathematics would be able to pin it down), so I have indexical uncertainty.

The trouble is that both indexical and logical uncertainty are puzzling in their own ways.

With indexical uncertainty, the usual example that breaks probabilistic reasoning is the Absent-Minded Driver problem. When the probability of you being this or that copy depends on the decision you're about to make, these probabilities are unusable for decision-making. Since Bayesian probability is in large part justified by decision-making, we're in trouble. And the AMD is not an isolated problem. In many imaginable situations faced by humans or idealized agents, there's a nonzero chance of returning to the same state of mind in the future, and that chance slightly depends on the current action. To the extent that's true, Bayesian probability is an imperfect approximation.

With logical uncertainty, the situation is even worse. We don't have a good theory of how logical uncertainty should work. (Though there have been several attempts, like Benja and Paul's prior, Manfred's prior, or my own recent attempt.) Since Bayesian probability is in large part justified by having perfect agreement with logic, it seems likely that the correct theory of logical uncertainty won't look very Bayesian, because the whole point is to have limited computational resources and only approximate agreement with logic.

Another troubling point is that if Bayesian probability is suspect, the idea of "priors" becomes suspect by association. Our best ideas for decision-making under indexical uncertainty (UDT) and logical uncertainty (priors over theories) involve some kind of priors, or more generally probability distributions, so we might want to reexamine those as well. Though if we interpret a UDT-ish prior as a measure of care rather than belief, maybe the problem goes away...