The OEIS Foundation is supported by donations from users of the OEIS and by a grant from the Simons Foundation. 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 Cf. A101273, A100200, A101248, A101273. Sequence in context: A234671 A043650 A234082 * A234866 A249196 A137819 Adjacent sequences:  A140858 A140859 A140860 * A140862 A140863 A140864 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 | Recent
The OEIS Community | Maintained by The OEIS Foundation Inc.

Last modified April 1 07:29 EDT 2020. Contains 333155 sequences. (Running on oeis4.)