

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 [This comment is referring to A100200 and A101248.  N. J. A. Sloane, May 19 2020]
Comment from Charles R Greathouse IV, May 17 2020: (Start)
Each positive integer represents a string of one or more symbols, as described above. Some represent wellformed formulas. Of those, some are theorems (A101273) while others are antitheorems (A100200) with the remaining wffs in A101248. The first few theorems are
171, A > A
181, A <> A
272, B > B
282, B <> B
1531, A XOR ~A,
with 1 = A, 7 = >, etc. (End)
In short: any wellformed 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


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

See A100200 and A101248 for further information.
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



