A369409 Irregular triangle read by rows: row n lists the lines of a "normal" proof (see comments) for the MIU formal system string (theorem) given by A369173(n+1).

31, 31, 311, 31111, 301, 31, 311, 31111, 310, 31, 311, 31, 311, 31111, 311111111, 3111111110, 31111100, 311111, 31111111111, 311111111110, 3111111100, 31111111, 311101, 3001, 31, 311, 31111, 311111111, 3111111110, 31111100, 311111, 31111111111, 311111111110, 3111111100, 31111111

Offset: 1

Author

Paolo Xausa, Jan 23 2024

Keywords

• nonn
• tabf

Comments

See A368946 for the description of the MIU formal system.

Matos and Antunes (1998) define a "normal" proof for a string (theorem) S the output of the following algorithm, which generates the lines (strings) of the proof.

Step 1. Replace in turn every occurrence of U in S by III.

Step 2. Until we get MI:

Step 2a. If the number of I characters is even, remove half of them.

Step 2b. Otherwise, apply in turn the following transformations: append UU, replace the first U by III, remove the remaining U, remove half of the I characters.

Step 3. Reverse the order of the lines.

This algorithm generates a short proof, but not necessarily the shortest one.

Strings are encoded by mapping the characters M, I, and U to 3, 1, and 0, respectively.

Examples

			Triangle begins:
  [1] 31;
  [2] 31 311 31111 301;
  [3] 31 311 31111 310;
  [4] 31 311;
  [5] 31 311 31111 ... 31111100 ... 31111111111 ... 3111111100 31111111 311101 3001;
  ...
For the theorem MUI (301), which is given by A369173(3,1) or (after flattening) A369173(3), steps 1 and 2 of the algorithm generate the lines 301 -> 31111 -> 311 -> 31 which, when reversed (step 3), give row 2 of the present sequence.
For the theorem MIUU (3100), which is given by A369173(4,4) or (after flattening) A369173(9), steps 1 and 2 of the algorithm generate the lines 3100 -> 311110 -> 31111111 -> 3111111100 -> 311111111110 -> 31111111111 -> 311111 -> 31111100 -> 3111111110 -> 311111111 -> 31111 -> 311 -> 31 which, when reversed (step 3), give row 8 of the present sequence.
		

References

• Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.

Links

• Paolo Xausa, Table of n, a(n) for n = 1..10823 (rows 1..682 of the triangle, flattened).
• Armando B. Matos and Luis Filipe Antunes, Short Proofs for MIU theorems, Technical Report Series DCC-98-01, University of Porto, 1998.
• Wikipedia, MU Puzzle.
• Index entries for sequences from "Goedel, Escher, Bach".

Crossrefs

Cf. A368946, A369173, A369408, A369410 (row lengths), A369411, A369414.

Cf. A369586 (analog for shortest proofs).

Programs

Mathematica

MIUStrings[n_] := Map["3" <> FromCharacterCode[# + 48]&, Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&]];
MIUProofLines[t_] := Module[{s = t}, Reverse[Flatten[Reap[Sow[s]; While[StringCount[s, "0"] > 0, Sow[s = StringReplace[s, "0" -> "111", 1]]]; While[s != "31", If[EvenQ[StringCount[s, "1"]], Sow[s = StringDrop[s, -(StringLength[s]-1)/2]], Sow[{s <> "00", s <> "1110", s <> "111", s = StringDrop[s, -(StringLength[s]-4)/2]}]]]][[2,1]]]]];
Map[FromDigits, Map[MIUProofLines, Flatten[Array[MIUStrings, 3, 2]]], {2}]