See, I'm not an academic - proving that addition is commutative is not in scope for what I'm wanting to do. It is not a big leap for me to make that an axiom in my system, I'm almost entirely disinterested in trying to innovate in the pure theory of foundational mathematics. I find the theory itself extremely interesting but that's just not my path. I thought I was clear about what I was wanting to build - a practical system for categorising functions that can be shown to halt or not always halt, lumping everything else into a third category. Academia and pure maths just isn't for me, this is so I can build a language with minimal bugs.
Yes, you were very clear. But saying "I want to build a practical system for categorising functions that can be shown to halt or not always halt, but I'm not interested in theory" is kind of like saying, "I want to build a practical warp drive, but I'm not interested in physics."
I'm not interested in trying to encode a proof that addition is commutative. I'm interested in the theory to the point where I'll enjoy (and have been enjoying) learning about the math, but in terms of implementation I just don't want or need to start that low.
