A101273 Theorems from propositional calculus, translated into decimal digits.

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

Offset: 1

Author

Richard C. Schroeppel, Dec 19 2004

Keywords

• nonn
• base

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 non-associative "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 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

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 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

Examples

			Example: 17162 is the theorem A->AvB.
		

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.

Crossrefs

See A100200 and A101248 for further information.

Formula

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

Extensions

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