[FOM] decidability of intuitionistic propositional logic

[A.P. Hazen]

Neil Tennant asks:
	Who was the first person to state and/or prove that theoremhood
	in intuitionistic propositional logic is decidable?
Church (in the text associated with footnote 212 in the book which 
doesn't have to be named because we all know it) says that 
decidability was proven by Gentzen and "again" by Wajsberg.
     The footnote refers us to Gentzen's  1934 "Untersuchungen" (Eng. 
tr. in volumes  I and II of "American Philosophical Quarterly," which 
I don't think has ever published anything else as good since!).  No 
reference for Wajsberg there, but the preceding footnote refers to a 
1938 paper.
    (Neil knows the "Untersuchungen" by heart, but in case anyone here 
doesn't: one of the corollaries Gentzen draws from the Hauptsatz in 
the last part of the paper is that if a propositional formula is 
intuitionistically provable AT ALL, it has a proof of  complexity 
limited by a bound that can be calculated from the length of the 
formula.  I'd guess that this is a fairly early example of this now 
familiar sort of argument in settling decidability questions, but 
don't claim to really know the history....)
---
Allen Hazen
Philosophy Department
University of Melbourne