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...
Main Author: | |
---|---|
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 |