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.