

A101273


Theorems from propositional calculus, translated into decimal digits.


5



171, 181, 272, 282, 1531, 1631, 2532, 2632, 3151, 3161, 3252, 3262, 11711, 11811, 12712, 12812, 14171, 14181, 14271, 14272, 15171, 15172, 16171, 16181, 17141, 17161, 17162, 17261, 17331, 17910, 18141, 18161, 18331, 18910, 21721, 21821, 22722, 22822, 24171
(list;
graph;
refs;
listen;
history;
text;
internal format)



OFFSET

1,1


COMMENTS

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.
Operator binding strength is in numerical order, Not > And > ... > Equiv.
The nonassociative "Implies" is evaluated from Left to Right; A>B>C = is interpreted (A>B)>C. Redundant parentheses are permitted.
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


REFERENCES

M. Davis, Computability and Unsolvability. New York: Dover 1982.
D. R. Hofstadter, Goedel, Escher, Bach: An Eternal Golden Braid. New York: Vintage Books, p. 18, 1989.
S. C. Kleene, Mathematical Logic. New York: Dover, 2002.


LINKS

Charles R Greathouse IV, Table of n, a(n) for n=1..10000
Eric Weisstein et al., GĂ¶del Number.


FORMULA

It appears that the nth term is very roughly n^c, for some c>1.


EXAMPLE

Example: 17162 is the theorem A>AvB.


CROSSREFS

Sequence in context: A185845 A045149 A031511 * A136365 A031900 A120819
Adjacent sequences: A101270 A101271 A101272 * A101274 A101275 A101276


KEYWORD

nonn,base


AUTHOR

Richard C. Schroeppel, Dec 19 2004


EXTENSIONS

Corrected and edited by Charles R Greathouse IV, Oct 06 2009


STATUS

approved



