  The axioms that Ketonen considers are  those of projective and affine geometry, the former taken from  Skolem's 1920 paper discussed in the first section above. Ketonen  wanted to formulate Skolem's formal rules of proof within sequent  calculus. However, Ketonen's work was mostly known only through its  review by Bernays and only the logical part on sequent calculus was  explained in detail there.