The ordinal formalism turned out to be erroneous (see remark I added in beginning of post). Regarding the oracle version of “usual” parametric polymorphism, it is in a way closer to Marcello’s waterfall than to the original parametric polymorphism: it doesn’t “lose proof strength” but it is vulnerable to the procrastination paradox. On the other hand I don’t think the procrastination paradox is a severe problem, it only means you need to require your utility function to be semicontinuous wrt the product topology of the set of possible universes, where the product is over time slices. Also, the oracle formalism has an advantage over Marcello’s waterfall in that it doesn’t rely on an arbitrary choice of unprovable formula.
Sidenote: Is a workshop planned sometime soon? It would be very interesting for me to attend and exchange ideas with other people.
Benja and I have been pretty busy writing papers and attending some non-MIRI workshops. Eventually, we’ll get back around to feeling out this system, but I have not had the time to go back through your posts in depth so as to understand the motivation. It will take me some time and effort to give your system the attention it deserves, and I still haven’t been able to find that time :-)
There aren’t any workshops coming up in the immediate future, but did you hear about MIRIx workshops? If you set up a your own local workshop, MIRI can reimburse certain expenses and may even send a researcher to the first workshop to give tutorials and/or chat, depending on the situation.
Hi, haven’t heard from you for a while.
The ordinal formalism turned out to be erroneous (see remark I added in beginning of post). Regarding the oracle version of “usual” parametric polymorphism, it is in a way closer to Marcello’s waterfall than to the original parametric polymorphism: it doesn’t “lose proof strength” but it is vulnerable to the procrastination paradox. On the other hand I don’t think the procrastination paradox is a severe problem, it only means you need to require your utility function to be semicontinuous wrt the product topology of the set of possible universes, where the product is over time slices. Also, the oracle formalism has an advantage over Marcello’s waterfall in that it doesn’t rely on an arbitrary choice of unprovable formula.
Sidenote: Is a workshop planned sometime soon? It would be very interesting for me to attend and exchange ideas with other people.
Benja and I have been pretty busy writing papers and attending some non-MIRI workshops. Eventually, we’ll get back around to feeling out this system, but I have not had the time to go back through your posts in depth so as to understand the motivation. It will take me some time and effort to give your system the attention it deserves, and I still haven’t been able to find that time :-)
There aren’t any workshops coming up in the immediate future, but did you hear about MIRIx workshops? If you set up a your own local workshop, MIRI can reimburse certain expenses and may even send a researcher to the first workshop to give tutorials and/or chat, depending on the situation.