Utilize este identificador para referenciar este registo: http://hdl.handle.net/1822/44808

TítuloA note on strong normalization in classical natural deduction
Autor(es)Espírito Santo, José
Data21-Jun-2016
EditoraOpen Publishing Association
RevistaElectronic Proceedings in Theoretical Computer Science
Resumo(s)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.
Tipoarticle
URIhttp://hdl.handle.net/1822/44808
DOI10.4204/EPTCS.213.4
e-ISSN2075-2180
Arbitragem científicayes
AcessoopenAccess
Aparece nas coleções:CMAT - Artigos com arbitragem/Papers with refereeing

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
SN-CL(GeneratedByEPTCS).pdf99,9 kBAdobe PDFVer/Abrir

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu Currículo DeGóis