Comments on: Crude but Effective Stratification http://www.e-pig.org/epilogue/?p=857 for Epigram Sun, 6 Nov 2011 09:25:45 +0000 http://wordpress.org/?v=2.8.4 hourly 1 By: Conor http://www.e-pig.org/epilogue/?p=857&cpage=1#comment-79220 Conor Wed, 29 Jun 2011 16:43:58 +0000 http://www.e-pig.org/epilogue/?p=857#comment-79220 No, but it has occurred to me that it might be interesting to think in that direction, not least because it would be an excellent excuse to visit my old teacher, Tom Forster. There's nothing about these rules which suggests that there has to be a bottom universe. Things might shift downwards as easily as they shift up. That said, the usual inductive-recursive method for making models of predicative type theories might struggle without an inductive characterization of the hierarchy. I wonder what we'd do instead... No, but it has occurred to me that it might be interesting to think in that direction, not least because it would be an excellent excuse to visit my old teacher, Tom Forster. There’s nothing about these rules which suggests that there has to be a bottom universe. Things might shift downwards as easily as they shift up.

That said, the usual inductive-recursive method for making models of predicative type theories might struggle without an inductive characterization of the hierarchy. I wonder what we’d do instead…

]]> By: Mathnerd314 http://www.e-pig.org/epilogue/?p=857&cpage=1#comment-79121 Mathnerd314 Thu, 23 Jun 2011 15:21:08 +0000 http://www.e-pig.org/epilogue/?p=857#comment-79121 Have you looked at implementing <a href="http://en.wikipedia.org/wiki/New_Foundations" rel="nofollow">NFU</a>? Have you looked at implementing NFU?

]]>