[FOM] decid'ity of int pro logic & Jaskowski

[A.P. Hazen]

  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