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 L-models can be defined by a formula or a set of formu...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Areces, Carlos Eduardo, Carreiro, Facundo Matías, Figueira, Santiago Daniel
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_Areces2023-06-08T15: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 L-models 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 L-models 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 Hennessy-Milner 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 I-28
repository_str R-134
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 L-models 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 L-models 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 Hennessy-Milner 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