Characterization, definability and separation via saturated models
Three important results about the expressivity of a modal logic L are the Characterization Theorem (that identifies a modal logic L as a fragment of a better known logic), the Definability Theorem (that provides conditions under which a class of Lmodels can be defined by a formula or a set of formu...
Guardado en:
Autores principales:  , , 

Publicado: 
2014

Materias:  
Acceso en línea:  https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03043975_v537_nC_p72_Areces http://hdl.handle.net/20.500.12110/paper_03043975_v537_nC_p72_Areces 
Aporte de: 
id 
paper:paper_03043975_v537_nC_p72_Areces 

record_format 
dspace 
spelling 
paper:paper_03043975_v537_nC_p72_Areces20230608T15:29:39Z Characterization, definability and separation via saturated models Areces, Carlos Eduardo Carreiro, Facundo Matías Figueira, Santiago Daniel Characterization Definability Modal logics Model theory Saturation Separation Simulation Characterization Formal logic Saturation (materials composition) Separation Characterization theorems Definability First order logic Modal logic Model theory Observational equivalences Separation theorem Simulation Computer simulation Three important results about the expressivity of a modal logic L are the Characterization Theorem (that identifies a modal logic L as a fragment of a better known logic), the Definability Theorem (that provides conditions under which a class of Lmodels can be defined by a formula or a set of formulas of L), and the Separation Theorem (that provides conditions under which two disjoint classes of Lmodels can be separated by a class definable in L).We provide general conditions under which these results can be established for a given choice of model class and modal language whose expressivity is below first order logic. Besides some basic constraints that most modal logics easily satisfy, the fundamental condition that we require is that the class of ωsaturated models in question has the HennessyMilner property with respect to the notion of observational equivalence under consideration. Given that the Characterization, Definability and Separation theorems are among the cornerstones in the model theory of L, this property can be seen as a test that identifies the adequate notion of observational equivalence for a particular modal logic. © 2014 Elsevier B.V. Fil:Areces, C. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Carreiro, F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Figueira, S. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2014 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03043975_v537_nC_p72_Areces http://hdl.handle.net/20.500.12110/paper_03043975_v537_nC_p72_Areces 
institution 
Universidad de Buenos Aires 
institution_str 
I28 
repository_str 
R134 
collection 
Biblioteca Digital  Facultad de Ciencias Exactas y Naturales (UBA) 
topic 
Characterization Definability Modal logics Model theory Saturation Separation Simulation Characterization Formal logic Saturation (materials composition) Separation Characterization theorems Definability First order logic Modal logic Model theory Observational equivalences Separation theorem Simulation Computer simulation 
spellingShingle 
Characterization Definability Modal logics Model theory Saturation Separation Simulation Characterization Formal logic Saturation (materials composition) Separation Characterization theorems Definability First order logic Modal logic Model theory Observational equivalences Separation theorem Simulation Computer simulation Areces, Carlos Eduardo Carreiro, Facundo Matías Figueira, Santiago Daniel Characterization, definability and separation via saturated models 
topic_facet 
Characterization Definability Modal logics Model theory Saturation Separation Simulation Characterization Formal logic Saturation (materials composition) Separation Characterization theorems Definability First order logic Modal logic Model theory Observational equivalences Separation theorem Simulation Computer simulation 
description 
Three important results about the expressivity of a modal logic L are the Characterization Theorem (that identifies a modal logic L as a fragment of a better known logic), the Definability Theorem (that provides conditions under which a class of Lmodels can be defined by a formula or a set of formulas of L), and the Separation Theorem (that provides conditions under which two disjoint classes of Lmodels can be separated by a class definable in L).We provide general conditions under which these results can be established for a given choice of model class and modal language whose expressivity is below first order logic. Besides some basic constraints that most modal logics easily satisfy, the fundamental condition that we require is that the class of ωsaturated models in question has the HennessyMilner property with respect to the notion of observational equivalence under consideration. Given that the Characterization, Definability and Separation theorems are among the cornerstones in the model theory of L, this property can be seen as a test that identifies the adequate notion of observational equivalence for a particular modal logic. © 2014 Elsevier B.V. 
author 
Areces, Carlos Eduardo Carreiro, Facundo Matías Figueira, Santiago Daniel 
author_facet 
Areces, Carlos Eduardo Carreiro, Facundo Matías Figueira, Santiago Daniel 
author_sort 
Areces, Carlos Eduardo 
title 
Characterization, definability and separation via saturated models 
title_short 
Characterization, definability and separation via saturated models 
title_full 
Characterization, definability and separation via saturated models 
title_fullStr 
Characterization, definability and separation via saturated models 
title_full_unstemmed 
Characterization, definability and separation via saturated models 
title_sort 
characterization, definability and separation via saturated models 
publishDate 
2014 
url 
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03043975_v537_nC_p72_Areces http://hdl.handle.net/20.500.12110/paper_03043975_v537_nC_p72_Areces 
work_keys_str_mv 
AT arecescarloseduardo characterizationdefinabilityandseparationviasaturatedmodels AT carreirofacundomatias characterizationdefinabilityandseparationviasaturatedmodels AT figueirasantiagodaniel characterizationdefinabilityandseparationviasaturatedmodels 
_version_ 
1768544777021685760 