Double exponentials in weak arithmetic

26 Views Asked by At

In arithmetic without total exponentiation, the exponentiable numbers are closed under addition. It is thus common to think of natural numbers as binary strings $n : |n| \to 2$, whose (unary) lengths $|n|$ may be added but not necessarily multiplied.

Likewise, the twice exponentiable numbers form a cut. We could thus think of natural numbers as predicates $n : |n| \to 2$, whose domains $|n|$ are now collections of binary strings $||n|| \to 2$, whose lengths $||n||$ still have successors but may not necessarily be added. I visualize the $n$ as coloured binary trees, whose widths $|n|$ may be added but heights $||n||$ may not.

Has this perspective been used in the literature? What would be some good places to start reading in order to understand how it connects to existing theory and results?

I'm a novice to logic, so there's a lot of standard terminology that I'm not yet familiar with.