If you think that True + 2 makes sense, you can just define your own judgments t...

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.