Well ordering principles and bar induction

TL;DR

This paper establishes an equivalence between the existence of omega-models of bar induction and a principle involving the Howard-Bachmann operation on well-orderings, linking proof-theoretic and ordinal-theoretic concepts.

Contribution

It demonstrates a novel equivalence connecting bar induction models with a well-ordering preservation principle via the Howard-Bachmann operation.

Findings

Equivalence between omega-models of bar induction and well-ordering preservation.

The Howard-Bachmann operation preserves well-orderings.

Bridges proof theory and ordinal analysis through this equivalence.

Abstract

In this paper we show that the existence of omega-models of bar induction is equivalent to the principle saying that applying the Howard-Bachmann operation to any well-ordering yields again a well-ordering.