Thank you, Robin. Yes, it helps. I wasn't aware of your work, so I am happy now to see it. I will read it more carefully to connect it with my thinking. What I dare say in this quick reply is that your approach to "Turing category" is closer to what I had in mind as compared to "Category of Turing". The latter is more like a category of machines and is related to work e.g. by Betti, Kasangian, Rosebrugh, Rosenthal, and probably many others. The Rosenthal approach differs a bit from the Betti-Kasangian-Rosebrugh view, as Rosenthal brings in quantaloids and such things (which is a bit of that "stuff in between", but perhaps in another sense, I guess), i.e., really focusing on transition in machines as modules (actions). However, a category of such machines as objects does not e.g. enable to bring recursion into play, as you do. Or to put it in another way, a "Category of Turing" is a category of computabilities, in some sense, whereas a Turing category is expected to be a computability category. It's a bit similar in the community of "fuzzy", where they speak about "fuzzy logic", which it actually isn't. It's "logic with fuzzy", and "fuzzy logic" is different. Understanding many-valuedness from the viewpoint of quantales and modules is a bit related to both areas, I think. It's my gut feeling. I need to read your descriptions more carefully. Partial is part of it, and I've always been scared about partial functions, but perhaps I shouldn't be. You also involve cartesian so I will try to find monoidal closedness in there. This, to me intuitively, may be somehow related a bit to Thue 1914, i.e., not just using rewrite rules on words built upon an alphabet and using a binary operation, but indeed using the tensor in a monoidal closed category. Of course, we do not have "free monoidal categories" in this required sense, so it is still open to me what happens when we try to invoke recursion into categories. You indeed have it in some form, so I will now read more carefully, and probably come back to you when I fail to understand, which I frequently do. This is a good one, so thanks again. And thanks also for the "can't have the cake and eat it". You're right on target. Best, Patrik PS Maybe such enriched models of computations are needed to understand things like global warming? Obviously, hypothesis testing won't suffice. I.e. a BIGGER question (referring to your BIG question in your 2007 slides) might be "Can we turn this way of computing into real world applications?" On 2017-01-19 03:08, Robin Cockett wrote:
Some more comment on Godel's theorem:
In my Estonia notes on Turing categories there is a section in which I prove Godel's theorem for a Turing category with a "provability" predicate.
http://pages.cpsc.ucalgary.ca/~robin/talks/estonia-winter-2010/estonia-notes...
It also contains some general comments about the Godel's theorem (which I hope you like :-)). See section 7.5.
The main point of the theorem from a categorical perspective is to show that one cannot have a provability predicate (extensional) and a setting in which there are only two subobjects of 1 (namely empty subobject and the whole thing). This is dramatic enough as it means mere truth and falsity does not suffice there must be stuff in between (lots of it)!
The theorem in the notes is a bit more general than Joyal's theorem but also weaker in the sense that there is an assumption of a "provability" predicate. Well you can't have your cake and eat it!
Hope this helps ...
-robin
(Robin Cockett)
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]