A semantical proof of the strong normalization theorem for full propositional classical natural deduction
classification
🧮 math.LO
keywords
classicalproofdeductionfullnaturalnormalizationpropositionalsemantical
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.