The implication problem for functional and inclusion dependencies

There are two implication problems for functional dependencies and inclusion dependencies: general implication and finite implication. Given a set of dependencies Σ ∪ {σ}, the problems are to determine whether σ holds in all databases satisfying Σ or all finite databases satisfying Σ. Contrary to the possibility suggested in Casanova, Fagin, and Papadimitriou (“Proceedings, 1st ACM Conf. on Principles of Database System,” pp. 171–176, 1982), there is a natural, complete axiom system for general implication. However, a simple observation shows that both implication problems are recursively unsolvable. It follows that there is no recursively enumerable set of axioms for finite implication