As far as the thesis went, I only read the introduction and the background chapters so I haven't gotten into the heart of it yet. Funnily enough, the background chapter did have some food for thought in the distinction between derivability and admissibility. I don't know if this is a common way of looking at things that I would have seen if I had ever really taken courses in logic, but in any case I think it makes a lot of sense. I'll probably try to read a chapter three tomorrow.
Alright, so now we come to the things I'm still chewing on. First, there's the Hoffman & Streicher paper. The basic point of the paper was really about proving that uniqueness of identity proofs doesn't follow from intensional type theory by constructing a model where it didn't hold, but I can see that there was some deeper insight in terms of using groupoids to model types - setting the stage for the later omega-groupoid models which I intend to read about tomorrow - as well as it being a good illustration of the general technique of constructing models to help determine if a property of the logical system is necessarily true. I'll probably review some of the constructions again tomorrow, though, before I read some of the papers on omega-groupoid models.
Speaking of models, that's the main thing I've gotten so far out of the other Altenkirch paper: the idea that one can construct a model of your proposed theory within another type theory to determine if it is even possible to make. I think there's more I should be getting out of it, but honestly it was the last thing I read today and I was a bit burned out. I think I'll put it back on the pile for tomorrow for another attack.
No comments:
Post a Comment