[FOM] decidability of intuitionistic propositional logic

[Arnon Avron]

> 
> Question for fom-ers:
> 
> Who was the first person to state and/or prove that theoremhood in
> intuitionistic propositional logic is decidable?

If my memory is not betraying me, it was Gentzen in his "Investigations
into Logical Deduction", where the sequential calculi for classical
and intuitionistic logics were first introduced and the cut-elimination
theorems for them proved.

Arnon Avron