Normal forms for sequent derivations. (English) Zbl 0897.03053

Mints, Gregory

Odifreddi, Piergiorgio (ed.), Kreiseliana: about and around Georg Kreisel. Wellesley, MA: A K Peters. 469-492 (1996).

The author investigates derivations in intuitionistic predicate logic and its fragment, linear logic. He starts from a difference between normal natural deductions and cut-free L-derivations in the intuitionistic predicate calculus. He writes: “Normal form of a natural deduction is unique, but L-derivation can have different cut-free forms depending of the order of cut-elimination. On the other hand, one and the same normal natural deduction corresponds to these cut-free forms, and they can be obtained from each other by permutation of some antecedent rules” (p. 470). The author considers a formulation GJ of the intuitionistic predicate calculus, close to Gentzen’s system LJ and Kleene’s system G. He further considers natural deductions in multiplicative linear logic, the order of cut-elimination and permutation rules in a cut-free derivation, and equivalent forms for LJ which are free of structural rules.
For the entire collection see [Zbl 0894.03002].

Reviewer: V.Peckhaus (Erlangen)

MSC:

03F05	Cut-elimination and normal-form theorems
03B20	Subsystems of classical logic (including intuitionistic logic)
03F50	Metamathematics of constructive systems

Keywords:

intuitionistic predicate logic; cut-free derivations; multiplicative linear logic; natural deduction in linear logic