SCAN

Computing Correspondences

An algebraic version of the same problem turns up if you consider Boolean algebras with operators. Jónnson and Tarksi have shown that under certain conditions the operators can be represented with binary relations in the same way as modal operators can be represented with accessibility relations (at a certain abstraction there is no difference any more). The correspondence problem here is to find the correspondences between additional axioms in terms of the operators on one side and the underlying relation on the other side.

Let us use the modal logic example to illustrate how SCAN can be used for computing the corresponding frame properties. Suppose we are given the Hilbert axiom []p ->p and the standard possible worlds semantics of the modal operator:

w |= []p iff for all v: if r(w,v) then v |= []p

(|= is the satisfiability relation.) This semantics, together with the usual possible worlds semantics of the ordinary propositional connectives can be taken as a rewrite rules for translating the Hilbert axiom into predicate logic. For the above axiom we get:

all p all w (all v r(w,v) -> p(v)) -> p(w)

The outer quantifier all p comes because Hilbert axioms implicitly assume universal quantification over all formulae. The quantifier all w comes because Hilbert axioms are required to hold in all worlds. (all v r(w,v) -> p(v)) is the translation of []p where p(v) means that p is true in world v. This is now a second-order predicate logic formula. Since we want to apply SCAN, we negate it first:

exists p exists w (all v r(w,v) -> p(v)) & -p(w)

and give it as input to SCAN. The clause form is

C1: -r(w,v) v p(v)

C2: -p(w)

where w is a Skolem constant and v is a variable. There is only one resolvent possible: -r(w,w). Reconstructing the existential quantifier, we thus get the result exists w -r(w,w), which is to be negated again:

all w r(w,w),

and this is the desired frame property.

Qualifications

Our procedure for computing correspondences now works as follows:

We specify a possible worlds semantics for all connectives.
We use this specification as rewrite rule for translating the Hilbert axioms into predicate logic.
Since the formula variables are taken to be universally quantified, we negate the formula.
SCAN is applied to the negated formula and the result is negated again.

Unfortunately this procedure is not sufficient for logics weaker than propositional logic, such as intuitionistic logic or relevance logic. In these logics there is an extra condition on the assignment of values to the predicates. In intuitionistic logic for example the requirement is that if a predicate P is true in a world w it remains to be true in all higher worlds:

all w P(w) -> (all v r(w,v) -> P(v))

Nevertheless, we still can use SCAN for computing corresponding frame properties. We just add this assignment condition as a premise

all p assignment_condition(p) -> ...

to the translated Hilbert axioms. But this is still not enough. The assignment conditions, in particular that one for intuitionistic logic is a self resolving clause which causes the resolution in SCAN to loop. This loop can only be stopped by showing that from a certain level on the new resolvents are redundant because they are implied by other clauses. Unfortunately in may cases this can be shown only with help of additional properties, in the intuitionistic logic case it is the transitivity of the accessibility relation which is essential for stopping the loop. Therefore the input to our correspondence computation algorithm consists of four main parts:

the formula to be translated,
the semantics of the operators,
the `predicate qualifications', for example the assignment conditions they become part of the resolution process,
the additional assumptions, for example the transitivity of the accessibility relation, these are only used for simplification purposes.

For modal logic and other logics above standard propositional logic the first two parts are sufficient.

When using SCAN for computing the corresponding frame property for a given Hilbert axiom, four different things may happen.

SCAN terminates and returns a first-order predicate logic formula as the corresponding frame property. The correctness proof of the SCAN algorithm itself then guarantees that the second-order formula which is given as input to SCAN is logically equivalent to the result. Since our implementation is not formally verified, we can of course not give a 100% guarantee that the actually computed formula is correct, but we are pretty sure that it is.
SCAN terminates and returns a second-order predicate logic formula with a parallel Henkin quantifier. For example the translation of the modal logic McKinsey axiom []<>p -> <>[]p with SCAN yields

all w -(H[all x1 exists y1/all x2 exists y2] (r(w,x1) -> r(x1,y1)) & (r(w,x2) -> r(x2,y2)) & (r(w,x1) & r(w,x2) -> y1 =/= y2)).
This is to be read as follows: H[all x1 exists y1/all x2 exists y2] is the parallel Henkin quantifier. y1 depends on x1 only and y2 depends on x2 only. The whole formula with the Henkin quantifier is negated. (Negation of a Henkin quantifier does NOT simply swap the quantifiers!).
We cannot guarantee is that there is no first-order formula which is equivalent to this second-order formula. (The unskolemization is a quite sophisticated search process which is not guaranteed to find all possible unskolemization possibilities.)
In modal logic it is known that the conjunction of the Mc Kinsey axiom together with the axiom []p -> [][]p, which specifies transitivity of the accessibility relation, correspond to the atomicity of the frames: all x exists y r(x,y) & all z r(y,z) -> y = z. For the current version of SCAN there is no way to find this out. SCAN would compute the Mc Kinsey axiom and then transitivity axiom separately and not relate the conjunction with atomicity.
That means the computation of correspondence properties for conjunctions of Hilbert axioms may not give the optimal result.
SCAN does not terminate, i.e. the resolution process loops. In this case we cannot guarantee that there is in fact not a corresponding first-order property. But we can observe certain patterns. It may turn out that infinitely many resolvents are generated, but once in a while a clause without the predicates to be eliminated drops out. Moreover the sequence of these resolvents follow a certain pattern which can be finitely represented using infinite conjunctions and disjunctions. This happens when applying SCAN to the Löb axiom []([]p -> p) -> []p. The resulting infinite p-free clause set in fact specifies the correspondence property, finiteness of the R-chains.
The last thing which may happen is that SCAN does not terminate and none of the resolvents is without one of the predicates to be eliminated. This happens for example for the modal axiom <>[]p | []([]([]q -> q) -> q) which is known to be frame incomplete, i.e. there is no class of frames characteristic for this axiom. Again, we cannot guarantee that if SCAN behaves like this, it is a frame incomplete axiom, but it seems to be a strong indication.

References