cp's OEIS Frontend

This is a front-end for the Online Encyclopedia of Integer Sequences, made by Christian Perfect. The idea is to provide OEIS entries in non-ancient HTML, and then to think about how they're presented visually. The source code is on GitHub.

Showing 1-4 of 4 results.

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

Original entry on oeis.org

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

Views

Author

Paolo Xausa, Jan 23 2024

Keywords

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

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}]

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

Original entry on oeis.org

1, 4, 2, 2, 11, 5, 8, 5, 8, 3, 9, 9, 6, 9, 5, 6, 9, 6, 3, 6, 3
Offset: 2

Views

Author

Paolo Xausa, Jan 22 2024

Keywords

Comments

See A368946 for the description of the MIU formal system and A369173 for the triangle of the corresponding derivable strings.
The length of the shortest proof for a string (theorem) S is the number of lines of the shortest possible derivation of S.
A369173(n,k) first appears in row T(n,k) - 1 in triangle A368946.

Examples

			Triangle begins:
  [2]  1;
  [3]  4  2  2;
  [4] 11  5  8  5  8  3;
  [5]  9  9  6  9  5  6  9  6  3  6  3;
  ...
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.

References

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

Links

Crossrefs

Cf. A024495 (row lengths), A331536, A368946, A369173, A369410.
Cf. A369586 (proofs), A369587 (number of symbols).

Programs

  • Mathematica
    MIUStringsW3[n_] := Map[FromCharacterCode[# + 48]&, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
MIUStepDW3[s_] := DeleteDuplicates[Flatten[Map[{If[StringEndsQ[#, "1"], # <> "0", Nothing], # <> #, StringReplaceList[#, {"111" -> "0", "00" -> ""}]} &, s]]];
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}]]

Formula

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

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

Original entry on oeis.org

2, 13, 13, 5, 94, 94, 47, 94, 47, 47, 75, 75, 31, 75, 31, 31, 75, 31, 31, 31, 10, 120, 120, 165, 120, 165, 165, 120, 165, 165, 165, 90, 120, 165, 165, 165, 90, 165, 90, 90, 90, 43, 91, 91, 139, 91, 139, 139, 91, 139, 139, 139, 70, 91, 139, 139, 139, 70, 139, 70
Offset: 2

Views

Author

Paolo Xausa, Jan 23 2024

Keywords

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.
The number of symbols of a proof is the sum of the number of characters contained in all of the strings (lines) of the proof; cf. Matos and Antunes (1998).

Examples

			Triangle begins:
  [2]  2;
  [3] 13 13  5;
  [4] 94 94 47 94 47 47;
  [5] 75 75 31 75 31 31 75 31 31 31 10;
  ...
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 a total of 13 symbols (counting only M, I and U characters): T(3,2) is therefore 13.

References

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

Links

Crossrefs

Cf. A368946, A369173, A369408, A369409, A369410, A369413.
Cf. A369587 (analog for shortest proofs).
Cf. A024495 (row lengths).

Programs

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

Formula

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

A369412 Maximum length of a "normal" proof (see comments) for strings (theorems) in the MIU formal system that are n characters long.

Original entry on oeis.org

1, 4, 13, 11, 18, 16, 25, 23, 24, 22, 26, 24, 34, 32, 33, 31, 35, 33, 34, 32, 39, 37, 49
Offset: 2

Views

Author

Paolo Xausa, Jan 23 2024

Keywords

Comments

See A368946 for the description of the MIU formal system, A369410 for the triangle of the corresponding proof lengths and A369409 for the definition of "normal" proof.

References

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

Links

Crossrefs

Cf. A024495, A368946, A369173, A369409, A369410, A369413.

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[Max, Map[MIUProofLineCount, Array[MIUDigitsW3, 15, 2], {2}]]

Formula

a(n) = max_{k=1..A024495(n)} A369410(n,k).
Showing 1-4 of 4 results.

Started in 1964 by Neil J. A. Sloane | Maintained by The OEIS Foundation Inc.

Content is available under The OEIS End-User License Agreement.