If you think that True + 2 makes sense, you can just define your own judgments that allow it (*). Logic, and the theory behind type systems, don't care about yo

If you think that True + 2 makes sense, you can just define your own judgments that allow it (*). Logic, and the theory behind type systems, don't care about your axioms and inference rules, they just let you reason about them, and their interactions. (*) Something like |- True : Bool |- True : Int or, if you only want to allow it in certain expressions |- x : Int ----------- |- True + x: Int etc.