When we use logic to study a subject, the logic does not necessarily cover the entire semantic domain. Often we can only carve out some subsection of our domain and reason about it through a logic, especially if that logic is to be simple. This is not necessarily a bad thing- carving out total subsets of untyped lambda calculus by type theories (slightly different from whats in the lectures, but corresponding ideas) is a common pass-time in computer science. Being able to talk about a subject purely syntactically has several advantages to studying it directly. It is a common language which can be studied in isolation. This lets us study properties such as computability of, say, first order theories and apply the results to a large class of situations. It also allows a subject to be transformed into the unambiguous language of symbols. If that language is intended to describe a real-world phenomenon, like situations where the truth of something changes over time or where truths are added as proofs are discovered, then encoding it in a logic and finding a semantics for the logic gives the encoding of the real-world situation in math. This is what gives logic that truly foundational feel to me- over systems can be taken as a foundation, but logic has to do with symbols, and any other system will be manipulated and reasoned about using symbols written on chalkboards (or other surfaces, I suppose). This also applies to computer science, where I think of type theory as being "more foundational" (subjectively) then other systems.
This makes a lot of things clearer to me. Logicians like systems that are sound and complete with respect to their models because then the logic can be used to reason about the semantics without problems in the logic or in the semantic domain. It also makes more sense why Kripke models are so important- they give a mathematical setting for the subject of interesting logics.
Thinking about this in the context of constructive logic lead me to what I think is a better understanding of why domain theory is set up the way it is. I may be completely wrong about this, but what I'm thinking is that in constructive logic there are more then two truth values. It is not that there are three- which would be a tristate logic- but more like there are a countably infinite number of truth values. The truth value "true" is at the top, "false" is at the bottom, and all the rest are, in some sense, between them. The sense in which there is something between true and false is that a value may be partially defined. If a data structure can be evaluated part of the way to normal form it is more defined then one that has not been evaluated. It may not be fully evaluatable, but there is a real sense in which it is "more evaluatable" then a structure that can be evaluated less then it. This means that there is an ordering (a partial order) of structures by how "true" they are, or how much they can be evaluated before becoming completely evaluated or being equal to bottom. There is probably a mistake in my understanding here, as this ordering is over the terms, not the types, but the types are the equivalent of logical terms, but I don't know enough to be sure where my mistake it.
This also firms up my understanding of the relationship between category theory and logic. I've seen before how categories have internal logics, but when talking about things like translating syntactic objects to semantic ones, it clearer to me now how one might define a syntactic category and then one or more functors to a semantic category. I will have to go back to reading "Categories for Types" to see if I understand more now.
Again, don't take this post too seriously- I'm still learning and I have no formal background in this subject. My interest in it has carried me pretty far in understanding, but there are lots of details I get wrong still. Interesting stuff, nevertheless.
No comments:
Post a Comment