[FOM] decidability of intuitionistic propositional logic

[Alasdair Urquhart]

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.