Abstract:
We suggest an algebraic approach to proof-theoretic analysis
based on the notion of \textit{graded provability algebra}, that is,
Lindenbaum boolean algebra of a theory
enriched by additional operators which allow for the structure to
capture proof-theoretic (syntax-sensitive) information.
We use this method to analyze Peano arithmetic and show how
an ordinal notation system up to $\epsilon_0$
can be recovered from
the corresponding algebra in a canonical way.
This method also establishes links between proof-theoretic
ordinal analysis and the work which has been done in the last
two decades on provability logic and reflection principles.
Because of its abstract algebraic nature, we hope that it
will also be of interest for non-prooftheorists.