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