I read in some books that propositional calculus is decidable (e.g. with truth tables), and predicate calculus is not decidable (as proved by Church and Turing). Unfortunately, I do not exactly understand the scope of the latter claim. Let me explain what I know about predicate calculus (please correct me if I'm wrong):
In its minimal form, predicate calculus is the pure predicate calculus with equality: its language has a complete set of logical connectives, unlimited supply of individual variables, quantifiers $\forall,\exists$, and a special binary predicate symbol $=$ for equality. It also has usual logical axioms and inference rules, including axioms for equality.
In a more rich form, predicate calculus can additionally have a finite set of individual constants, a finite set of n-ary functional symbols, a finite set of n-ary predicate symbols, and additional axioms for manipulating those symbols (we assume that the axioms are effectively generated, and "being an axiom" is a decidable property of a formula).
Does the undecidability result applies to the minimal form (the pure predicate calculus with equality), or it's a weaker result saying that no decision procedure exist that would handle all general forms of predicate calculus?
Thanks!
You might be looking for something such as monadic predicate calculus.
This is a fragment of the predicate calculus very much alike the "minimal form" you described: in monadic predicate calculus all the relation and function symbols are monadic, that is, there are no n-ary function and relation symbols.
Now, to answer to your question, what is interesting about monadic predicate calculus is that it is decidable (Löwenheim 1915), that is, the undecidability result does not apply to it.