Andererseits kann es in keinem wesentlichen Sinne eine Metamathematik geben. Alles muss in einer Type (oder also in keiner Type) liegen.