On the decidability of monadic first order logic in sequent calculus
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 ther...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | Portuguese |
| Published: |
Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio)
2016-12-01
|
| Series: | O Que Nos Faz Pensar |
| Online Access: | http://www.oquenosfazpensar.fil.puc-rio.br/index.php/oqnfp/article/view/515 |
| _version_ | 1811334258925502464 |
|---|---|
| author | Jean-Baptiste Joinet |
| author_facet | Jean-Baptiste Joinet |
| author_sort | Jean-Baptiste Joinet |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T17:06:03Z |
| format | Article |
| id | doaj.art-6bfe2df5e6474386b2d7a1808eb16ca8 |
| institution | Directory Open Access Journal |
| issn | 0104-6675 |
| language | Portuguese |
| last_indexed | 2024-04-13T17:06:03Z |
| publishDate | 2016-12-01 |
| publisher | Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio) |
| record_format | Article |
| series | O Que Nos Faz Pensar |
| spelling | doaj.art-6bfe2df5e6474386b2d7a1808eb16ca82022-12-22T02:38:28ZporPontifícia Universidade Católica do Rio de Janeiro (PUC-Rio)O Que Nos Faz Pensar0104-66752016-12-0125395569515On the decidability of monadic first order logic in sequent calculusJean-Baptiste Joinet0Université Jean Moulin, Lyon 3In 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.http://www.oquenosfazpensar.fil.puc-rio.br/index.php/oqnfp/article/view/515 |
| spellingShingle | Jean-Baptiste Joinet On the decidability of monadic first order logic in sequent calculus O Que Nos Faz Pensar |
| title | On the decidability of monadic first order logic in sequent calculus |
| title_full | On the decidability of monadic first order logic in sequent calculus |
| title_fullStr | On the decidability of monadic first order logic in sequent calculus |
| title_full_unstemmed | On the decidability of monadic first order logic in sequent calculus |
| title_short | On the decidability of monadic first order logic in sequent calculus |
| title_sort | on the decidability of monadic first order logic in sequent calculus |
| url | http://www.oquenosfazpensar.fil.puc-rio.br/index.php/oqnfp/article/view/515 |
| work_keys_str_mv | AT jeanbaptistejoinet onthedecidabilityofmonadicfirstorderlogicinsequentcalculus |