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

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')) $$

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.