[FOM] decidability of intuitionistic propositional logic
a.hazen at philosophy.unimelb.edu.au
Wed Dec 1 00:19:17 EST 2004
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
(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....)
University of Melbourne
More information about the FOM