The Development of Intuitionistic Logic

Mark van Atten (2008). The Development of Intuitionistic Logic. Stanford Encyclopedia of Philosophy.

This article gives an excellent account of the development of intuitionistic logic, from its roots in Brouwer's theological metaphysics, through to its formal presentation by Heyting in 1956. The account is strong on the tensions between the subjectivist motif and the urge to formalise. Via Richard Zach.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Highly recommended

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

Intuitionistic logic

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?

Intuitionistic model theory

The model theory of intuitionistic logic gives a notion of refutation models for non-theorems of intuitionistic logic, such as EFQ.

Kripke's model theory for (propositional) intuitionistic logic came out of his model theory for modal logic, together with his observation that intuitionistic logic can be embedded in S4 through a very simple embedding. Wikipedia has all the details.

This kind of model theoretic demonstration is vulnerable to the kind of intuitionist criticism seen in section 4.5.2 of van Atten's article, namely that the explanation is not made in terms that go with the grain of intuitionistic semantics. Lipton and O'Donnell's impressive Some Intuitions Behind Realizability Semantics for Constructive Logic (.ps) attempts to deal with this criticism using a variant kind of model theory, Lauchli semantics.

Decimal Goedelization of Heyting's 11 axioms

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
==============

use postfix

I don't know what this is about (so my apologies if this doesn't make sense or is irrelevant) but I guess using postfix notation would give nicer results, making it easier to list provable theorems. You won't need parenthesis, so 9 and 0 can be used for variables as well, and the numbers are a lot shorter. (You could use the following encoding for variables: 1,2,9,10,20,90,100,200,900 etc, because now variables can appear next to each other.)

11417
1242147
92491472177
91792721747
21727
27217147
21617
1262167
9216792791747
217137
13231721747

Nicely done, Sjoerd Visscher: postfix notation for Decimal Goede

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.

Schroeppel's conjecture, Jonathan Swift, Fritz Zwicky, Wolfram

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.