Geodesic
A Syntactic Proof of the Decidability of First-Order Monadic Logic
Bulletin of the Section of Logic, Tome 53 (2024) no. 2, pp. 223-244.

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: proof theory, classical logic, decidability, Herbrand theorem 
@article{BSL_2024_53_2_a4,
     author = {Orlandelli, Eugenio and Tesi, Matteo},
     title = {A {Syntactic} {Proof} of the {Decidability} of {First-Order} {Monadic} {Logic}},
     journal = {Bulletin of the Section of Logic},
     pages = {223--244},
     publisher = {mathdoc},
     volume = {53},
     number = {2},
     year = {2024},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2024_53_2_a4/}
}
TY  - JOUR
AU  - Orlandelli, Eugenio
AU  - Tesi, Matteo
TI  - A Syntactic Proof of the Decidability of First-Order Monadic Logic
JO  - Bulletin of the Section of Logic
PY  - 2024
SP  - 223
EP  - 244
VL  - 53
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2024_53_2_a4/
LA  - en
ID  - BSL_2024_53_2_a4
ER  - 
%0 Journal Article
%A Orlandelli, Eugenio
%A Tesi, Matteo
%T A Syntactic Proof of the Decidability of First-Order Monadic Logic
%J Bulletin of the Section of Logic
%D 2024
%P 223-244
%V 53
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2024_53_2_a4/
%G en
%F BSL_2024_53_2_a4
Orlandelli, Eugenio; Tesi, Matteo. A Syntactic Proof of the Decidability of First-Order Monadic Logic. Bulletin of the Section of Logic, Tome 53 (2024) no. 2, pp. 223-244. http://geodesic.mathdoc.fr/item/BSL_2024_53_2_a4/

[1] G. S. Boolos, J. P. Burgess, R. C. Jeffrey, Computability and Logic, 5th ed., Cambridge University Press, Cambridge (2007) | DOI

[2] 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

[3] A. Church, A note on the Entscheidungsproblem, The Journal of Symbolic Logic, vol. 1(1) (1936), p. 40–41 | DOI

[4] H. R. Lewis, Complexity results for classes of quantificational formulas, Journal of Computer and System Sciences, vol. 21(3) (1980), pp. 317–353 | DOI

[5] C. Liang, D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol. 410(46) (2009), pp. 4747–4768, special issue: Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi. | DOI

[6] L. Löwenheim, Über Möglichkeiten im Relativkalkül, Mathematische Annalen, vol. 76 (1915), pp. 447–470 | DOI

[7] W. V. Quine, On the logic of quantification, The Journal of Symbolic Logic, vol. 10(1) (1945), p. 1–12 | DOI

[8] A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd ed., Cambridge University Press, Cambridge (2000) | DOI