It’s less well appreciated, but I think true (though fuzzy), that many fields manage to circumvent the effects of diagonalization a bit further by considering objects that in some sense live on multiple levels of the hierarchy at the same time. I’d call that “the parametric polymorphism trick”, perhaps.
Was the PA_K trick invented by you, and if not where can I learn more about it? Can you also give some references for other instances of this “parametric polymorphism trick”?
The PA_K trick is mine. (Still hope to find a version of it that works—I have an idea, but need some time to try whether it can fix the proof...) A polymorphic variant of simple type theory is used in Isabelle/HOL; if you know Hindley-Milner polymorphism as used in Haskell, it’s a variant of that. Probably the most useful thing to read more about is models of the untyped lambda calculus: I’d recommend Chantal Berline’s From computation to foundations via functions and application: The λ-calculus and its webbed models00057-8) (I think there’s a non-paywall copy on her homepage, which is down currently); you don’t need to read about all the models in that paper, the basic one in Section 4.6 exemplifies the basic idea. The von Neumann hierarchy stuff is basic model-theory-in-ZFC-extensions stuff.
Besides what I wrote about in the post, Coq’s universe hierarchy is definitely an example; Chapter 12 of Adam Chipala’s draft Certified Programming with Dependent Types seemed the most helpful thing among what Google turned up (HTML version here). Finally, Reynold’s and Girard’s parametricity is the best example I know of that gives a formal meaning to “the same words being interpreted in different ways on different levels” [ETA: and then does something relatively deep with it]. Wadler’s Theorems for Free! is the best thing I can think of as an entry point.
The above list doesn’t really make me happy. Polymorphic type theory is very simple, but it also isn’t very deep. Other than that, Berline’s and Wadler’s papers are the only things that seem to give a reasonable return on time invested if you don’t know the field in question already, and even they aren’t really casual reading and all they’ll give you in the present context is examples of where I’m coming from in this post (not that both subjects aren’t worth studying for their own sake).
Oh, actually, I would say that NF is not an instance of the “parametric polymorphism trick”, but yet something else and much stranger that we don’t understand nearly as well. NF’s motivation is very much related, but—this is very fuzzy, but models of NFU seem to have to use much deeper logical trickery than the examples I was talking about, and it seems from my amateurish perspective that the reason is that NF “crosses levels” in stronger ways than the basic parametric polymorphism trick. Also, I’ve tried in the past to apply the trick to find simpler models of NFU and failed completely, though that’s very weak evidence.
Was the PA_K trick invented by you, and if not where can I learn more about it? Can you also give some references for other instances of this “parametric polymorphism trick”?
The PA_K trick is mine. (Still hope to find a version of it that works—I have an idea, but need some time to try whether it can fix the proof...) A polymorphic variant of simple type theory is used in Isabelle/HOL; if you know Hindley-Milner polymorphism as used in Haskell, it’s a variant of that. Probably the most useful thing to read more about is models of the untyped lambda calculus: I’d recommend Chantal Berline’s From computation to foundations via functions and application: The λ-calculus and its webbed models00057-8) (I think there’s a non-paywall copy on her homepage, which is down currently); you don’t need to read about all the models in that paper, the basic one in Section 4.6 exemplifies the basic idea. The von Neumann hierarchy stuff is basic model-theory-in-ZFC-extensions stuff.
Besides what I wrote about in the post, Coq’s universe hierarchy is definitely an example; Chapter 12 of Adam Chipala’s draft Certified Programming with Dependent Types seemed the most helpful thing among what Google turned up (HTML version here). Finally, Reynold’s and Girard’s parametricity is the best example I know of that gives a formal meaning to “the same words being interpreted in different ways on different levels” [ETA: and then does something relatively deep with it]. Wadler’s Theorems for Free! is the best thing I can think of as an entry point.
The above list doesn’t really make me happy. Polymorphic type theory is very simple, but it also isn’t very deep. Other than that, Berline’s and Wadler’s papers are the only things that seem to give a reasonable return on time invested if you don’t know the field in question already, and even they aren’t really casual reading and all they’ll give you in the present context is examples of where I’m coming from in this post (not that both subjects aren’t worth studying for their own sake).
PDF of Chantal Berline paper.
This seems related to New Foundations set theory: http://en.wikipedia.org/wiki/New_Foundations
Oh, actually, I would say that NF is not an instance of the “parametric polymorphism trick”, but yet something else and much stranger that we don’t understand nearly as well. NF’s motivation is very much related, but—this is very fuzzy, but models of NFU seem to have to use much deeper logical trickery than the examples I was talking about, and it seems from my amateurish perspective that the reason is that NF “crosses levels” in stronger ways than the basic parametric polymorphism trick. Also, I’ve tried in the past to apply the trick to find simpler models of NFU and failed completely, though that’s very weak evidence.