Meta-mathematical arguments establishing the consistency of formal systems such as PM have, in fact, been devised, notably by Gerhard Gentzen, a member of the Hilbert school, in 1936, and by others since then.38 These proofs are of great logical significance, among other reasons because they propose new forms of meta-mathematical constructions, and because they thereby help make clear how the class of rules of inference needs to be enlarged if the consistency of PM and related systems is to be established. But these proofs cannot be mirrored inside the systems that they concern, and, since
...more
