2026-08-06T08:11:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13880 2024-03-06T10:52:43Z ddc:004 open_access

On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction Abel, Andreas Natural deduction Permutative conversion Reducibility Strong normalization Truth table 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 βπ. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andreas Abel 2021 Is Part Of LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2020.1 urn:nbn:de:0030-drops-138805 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.1 eng https://creativecommons.org/licenses/by/4.0/legalcode