On the decidability of monadic first order logic in sequent calculus
Article Sidebar
Main Article Content
Abstract
In this article, a syntactical proof of decidability ofmonadic first-order logic (and of its completeness for finite models) is given. Theproof is obtained by adapting to the case of monadic logic, the proof given byKetonen/Schütte for first-order logic completeness (method of “construction of therefutation tree”, which actually describes, for the propositional fragment, adecision algorithm). In the general case (i.e. not restricted to monadic logic), the treatment of existential quantifiers imposes an enumeration of all the terms ofthe language, treatment that prevents the algorithm’s termination, and thus the decision. In the monadic case, however, any formula can be put in a specificcanonical form, a result due to H. Behmann (1922), canonical form which implies thatonly a bounded set of terms have to be taken in consideration. The treatment of existential quantifiers can thus be done with a finite number of terms.Decidability (and completeness for finite models) of the monadic case follows.
---
Original in French.
Article Details
Copyright Notice
The author of the article or book reviews submitted and approved for publication authorizes the editors to reproduce it and publish it in the journal O que nos faz pensar, with the terms “reproduction” and “publication” being understood in accordance with the definitions of the Creative Commons Attribution-NonCommercial 4.0 International license. The article or book reviews may be accessed both via the World Wide Web – Internet (WWW – Internet), and in printed form, its being permitted, free of charge, to consult and reproduce the text for the personal use of whoever consults it. This authorization of publication has no time limit, with the editors of the journal O que nos faz pensar being responsible for maintaining the identification of the author of the article.