[FOM] decidability of intuitionistic propositional logic

Arnon Avron aa at tau.ac.il
Wed Dec 1 01:23:21 EST 2004

> 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  

More information about the FOM mailing list