A type of halting-problem focussed on formal systems.
Suppose you have a formal system and a grammatical sentence in that system. Can you use the rules and axioms of that system to tell whether or not the sentence is in the system?
You don’t have any information about the system and sentence - they could be anything.