cp's OEIS Frontend

A101273 Theorems from propositional calculus, translated into decimal digits.

%I A101273 #41 Feb 16 2025 08:32:55
%S A101273 171,181,272,282,1531,1631,2532,2632,3151,3161,3252,3262,11711,11811,
%T A101273 12712,12812,14171,14181,14271,14272,15171,15172,16171,16181,17141,
%U A101273 17161,17162,17261,17331,17910,18141,18161,18331,18910,21721,21821,22722,22822,24171
%N A101273 Theorems from propositional calculus, translated into decimal digits.
%C A101273 Blocks of 1s and 2s are variables: A = 1, B = 2, C = 11, D = 12, E = 21, ... Not = 3; And = 4; Xor = 5; Or = 6; Implies = 7; Equiv = 8; Left Parenthesis = 9; Right Parenthesis = 0.
%C A101273 Operator binding strength is in numerical order, Not > And > ... > Equiv.
%C A101273 The non-associative "Implies" is evaluated from Left to Right; A->B->C = is interpreted (A->B)->C. Redundant parentheses are permitted.
%C A101273 This is a decimal Goedelization of theorems from a particular axiomatization of propositional calculus. This should be linked to the subsequences of theorems and antitheorems. - _Jonathan Vos Post_, Dec 19 2004 [This comment is referring to A100200 and A101248. - _N. J. A. Sloane_, May 19 2020]
%C A101273 Comment from _Charles R Greathouse IV_, May 17 2020: (Start)
%C A101273 Each positive integer represents a string of one or more symbols, as described above. Some represent well-formed formulas. Of those, some are theorems (A101273) while others are antitheorems (A100200) with the remaining wffs in A101248. The first few theorems are
%C A101273 171, A -> A
%C A101273 181, A <-> A
%C A101273 272, B -> B
%C A101273 282, B <-> B
%C A101273 1531, A XOR ~A,
%C A101273 with 1 = A, 7 = ->, etc. (End)
%C A101273 In short: any well-formed formula (wff) can be mapped to an integer. The sequence lists those integers that correspond to wff's that are theorems. - _N. J. A. Sloane_, May 19 2020
%D A101273 M. Davis, Computability and Unsolvability. New York: Dover 1982.
%D A101273 D. R. Hofstadter, Goedel, Escher, Bach: An Eternal Golden Braid. New York: Vintage Books, p. 18, 1989.
%D A101273 S. C. Kleene, Mathematical Logic. New York: Dover, 2002.
%H A101273 Charles R Greathouse IV, <a href="/A101273/b101273.txt">Table of n, a(n) for n=1..10000</a>
%H A101273 Eric Weisstein et al., <a href="https://mathworld.wolfram.com/GoedelNumber.html">Gödel Number</a>.
%F A101273 It appears that the n-th term is very roughly n^c, for some c>1.
%e A101273 Example: 17162 is the theorem A->AvB.
%Y A101273 See A100200 and A101248 for further information.
%K A101273 nonn,base
%O A101273 1,1
%A A101273 Richard C. Schroeppel, Dec 19 2004
%E A101273 Corrected and edited by _Charles R Greathouse IV_, Oct 06 2009