Deduction-detachment theorem in hidden k-logics

作者：Babenyshev Sergey^*; Martins Manuel A

来源：Journal of Logic and Computation, 2014, 24(1): 233-255.

DOI：10.1093/logcom/ext008

• Behavioural equivalence relation
• hidden k-logic
• equivalence between logics
• Leibniz congruence
• deduction-detachment theorem
• Craig interpolation property

Modern software systems usually deal with several sorts (types) of data elements simultaneously. Some of these sorts, like integers, booleans, and so on, can be seen as having an immediate, direct nature and therefore are called visible, and they are contrasted with the others, like types of objects (in object-oriented (OO) sense), which are called hidden sorts. A language used to specify such software system has to be heterogeneous. In addition, to reason about such computations, we have to consider k-tuples of formulas (for instance, pairs in equational reasoning). Consequently, a consequence relation used to specify and verify the properties of those systems must relate sorted sets of k-formulas with individual k-formulas. Logics usually employed in this process are called hidden k-logics and are very general in nature: they comprise several classes of logical systems, including the 2-dimensional hidden and standard equational logics, and Boolean logic. In this article, we propose a generalization of the notion of deduction-detachment system for hidden k-logics. We introduce a syntactic notion of translation, which will be used to define an equivalence relation between hidden k-logics. We show that this notion of equivalence preserves some logical properties, namely the deduction-detachment theorem (DDT) and the Craig interpolation property. We also show that if a specifiable hidden k-logic admits the DDT then it admits a presentation whose only inference rules are the generalized modus ponens rules with respect to the deduction-detachment system.

• 出版日期2014-2