 Heyting shows the independence of his axioms using a method given by Bernays (1926); this use of a non-intended interpretation for metamathematical purposes Heyting accepted without hesitation, but he remarked that such metamathematics is “less important for us [intuitionists]” than the approach where all formulas are considered to be meaningful propositions (Heyting 1930: 43 [Mancosu 1998: 312]).