login
The OEIS Foundation is supported by donations from users of the OEIS and by a grant from the Simons Foundation.

 

Logo


Hints
(Greetings from The On-Line Encyclopedia of Integer Sequences!)
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 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)

AIn 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

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 n-th 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,changed

AUTHOR

Richard C. Schroeppel, Dec 19 2004

EXTENSIONS

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

STATUS

approved

Lookup | Welcome | Wiki | Register | Music | Plot 2 | Demos | Index | Browse | More | WebCam
Contribute new seq. or comment | Format | Style Sheet | Transforms | Superseeker | Recent
The OEIS Community | Maintained by The OEIS Foundation Inc.

License Agreements, Terms of Use, Privacy Policy. .

Last modified May 24 19:14 EDT 2020. Contains 334580 sequences. (Running on oeis4.)