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

1791410, 91420792410, 91720799141109241100, 991720492711007917, 2791720, 91491720072, 1791620, 91620792610, 99171104927110079916207110, 31791720, 99172049173200731

Offset: 1

Author

Jonathan Vos Post, Jul 18 2008

Keywords

• easy
• fini
• full
• nonn
• base

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.

Examples

			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.
		

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.

Crossrefs

Cf. A101273, A100200, A101248, A101273.