A note on strong normalization in classical natural deduction

In the context of natural deduction for propositional classical logic, with classicality given by the inference rule reductio ad absurdum, we investigate the De Morgan translation of disjunction in terms of negation and conjunction. Once the translation is extended to proofs, it obtains a reduction...

Full description

Bibliographic Details
Main Author: José Espírito Santo
Format: Article
Language:English
Published: Open Publishing Association 2016-06-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1606.06387v1
_version_ 1811341031565688832
author José Espírito Santo
author_facet José Espírito Santo
author_sort José Espírito Santo
collection DOAJ
description In the context of natural deduction for propositional classical logic, with classicality given by the inference rule reductio ad absurdum, we investigate the De Morgan translation of disjunction in terms of negation and conjunction. Once the translation is extended to proofs, it obtains a reduction of provability to provability in the disjunction-free subsystem. It is natural to ask whether a reduction is also obtained for, say, strong normalization; that is, whether strong normalization for the disjunction-free system implies the same property for the full system, and whether such lifting of the property can be done along the De Morgan translation. Although natural, these questions are neglected by the literature. We spell out the map of reduction steps induced by the De Morgan translation of proofs. But we need to ``optimize'' such a map in order to show that a reduction sequence in the full system from a proof determines, in a length-preserving way, a reduction sequence in the disjunction-free system from the De Morgan translation of the proof. In this sense, the above questions have a positive answer.
first_indexed 2024-04-13T18:50:42Z
format Article
id doaj.art-341bc60dd3874f03b6c7102beeebec46
institution Directory Open Access Journal
issn 2075-2180
language English
last_indexed 2024-04-13T18:50:42Z
publishDate 2016-06-01
publisher Open Publishing Association
record_format Article
series Electronic Proceedings in Theoretical Computer Science
spelling doaj.art-341bc60dd3874f03b6c7102beeebec462022-12-22T02:34:25ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-06-01213Proc. CL&C 2016415110.4204/EPTCS.213.4:11A note on strong normalization in classical natural deductionJosé Espírito Santo0 Centro de Matemática, Universidade do Minho In the context of natural deduction for propositional classical logic, with classicality given by the inference rule reductio ad absurdum, we investigate the De Morgan translation of disjunction in terms of negation and conjunction. Once the translation is extended to proofs, it obtains a reduction of provability to provability in the disjunction-free subsystem. It is natural to ask whether a reduction is also obtained for, say, strong normalization; that is, whether strong normalization for the disjunction-free system implies the same property for the full system, and whether such lifting of the property can be done along the De Morgan translation. Although natural, these questions are neglected by the literature. We spell out the map of reduction steps induced by the De Morgan translation of proofs. But we need to ``optimize'' such a map in order to show that a reduction sequence in the full system from a proof determines, in a length-preserving way, a reduction sequence in the disjunction-free system from the De Morgan translation of the proof. In this sense, the above questions have a positive answer.http://arxiv.org/pdf/1606.06387v1
spellingShingle José Espírito Santo
A note on strong normalization in classical natural deduction
Electronic Proceedings in Theoretical Computer Science
title A note on strong normalization in classical natural deduction
title_full A note on strong normalization in classical natural deduction
title_fullStr A note on strong normalization in classical natural deduction
title_full_unstemmed A note on strong normalization in classical natural deduction
title_short A note on strong normalization in classical natural deduction
title_sort note on strong normalization in classical natural deduction
url http://arxiv.org/pdf/1606.06387v1
work_keys_str_mv AT joseespiritosanto anoteonstrongnormalizationinclassicalnaturaldeduction
AT joseespiritosanto noteonstrongnormalizationinclassicalnaturaldeduction