About the Unification Type of Modal Logics Between $$\mathbf {KB}$$ KB and $$\mathbf {KTB}$$ KTB
- PDF / 456,239 Bytes
- 26 Pages / 453.543 x 680.315 pts Page_size
- 85 Downloads / 159 Views
About the Unification Type of Modal Logics Between KB and KTB
Abstract. The unification problem in a normal modal logic is to determine, given a formula ϕ, whether there exists a substitution σ such that σ(ϕ) is in that logic. In that case, σ is a unifier of ϕ. We shall say that a set of unifiers of a unifiable formula ϕ is minimal complete if for all unifiers σ of ϕ, there exists a unifier τ of ϕ in that set such that τ is more general than σ and for all σ, τ in that set, σ = τ , neither σ is more general than τ , nor τ is more general than σ. When a unifiable formula has no minimal complete set of unifiers, the formula is nullary. We usually distinguish between elementary unification and unification with parameters. In elementary unification, all variables are likely to be replaced by formulas when one applies a substitution. In unification with parameters, some variables—called parameters—remain unchanged. In this paper, we prove that normal modal logics KB, KDB and KTB as well as infinitely many normal modal logics between KDB and KTB possess nullary formulas for unification with parameters. Keywords: Normal modal logics KB, KDB and KTB, Unification with parameters, Unification type.
1.
Introduction
The unification problem in a normal modal logic1 is to determine, given a formula ϕ, whether there exists a substitution σ such that σ(ϕ) is in that logic. In that case, σ is a unifier of ϕ. We shall say that a set of unifiers of a formula ϕ is minimal complete if for all unifiers σ of ϕ, there exists a unifier τ of ϕ in that set such that τ σ, i.e. τ is more general than σ, and for all σ, τ in that set, σ = τ , neither σ τ , nor τ σ, i.e. neither σ is more general than τ , nor τ is more general than σ. An important question is the following [1,12]: when a formula is unifiable, has it a minimal complete set of unifiers? When the answer is “no”, the formula is nullary. When the answer is “yes”,
1
In this paper, all modal logics are normal.
Presented by Heinrich Wansing; Received December 17, 2018
Studia Logica https://doi.org/10.1007/s11225-019-09883-0
c Springer Nature B.V. 2019
P. Balbiani, C. Gencer
the formula is either unitary, or finitary, or infinitary depending on the cardinality of its minimal complete sets of unifiers.2 A modal logic is called nullary if it possesses a nullary unifiable formula. Otherwise, it is called either unitary, or finitary, or infinitary depending on the types of its unifiable formulas. We usually distinguish between elementary unification and unification with parameters. In elementary unification, all variables are likely to be replaced by formulas when one applies a substitution. In unification with parameters, some variables—called parameters—remain unchanged. The problem of checking the unifiability of formulas is a special case of the problem of checking the admissibility of inference rules [20]. Intuitively, for an axiomatically presented modal logic, the admissibility problem asks whether a given inference rule can be added to the axiomatization of the logic without changing
Data Loading...
