Document type
Master thesisPublication date
Publication license
Please use this identifier to cite or link to this item: https://hdl.handle.net/2445/201919
Unification in intuitionistic logic
Journal Title
Authors
Director/Tutor
Journal ISSN
Volume Title
Related resource
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.
Description
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
Subject (English)
Citation
Citation
CRISTANCHO S., Sebastián R. Unification in intuitionistic logic. [consulted: 11 of August of 2026]. Available at: https://hdl.handle.net/2445/201919