Salvato in:
Dettagli Bibliografici
Autori principali: Martins, Miguel, Moraschini, Tommaso
Natura: Preprint
Pubblicazione: 2024
Soggetti:
Accesso online:https://arxiv.org/abs/2409.14998
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866916407041589248
author Martins, Miguel
Moraschini, Tommaso
author_facet Martins, Miguel
Moraschini, Tommaso
contents A bi-Heyting algebra validates the Gödel-Dummett axiom $(p\to q)\vee (q\to p)$ iff the poset of its prime filters is a disjoint union of co-trees (i.e., order duals of trees). Bi-Heyting algebras of this kind are called bi-Gödel algebras and form a variety that algebraizes the extension $\operatorname{\mathsf{bi-GD}}$ of bi-intuitionistic logic axiomatized by the Gödel-Dummett axiom. In this paper we establish the decidability of the problem of determining if a finitely axiomatizable extension of $\operatorname{\mathsf{bi-GD}}$ is locally tabular. Notably, if $L$ is an extension of $\operatorname{\mathsf{bi-GD}}$, then $L$ is locally tabular iff $L$ is not contained in $Log(FC)$, the logic of a particular family of finite co-trees, called the finite combs. We prove that $Log(FC)$ is finitely axiomatizable. Since this logic also has the finite model property, it is therefore decidable. Thus, the above characterization of local tabularity ensures the decidability of the aforementioned problem.
format Preprint
id arxiv_https___arxiv_org_abs_2409_14998
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Local Tabularity is Decidable for Bi-Intermediate Logics of Trees and of Co-Trees
Martins, Miguel
Moraschini, Tommaso
Logic
A bi-Heyting algebra validates the Gödel-Dummett axiom $(p\to q)\vee (q\to p)$ iff the poset of its prime filters is a disjoint union of co-trees (i.e., order duals of trees). Bi-Heyting algebras of this kind are called bi-Gödel algebras and form a variety that algebraizes the extension $\operatorname{\mathsf{bi-GD}}$ of bi-intuitionistic logic axiomatized by the Gödel-Dummett axiom. In this paper we establish the decidability of the problem of determining if a finitely axiomatizable extension of $\operatorname{\mathsf{bi-GD}}$ is locally tabular. Notably, if $L$ is an extension of $\operatorname{\mathsf{bi-GD}}$, then $L$ is locally tabular iff $L$ is not contained in $Log(FC)$, the logic of a particular family of finite co-trees, called the finite combs. We prove that $Log(FC)$ is finitely axiomatizable. Since this logic also has the finite model property, it is therefore decidable. Thus, the above characterization of local tabularity ensures the decidability of the aforementioned problem.
title Local Tabularity is Decidable for Bi-Intermediate Logics of Trees and of Co-Trees
topic Logic
url https://arxiv.org/abs/2409.14998