I really enjoy non-classical logic, and all kinds of interesting systems arise when you remove one of the structural rules of classical or intuitionalistic logi

I really enjoy non-classical logic, and all kinds of interesting systems arise when you remove one of the structural rules of classical or intuitionalistic logic. I'm at best an armchair logician, and I'd love for anyone to point out any flaws in my understanding, but I'll take a stab at describing linear logic and Evans' cathoristic logic. Linear logic is obtained from a classical logic in which entailment is not monotonic or idempotent. That is, a statement X && Y && Y proves Z cannot be contracted to X && Y proves Z, nor can the statement X proves Z be weakened to X && Y proves Z. One interpretation of this lets you treat terms as resources which cannot be created out of thin air. This is really useful for modeling logical constraints on resources and their allocation. Modal logics on the other hand are a very wide family of logic systems (see [0] for a diagram of some of the most simple modal logics) which introduce new operators to encode modality, a kind of qualification of the truth of a statement. For example a modal operator might encode that a statement is prohibited, that its truth is unknown, or that a statement will be true at some point in the future. These modal operators make modal logics useful for describing temporal constraints, or encoding logical statements about the belief of agents in a system (imagine giving each agent a modal operator B_i(X) which means, agent i believes X). In the latter case, different agents can hold incompatible beliefs without creating contradiction. As I understand it, Evans' cathoristic logic (the name of which the paper claims has greek origins, meaning "to impose narrow boundaries") arises from the desire to simply express inferences between atomic sentences with the expressivity of natural language. First-order logic is able to encode many natural language statements, such as adverbials, inference from dyadic to monadic propositions, and handling incompatible statements. However, first-order logic requires us to introduce quantifiers to do so, vastly increasing the search space for decision and resolution of these propositions. To get around the problem of quantifiers without losing expressivity, cathoristic logic uses subset of Hennessey-Milner logic[1] as a starting point. Negation is excluded, as it is the weakest form of encoding incompatibilities. For instance, in first-order logic, asserting "Pierre is the only king of Spain" is the same as saying "For all individuals other than Pierre, that individual is not the king of Spain". This weakness requires the knowledge-representer to include an axiom for every excluded possibility, or generalize the statement with a quantifier so that it no longer becomes atomic. Evans' therefore introduces the Tantum operator (written !A, for some set A) to express that the members of A exhaust all possibilities (almost like the latin abbreviation viz). Using the Tantum operator, we can reformulate the example above to be: "The king of spain is (Pierre && !{Pierre})". Using this operator lets one make specific optimizations when running the decision algorithm, and the paper shows that it's able to perform decisions in quadratic time. If negation were included, the running time for decision would be superpolynomial. Thanks for sharing the paper and prompting my read-through of it! [0]: http://plato.stanford.edu/entries/logic-modal/#MapRelBetModLog http://plato.stanford.edu/entries/logic-modal/#MapRelBetModL... [1]: https://en.wikipedia.org/wiki/Hennessy%E2%80%93Milner_logic https://en.wikipedia.org/wiki/Hennessy%E2%80%93Milner_logic