Strong Normalization for Truth Table Natural Deduction

Herman Geuvers, I. van der Giessen, Tonny Hurkens

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

We present a proof of strong normalization of proof-reduction in a general system of natural deduction called truth table natural deduction. In previous work, we have defined truth table natural deduction, which is a method for deriving intuitionistic derivation rules for a connective from its truth table. This yields natural deduction rules for each connective separately. Moreover, these rules adhere to a standard format which gives rise to a general notions of detour and permutation conversion for natural deductions. The aim is to remove all convertibilities and obtain a deduction in normal form. In general, conversion of truth table natural deductions is non-deterministic, which makes it more challenging to study. It has already been shown that this conversion is weakly normalizing. To prove strong normalization, we construct a conversionpreserving translation from deductions to terms in an extension of simply typed lambda calculus which we call parallel simply typed lambda calculus and which we prove to be strongly normalizing.
This makes it possible to get a grip on the non-deterministic character of conversion in the intuitionistic truth table natural deduction system.
Original languageEnglish
Pages (from-to)139-176
JournalFundamenta Informaticae
Volume170
Issue number1-3
DOIs
Publication statusPublished - 2019

Keywords

  • natural deduction
  • truth tables
  • intuitionistic logic
  • detour conversion
  • permutation conversion
  • strong normalization

Fingerprint

Dive into the research topics of 'Strong Normalization for Truth Table Natural Deduction'. Together they form a unique fingerprint.

Cite this