Bernd Buldt

While Gödel’s first theorem remains valid under substitution of various provability predicates, Gödel’s second theorem does not. This is one reason to label G1 as “extensional” but to call G2 “intensional.” Although this asymmetry between G1 and G2 is known for long, no satisfying account of G2’s intensionality has been put forward. After briefly reviewing the discussion so far, the paper presents a new analysis based on two observations. First, the underestimated role of provable closure under modus. Provable closure under modus ponens—usually listed as the second derivability condition—or similar requirements, do not get much attention since their proof isn’t perceived as much of challenge. Closer inspection shows, however, that the requirement of provable closure under modus ponens interacts differently with different formalized proof predicates and has thus a direct bearing on the discussion of G2’s intensionality. Second, in order to establish the co-extensionality of various proof predicates and hence the extensionality of G1, the role informal consistency assumption play goes largely unnoticed and unanalyzed. Closer inspection shows, however, that if such informal consistency assumptions are being made precise, the former distinction between G1 and G2 becomes blurry and G2’s intensionality can be made go away. Both observation then support the thesis that the traditional extensional/intensional distinction is not as robust as the received view believed it to be.