Skip to Main content Skip to Navigation
Reports

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

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.
Complete list of metadata

https://hal.inria.fr/hal-03414862
Contributor : Guillaume Aucher Connect in order to contact the contributor
Submitted on : Thursday, December 2, 2021 - 9:19:01 AM
Last modification on : Wednesday, January 26, 2022 - 5:42:06 PM

File

TechnicalReport2021.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NonCommercial - NoDerivatives 4.0 International License

Identifiers

  • HAL Id : hal-03414862, version 2

Citation

Guillaume Aucher. Towards a Generic Model Theory: Automatic Bisimulations for Atomic, Molecular and First-order Logics. [Research Report] Université de Rennes 1 (UR1). 2021. ⟨hal-03414862v2⟩

Share

Metrics

Les métriques sont temporairement indisponibles