License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2020.1
URN: urn:nbn:de:0030-drops-138805
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13880/
Abel, Andreas
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction
Abstract
Intuitionistic truth table natural deduction (ITTND) by Geuvers and Hurkens (2017), which is inherently non-confluent, has been shown strongly normalizing (SN) using continuation-passing-style translations to parallel lambda calculus by Geuvers, van der Giessen, and Hurkens (2019). We investigate the applicability of standard model-theoretic proof techniques and show (1) SN of detour reduction (β) using Girard’s reducibility candidates, and (2) SN of detour and permutation reduction (βπ) using biorthogonals. In the appendix, we adapt Tait’s method of saturated sets to β, clarifying the original proof of 2017, and extend it to βπ.
BibTeX - Entry
@InProceedings{abel:LIPIcs.TYPES.2020.1,
author = {Abel, Andreas},
title = {{On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {1:1--1:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13880},
URN = {urn:nbn:de:0030-drops-138805},
doi = {10.4230/LIPIcs.TYPES.2020.1},
annote = {Keywords: Natural deduction, Permutative conversion, Reducibility, Strong normalization, Truth table}
}
