# Local reflection, definable elements and 1-provability

## TL;DR

This paper explores local reflection principles, definable elements, and 1-provability, providing new model-theoretic and proof-theoretic insights into their relationships and strength within formal systems.

## Contribution

It introduces uniform reflection with definable parameters, relates it to local reflection principles, and offers new proofs and axiomatizations for related logical systems.

## Key findings

- Established the $oldsymbol{oldsymbol{oldsymbol{oldsymbol{ ext{Σ}}_{n+2}}}}$-conservativity of uniform $oldsymbol{oldsymbol{ ext{Σ}}_{n+1}}$-reflection.
- Provided a new model-theoretic proof of conservativity results.
- Connected 1-provability in $S$ with uniform $oldsymbol{ ext{Σ}}_2$-reflection schema and axiomatized $ ext{I}oldsymbol{ ext{Σ}}_1$.

## Abstract

In this note we study several topics related to the schema of local reflection $\mathsf{Rfn}(T)$ and its partial and relativized variants. Firstly, we introduce the principle of uniform reflection with $\Sigma_n$-definable parameters, establish its relationship with the relativized local reflection principles and corresponding versions of induction with definable parameters. Using this schema we give a new model-theoretic proof of the $\Sigma_{n+2}$-conservativity of uniform $\Sigma_{n+1}$-reflection over relativized local $\Sigma_{n+1}$-reflection. We also study the proof-theoretic strength of Feferman's theorem, i.e., the assertion of $1$-provability in $S$ of the local reflection schema $\mathsf{Rfn}(S)$, and its generalized versions. We relate this assertion to the uniform $\Sigma_2$-reflection schema and, in particular, obtain an alternative axiomatization of $\mathsf{I}\Sigma_1$.