GEB: How to write "b is a MIU-number" in TNT notation

Question

(NB: This question requires access to, and familiarity with, the book Gödel, Escher, Bach, by Douglas Hofstadter. Unfortunately, I am not able to make the question entirely self-contained. In any case, for a description of the MIU system, see here, and for one of TNT, see here.)

---

This question refers to p. 263 of the latest American edition of Gödel, Escher, Bach.

In that page, Hofstadter writes (my emphasis):

...I pointed out in Chapter VIII that even such a simple arithmetical predicate as "b is a power of 10" is very tricky to code into TNT-notation—and the predicate "b is a MIU-number" is a lot more complicated than that! Still it can be found, ...

I emphasized the last sentence above because, in my opinion, the book's entire rendition of Gödel's proof (arguably its centerpiece) rests squarely on it. If that assertion must be taken on faith, then the book's entire proof must be taken on faith.

It's terribly disappointing that in a book of this size, one that makes such demands of its readers, and one that is filled with massive illustrations (such as the full sequence of a viral genome, on p. 176), the author chose not to provide explicitly such a crucial exhibit in the argument. Yes, I know that the resulting TNT string would be huge (even before substituting SSSSSSSSSSSSSSSSSSSSSSSSSSSSSS0 for every occurrence of b), and basically incomprehensible (though I doubt it would be any more so than the genome alluded to earlier), but it is such an important bit of evidence that to have to take its existence on faith is, as I said, terribly disappointing.

Therefore, as this question title says, I am looking for the translation of the predicate "b is a MIU-number" to TNT notation.

I have searched online for this translation without success.

As I already alluded to, I realize that the translation of this predicate to TNT notation could result in an enormous string, perhaps unmanageably so.

In that case, the next best thing would be a scaffold written in a formal language L more expressive (hence more succinct) than TNT, but from which one could translate into TNT through a straightforward process of expansion (i.e. replacement of succinct L expressions by full-blown TNT expressions).

For example, such a language L may include a symbol $\leq$ that could be translated to "lax TNT" by applying the following substitution: $$a\leq b \to \exists c:(a+c)=b$$

...or to "austere TNT":

$$a\leq a^\prime \to \exists a^{\prime\prime}:(a+a^{\prime\prime})=a^\prime$$

Likewise, L could include a symbol $\lt$, that could be translated to TNT with the substitution:

$$a \lt b \to \mathbf{S}a \le b \;,$$

or

$$a \lt a^\prime \to \mathbf{S}a \le a^\prime\;.$$

The point here is that the LHSs above are considerably more succinct than the corresponding RHSs, and an expression containing the former can be translated "mechanically" to one consisting only of valid TNT symbols through relatively straightforward substitutions. Therefore, L may be thought of as TNT augmented with a finite set of "abbreviations", like those exemplified by $\le$ and $\lt$ above.

It's not hard to see that, with enough "abbreviations" of this sort, one may be able to translate the predicate "b is a MIU-number" to an L-string of manageable length, even if the corresponding TNT string is a couple of orders of magnitude larger.

---

For what it's worth, I know that the predicate "b is a MIU-number" is equivalent to the following predicate:

b is a number consisting of $3$ followed by $0$'s and $1$'s, where the number $n_1$ of $1$'s satisfies $n_1 \not \equiv 0 \pmod 3$.

(See this answer by Eric Wofsey for a nice proof of this equivalence.)

Therefore, to answer this question, it would suffice to translate this alternative, but equivalent, predicate to TNT notation.

---

UPDATE

Below are two versions of my rendition of "b is a MIU-number" (wrapped at 100-characters per line) using my interpretation of Y. Forman's answer.

