Revisiting the proof theory of Classical S4

TL;DR

This paper revisits the proof theory of Classical S4, addressing previous gaps by providing a new proof of the critical lemma, thereby establishing normalization for the system NS4.

Contribution

It offers a corrected proof of the critical lemma, leading to a valid normalization proof for the logical system NS4, which was previously unresolved.

Findings

Proof of the critical lemma in NS4

Normalization established for NS4

Addresses previous gaps in proof of classical S4

Abstract

In 1965 Dag Prawitz presented an extension of Gentzen-type systems of Natural Deduction to modal concepts of S4. Maria da Paz Medeiros showed in 2006 that the proof of normalisation for classical S4 does not hold and proposed a new proof of normalisation for a logically equivalent system, the system NS4. However two problems in the proof of the critical lemma used by Medeiros in her proof were pointed out by Yuuki Andou in 2009. This paper presents a proof of the critical lemma, resulting in a proof of normalisation for NS4.