= 27d567bc2d48d9f40e9ccc20ea370b15)
khafra comments on Open thread, 24-30 March 2014 - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (156)
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?
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.
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:
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.
The two usual implied prior taken from Level IV are a)that every possible universe is equally likely and b)that universe are likely in direct proportion to the simplicity of their description. Some attempts have been made to show that the second falls out of the first.