hide
Free keywords:
-
Abstract:
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.
