A Syntactic Proof of the Decidability of First-Order Monadic Logic

Orlandelli, Eugenio; Tesi, Matteo

dc.contributor.author	Orlandelli, Eugenio
dc.contributor.author	Tesi, Matteo
dc.date.accessioned	2024-06-24T08:31:41Z
dc.date.available	2024-06-24T08:31:41Z
dc.date.issued	2024-02-09
dc.identifier.issn	0138-0680
dc.identifier.uri	http://hdl.handle.net/11089/52598
dc.description.abstract	Decidability of monadic first-order classical logic was established by Löwenheim in 1915. The proof made use of a semantic argument and a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3-style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal logic T.	en
dc.language.iso	en
dc.publisher	Wydawnictwo Uniwersytetu Łódzkiego	pl
dc.relation.ispartofseries	Bulletin of the Section of Logic;2	en
dc.rights.uri	https://creativecommons.org/licenses/by-nc-nd/4.0
dc.subject	proof theory	en
dc.subject	classical logic	en
dc.subject	decidability	en
dc.subject	Herbrand theorem	en
dc.title	A Syntactic Proof of the Decidability of First-Order Monadic Logic	en
dc.type	Article
dc.page.number	223-244
dc.contributor.authorAffiliation	Orlandelli, Eugenio - University of Bologna, Department of the Arts, Bologna, Italy	en
dc.contributor.authorAffiliation	Tesi, Matteo - Vienna University of Technology, Faculty of Informatics, Vienna, Austria	en
dc.identifier.eissn	2449-836X
dc.references	G. S. Boolos, J. P. Burgess, R. C. Jeffrey, Computability and Logic, 5th ed., Cambridge University Press, Cambridge (2007), DOI: https://doi.org/10.1017/CBO9780511804076	en
dc.references	T. Bräuner, A cut-free Gentzen formulation of the modal logic S5, Logic Journal of the IGPL, vol. 8(5) (2000), pp. 629–643, DOI: https://doi.org/10.1093/jigpal/8.5.629	en
dc.references	A. Church, A note on the Entscheidungsproblem, The Journal of Symbolic Logic, vol. 1(1) (1936), p. 40–41, DOI: https://doi.org/10.2307/2269326	en
dc.references	H. R. Lewis, Complexity results for classes of quantificational formulas, Journal of Computer and System Sciences, vol. 21(3) (1980), pp. 317–353, DOI: https://doi.org/10.1016/0022-0000(80)90027-6	en
dc.references	C. Liang, D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol. 410(46) (2009), pp. 4747–4768, DOI: https://doi.org/10.1016/j.tcs.2009.07.041, special issue: Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi.	en
dc.references	L. Löwenheim, Über Möglichkeiten im Relativkalkül, Mathematische Annalen, vol. 76 (1915), pp. 447–470, DOI: https://doi.org/10.1007/BF01458217	en
dc.references	W. V. Quine, On the logic of quantification, The Journal of Symbolic Logic, vol. 10(1) (1945), p. 1–12, DOI: https://doi.org/10.2307/2267200	en
dc.references	A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd ed., Cambridge University Press, Cambridge (2000), DOI: https://doi.org/10.1017/CBO9781139168717	en
dc.contributor.authorEmail	Orlandelli, Eugenio - eugenio.orlandelli@unibo.it
dc.contributor.authorEmail	Tesi, Matteo - tesi@logic.at
dc.identifier.doi	10.18778/0138-0680.2024.03
dc.relation.volume	53

Pliki tej pozycji

Nazwa:: 223-244_Orlandelli_Tesi.pdf
Rozmiar:: 1.800MB
Format:: PDF

Oglądaj/Otwórz

Pozycja umieszczona jest w następujących kolekcjach

Bulletin of the Section of Logic 53/2 (2024) [6]

Pokaż uproszczony rekord

Poza zaznaczonymi wyjątkami, licencja tej pozycji opisana jest jako https://creativecommons.org/licenses/by-nc-nd/4.0