4 - Gödel and Formalism Independence

Summary

Gödel’s suggestion in his 1946 Princeton Bicentennial Lecture, to extend what he characterises as the formalism independence of the concept of computabilityto definability and provability, are discussed and implenented. The implementation for the concept of definabilitytakes the form of extended constructibility. Possible implementations having to do with provability are also discussed, mainly in connection with informal proof systems involving Gödel’s so-called large cardinal program.