The OEIS is supported by the many generous donors to the OEIS Foundation.
%I #40 Oct 21 2020 03:45:23
%S 171,181,272,282,1531,1631,2532,2632,3151,3161,3252,3262,11711,11811,
%T 12712,12812,14171,14181,14271,14272,15171,15172,16171,16181,17141,
%U 17161,17162,17261,17331,17910,18141,18161,18331,18910,21721,21821,22722,22822,24171
%N Theorems from propositional calculus, translated into decimal digits.
%C 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 Operator binding strength is in numerical order, Not > And > ... > Equiv.
%C The non-associative "Implies" is evaluated from Left to Right; A->B->C = is interpreted (A->B)->C. Redundant parentheses are permitted.
%C 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 Comment from _Charles R Greathouse IV_, May 17 2020: (Start)
%C 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 171, A -> A
%C 181, A <-> A
%C 272, B -> B
%C 282, B <-> B
%C 1531, A XOR ~A,
%C with 1 = A, 7 = ->, etc. (End)
%C 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 M. Davis, Computability and Unsolvability. New York: Dover 1982.
%D D. R. Hofstadter, Goedel, Escher, Bach: An Eternal Golden Braid. New York: Vintage Books, p. 18, 1989.
%D S. C. Kleene, Mathematical Logic. New York: Dover, 2002.
%H Charles R Greathouse IV, <a href="/A101273/b101273.txt">Table of n, a(n) for n=1..10000</a>
%H Eric Weisstein et al., <a href="http://mathworld.wolfram.com/GoedelNumber.html">Gödel Number</a>.
%F It appears that the n-th term is very roughly n^c, for some c>1.
%e Example: 17162 is the theorem A->AvB.
%Y See A100200 and A101248 for further information.
%K nonn,base
%O 1,1
%A Richard C. Schroeppel, Dec 19 2004
%E Corrected and edited by _Charles R Greathouse IV_, Oct 06 2009