[FOM] decidability of intuitionistic propositional logic
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