7
$\begingroup$

(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.

enter image description here

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''''''''''''''''''''''''''''''''''''''''''''''''''')>>>>>>>>>
$\endgroup$
13
  • 4
    $\begingroup$ To begin with one needs to define "MIU-number" before you "translate this description to TNT". For that matter, please add a definition or reference to TNT (which is evidently meant to be a formal language). Potentially a page (and edition) reference for this material in Gödel, Escher, Bach would satisfy this, but you seem to have started along the lines of including some attempts in the body of your Question (which will make it accessible to Readers who don't have a copy of D. Hofstadter's book). $\endgroup$
    – hardmath
    Commented Apr 26, 2018 at 16:37
  • 1
    $\begingroup$ See stackoverflow.com/questions/644569/… for a discussion of powers. "b is a MIU number" requires an encoding of the processes for building MIU numbers, just as "b is a power of 10$ requires some encoding - prime powers are much easier. I don't think you are right to suggest this is a hole in the book - rather it is a challenge to those who want to take it up. $\endgroup$ Commented Apr 26, 2018 at 16:57
  • 1
    $\begingroup$ @MarkBennet: Hofstadter is very explicit when he intend something to be a challenge; in this case I see no indication that he intends this as a challenge; alternative explanations (that he didn't know how to do it himself, or didn't bother to) seem to me more plausible. A matter of opinion, in the end. $\endgroup$
    – kjo
    Commented Apr 26, 2018 at 17:04
  • 5
    $\begingroup$ If I remember correctly, there is one hugely nontrivial step that Hofstadter completely leaves out, and that is using the Chinese remainder theorem to encode sequences in the language of arithmetic. See en.wikipedia.org/wiki/G%C3%B6del_numbering_for_sequences. $\endgroup$ Commented Apr 27, 2018 at 21:26
  • 1
    $\begingroup$ related ? math.stackexchange.com/questions/312891/… $\endgroup$
    – mercio
    Commented Apr 28, 2018 at 12:22

2 Answers 2

7
+500
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ Sorry, I cannot understand the post that serves as the basis for your answer. I just posted a question about it here: math.stackexchange.com/q/2761716/13675 $\endgroup$
    – kjo
    Commented May 1, 2018 at 11:59
  • 1
    $\begingroup$ @kjo Just posted an answer there; hope it's helpful. $\endgroup$
    – BallBoy
    Commented May 1, 2018 at 12:40
3
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Nice digit-checking sentence! $\endgroup$
    – BallBoy
    Commented Apr 30, 2018 at 19:26
  • $\begingroup$ Sorry, I cannot understand the post that serves as the basis for your answer. I just posted a question about it here: math.stackexchange.com/q/2761716/13675 $\endgroup$
    – kjo
    Commented May 1, 2018 at 11:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .