[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Marc Denecker writes: > "It is time to leave behind the classical logic. In fact, we should > have done it a long time ago." > > To me, that sounds like a total and unconditional rejection. No, what I meant is that the classical logic represents a stage in the development of logic. It cannot be taken as the final answer. In fact, we cannot accept that we have a final answer until the entire natural language has been formalized, which might take a very very long time indeed! (The view I take, following Quine, is that logic is a regimentation of natural language. We can perfectly well circumscribe various regimens for various purposes.) I am entirely happy with the characterization of logical connectives as "information composition" operators. But we can only accept it as a good, but vague, intuition. We do not know what this "information" is. Neither do we know what the information is about. So, in order to claim that classical logic is a canonical information composition calculus, somebody would need to formalize those notions. Even though Vladimir has omitted the word "programming" in titling this subthread, the discussion has been about "declarative" and "imperative" as paradigms of programming. So, I would rather not divorce myself from programming concerns in discussing these issues. Cheers, Uday PS. I will try to respond to your more detailed points a little later. For now, I just wanted to set the record straight about what you called my "total and unconditional rejection" of classical logic, which it wasn't.
