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.
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
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.
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.
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?
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.
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.
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.