Resúmen: El siguiente TFM presenta una semántica con cuantificación actualista para la Lógica Modal de Primer Orden; esto es: los dominios de cuantificación pueden ser distintos de un mundo a otro. Además, esta semántica permite que haya términos que no denotan. Esto es posible porque, al trabajar con lógica modal, la “verdad en un modelo” se convierte en “verdad en un mundo de una modelo”. Entonces, al interpretar términos en un mundo, puede ser que lo que denotan pertenezca al dominio local (el dominio del mundo donde se están interpretando); que pertenezca al dominio del modelo (fuera del local); o que no denoten ningún elemento del dominio del modelo. Además, es posible ofrecer un tratamiento sintáctico de la denotación de términos y la existencia de los objetos que son denotados. Para ello será necesario añadir una relación binaria entre términos que interpreta- remos como la identidad entre los objetos del dominio del modelo que tales términos denotan en el mundo de evaluación. Finalmente, se expondrá un cálculo de secuentes que se apoya en la contrapartida sintáctica de la denota- ción para dar las reglas de los cuantificadores y el abstractor. Tras proporcionar las reglas de este cálculo, se probará Teorema de Corrección.

Palabras clave: 1) Parcial 2) Denotación 3) Existencia 4) Secuente 

Abstract: The following TFM presents a semantics with actualist quantification for FOML; this is: the quantification domains can differ from one world to another. Also, this semantics allows to work with terms that do not denote. This is possible because, when working with modal logic, the "truth in a model" becomes "truth in a world of a model". Then, when interpreting terms in a world, they may denote objects which belongs to the local domain (the domain of the world where they are being interpreted); to the domain of the model (outside of the local domain); or do not denote anything in the domain of the model. Also, it is possible to offer a syntactic treatment of the denotation of terms and existence of objects that are denoted. For this it will be necessary to add a binary relation between terms which we will interpret as identity between objects of the domain of the model which are denoted in the world of evaluation by the terms. Finally, a sequent calculus will be exposed which uses the syntactic counterpart of the denotation to give the rules of the quantifiers and the abstractor. After providing the rules, Soundness Theorem will be proven.

Key words: 1) Partial 2) Denotation 3) Existence 4) Sequent