Lambda the Ultimate

I was just going to post this link. It is indeed excellent and highly significant to several topics often discussed on LtU (Curry-Howard being the most obvious).

Interesting, I was not aware of all this (I remember vaguely a mention of "three-valued logic" which was not one in my CS studies).

Anyway, is there a definitive demonstration of Ex Falso or is Kolmogorov's the best we have?

This is in pre-formatted hard-to-read ascii, as submitted to the Online Encyclopedia of Integer Sequences.

==============
"... an incorrect theory, even if it cannot be inhibited by any
contradiction that would refute it, is none the less incorrect, just
as a criminal policy is none the less criminal even if it cannot be
inhibited by any court that would curb it."
==============
The following is a copy of the email message that was sent to njas
containing the sequence you submitted.

All greater than and less than signs have been replaced by their html
equivalents. They will be changed back when the message is processed.
{JVP I've turned back "->" to "->" to show "implies"}

This copy is just for your records. No reply is expected.
Subject: NEW SEQUENCE FROM Jonathan Vos Post

%I A000001
%S A000001 1791410, 91420792410, 91720799141109241100,
991720492711007917, 2791720, 91491720072, 1791620, 91620792610,
99171104927110079916207110, 31791720, 99172049173200731
%N A000001 Decimal Goedelization of Heyting's 11 axioms for
intuitionistic propositional logic.
%C A000001 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.
%D A000001 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 A000001 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 A000001 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.
%Y A000001 Cf. A101273, A100200, A101248, A101273.
%O A000001 1,1
%K A000001 ,easy,fini,full,nonn,
%A A000001 Jonathan Vos Post (jvospost3@gmail.com), Jul 18 2008
RH
RA 192.20.225.32
RU
RI
==============

Nicely done, Sjoerd Visscher. I should like to cite your re4sults in the paper that I expect to present on this at the 2009 Internatioanl Conference on Complex System. I have been unable to contact Richard Schroeppel to discuss this. He has dealt with redundant or un-needed parentheses thus:

The non-associative "Implies" is evaluated from Left to Right; A->B->C = is interpreted (A->B)->C. Redundant parentheses are permitted.

http://www.research.att.com/~njas/sequences/A140861

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,1

COMMENT
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
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.

KEYWORD
easy,fini,full,nonn,new

AUTHOR
Jonathan Vos Post (jvospost3(AT)gmail.com), Jul 18 2008

Richard Schroeppel also makes the interesting conjecture: "It appears that the n-th term is very roughly n^c, for some c>1." He cites:

Davis, M., Computability and Unsolvability. New York: Dover 1982.

Hofstadter, D. R., Goedel, Escher, Bach: An Eternal Golden Braid. New York: Vintage Books, p. 18, 1989.

Kleene S. C., Mathematical Logic. New York: Dover, 2002.

And, by the way, harkening back to the prime decomposition style of Goedel himself, among your numbers:

91792721747 is prime, 21727 is prime, 27217147 is prime, and 21617 is prime.

Your numbers are more dense with primes, being shorter, given the
1/ln n asymptotics of primes.

Richard Schroeppel's conjecture: "It appears that the n-th term is very roughly n^c, for some c>1" would still apply to your postfix approach, albeit with a different value of c than mine. I wonder if someone with supercomputer access has taken this much further, has a good estimate of c, and is doing somethinbg interesting with this that they don't want to place in open literature?

In any case, it is relevant to Jonathan Swift's deadly-accurate satire of academe in TRAVELS, PART III: A VOYAGE TO LAPUTA, BALNIBARBI, LUGGNAGG, GLUBBDUBDRIB AND JAPAN, Chapter V.

The Author permitted to see the grand Academy of Lagado. The
Academy largely described. The Arts wherein the Professors employ
themselves.

There was a most ingenious Architect who had contrived a new Method
for building Houses, by beginning at the Roof, and working downwards
to the Foundation; which he justified to me by the like Practice of
those two prudent Insects, the Bee and the Spider.

There was a Man born blind, who had several Apprentices in his own
Condition: Their Employment was to mix Colours for Painters, which
their Master taught them to distinguish by feeling and smelling. It
was indeed my Misfortune to find them at that Time not very perfect in their Lessons; and the Professor himself happened to be generally
mistaken: This Artist is much encouraged and esteemed by the whole
Fraternity....

There was an Astronomer who had undertaken to place a Sun-Dial upon
the great Weather-Cock on the Town-House, by adjusting the annual and
diurnal Motions of the Earth and Sun, so as to answer and coincide
with all accidental Turnings of the Wind....

Project for improving speculative Knowledge by practical and
mechanical Operations. But the World would soon be sensible of its
Usefulness, and he flattered himself that a more noble exalted Thought never sprung in any other Man's Head. Every one knew how laborious the usual Method is of attaining to Arts and Sciences; whereas by his Contrivance, the most ignorant Person at a reasonable Charge, and with a little bodily Labour, may write Books in Philosophy, Poetry, Politicks, Law, Mathematicks and Theology, without the least Assistance from Genius or Study. He then led me to the Frame, about the Sides whereof all his Pupils stood in Ranks. It was twenty Foot Square, placed in the middle of the Room. The Superficies was composed of several bits of Wood, about the bigness of a Dye, but some larger than others. They were all linked together by slender Wires. These bits of Wood were covered on every Square with Paper pasted on them, and on these Papers were written all the Words of their Language, in their several Moods, Tenses, and Declensions, but without any Order. The Professor then desired me to observe, for he was going to set his Engine at Work.

I have commented in another thread about the Combinatorics satirized
by Swift, in the last paragraph above, on filtering meaning from
randomly generated strings of words, as it relates to Lull and later
to Babbage and then "The Library of Babel" by Borges and the mining of ideocosm (to use Zwicky's fine term) by Wolfram et al.