As for expressing “b is a power of 10”: if we could just find a way to simulate finite lists of numbers within TNT, we would be set. For then we could define “b is a power of 10” as “there exists a list whose initial element is 1, whose (k+1)-th element is 10 * its k-th element [for all k], and whose last element is b”.

And, as it turns out, we *can* simulate finite lists of numbers within TNT. The Chinese Remainder Theorem is key to the usual parlor trick here. But it’s just a convoluted hack to prove a technical curiosity; if you really cared about having the ability to express such things, you’d work (explicitly or implicitly) in a system that had more directly built-in than just TNT (even if, at the end of the day, it turns out that TNT could, contrivedly express all the same things).

Still, if you care to see the hack (creditable to a throwaway line by Goedel in his 1931 paper, and on which far too much time and mental space has been spent ever since): let’s start by considering how to specify some very simple sequences. For example, an arithmetic sequence (that is, in which each element is some fixed value plus the previous element, such as <1, 2, 3, …> or <7, 10, 13, 16, …>) can be specified by giving two values: the first element (call this Start), and the amount by which to increase each time (call this Jump). Obviously, to extract the k-th element of such a sequence, one just uses the formula Start + k*Jump. [Pedantry: This is on the convention that the first element is the 0-th one]

This is all good and well, but what we want is a way of simulating arbitrary finite lists, not very particular infinite sequences. Patience, patience. Let’s see if we can simulate more complicated sequences.

Well, if we can simulate arithmetic sequences, then we can also simulate the results of applying any definable operation to arithmetic sequences. In particular, let’s now talk about specifying a sequence with three values: let’s call them Start, Jump, and Div. The sequence this specifies will be the result of applying the operation “Div mod _” to the arithmetic sequence specified by Start and Jump; that is, the k-th element of this sequence will be Div mod (Start + k*Jump). [In case you don’t know, “Div mod x” means “The remainder when Div is divided by x”]. So, for example, the sequence specified with Start = 7, Jump = 3, Div = 100 will be <100 mod 7, 100 mod 10, 100 mod 13, 100 mod 16, …> = <2, 0, 9, 4, …>. Let’s call such sequences, I dunno, how about “divarithmetic sequences”?.

What’s the use of these convoluted things? Well, supposing I told you that any finite list you can think of is the start of some divarithmetic sequence. Then we can actually specify a finite list using four numbers: Start, Jump, Div, and the Length of the list.

And we’d then be able to define “b is a power of 10” as “there exist numbers Start, Jump, Div, and Length such that the corresponding list has a first element of 1, a last element of b, and each element within it is 10 times the previous one”, which is to say, “there exist numbers Start, Jump, Div, and Length such that Div mod Start = 1, Div mod (Start + Length * Jump) = b, and for all k < Length, Div mod (Start + (k+1)*Jump) = 10 * (Div mod (Start + k*Jump))”. [Pedantry: Technically, what I’ve written here actually takes the length of the list to be Length + 1. It was easier to write and makes no difference for our purposes.]

If you really care about expressing it in symbols, well, you can expand it all out (remember to expand out the definitions of “mod” and “<”).

Ok, then, the only thing that’s left for us to prove is that it really is true that any finite list of numbers is the start of some divarithmetic sequence. I’ll put that in another post for cleanliness’s sake.