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.


Our procedure for computing correspondences now works as follows: 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: 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.


Forms: Basic Form | Correspondences Form | Circumscription Form | Help
Documentation: Theory | Computing Correspondences | Computing Circumscription | The System | Conventions | Syntax | Literature

Maintained by Last modified: 7 Nov 2000
Copyright © 1995-2000 by Max-Planck-Institut für Informatik. All rights reserved.

Imprint | Data Protection