Unification in Modal Logic

摘要

Let Φ_1,..., Φ_n and ψ be some formulas. The figure {formula} is the inference rule which for all substitutions σ, derives σ(ψ) from σ(Φ_1), ...σ(Φ_n). It is admissible in a propositional logic L whenever for all substitutions a, a(ψ) ∈ L if a(Φ_1),..., σ(Φ_n) ∈ L. It is derivable in L whenever there is a derivation of ψ in L from the hypothesis Φ_1,...,Φ_n. It is evident that every derivable rule is also admissible. L is called structurally complete when the converse holds. Some propositional logics -- such as Classical Propositional Logic -- are structurally complete. Others -- like Intuitionistic Propositional Logic -- are not. See [14, Chap. 2]. When L is not structurally complete, owing to the importance of the admissibility problem in the mechanization of propositional logics, it is crucial to be able to recognize whether a given inference rule is admissible. The question of the existence of a decidable modal logic with an undecidable admissibility problem has been negatively answered by Wolter and Zakharyaschev [41] within the context of normal modal logics between K and K4 enriched with the universal modality -- see also the pioneering article of Chagrov [13] for an earlier example of a decidable modal logic with an undecidable admissibility problem. In some other cases, for instance Intuitionistic Propositional Logic and transitive normal modal logics like K4, the question of the decidability of the admissibility problem has been positively answered by Rybakov [33-35]. See also [15,25,27,28,32]. The truth is that Rybakov's decidability results are related to the fact that the propositional logics he has considered are finitary [22-24].