Every first-order positive inductive definition has a fixed point. It follows that, if the biconditional is thought of as an axiom in the language obtained from the background language by adding a new predicate, it will be conservative over the empty set. That is, any sentence not containing the new predicate derivable from the biconditional will be logically valid. Is there any way to obtain this observation proof theoretically, without the detour through the model theory of fixed points?
I have the same question about the axiom schema declaring that the extension of the new predicate is a fixed point contained in every other fixed point definable in the expanded language. We know it’s conservative because every first-order positive inductive definition has a smallest fixed point. Is there a syntactic proof of this?
I’ve been tinkering with the problem and not making any progress, not surprisingly, since I’m not a proof theorist. The only result I have is negative. For the second question, the conservativeness theorem can’t be proven in Peano arithmetic. Since we can characterize the standard integers as a smallest fixed point, the conservativeness theorem + Robinson’s arithmetic implies CON(PA).
