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.