A semantical proof of the strong normalization theorem for full propositional classical natural deduction

TL;DR

This paper presents a concise semantical proof of the strong normalization theorem for full propositional classical natural deduction, adapting Girard's reducibility candidates to the classical setting.

Contribution

It provides a simplified, semantical proof of strong normalization specifically tailored for classical natural deduction systems.

Findings

Proof confirms strong normalization for classical natural deduction

Simplifies previous proofs using reducibility candidates

Adapts Girard's method to classical logic

Abstract

We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidates introduced by J.-Y. Girard and simplified to the classical case by M. Parigot.