Wyniki wyszukiwania - BazTech

1

Strong Normalization for Truth Table Natural Deduction

Geuvers Herman, van der Giessen Iris, Hurkens Tonny

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

139--176

EN

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 conversion-preserving 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.

2

A natural deduction and its corresponding sequent calculus for positive contraction-less relevant logic

Ilić M.

Reports on Mathematical Logic

|

2017

|

Vol. 52

101--132

EN

We give a normalizing system of natural deduction for positive contraction-less relevant logic RW+⁰ . The specific characteristic of our calculus is that it has a simple translational relationship to a particular sequent calculus for RW+⁰, such that normal natural deduction derivations correspond to cut-free sequent calculus derivations and vice versa. By translations from natural deduction to sequent calculus derivations, and back, together with cut-elimination, we obtain an indirect proof of the normalization.

3

Instantiation overflow

Dinis B., Ferreira G.

Reports on Mathematical Logic

|

2016

|

Vol. 51

15--33

EN

The well-known embedding of full intuitionistic propositional calculus into the atomic polymorphic system Fat is possible due to the intriguing phenomenon of instantiation overow. Instantiation overow ensures that (in Fat) we can instantiate certain universal formulas by any formula of the system, not necessarily atomic. Until now only three types in Fat were identified with such property: the types that result from the Prawitz translation of the propositional connectives (, , ) into Fat (or Girard's system F). Are there other types in Fat with instantiation overow ? In this paper we show that the answer is yes and we isolate a class of formulas with such property.

4

Metoda założeniowa odrzucania wyrażeń dla intuicjonistycznego rachunku zdań i systemu S4 Lewisa

Kostrzycka Z., Bryll G.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

1999

|

Vol. 7

50--59