| Summary: | 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.
|
|---|