Since you didn't specify under what system we need to prove that 0=1 doesn't exist, I vaguely remembered or figured there was a simpler version of arithmetic under which that concept makes sense, but which wouldn't be strong enough to fall into incompleteness territory (so it would have to be weaker than Peano arithmetic, like you said).
> The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely. The theory is computably axiomatizable; the axioms include a schema of induction.
So a very dumbed-down version of arithmetic, but which does contain a notion like 0=1, and which is complete and consistent, so it can't contain a proof of 0=1.
Obviously, this is probably not the kind of thing you meant, hence my cheekily bringing it up :)
