Mislead by Intuition(ism)

From korrekt.org

Revision as of 15:04, 17 September 2008 by Markus Krötzsch (Talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Jan 14 2008. Sure, I could have seen that earlier. Instead, I spent quite some time pondering about how to use intuitionistic semantics as an approximation for faster ontological reasoning. I still claim that this is not completely stupid: intuitionistic logic is known to be strictly weaker than the classical Boolean calculus, and it thus allows us to conclude only some of the classical consequences of, say, an ontological theory. For that purpose it introduces weaker forms of implication and universal quantification, and does not allow for a classical negation operator. So couldn't there be an interesting fragment of intuitionistic logic that is easier to compute with, while still giving a lot of interesting consequences? Probably not – at least I will show below how even weak intuitionistic negation leads to computational intractability.

I cannot avoid to recall some basics first, and you may skim through the next paragraphs if you know intuitionistic logic already.

A quick overview of intuitionistic logic

Semantically, intuitionism is not really intuitive in an obvious sense of the word. The logic is strictly weaker than classical logic, i.e. every intuitionistic consequence is also a classical consequence but some classical consequences are not valid in intuitionism. The primary example of such a formula is p\vee\neg p which is not true in intuitionistic logic. The best approach to understanding this is to think of intuitionistic logic as a logic that does not deal with truth but with provability: while classical logic asks whether a statement is true or false, intuitionistic logics asks whether it is proven or refuted. Clearly, (in some concrete logical interpretation) any formula is either true or false (both classically and intuitionistically), but it may well be that a formula is neither proven nor refuted. I think this approach makes it easier even for non-constructivists to understand what intuitionism concludes.

Now this can all be formalised in a model-theoretic semantics based on the notion of possible worlds. Wikipedia has an overview of the Kripke semantics of intuitionistic logic. Basically, the idea is to consider many possible «worlds» in each interpretation, which may be thought of as reflecting different states of knowledge about the world. The model theory is still very similar to that of classical logic, but it adds the condition that an intuitionistic statement is only true in some state if it is true in all future states. One could also say: whatever additional facts we learn about the world, this statement must always be true (note that some cases in the definition of intuitionistic models do usually not refer to future states, simply because it would be redundant; a simple induction shows that one could equivalently make requirements for all future states in all cases).

It is much easier to obtain an intuitionistic proof theory from calculi for classical logic: one usually just leaves away or weakens some inference rule. This also brings us to believe that inferencing with some fragments of intuitionistic logic may really be simpler as for classical logic. As mentioned above, intuitionistic logic has no real negation, but it rather just simulates a weak negation with the formula F\to\bot – in all future worlds, F is only true when bottom is also true, i.e. never. Thus it is not possible to state that some formula is false in the current world, but only that it is false in the current and all future worlds.

Constructive ≠ tractable

Back to the main topic: can we find interesting tractable fragments of intuitionistic logic? Propositional Horn logic is a tractable fragment of classical logic, and thus it seems to be a nice basis for our investigation. Indeed, one can show that classical and intuitionistic semantics coincide on that fragment (this bascially also carries over to the first-order case, and to many non-Horn formulae with suitable restrictions on the syntax of implication premisses). But if classical Horn-logic is extended by disjunction (in implication heads), negation, or nested implications (in implication bodies), it immediately becomes NP-complete, just like full propostional logic. By basic laws of classical logic, these extensions are easily seen to be mere syntactic variants of each other.

Intuitionistic Horn-logic, however, could be extended in a weaker sense, using intuitionistic connectives. It is not hard to see that disjunction is not a promissing candidate here, since it introduces the same non-deterministic behaviour as in classical logic. But implication and disjunction are not so closely related in the intuitionistic case, and thus one could still use implications. If those are too much, restricting to intuitionistic negation (implications with unsatisfiable consequence) could further simplify the treatment.

Alas, none of those works: intuitionistic Horn-logic with intuitionistic negations in premisses is NP-hard. This can be shown by reducing, e.g., the 3SAT problem to checking the consistency of such a logical theory. To this end, consider some instance of 3SAT:

(x11 OR x12 OR x13) AND
(x21 OR x22 OR x23) AND
(xn1 OR xn2 OR xn3)

where each xij is some propositional variable or its negation. Assume that the set of propositional variables used here is p_1,\ldots,p_m. We consider intuitionistic formulae over the alphabet \{P_1,\ldots,P_m,N_1,\ldots,N_m\}. Now we need the following axioms:

(P_i\to\bot)\to N_i,  (P_i\wedge N_i)\to \bot  (1\le i\le m).

The models of this theory already have the property that, eventually, there must be worlds for which exactly one of {Pi,Ni} is true for each i, i.e. which are basically classical. Finally, we only have to formalise the above 3SAT by the formulae:

(\bar{X}_{i1}\wedge \bar{X}_{i2}\wedge\bar{X}_{i3})\to\bot

where \bar{X}_{ij} is \,\!P_k if xij is \neg p_k, and \,\!N_k if xij is \,\!p_k. Clearly, these axioms (for all clauses i of the 3SAT) exclude all worlds within which the given 3SAT is not satisfied. Together with the fact that any intuitionistic model must contain some world that assigns values to all variables via our encoding, this reduces 3SAT to satisfiability of intuitionistic logic theories.

Concluding, we have shown that even apparently weak intuitionistic fragments are computationally (at least) as complex as classical logic, and it is not hard to see that this result is modular enough to carry over to non-propositional cases (e.g. to modal logics or to description logics).

If you have any comments on this, feel free to drop me a line.

Personal tools