cp's OEIS Frontend

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

%I A369409 #21 Jan 30 2024 04:11:43
%S A369409 31,31,311,31111,301,31,311,31111,310,31,311,31,311,31111,311111111,
%T A369409 3111111110,31111100,311111,31111111111,311111111110,3111111100,
%U A369409 31111111,311101,3001,31,311,31111,311111111,3111111110,31111100,311111,31111111111,311111111110,3111111100,31111111
%N 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).
%C A369409 See A368946 for the description of the MIU formal system.
%C A369409 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.
%C A369409 Step 1. Replace in turn every occurrence of U in S by III.
%C A369409 Step 2. Until we get MI:
%C A369409 Step 2a. If the number of I characters is even, remove half of them.
%C A369409 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.
%C A369409 Step 3. Reverse the order of the lines.
%C A369409 This algorithm generates a short proof, but not necessarily the shortest one.
%C A369409 Strings are encoded by mapping the characters M, I, and U to 3, 1, and 0, respectively.
%D A369409 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
%H A369409 Paolo Xausa, <a href="/A369409/b369409.txt">Table of n, a(n) for n = 1..10823</a> (rows 1..682 of the triangle, flattened).
%H A369409 Armando B. Matos and Luis Filipe Antunes, <a href="https://www.researchgate.net/publication/2845974_Short_proofs_for_MIU_theorems">Short Proofs for MIU theorems</a>, Technical Report Series DCC-98-01, University of Porto, 1998.
%H A369409 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H A369409 <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%e A369409 Triangle begins:
%e A369409   [1] 31;
%e A369409   [2] 31 311 31111 301;
%e A369409   [3] 31 311 31111 310;
%e A369409   [4] 31 311;
%e A369409   [5] 31 311 31111 ... 31111100 ... 31111111111 ... 3111111100 31111111 311101 3001;
%e A369409   ...
%e A369409 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.
%e A369409 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.
%t A369409 MIUStrings[n_] := Map["3" <> FromCharacterCode[# + 48]&, Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&]];
%t A369409 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]]]]];
%t A369409 Map[FromDigits, Map[MIUProofLines, Flatten[Array[MIUStrings, 3, 2]]], {2}]
%Y A369409 Cf. A368946, A369173, A369408, A369410 (row lengths), A369411, A369414.
%Y A369409 Cf. A369586 (analog for shortest proofs).
%K A369409 nonn,tabf
%O A369409 1,1
%A A369409 _Paolo Xausa_, Jan 23 2024