Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules

TL;DR

This paper formalizes a version of intuitionistic logic with general rules, proving it has normalization and the subformula property, which are important for logical consistency and proof analysis.

Contribution

It introduces definitions and reduction procedures for a system of intuitionistic logic with general rules, demonstrating normalization and the subformula property.

Findings

Deductions in the system can be converted into normal form.

Normal form deductions possess the subformula property.

The paper provides alternative reduction methods.

Abstract

This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of `maximal formula', `segment' and `maximal segment' suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions in normal form have the subformula property.