[FOM] decidability of intuitionistic propositional logic

[Neil Tennant]

Thanks to all the fom-ers who wrote, either to the list or to me
privately, with the answer to my question. This note is just to mention to
the list a contribution of which Dana Scott has reminded me: 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.

___________________________________________________________________
Neil W. Tennant
Humanities Distinguished Professor of Philosophy
Adjunct Professor of Cognitive Science

http://people.cohums.ohio-state.edu/tennant9/

Please send snail mail to:

		Department of Philosophy
		230 North Oval
		The Ohio State University
		Columbus, OH 43210

Work telephone 	(614)292-1591