%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
%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.
%A Richard C. Schroeppel, Dec 19 2004
%E Corrected and edited by _Charles R Greathouse IV_, Oct 06 2009