Informal and absolute provability: from Kreisel and Gödel to Prawitz and Girard

Abstract

We investigate whether some basic tenets of Kreisel’s theory informal rigour and of Gödel’s notion of absolute provability match some aspects of Prawitz’s
proof-based semantics. The comparison relies upon the fact that, because of its semantic character and of Gödel’s incompleteness, Prawitz’s provability is not tantamount to formal derivability. We argue that Prawitz’s standpoint might cope with Kreisel’s informal rigour, while G ̈odel seems to undertake a different approach. We propose that GGödeldel’s approach may be read in terms of Girard’s proof-nets and, to conclude, we raise the question about whether the differences between Prawitz and GGödeldel can be overcome via a further bridging from Prawitz to Girard.