Unification in intuitionistic logic

Abstract

The concept of unification has been widely studied from a logical perspective. In the context of logic, a formula A is said to be unifiable in a logic ⊢ if there is a substitution σ that turns A into a theorem of ⊢. In this case, we say that σ is a unifier (in ⊢) of A, or that A is unifiable (in ⊢) by σ. Given a logic ⊢ and a unifiable formula A (in ⊢), there is a natural way to compare its unifiers in terms of generality using the fact that, up to logical equivalence, some unifiers can be ‘obtained’ from others. More precisely, we say that the unifier σ1 of A is less general than the unifier σ2 of A if there is a substitution τ such that σ1(x) is logically equivalent to τ(σ2(x)) in ⊢ for all propositional variables x in the domain of σ1 and σ2. This gives rise to a hierarchy among the set of unifiers of A, where the unifiers in lower levels can be obtained from the unifiers in upper levels. A basis of unifiers of a unifiable formula A is a set of incomparable elements that ‘generates’ any other unifier of A. The study of the hierarchy among unifiers rises some interesting questions: Given a unifiable formula A in ⊢, is there a basis of unifiers of A? If so, is it finite or infinite? If it is finite, does it have one or more elements? These questions can be stated not only for formulas, but for logics in general.