Normalisation for Negative Free Logics without and with Definite Descriptions

TL;DR

This paper establishes normalization theorems for negative free logic, both intuitionist and classical, with and without definite descriptions, ensuring consistency and control over maximal formulas during reductions.

Contribution

It introduces new normalization results for free logic with definite descriptions and develops rules to prevent the introduction of higher-degree maximal formulas during reductions.

Findings

Normalization theorems proved for intuitionist and classical negative free logic

New rules restrict parameters to prevent higher-degree maximal formulas

Improved subformula property for deductions in free logic systems

Abstract

This paper proves normalisation theorems for intuitionist and classical negative free logic, without and with the $\invertediota$ operator for definite descriptions. Rules specific to free logic give rise to new kinds of maximal formulas additional to those familiar from standard intuitionist and classical logic. When $\invertediota$ is added it must be ensured that reduction procedures involving replacements of parameters by terms do not introduce new maximal formulas of higher degree than the ones removed. The problem is solved by a rule that permits restricting these terms in the rules for $\forall$, $\exists$ and $\invertediota$ to parameters or constants. A restricted subformula property for deductions in systems without $\invertediota$ is considered. It is improved upon by an alternative formalisation of free logic building on an idea of Ja\'skowski's. In the classical system the rules for $\invertediota$ require treatment known from normalisation for classical logic with $\lor$ or $\exists$. The philosophical significance of the results is also indicated.