MPI-I-94-225

Given a Hilbert style specification of a propositional extension of standard propositional logic, it is shown how the basic model theoretic semantics can be obtained from the axioms by syntactic transformations. The transformations are designed in such a way that they eliminate certain derived theorems from the Hilbert axiomatization by turning them into tautologies. The following transformations are considered. Elimination of the reflexivity and transitivity of a binary consequence relation yields the basic possible worlds framework. Elimination of the congruence properties of the connectives yields weak neighbourhood semantics. Elimination of certain monotonicity properties yields a stronger neighbourhood semantics. Elimination of certain closure properties yields relational possible worlds semantics for the connectives. If propositional logic is the basis of the specification, the translated Hilbert axioms can be simplified by eliminating the formula variables with a quantifier elimination algorithm. This way we obtain the frame conditions for the semantic structures. All transformations work for arbitrary n-place connectives. The steps can be fully automated by means of PL1 theorem provers and quantifier elimination algorithms. The meta theory guarantees soundness and completeness of all transformation steps. As a by--product, translations into multi--modal logic are developed.

Categories / Keywords:

Logic, semantics, transformation