If there is a test for theoremhood, a test which does always terminate in a finite The MU-puzzle 48 amount of time, then that test is called a decision procedure for the given formal system. When you have a decision procedure, then you have a very concrete characterization of the nature of all theorems in the system.

• time
• nature