%I
%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 nonassociative "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 nth term is very roughly n^c, for some c>1.
%e Example: 17162 is the theorem A>AvB.
%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