(The purpose of these print outs is only to get a sense of the actual size and composition of these strings. It's not meant to be illuminating in any other way.)

The first version (length = 1,497, including two occurrences of b) deviates from austere TNT notation in two ways:

1. Instead of, e.g., SSSSSSSSSS0, I write 10.
2. Instead of primes ('), I use numerical suffixes to generate variable names; thus, instead of a''''''''', I use a9.

∃a0:∃a1:∃a2:<∃a6:<a0=((S(a1·S0)·a6)+31)∧∃a7:(S31+a7)=S(a1·S0)>∧<∃a8:<a0=((S(a1·Sa2)·a8)+b)∧∃a9:(Sb+a
9)=S(a1·Sa2)>∧∀a3:∀a4:∀a5:<<∃a10:(Sa3+a10)=a2∧<∃a11:<a0=((S(a1·Sa3)·a11)+a4)∧∃a12:(Sa4+a12)=S(a1·Sa3
)>∧∃a13:<a0=((S(a1·SSa3)·a13)+a5)∧∃a14:(Sa5+a14)=S(a1·SSa3)>>>⊃<∃a15:<a4=((10·a15)+1)∧a5=(10·a4)>∨<∃
a16:∃a17:∃a18:<a4=((3·a18)+a16)∧<∃a19:∃a20:<∃a23:<a19=((S(a20·S0)·a23)+S0)∧∃a24:(SS0+a24)=S(a20·S0)>
∧<∃a25:<a19=((S(a20·Sa17)·a25)+a18)∧∃a26:(Sa18+a26)=S(a20·Sa17)>∧∀a21:∀a22:<<∃a27:(Sa21+a27)=a17∧∃a2
8:<a19=((S(a20·Sa21)·a28)+a22)∧∃a29:(Sa22+a29)=S(a20·Sa21)>>⊃∃a30:<a19=((S(a20·SSa21)·a30)+(10·a22))
∧∃a31:(S(10·a22)+a31)=S(a20·SSa21)>>>>∧<∃a32:(Sa16+a32)=a18∧a5=((a18·a4)+a16)>>>∨<∃a33:∃a34:∃a35:∃a3
6:<a4=((a36·(1000·a35))+((111·a35)+a33))∧<∃a37:∃a38:<∃a41:<a37=((S(a38·S0)·a41)+S0)∧∃a42:(SS0+a42)=S
(a38·S0)>∧<∃a43:<a37=((S(a38·Sa34)·a43)+a35)∧∃a44:(Sa35+a44)=S(a38·Sa34)>∧∀a39:∀a40:<<∃a45:(Sa39+a45
)=a34∧∃a46:<a37=((S(a38·Sa39)·a46)+a40)∧∃a47:(Sa40+a47)=S(a38·Sa39)>>⊃∃a48:<a37=((S(a38·SSa39)·a48)+
(10·a40))∧∃a49:(S(10·a40)+a49)=S(a38·SSa39)>>>>∧<∃a50:(Sa33+a50)=a35∧a5=((a36·(10·a35))+a33)>>>∨∃a51
:∃a52:∃a53:∃a54:<a4=((a54·(100·a53))+a51)∧<∃a55:∃a56:<∃a59:<a55=((S(a56·S0)·a59)+S0)∧∃a60:(SS0+a60)=
S(a56·S0)>∧<∃a61:<a55=((S(a56·Sa52)·a61)+a53)∧∃a62:(Sa53+a62)=S(a56·Sa52)>∧∀a57:∀a58:<<∃a63:(Sa57+a6
3)=a52∧∃a64:<a55=((S(a56·Sa57)·a64)+a58)∧∃a65:(Sa58+a65)=S(a56·Sa57)>>⊃∃a66:<a55=((S(a56·SSa57)·a66)
+(10·a58))∧∃a67:(S(10·a58)+a67)=S(a56·SSa57)>>>>∧<∃a68:(Sa51+a68)=a53∧a5=((a54·a53)+a51)>>>>>>>>>

The second version (length = 10,088, including two occurrences of b) follows austere TNT notation.

∃a:∃a':∃a'':<∃a'''''':<a=((S(a'·S0)·a'''''')+SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS0)∧∃a''''''':(SSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSS0+a''''''')=S(a'·S0)>∧<∃a'''''''':<a=((S(a'·Sa'')·a'''''''')+b)∧∃a''''''''':(S
b+a''''''''')=S(a'·Sa'')>∧∀a''':∀a'''':∀a''''':<<∃a'''''''''':(Sa'''+a'''''''''')=a''∧<∃a'''''''''''
:<a=((S(a'·Sa''')·a''''''''''')+a'''')∧∃a'''''''''''':(Sa''''+a'''''''''''')=S(a'·Sa''')>∧∃a''''''''
''''':<a=((S(a'·SSa''')·a''''''''''''')+a''''')∧∃a'''''''''''''':(Sa'''''+a'''''''''''''')=S(a'·SSa'
'')>>>⊃<∃a''''''''''''''':<a''''=((SSSSSSSSSS0·a''''''''''''''')+S0)∧a'''''=(SSSSSSSSSS0·a'''')>∨<∃a
'''''''''''''''':∃a''''''''''''''''':∃a'''''''''''''''''':<a''''=((SSS0·a'''''''''''''''''')+a''''''
'''''''''')∧<∃a''''''''''''''''''':∃a'''''''''''''''''''':<∃a''''''''''''''''''''''':<a'''''''''''''
''''''=((S(a''''''''''''''''''''·S0)·a''''''''''''''''''''''')+S0)∧∃a'''''''''''''''''''''''':(SS0+a
'''''''''''''''''''''''')=S(a''''''''''''''''''''·S0)>∧<∃a''''''''''''''''''''''''':<a''''''''''''''
'''''=((S(a''''''''''''''''''''·Sa''''''''''''''''')·a''''''''''''''''''''''''')+a''''''''''''''''''
)∧∃a'''''''''''''''''''''''''':(Sa''''''''''''''''''+a'''''''''''''''''''''''''')=S(a'''''''''''''''
'''''·Sa''''''''''''''''')>∧∀a''''''''''''''''''''':∀a'''''''''''''''''''''':<<∃a'''''''''''''''''''
'''''''':(Sa'''''''''''''''''''''+a''''''''''''''''''''''''''')=a'''''''''''''''''∧∃a'''''''''''''''
''''''''''''':<a'''''''''''''''''''=((S(a''''''''''''''''''''·Sa''''''''''''''''''''')·a''''''''''''
'''''''''''''''')+a'''''''''''''''''''''')∧∃a''''''''''''''''''''''''''''':(Sa''''''''''''''''''''''
+a''''''''''''''''''''''''''''')=S(a''''''''''''''''''''·Sa''''''''''''''''''''')>>⊃∃a''''''''''''''
'''''''''''''''':<a'''''''''''''''''''=((S(a''''''''''''''''''''·SSa''''''''''''''''''''')·a''''''''
'''''''''''''''''''''')+(SSSSSSSSSS0·a''''''''''''''''''''''))∧∃a''''''''''''''''''''''''''''''':(S(
SSSSSSSSSS0·a'''''''''''''''''''''')+a''''''''''''''''''''''''''''''')=S(a''''''''''''''''''''·SSa''
''''''''''''''''''')>>>>∧<∃a'''''''''''''''''''''''''''''''':(Sa''''''''''''''''+a''''''''''''''''''
'''''''''''''')=a''''''''''''''''''∧a'''''=((a''''''''''''''''''·a'''')+a'''''''''''''''')>>>∨<∃a'''
'''''''''''''''''''''''''''''':∃a'''''''''''''''''''''''''''''''''':∃a''''''''''''''''''''''''''''''
''''':∃a'''''''''''''''''''''''''''''''''''':<a''''=((a''''''''''''''''''''''''''''''''''''·(SSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS0·a''''
'''''''''''''''''''''''''''''''))+((SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS0·a''''''''''''''''''''''''''''''''''')+a''''''''''''
'''''''''''''''''''''))∧<∃a''''''''''''''''''''''''''''''''''''':∃a'''''''''''''''''''''''''''''''''
''''':<∃a''''''''''''''''''''''''''''''''''''''''':<a'''''''''''''''''''''''''''''''''''''=((S(a''''
''''''''''''''''''''''''''''''''''·S0)·a''''''''''''''''''''''''''''''''''''''''')+S0)∧∃a'''''''''''
''''''''''''''''''''''''''''''':(SS0+a'''''''''''''''''''''''''''''''''''''''''')=S(a'''''''''''''''
'''''''''''''''''''''''·S0)>∧<∃a''''''''''''''''''''''''''''''''''''''''''':<a''''''''''''''''''''''
'''''''''''''''=((S(a''''''''''''''''''''''''''''''''''''''·Sa'''''''''''''''''''''''''''''''''')·a'
'''''''''''''''''''''''''''''''''''''''''')+a''''''''''''''''''''''''''''''''''')∧∃a''''''''''''''''
'''''''''''''''''''''''''''':(Sa'''''''''''''''''''''''''''''''''''+a'''''''''''''''''''''''''''''''
''''''''''''')=S(a''''''''''''''''''''''''''''''''''''''·Sa'''''''''''''''''''''''''''''''''')>∧∀a''
''''''''''''''''''''''''''''''''''''':∀a'''''''''''''''''''''''''''''''''''''''':<<∃a'''''''''''''''
'''''''''''''''''''''''''''''':(Sa'''''''''''''''''''''''''''''''''''''''+a'''''''''''''''''''''''''
'''''''''''''''''''')=a''''''''''''''''''''''''''''''''''∧∃a''''''''''''''''''''''''''''''''''''''''
'''''':<a'''''''''''''''''''''''''''''''''''''=((S(a''''''''''''''''''''''''''''''''''''''·Sa'''''''
'''''''''''''''''''''''''''''''')·a'''''''''''''''''''''''''''''''''''''''''''''')+a''''''''''''''''
'''''''''''''''''''''''')∧∃a''''''''''''''''''''''''''''''''''''''''''''''':(Sa'''''''''''''''''''''
'''''''''''''''''''+a''''''''''''''''''''''''''''''''''''''''''''''')=S(a'''''''''''''''''''''''''''
'''''''''''·Sa''''''''''''''''''''''''''''''''''''''')>>⊃∃a'''''''''''''''''''''''''''''''''''''''''
''''''':<a'''''''''''''''''''''''''''''''''''''=((S(a''''''''''''''''''''''''''''''''''''''·SSa'''''
'''''''''''''''''''''''''''''''''')·a'''''''''''''''''''''''''''''''''''''''''''''''')+(SSSSSSSSSS0·
a''''''''''''''''''''''''''''''''''''''''))∧∃a''''''''''''''''''''''''''''''''''''''''''''''''':(S(S
SSSSSSSSS0·a'''''''''''''''''''''''''''''''''''''''')+a'''''''''''''''''''''''''''''''''''''''''''''
'''')=S(a''''''''''''''''''''''''''''''''''''''·SSa''''''''''''''''''''''''''''''''''''''')>>>>∧<∃a'
''''''''''''''''''''''''''''''''''''''''''''''''':(Sa'''''''''''''''''''''''''''''''''+a''''''''''''
'''''''''''''''''''''''''''''''''''''')=a'''''''''''''''''''''''''''''''''''∧a'''''=((a'''''''''''''
'''''''''''''''''''''''·(SSSSSSSSSS0·a'''''''''''''''''''''''''''''''''''))+a'''''''''''''''''''''''
'''''''''')>>>∨∃a''''''''''''''''''''''''''''''''''''''''''''''''''':∃a'''''''''''''''''''''''''''''
''''''''''''''''''''''':∃a''''''''''''''''''''''''''''''''''''''''''''''''''''':∃a''''''''''''''''''
'''''''''''''''''''''''''''''''''''':<a''''=((a'''''''''''''''''''''''''''''''''''''''''''''''''''''
'·(SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS
SSS0·a'''''''''''''''''''''''''''''''''''''''''''''''''''''))+a'''''''''''''''''''''''''''''''''''''
'''''''''''''')∧<∃a''''''''''''''''''''''''''''''''''''''''''''''''''''''':∃a'''''''''''''''''''''''
''''''''''''''''''''''''''''''''':<∃a''''''''''''''''''''''''''''''''''''''''''''''''''''''''''':<a'
''''''''''''''''''''''''''''''''''''''''''''''''''''''=((S(a''''''''''''''''''''''''''''''''''''''''
''''''''''''''''·S0)·a''''''''''''''''''''''''''''''''''''''''''''''''''''''''''')+S0)∧∃a'''''''''''
''''''''''''''''''''''''''''''''''''''''''''''''':(SS0+a''''''''''''''''''''''''''''''''''''''''''''
'''''''''''''''')=S(a''''''''''''''''''''''''''''''''''''''''''''''''''''''''·S0)>∧<∃a''''''''''''''
''''''''''''''''''''''''''''''''''''''''''''''':<a''''''''''''''''''''''''''''''''''''''''''''''''''
'''''=((S(a''''''''''''''''''''''''''''''''''''''''''''''''''''''''·Sa''''''''''''''''''''''''''''''
'''''''''''''''''''''')·a''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''')+a'''''''''''
'''''''''''''''''''''''''''''''''''''''''')∧∃a''''''''''''''''''''''''''''''''''''''''''''''''''''''
'''''''':(Sa'''''''''''''''''''''''''''''''''''''''''''''''''''''+a'''''''''''''''''''''''''''''''''
''''''''''''''''''''''''''''')=S(a''''''''''''''''''''''''''''''''''''''''''''''''''''''''·Sa'''''''
''''''''''''''''''''''''''''''''''''''''''''')>∧∀a''''''''''''''''''''''''''''''''''''''''''''''''''
''''''':∀a'''''''''''''''''''''''''''''''''''''''''''''''''''''''''':<<∃a'''''''''''''''''''''''''''
'''''''''''''''''''''''''''''''''''':(Sa'''''''''''''''''''''''''''''''''''''''''''''''''''''''''+a'
'''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''')=a'''''''''''''''''''''''''''''''''''
'''''''''''''''''∧∃a'''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''':<a'''''''''''''
''''''''''''''''''''''''''''''''''''''''''=((S(a''''''''''''''''''''''''''''''''''''''''''''''''''''
''''·Sa''''''''''''''''''''''''''''''''''''''''''''''''''''''''')·a'''''''''''''''''''''''''''''''''
''''''''''''''''''''''''''''''')+a'''''''''''''''''''''''''''''''''''''''''''''''''''''''''')∧∃a''''
''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''':(Sa'''''''''''''''''''''''''''''''''''
'''''''''''''''''''''''+a''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''')=S(a'''''
'''''''''''''''''''''''''''''''''''''''''''''''''''·Sa''''''''''''''''''''''''''''''''''''''''''''''
''''''''''')>>⊃∃a'''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''':<a''''''''''''''
'''''''''''''''''''''''''''''''''''''''''=((S(a'''''''''''''''''''''''''''''''''''''''''''''''''''''
'''·SSa''''''''''''''''''''''''''''''''''''''''''''''''''''''''')·a'''''''''''''''''''''''''''''''''
''''''''''''''''''''''''''''''''')+(SSSSSSSSSS0·a'''''''''''''''''''''''''''''''''''''''''''''''''''
'''''''))∧∃a''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''':(S(SSSSSSSSSS0·a''''
'''''''''''''''''''''''''''''''''''''''''''''''''''''')+a'''''''''''''''''''''''''''''''''''''''''''
'''''''''''''''''''''''')=S(a''''''''''''''''''''''''''''''''''''''''''''''''''''''''·SSa'''''''''''
'''''''''''''''''''''''''''''''''''''''''''''')>>>>∧<∃a'''''''''''''''''''''''''''''''''''''''''''''
''''''''''''''''''''''':(Sa'''''''''''''''''''''''''''''''''''''''''''''''''''+a''''''''''''''''''''
'''''''''''''''''''''''''''''''''''''''''''''''')=a'''''''''''''''''''''''''''''''''''''''''''''''''
''''∧a'''''=((a''''''''''''''''''''''''''''''''''''''''''''''''''''''·a'''''''''''''''''''''''''''''
'''''''''''''''''''''''')+a''''''''''''''''''''''''''''''''''''''''''''''''''')>>>>>>>>>

Answer 1

One way to do this involves (as Eric Wofsey alluded to) encoding a sequence into a number. Once we can do this, we can define an MIU-sequence as a sequence where the first term is $31$, and each term is obtainable from the previous by one of the four MIU rules. Then $b$ is an MIU-number iff there is an MIU-sequence terminating with $b$.

There's a discussion of how to encode sequences here (and in other related questions on the site); I'll use Hagen von Eitzen's encoding there.

Hagen von Eitzen introduces the following abbreviations:

$$\begin{align}a\le b&\equiv\exists c\colon (a+c)=b\\ a< b&\equiv Sa\le b\\ \operatorname{mod}(a,b,c)&\equiv \exists d\colon a=((b\cdot d)+c)\land c<b\\ \operatorname{seq}(a,b,e,c)&\equiv \operatorname{mod}(a,S(b\cdot Se),c)\\ \operatorname{pow}(a,b,c)&\equiv\exists x\exists y\colon\operatorname{seq}(x,y,0,S0)\land\operatorname{seq}(x,y,b,c)\land \\&\quad\forall k\forall z\colon((k<b\land \operatorname{seq}(x,y,k,z))\supset\operatorname{seq}(x,y,Sk,a\cdot z))\end{align}$$

Intuitively, $\operatorname{seq}(a,b,e,c)$ is supposed to mean that the pair of numbers $a$ and $b$ encode a sequence where $c$ is the $e$th term of the sequence.

$\operatorname{pow}(a,b,c)$ is supposed to mean $c=a^b$; this isn't part of the sequence encoding but was relevant to the question asked there and will be helpful for encoding the MIU rules. (I hope you'll excuse the use of variables $k,x,z$ which aren't part of TNT; they can of course be considered as shorthand for $d',d'',d'''$ or something like that).

We also want to encode the MIU rules (I'm going to use $10$ as shorthand for $SSSSSSSSSS0$, etc.): $$\begin{align} \operatorname{M1}(a,b) &\equiv \exists c: a = ((10 \cdot c)+1)\land b = (10\cdot a) \\\operatorname{M2}(a,b) &\equiv \exists c \exists d \exists e : a=((3\cdot e)+c)\land \operatorname{pow}(10,d,e) \land c<e \land b = ((e \cdot a)+c) \\\operatorname{M3}(a,b) &\equiv \exists c \exists d \exists e \exists c': a = ((c' \cdot (1000 \cdot e))+(111 \cdot e)+c) \land \operatorname{pow}(10,d,e) \land c<e \land b = ((c' \cdot (10 \cdot e))+c) \\\operatorname{M4}(a,b) &\equiv \exists c \exists d \exists e \exists c': a = ((c' \cdot (100 \cdot e))+c) \land \operatorname{pow}(10,d,e) \land c<e \land b = ((c' \cdot e)+c) \end{align}$$

Intuitively, $\operatorname{M1}(a,b)$ says $b$ is obtainable from $a$ by the first MIU rule (according to their numbering in the Wikipedia article), etc.

Finally, to assert that $b$ is an MIU-number, we want to assert that there is a sequence encoded by a pair of numbers such that the first term is $31$, the last term is $b$, and each term is obtainable from the previous by one of the four rules. We can model off of Hagen von Eitzen's $\operatorname{pow}$ sentence, using $e$ for the length of the sequence and $x,y$ for the pair encoding it.

$$ \operatorname{MIUnumb}(b) \equiv \exists x \exists y \exists e : \operatorname{seq}(x,y,0,31) \land \operatorname{seq}(x,y,e,b) \land \forall d \forall a \forall a' : (d<e \land \operatorname{seq}(x,y,d,a) \land \operatorname{seq}(x,y,Sd,a')) \supset (\operatorname{M1}(a,a') \lor \operatorname{M2}(a,a') \lor \operatorname{M3}(a,a') \lor \operatorname{M4}(a,a')) $$

Answer 2

Just like Y. Forman's answer, I'll make use of Hagen von Eitzen's elegant solution for the power-of-ten problem. However, instead of following the actual definition of MIU numbers, I'll use the one quoted as being equivalent:

b is a number consisting of $3$ followed by $0$'s and $1$'s, where the number $n_1$ of $1$'s satisfies $n_1 \not\equiv 0\pmod 3$.

First, let's check if number $b$ consists solely of zeros and ones, apart from the very first digit which must be equal to $3$. Using the "$\operatorname{pow}$", "$<$", "$10$" and "$3$" abbreviations from the referenced post, we can express this as follows:

$$(\forall e)(\forall m)(\operatorname{pow}(10,e,m)\implies (\exists q)(\exists r)(b = q\times m + r \land (r<m)\land (q=0\lor q=3\lor (\exists q')(q = 10\times Sq' \lor q=S(10\times Sq')))))$$

In this expression, $e$ is used as exponent of $10$ used to check each digit of $b$ separately, with $m=10^e$. Dividing $b$ by $m$ yields $q$(uotient) and $r$(emainder), where the quotient can be equal to $3$ (the leading digit of $b$), zero (if we're looking at "digits" preceding the first one) or it must be greater or equal to $10$ and its last digit must be $0$ or $1$.

This "almost" works; it only fails for $b=0$ where all the digits fall into the $q=0$ category. We could fix this simply by adding a condition of $b\not =0$, but as it turns out, it will be resolved for free by the other property: The condition $n_1\not\equiv 0\pmod 3$.

This one can be checked in a very compact way: $$\neg(\exists k) b=3\times k$$

It works because a number is divisible by $3$ if and only if its digital sum is divisible by $3$ and the digital sum of $b$ is $(3+n_1)$. Thus, $b$ itself is forbidden from being a multiple of $3$; which also resolves the $b=0$ case.

Combining the two formulas above and substituting the definitions of $\operatorname{pow}$, $<$, the constants and renaming the variables would give the desired predicate expressed in pure TNT... but it would be no pretty sight. However, due to using just one occurrence of $\operatorname{pow}$, this expression should be considerably shorter than the one built straight from the definition of MIU.