A369408 - OEIS

%I #28 Jan 30 2024 04:11:11

%S 1,4,2,2,11,5,8,5,8,3,9,9,6,9,5,6,9,6,3,6,3

%N Irregular triangle read by rows: T(n,k) is the length of the shortest proof for the MIU formal system string (theorem) given by A369173(n,k).

%C See A368946 for the description of the MIU formal system and A369173 for the triangle of the corresponding derivable strings.

%C The length of the shortest proof for a string (theorem) S is the number of lines of the shortest possible derivation of S.

%C A369173(n,k) first appears in row T(n,k) - 1 in triangle A368946.

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

%H Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.

%H <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.

%F T(n,k) <= A369410(n,k).

%e Triangle begins:

%e   [2]  1;

%e   [3]  4  2  2;

%e   [4] 11  5  8  5  8  3;

%e   [5]  9  9  6  9  5  6  9  6  3  6  3;

%e   ...

%e For the theorem MUI (301), which is given by A369173(3,1), the shortest derivation from the axiom MI is MI (31) -> MII (311) -> MIIII (31111) -> MIU (301) (4 lines), so T(3,1) = 4.

%t MIUStringsW3[n_] := Map[FromCharacterCode[# + 48]&, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];

%t MIUStepDW3[s_] := DeleteDuplicates[Flatten[Map[{If[StringEndsQ[#, "1"], # <> "0", Nothing], # <> #, StringReplaceList[#, {"111" -> "0", "00" -> ""}]} &, s]]];

%t Module[{rowmax = 5, treedepth = 10, tree}, tree = NestList[MIUStepDW3, {"1"}, treedepth]; Map[Quiet[Check[Position[tree, #, {2}][[1,1]], "Not found"]]&, Array[MIUStringsW3, rowmax - 1, 2], {2}]]

%Y Cf. A024495 (row lengths), A331536, A368946, A369173, A369410.

%Y Cf. A369586 (proofs), A369587 (number of symbols).

%K nonn,tabf,hard,more

%O 2,2

%A _Paolo Xausa_, Jan 22 2024