cp's OEIS Frontend

A140861 Decimal Goedelization of Heyting's 11 axioms for intuitionistic propositional logic.

%I A140861 #10 Sep 30 2024 09:16:27
%S A140861 1791410,91420792410,91720799141109241100,991720492711007917,2791720,
%T A140861 91491720072,1791620,91620792610,99171104927110079916207110,31791720,
%U A140861 99172049173200731
%N A140861 Decimal Goedelization of Heyting's 11 axioms for intuitionistic propositional logic.
%C A140861 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.
%D A140861 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.
%H A140861 Mark van Atten, <a href="http://plato.stanford.edu/entries/intuitionistic-logic-development/">The Development of Intuitionistic Logic</a>, Stanford Encyclopedia of Philosophy, July 10, 2008.
%e A140861 axiom 1: A->(A^A).
%e A140861 axiom 2: (A^B)->(B^A).
%e A140861 axiom 3: (A->B)->((A^C)->(B^C)).
%e A140861 axiom 4: ((A->B)^(B->C))->(A->C).
%e A140861 axiom 5: B->(A->B).
%e A140861 axiom 6: (A^(A->B))->B.
%e A140861 axiom 7: A->(AvB).
%e A140861 axiom 8: (AvB)->(BvA).
%e A140861 axiom 9: ((A->C)^(B->C))->((AvB)->C).
%e A140861 axiom 10: -A->(A->B).
%e A140861 axiom 11: ((A->B)^(A->-B))->-A.
%Y A140861 Cf. A101273, A100200, A101248, A101273.
%K A140861 easy,fini,full,nonn,base
%O A140861 1,1
%A A140861 _Jonathan Vos Post_, Jul 18 2008