zbMATH — the first resource for mathematics

Unification types in logic. (English) Zbl 1148.03003
Prace Naukowe Uniwersytetu Śląskiego w Katowicach 2554. Katowice: Wydawnictwo Uniwersytetu Śląskiego (ISBN 978-83-226-1717-5/pbk). 192 p. + loose errata (2007).
Though unification as a proof method goes back to Herbrand’s theorem, a systematic investigation of unification theory in logic was initiated by S. Ghilardi only at the end of the 90s. Roughly, unification in logic is a search of a substitution that transforms a formula into a theorem or a tautology; following Ghilardi such substitutions are called unifiers. (There are also other definitions, which, for many but not all logical systems, are equivalent to this one.) A formula in some logic $$L$$ is said to be unifiable if it has a nonempty set of unifiers; the set can be ordered by the relation “is more general than”. The size of its subset of maximal elements determines the unification type of the formula: nullary, unitary, finitary, infinitary. By definition, the unification type of $$L$$ itself is the maximum type of its unifiable formulas. As the author writes in the Introduction, the subject of his book is to assign types to various logical systems, to describe the properties determining particular types of logics together with their location, and to apply unifiers to logic.
Traditionally, unification has been studied for intuitionistic logic, some modal logics and equivalential logic. In the monograph, the author presents results on unification types in non-Fregean logics, intermediate logics and some modal and multimodal logics, including tense and epistemic logics. It is shown that the non-Fregean logics are the only family of logics where numerous examples of all unification types are found. In particular, SCI, the sentential calculus with identity devised by R. Suzsko, is the only known example of a philosophically motivated logic of infinitary type (Theorem 3.6). In contrast, SCI has unitary type if unification is understood in algebraic sense as finding a substitution $$\tau$$ for two formulas $$f_1$$ and $$f_2$$ that makes $$\tau f_1 \equiv \tau f_2$$ provable in SCI. A chapter is devoted to unification in Fregean, in particular intermediate, logics. Particularly, a splitting of the lattice of intermediate logics that helps to locate logics with a specified unification type is found. This splitting turns out to be related with the so-called semi-constructivity of a logic. A similar splitting is found for the lattice of normal extensions of S4. The monograph contains also other results, both original ones and those obtained by other authors, as well as unsolved problems. It is self-contained: the first two chapters give the necessary background. The list of references covers about 150 items; the author certainly has not aimed to give an exhaustive bibliography.

MSC:
 03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations 03B35 Mechanization of proofs and logical operations 03B45 Modal logic (including the logic of norms) 03B55 Intermediate logics 03B60 Other nonclassical logic 03G25 Other algebras related to logic 03G99 Algebraic logic