Vorherrschafts Problem

My pitiful attempt to coin a phrase.... German for "domination problem", analogous to EntscheidungsProblem = "decision problem".

The VorherrschaftsProblem is the following:

For set S and functions A, B : S -> {TRUE,FALSE}, determine if for all t in S if A(t) => B(t). If this is true, then A is said to dominate B (A ==> B).

Like the EntscheidungsProblem, this is (in the general case) undecidable. Given the undecidability of the EntscheidungsProblem, proving this one undecidable is easy. (This proof is hardly original; many undergraduate math courses leave this as an ExerciseForTheReader?). Assume that it is decidable for for all S, A, and B. By renaming, it is also decidable to determine if B ==> A. Finally, consider the conjunction of the two cases, A ==> B and B ==> A -- if the VorherrschaftsProblem is decidable, so is this.

But the case of A ==> B && B ==> A can be shown to be equivalent to the question of whether or not A(t) == B(t) for all t in S -- which is the EntscheidungsProblem. In other words, decidability of the VorherrschaftsProblem implies decidability of the EntscheidungsProblem. Since the EntscheidungsProblem is known to be undecidable, we have a contradiction -- hence the VorherrschaftsProblem is also undecidable.

This is one reason why PredicateType? systems are undecidable -- a key typing judgement in TypeTheory is determining whether or not one type is a subtype of another; for arbitrary predicate types, this is equivalent to the VorherrschaftsProblem.