The formulation of the intuitionistic sequent calculus is due to Gentzen but is it also Gentzen who was responsible for coining the term 'intuitionistic'? What was the motivation for the choice of term? --- that intuitionistic sequents are more "intuitive" than classical ones? To my mind, it is the other way around... Was there some other precedent that motivated the adoption of "intuitionistic"? --FC