Ladrière : « [Hilbert] superpose une métamathématique ou théorie de la démonstration, chargée d'étudier les propriétés des formalismes de premier niveau et en particulier d'établir leur non-contradiction »
(Ladrière 1992 [1957] : 28).