Carregant...
Tipus de document
Treball de fi de màsterData de publicació
Llicència de publicació
Si us plau utilitzeu sempre aquest identificador per citar o enllaçar aquest document: https://hdl.handle.net/2445/201919
Unification in intuitionistic logic
Títol de la revista
Autors
Director/Tutor
ISSN de la revista
Títol del volum
Recurs relacionat
Resum
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.
Descripció
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
Matèries (anglès)
Citació
Citació
CRISTANCHO S., Sebastián r.. Unification in intuitionistic logic. [consulta: 30 de desembre de 2025]. [Disponible a: https://hdl.handle.net/2445/201919]