  Hilbert suggested further restrictions on the theory in addition to conservativity: simplicity, brevity of proofs, “economy of thought” and mathematical productivity. The formal system of transfinite logic is not arbitrary: “This formula game is carried out according to certain definite rules, in which the technique of our thinking is expressed. […] The fundamental idea of my proof theory is none other than to describe the activity of our understanding, to make a protocol of the rules according to which our thinking actually proceeds”  (Hilbert, 1928,  475). When  Weyl (1928)  eventually turned away from intuitionism (for the reasons, see  Mancosu and Ryckman, 2002),  he emphasized this motivation of Hilbert’s proof theory: not to turn mathematics into a meaningless game of symbols, but to turn it into a theoretical science which codifies scientific (mathematical) practice.