MacNeille completion and Buchholz' Omega rule for parameter-free second order logics

TL;DR

This paper explores the algebraic foundations of Buchholz's Omega-rule in second order logic, connecting it to MacNeille completion and providing a new algebraic proof of cut elimination for parameter-free fragments.

Contribution

It establishes a formal link between the Omega-rule and MacNeille completion, leading to an algebraic proof of cut elimination for second order intuitionistic logic fragments.

Findings

Omega-rule is algebraically grounded in MacNeille completion.

Provides algebraic proof of cut elimination for LIPn fragments.

Shows equivalence between cut elimination and 1-consistency of IDn.

Abstract

Buchholz' Omega-rule is a way to give a syntactic, possibly ordinal-free proof of cut elimination for various subsystems of second order arithmetic. Our goal is to understand it from an algebraic point of view. Among many proofs of cut elimination for higher order logics, Maehara and Okada's algebraic proofs are of particular interest, since the essence of their arguments can be algebraically described as the (Dedekind-)MacNeille completion together with Girard's reducibility candidates. Interestingly, it turns out that the $\Omega$-rule, formulated as a rule of logical inference, finds its algebraic foundation in the MacNeille completion. In this paper, we consider the parameter-free fragments LIP0, LIP1, LIP2, ... of the second order intuitionistic logic, that correspond to the arithmetical theories ID0, ID1, ID2, ... of iterated inductive definitions up to omega. In this setting, we observe a formal connection between the Omega-rule and the MacNeille completion, that leads to a way of interpreting second order quantifiers in a first order way in Heyting-valued semantics, called the Omega-interpretation. Based on this, we give an algebraic proof of cut elimination for LIPn for every n<omega that can be locally formalized in IDn. As a consequence, we obtain an equivalence between the cut elimination for LIPn and the 1-consistency of IDn that holds in a weak theory of arithmetic.