|
%I #6 Sep 21 2017 09:03:22
%S 1791410,91420792410,91720799141109241100,991720492711007917,2791720,
%T 91491720072,1791620,91620792610,99171104927110079916207110,31791720,
%U 99172049173200731
%N Decimal Goedelization of Heyting's 11 axioms for intuitionistic propositional logic.
%C 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 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 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 axiom 1: A->(A^A).
%e axiom 2: (A^B)->(B^A).
%e axiom 3: (A->B)->(((A^C)->(B^C)).
%e axiom 4: ((A->B)^(B->C))->(A->C).
%e axiom 5: B->(A->B).
%e axiom 6: (A^(A->B))->B.
%e axiom 7: A->(AvB).
%e axiom 8: (AvB)->(BvA).
%e axiom 9: ((A->C)^(B->C))->((AvB)->C).
%e axiom 10: -A->(A->B).
%e axiom 11: ((A->B)^(A->-B))->-A.
%Y Cf. A101273, A100200, A101248, A101273.
%K easy,fini,full,nonn,base
%O 1,1
%A _Jonathan Vos Post_, Jul 18 2008
| 