login
The OEIS is supported by the many generous donors to the OEIS Foundation.

 

Logo
Hints
(Greetings from The On-Line Encyclopedia of Integer Sequences!)
A140861 Decimal Goedelization of Heyting's 11 axioms for intuitionistic propositional logic. 0
1791410, 91420792410, 91720799141109241100, 991720492711007917, 2791720, 91491720072, 1791620, 91620792610, 99171104927110079916207110, 31791720, 99172049173200731 (list; graph; refs; listen; history; text; internal format)
OFFSET
1,1
COMMENTS
Axioms of Heyting (1930) as explained in Mark van Atten (2008). The same notation as in A101273, including: Blocks of 1's and 2s are variables: A = 1, B = 2, C = 11, D = 12, E = 21, ... Not (also written -) = 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 hard thing, given errors in my related earlier submissions within Richard C. Schroeppel's metatheory, is to list in numerical order the theorems that can be proved from these 11 axioms.
REFERENCES
Heyting, A., 1930, Die formalen Regeln der intuitionistischen Logik I, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 42-56. English translation in Mancosu, 1998, pp.311-327.
LINKS
Mark van Atten, The Development of Intuitionistic Logic, Stanford Encyclopedia of Philosophy, July 10, 2008.
EXAMPLE
axiom 1: A->(A^A).
axiom 2: (A^B)->(B^A).
axiom 3: (A->B)->(((A^C)->(B^C)).
axiom 4: ((A->B)^(B->C))->(A->C).
axiom 5: B->(A->B).
axiom 6: (A^(A->B))->B.
axiom 7: A->(AvB).
axiom 8: (AvB)->(BvA).
axiom 9: ((A->C)^(B->C))->((AvB)->C).
axiom 10: -A->(A->B).
axiom 11: ((A->B)^(A->-B))->-A.
CROSSREFS
Sequence in context: A234671 A043650 A234082 * A234866 A249196 A137819
KEYWORD
easy,fini,full,nonn,base
AUTHOR
Jonathan Vos Post, Jul 18 2008
STATUS
approved

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

License Agreements, Terms of Use, Privacy Policy. .

Last modified March 29 06:57 EDT 2024. Contains 371265 sequences. (Running on oeis4.)