Automatic structures and the problem of natural well-orderings

TL;DR

This paper investigates using automatic structures to address the challenge of natural proof-theoretic ordinal notations but finds that this approach does not achieve the desired goals.

Contribution

It evaluates the potential of automatic structures for representing natural proof-theoretic ordinals and concludes their limitations in this context.

Findings

Automatic structures are insufficient for natural proof-theoretic ordinal notations.

The approach does not meet the conceptual goals set for representing ordinals.

The study clarifies the limitations of automatic presentations in proof theory.

Abstract

We explore the idea of using automatic and similar kind of presentations of structures to deal with the conceptual problem of natural proof-theoretic ordinal notations. We conclude that this approach still does not meet the goals.