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:
(|= 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:
- w |= p iff for all v: if r(w,v) then v |= p
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:
- all p all w (all v r(w,v) -> p(v)) -> p(w)
and give it as input to SCAN.
The clause form is
- exists p exists w (all v r(w,v) -> p(v)) & -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:
- C1: -r(w,v) v p(v)
- C2: -p(w)
and this is the desired frame property.
Our procedure for computing correspondences now works as follows:
- all w r(w,w),
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:
- 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.
Nevertheless, we still can use SCAN for computing corresponding frame
We just add this assignment condition as a premise
- all w P(w) -> (all v r(w,v) -> P(v))
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:
- all p assignment_condition(p) -> ...
For modal logic and other logics above standard propositional logic
the first two parts are sufficient.
- 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.
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
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!).
- 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)).
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.
Basic Form |
Correspondences Form |
Circumscription Form |
Computing Correspondences |
Computing Circumscription |
The System |
Last modified: 7 Nov 2000
Copyright © 1995-2000 by Max-Planck-Institut
für Informatik. All rights reserved.
Imprint | Data Protection