My "other" vote is alternate-day fasting, which I've been doing all year. Not sure if that's what you're looking for, but I feel like it's a dietary restriction, and benefits my health.

Homotopy type theory differs from ZFC in two ways. One way is that it, like ordinary type theory, is constructive and ZFC is not. The other is that it is based in homotopy theory. It is that latter property which makes it well suited for proofs *in homotopy theory* (and category theory). Most of the examples in slides you link to are about homotopy theory.

Tegmark is quite explicit that he has no measure and thus no prior. Switching foundations doesn't help.

It is that latter property which makes it well suited for proofs in homotopy theory (and category theory). Most of the examples in slides you link to are about homotopy theory.

I found a textbook after reading the slides, which may be clearer. I really don't think their mathematical aspirations are limited to homotopy theory, after reading the book's introduction--or even the small text blurb on the site:

Homotopy type theory offers a new “univalent” foundation of mathematics, in which a central role is played by Voevodsky’s univalence axiom and higher inductive types. The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning

the implied prior

Which implied prior? My understanding is that the problem with Multiverse theories is that we don't have a way to assign probability measures to the different possible universes, and therefore we cannot formulate an unambiguous prior distribution.

Well, I don't really math; but the way I understand it, *computable* universe theory suggests Solomonoff's Universal prior, while the ZFC-based *mathematical* universe theory--being a superset of the computable--suggests a larger prior; thus weirder anthropic expectations. Unless you need to be computable to be a conscious observer, in which case we're back to SI.

Apparently, founding mathematics on Homotopy Type Theory instead of ZFC makes automated proof checking much simpler and more elegant. Has anybody tried reformulating Max Tegmark's Level IV Multiverse using Homotopy Type Theory instead of sets to see if the implied prior fits our anthropic observations better?

This is the same as Schmidhuber's compression-based theory of aesthetics, right?

I'd be quite cautious about seeking greater media coverage without a plan to deal with an "Eternal September" on Less Wrong.

Hacker News had a semi-joking strategy, "everyone post articles on Haskell internals*" on days following media exposure. It actually seemed to work pretty well--but I don't know if we have enough posting volume, and enough un-posted articles on the mathematical side of decision theory and anthropics to use a similar strategy.

*(edit: it was Erlang internals; gjm's memory is better than mine).

Good questions. I'll explain my reasoning:

Basically, after thinking about consciousness for a while, and personal identity, I've come to assign high probability to some sort of dualism/idealism being true. It might still be a sort of reductionist dualism, i.e. platonic computations.

So yes, the "platonic computation" theory would count. Do you think my original post ought to be revised given this information? I hope I haven't been misleading.

As for spacetime and causation: If I'm a platonic form, I'm not in spacetime, nor am I causally related to my body in any normal sense. It all depends on how we define causation, and I tend to be reductionist/eliminativist about causation.

I hope I haven't been misleading.

I don't think you've been any more misleading than a dualist is pretty much required to be. The basic ambiguities of dualism do, of course, remain:

How does the non-spacetime stuff produce subjective experience, when spacetime stuff can't?

How does your subjective experience correlate with the environment and actions of your material body, just as if there were two-way causation going on? (even when you reduce causation to a Pearl-style net, or to the large-scale behavior of many individually time-reversible components, this question remains).

Quotes from the Screwtape Letters have not been terribly well-received in this thread. So, perversely, I decided I had to take a turn:

Do what you will, there is going to be some benevolence, as well as some malice, in your patient's soul. The great thing is to direct the malice to his immediate neighbours whom he meets every day and to thrust his benevolence out to the remote circumference, to people he does not know. The malice thus becomes wholly real and the benevolence largely imaginary. There is no good at all in inflaming his hatred of Germans if, at the same time, a pernicious habit of charity is growing up between him and his mother, his employer, and the man he meets in the train. Think of your man as a series of concentric circles, his will being the innermost, his intellect coming next, and finally his fantasy...you must keep on shoving all the virtues outward till they are finally located in the circle of fantasy, and all the desirable qualities inward into the Will. It is only in so far as they reach the will and are there embodied in habits that the virtues are really fatal to us.

-- The demon Screwtape, on how best to tempt a human being to destruction.

The existence of souls notwithstanding, Screwtape is clearly right: if you are charitable to almost everybody--except for those your see every day!--then you are not practicing the virtue of charity and are ill-served to imagine otherwise. You cannot fantasize good mental habits into being; they must be acted upon.

Who does more good with their life--the person who contributes a large amount of money to efficient charities while avoiding the people nearby, or the person who ignores anyone more than 100 miles away while being nice to his mother, his employer, and the man he meets in the train?

View more: Next

Since one big problem with neural nets is their lack of analyzability, this geometric approach to deep learning neural networks seems probably useful.