Relative normalization

TL;DR

This paper explores the concept of relative normalization in formal theories, establishing conditions under which the normalization property of a theory can be proven relative to the consistency of another theory, despite limitations imposed by Gödel's second incompleteness theorem.

Contribution

It introduces a framework for proving relative normalization theorems, extending the idea of relative consistency to the normalization property of theories.

Findings

Proves that relative normalization theorems can be established under 1-consistency assumptions.

Shows that normalization properties can be derived relative to other theories' consistency.

Provides a method to circumvent limitations of Gödel's second incompleteness theorem in normalization proofs.

Abstract

G{\"o}del's second incompleteness theorem forbids to prove, in a given theory U, the consistency of many theories-in particular, of the theory U itself-as well as it forbids to prove the normalization property for these theories, since this property implies their consistency. When we cannot prove in a theory U the consistency of a theory T , we can try to prove a relative consistency theorem, that is, a theorem of the form: If U is consistent then T is consistent. Following the same spirit, we show in this paper how to prove relative normalization theorems, that is, theorems of the form: If U is 1-consistent, then T has the normalization property.