Hybrid terms and sentences (Q1313083)

Terms are built up from variables and operation symbols, hyperterms from variables and hypervariables. If one admits operation symbols and hypervariables simultaneously in a language, then one gets hybrid terms. Therefore the concept of hybrid terms is a generalization of hyperterms. In our approach we restrict the hypervariables respectively hyperpredicate variables to a fixed type. By this restriction a lot of problems become solvable, a fact which can also be concluded from Henkin's work on completeness. Furthermore we restrict the function symbols which are called hypervariables to terms. These hybrid logics have not the expressive power of a general second order logic. Nevertheless, proofs may be shorter and axiom systems may become finite in a hybrid logic. In this paper we present completeness theorems for hybrid logics, discuss the problem of finite axiomatization and study term rewriting and unification for two examples. These two examples are the variety of distributive lattices and the variety of 2-groups.