> Are you objecting to the formal system breaking down or to the deviation from expected meaning?
I'm saying that's a false distinction, because as soon as you have that deviation from expected meaning, you have valid theorems that silently stop being valid and your formal system quickly breaks down. And while you can redefine your way out of each individual instance of this, everything you redefine just means more and more theorems that don't have their normal meaning which in turn means more things that you have to redefine.
> You could just say something like "to simplify error handling, our programming language uses a 'zivision' operator that behaves exactly like regular division except zivision by zero is defined as zero".
This would be a much better approach, because then existing theorems that use or refer to division are obviously not necessarily true of zivision and if you want to use those theorems to talk about zivision then you have to check (and prove) that they're actually valid first.
I'm saying that's a false distinction, because as soon as you have that deviation from expected meaning, you have valid theorems that silently stop being valid and your formal system quickly breaks down. And while you can redefine your way out of each individual instance of this, everything you redefine just means more and more theorems that don't have their normal meaning which in turn means more things that you have to redefine.
> You could just say something like "to simplify error handling, our programming language uses a 'zivision' operator that behaves exactly like regular division except zivision by zero is defined as zero".
This would be a much better approach, because then existing theorems that use or refer to division are obviously not necessarily true of zivision and if you want to use those theorems to talk about zivision then you have to check (and prove) that they're actually valid first.