On Hewitt's Inconsistency Robustness, and given that my original posting was related to category theory as a metalanguage for logic in the sense of explaining extensions of the Goguen-Burstall and Meseguer approaches, phrases like "mathematics is inconsistent" and "proof does not intuitively increase our confidence in the consistency of mathematics" (appear in Hewitt's paper) really make no sense at all. Martin Escardo in his first reply to my posting says "I am not sure why these questions are being asked in this list". My simple reply is because my posting was suggesting to debate the use of category theory as a the underlying language for logic. Basically none of the replies to my posting has so far anything to do with category theory. Hewitt says "A mathematical theory is an extension of mathematics whose proofs are computationally enumerable." which basically means he says logic is an extension of mathematics. Logic is part of mathematics as a discipline, so logic cannot be the external canon for mathematics as little as philosophy can be the external canon for science. Nothing is global or canonic as far as mathematics is concerned. Many have tried to do so, but their is no consensus in that direction. Hewitt's note confirms that quite clearly. "Philosophy and mathematics can have a genuine connection", but that doesn't lead to anything useful. It just adds to fragmentation of the understanding of foundations. With category theory underlying type theory we believe we can manage type constructors more formally without restarting foundations a la HoTT. In Hewitt's note I am surprised not to see anything written about the 'iota' and 'o' types when speaking about Church. These are key types in the categorical description of the "lativity" of logic I mentioned earlier, and universal algebra comes short to deal with them. That lativity is important also otherwise. Proof mechanisms come after (not before or during) the bags of terms and sentences have been closed and sealed. So statements and enumerations involving proofs are not sentences in that sealed bag. This is the principle of lativity not respected by traditional logic where the metalanguage is absent. With categories in the meta for logic, we have term monads because we need substitutions to compose, but we only have sentence functors. A sentences functor being a monad simply means those sentences are terms. We have also said that an unquantified proposition P is not a sentence. It's a term. Quantifying it makes it a sentence, but then we have problems with the negation. The "not" before a P (as a term) is really different from a "not" before a quantifier, isn't it? Traditionally not, but when we start to construct terms and sentences otherwise than using natural language, we see it more clearly. All this is overlooked in traditional logic, and having category theory as a metalanguage for constructing terms and sentences, respectively as monads and functors, gives us something new to think about. This is our credo. Languages are more or less formal. Languages are more or less mathematically defined. Whatever the situation, if an object language allows less formal outsiders to be invoked side by side with its underlying metalanguage, ugly gets even worse. Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]