> At some level you need to add actual integers together. For that you need to access the internal representation of both integers at once
Not necessarily.
Not necessarily.
A proposition about an implementation aspect of the language you're working in is testable in that language if a program in that language can produce output which is different based on whether or not that proposition is true. If the proposition isn't testable in that language, then it doesn't lie on the "all the way down" path which begins inside the language.