[FOM] decidability of intuitionistic propositional logic

Alasdair Urquhart urquhart at cs.toronto.edu
Wed Dec 1 09:42:18 EST 2004

On Tuesday 30 November 2004 09:06, Neil Tennant wrote:
> Question for fom-ers:
> Who was the first person to state and/or prove that theoremhood in
> intuitionistic propositional logic is decidable?

Gerhard Gentzen, I believe.  In his famous paper of 1935, he states
and proves this result based on his sequent calculus for LJ.  It is on
pp. 103-105 of the Collected Papers edited by Szabo.

More information about the FOM mailing list