I wrote: ... For the special case of the definition of "1", let ε be "1", let L be the usual language {0.s,+,•} of number theory and let T be Peano Arithmetic (PA). Then where φ is any sentence of L involving "1", and ψ is the result of replacing every occurrence of "1" in φ with "s(0)", then by eliminability we have PA+"1 = s(0)" ⊢ φ ↔ ψ and, moreover, by conservativeness, if in fact PA+"1 = s(0)" ⊢ φ, then PA ⊢ ψ.
Sorry, I was hasty here; we don't have these results by eliminability and conservativeness. Rather: we can prove that PA+"1 = s(0)" ⊢ φ ↔ ψ and hence that the purported definition is eliminable and we can prove that, if in fact PA+"1 = s(0)" ⊢ φ, then PA ⊢ ψ and, hence, that the it is also conservative. We prove thereby that the purported definition is indeed legitimate.
-chris
|