A369410 Irregular triangle read by rows: row n lists the length of a "normal" proof (see comments) for each of the distinct derivable strings (theorems) in the MIU formal system that are n characters long.

1, 4, 4, 2, 13, 13, 8, 13, 8, 8, 11, 11, 6, 11, 6, 6, 11, 6, 6, 6, 3, 12, 12, 18, 12, 18, 18, 12, 18, 18, 18, 12, 12, 18, 18, 18, 12, 18, 12, 12, 12, 7, 10, 10, 16, 10, 16, 16, 10, 16, 16, 16, 10, 10, 16, 16, 16, 10, 16, 10, 10, 10, 5, 10, 16, 16, 16, 10, 16, 10, 10, 10, 5, 16, 10, 10, 10, 5, 10, 10, 5, 10, 5, 5

Offset: 2

Author

Paolo Xausa, Jan 23 2024

Keywords

• nonn
• tabf

Comments

See A368946 for the description of the MIU formal system, A369173 for the triangle of the corresponding strings (theorems) and A369409 for the definition of "normal" proof.

Examples

			Triangle begins:
  [2]  1;
  [3]  4  4  2;
  [4] 13 13  8 13  8  8;
  [5] 11 11  6 11  6  6 11  6  6  6  3;
  ...
For the theorem MIU (310), which is given by A369173(3,2), the "normal" proof is MI (31) -> MII (311) -> MIIII (31111) -> MIU (310), which consists of 4 lines: T(3,2) is therefore 4.
		

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 = 2..10922 (rows 2..14 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

Row lengths of A369409.

Cf. A368946, A369173, A369408, A369411, A369412.

Cf. A024495 (row lengths).

Programs

Mathematica

MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
MIUProofLineCount[t_] := Module[{c = Count[t, 0], ni}, ni = Length[t] + 2*c; While[ni > 1, If[OddQ[ni], ni = (ni+3)/2; c += 4, ni/=2; c++]]; c+1];
Map[MIUProofLineCount, Array[MIUDigitsW3, 7, 2], {2}]

Formula

T(n,k) >= A369408(n,k).

If A369173(n,k) contains no zeros and 3+2^m ones (for m >= 0), then T(n,k) = 4*m + 3.