On provability logic
Vítězslav Švejdar · 1999
This is an introductory paper about provability logic, a modal propositional logic in which necessity is interpreted as formal provability. I discuss the ideas that led to establishing this logic, I survey its history and the most important results, and I emphasize its applications in metamathematics. Stress is put on the use of Gentzen calculus for provability logic. I sketch my version of a decision procedure for provability logic and mention some connections to computational complexity.