21 - Monadic and Dyadic Logic

Summary

We have given in earlier chapters several different proofs of Church's theorem to the effect that first-order logic is undecidable: there is no effective procedure that applied to any first-order sentence will in a finite amount of time tell us whether or not it is valid. This negative result leaves room on the one hand for contrasting positive results, and on the other hand for sharper negative results. The most striking of the former is the Löwenheim–Behmann theorem, to the effect that the logic of monadic (one-place) predicates is decidable, even when the two-place logical predicate of identity is admitted. The most striking of the latter is the Church–Herbrand theorem that the logic of a single dyadic (two-place) predicate is undecidable. These theorems are presented in sections 21.2 and 21.3 after some general discussion of solvable and unsolvable cases of the decision problem for logic in section 21.1. While the proof of Church's theorem requires the use of considerable computability theory (the theory of recursive functions, or of Turing machines), that is not so for the proof of the Löwenheim–Behmann theorem or for the proof that Church's theorem implies the Church–Herbrand theorem. The former uses only material developed by Chapter 11. The latter uses also the elimination of function symbols and identity from section 19.4, but nothing more than this. The proofs of these two results, positive and negative, are independent of each other.