[FOM] decidability of intuitionistic propositional logic

Neil Tennant neilt at mercutio.cohums.ohio-state.edu
Thu Dec 2 13:19:06 EST 2004

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


Please send snail mail to:

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

Work telephone 	(614)292-1591 

More information about the FOM mailing list