Abstract
This paper contains a proof–theoretic account of unification in intermediate
logics. It is shown that many existing results can be extended to
fragments that at least contain implication and conjunction. For such
fragments, the connection between valuations and most general unifiers
is clarified, and it is shown how from the closure of a formula under the
Visser rules a proof of the formula under a projective unifier can be obtained.
This implies that in the logics considered, for the n-unification
type to be finitary it suffices that the m-th Visser rule is admissible for a
sufficiently large m. At the end of the paper it is shown how these results
imply several well-known results from the literature.
logics. It is shown that many existing results can be extended to
fragments that at least contain implication and conjunction. For such
fragments, the connection between valuations and most general unifiers
is clarified, and it is shown how from the closure of a formula under the
Visser rules a proof of the formula under a projective unifier can be obtained.
This implies that in the logics considered, for the n-unification
type to be finitary it suffices that the m-th Visser rule is admissible for a
sufficiently large m. At the end of the paper it is shown how these results
imply several well-known results from the literature.
Original language | English |
---|---|
Pages (from-to) | 713-729 |
Journal | Journal of Symbolic Logic |
Volume | 80 |
Issue number | 3 |
DOIs | |
Publication status | Published - 2015 |
Keywords
- unification
- admissible rules
- intermediate logics
- fragments