Towards a Generic Model Theory: Automatic Bisimulations for Atomic, Molecular and First-order Logics - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2021

Towards a Generic Model Theory: Automatic Bisimulations for Atomic, Molecular and First-order Logics

(1, 2, 3)
1
2
3

Abstract

After observing that the truth conditions of connectives of non-classical logics are generally defined in terms of formulas of first-order logic (FOL), we introduce protologics, a class of logics whose connectives are defined by arbitrary first-order formulas. Then, we identify two subclasses of protologics which are particularly well-behaved. We call them atomic and molecular logics. Notions of invariance for atomic and molecular logics can be automatically defined from the truth conditions of their connectives, bisimulations do not need to be defined by hand on a case by case basis for each logic. Moreover, molecular logics behave as 'paradigmatic logics': every first-order logic and every protologic is as expressive as a molecular logic. Then, we prove a series of model-theoretical results for molecular logics which characterize them as fragments of FOL and which provide criteria for axiomatizability and definability of a class of models in these logics. In particular, we rediscover van Benthem's theorem for modal logic as a specific instance of our generic theorems and other results for modal intuitionistic logic and temporal logic. We also discover a wide range of novel results, such as for the Lambek calculus. Then, we apply our method and generic results to FOL and find out novel invariance notions for FOL, that we call predicate bisimulation and first-order bisimulation. They refine the usual notions of isomorphism and partial isomorphism. We prove generalizations as well as new versions of the Keisler theorems for countable languages in which isomorphisms are replaced by predicate bisimulations and first-order bisimulations.
Fichier principal
Vignette du fichier
TechnicalReport2021.pdf (562.86 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Licence : CC BY NC ND - Attribution - NonCommercial - NoDerivatives

Dates and versions

hal-03414862 , version 1 (04-11-2021)
hal-03414862 , version 2 (02-12-2021)

Licence

Attribution - NonCommercial - NoDerivatives - CC BY 4.0

Identifiers

  • HAL Id : hal-03414862 , version 2

Cite

Guillaume Aucher. Towards a Generic Model Theory: Automatic Bisimulations for Atomic, Molecular and First-order Logics. [Research Report] Université de rennes 1. 2021. ⟨hal-03414862v2⟩
312 View
138 Download

Share

Gmail Facebook Twitter LinkedIn More