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: https://drops.dagstuhl.de/opus/volltexte/2021/13880/
Go to the corresponding LIPIcs Volume Portal


Abel, Andreas

On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction

pdf-format:
LIPIcs-TYPES-2020-1.pdf (0.9 MB)


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}
}

Keywords: Natural deduction, Permutative conversion, Reducibility, Strong normalization, Truth table
Collection: 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Issue Date: 2021
Date of publication: 07.06.2021
Supplementary Material: Software (Source Code): https://github.com/andreasabel/truthtable archived at: https://archive.softwareheritage.org/swh:1:dir:ad022539d7490ea9943b3f497f41ab2108acebc2


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI