Question. Is a predicate logic with discrete variables decidable? If yes, than whats is algorithm to obtain statement about truthiness of particular sentence? If yes, it would be good to have reference to literature source too.
Relevance. An example. Database structure may be described by ERR model witch resembles first order logic with discrete variables. I may be interesting to check whether two EER models are equivalent.
My research. I know that propositional logic is decidable. I know that for the case of finite discrete variables predicate logic looks very similar to propositional calculus and should be decidable. I guess than with use of induction it may be possible to prove that discrete predicate calculus is decidable. So I need to start with binary variables, and than prove that if n-ary variable predicate calculus is decidable, than n+1-ary variable predicate calculus is also decidable.
P.S. I am a chemist. Please be simple. Some things you find ridiculously simple may be inaccessibly hard for me.