login
This site is supported by donations 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 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

Table of n, a(n) for n=1..11.

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 | More pages
The OEIS Community | Maintained by The OEIS Foundation Inc.

License Agreements, Terms of Use, Privacy Policy .

Last modified March 28 02:40 EDT 2017. Contains 284182 sequences.