[FOM] decid'ity of int pro logic & Jaskowski
A.P. Hazen
a.hazen at philosophy.unimelb.edu.au
Fri Dec 3 22:34:11 EST 2004
Neil Tennant (thanking D. Scott for reminding him) mentions another
early proof of the decidability of intuitionistic propositional logic:
>the Jaskowski matrices. Any non-theorem of intuitionistic
>propositional logic can be counterexemplified in one of these finite
>matrices. So they afford an
>effective enumeration of the non-theorems, thereby rendering theoremhood
>decidable. Jaskowski's paper, however, was published in 1936 (according to
>the bibliography in Kleene's Introduction to Metamathematics); whereas
>Gentzen's Untersuchungen were published in 1934-5. So Gentzen gets
>priority by a year
Reference: An English translation of Jaskowski's paper is in Storrs
McCall, ed., "Polish Logic 1920-1939" (Oxford University Press 1967).
The timelag is very short indeed, since J's 1936 publication was
actually in the proceedings of a 1935 conference ("Actes du Congrès
Internationale de Philosophie Scientifique 6" pp. 58-61) and G's
discussion of decidability of Heyting's propositional logic, coming
at the end of the "Untersuchungen," was in the part that didn't get
into print until 1935.
Comment: Church's failure to mention J in connection with the
decidability result (given that he does mention Wajsberg's later
contribution) is a rare oversight. He was (of course!) familiar with
J's paper, citing it in footnote 217, but mentions it only in
connection with J's having provided a denumerable characteristic
matrix for Int. Prop. Logic. J's discussion is compressed, and he
does not explicitly mention decidability, but he does state that
every non-theorem of Heyting's prop. logic is refuted in some one of
an (effectively generated) sequence of finite matrices, from which a
decision algorithm can be extracted.
Further comment: Gentzen's decision procedure has an obvious estimate
of how long it will take (the obvious bound is what? doubly
exponential? in the length of the formula to be decided).
Jaskowski's, as so far described, comes with no bound at all: it's
the idiot algorithm of grinding out proofs and matrices side by side
until the formula you're interested in shows up. In fact there's
more in his paper: the size of the falsifying matrix for a
non-theorem can be calculated from the length of a normal-form
formula equivalent to it. He states the existence of these normal
equivalents without proof, but I suspect the process of finding them
is well-behaved enough to give some estimate of the complexity of the
decision procedure.
--
Allen Hazen
Philosophy Department
University of Melbourne
More information about the FOM
mailing list