Local reflection, definable elements and 1-provability
In this note we study several topics related to the schema of local reflection 𝖱𝖿𝗇(𝑇) and its partial and relativized variants. Firstly, we introduce the principle of uniform reflection with 𝛴𝑛-definable parameters, establish its relationship with relativized local reflection principles and corresponding versions of induction with definable parameters. Using this schema we give a new model-theoretic proof of the 𝛴𝑛+2-conservativity of uniform 𝛴𝑛+1-reflection over relativized local 𝛴𝑛+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 𝖱𝖿𝗇(𝑆), and its generalized versions. We relate this assertion to the uniform 𝛴2-reflection schema and, in particular, obtain an alternative axiomatization of 𝖨𝛴1.