# metadata.dc.description[].value
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2022-2023. Tutor: Tommaso Moraschini i Amanda Vidal Wandelmer

# metadata.dc.description.abstract[].value
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.

# metadata.dc.source[].value
Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada