Investigations into the Predicate Calculus
Oiva Ketonen (1913--2000) bol najbližším žiakom tvorcu modernej teórie dôkazov Gerharda Gentzena. Ich stretnutie sa uskutočnilo v rokoch 1938--39 v Göttingene, pričom Ketonen dúfal, že získa vhodnú tému na doktorskú dizertačnú prácu, a Gentzen bol namiesto toho hlboko ponorený do pokusov o dôkaz konzistencie analýzy.
Ketonenova dizertačná práca z roku 1944, jeho jediná práca v oblasti logiky, predstavila to, čo sa dnes nazýva G3-sekvenčný kalkul. Je to jeho najznámejší objav, sekvenčný kalkul pre klasickú výrokovú logiku, ktorého logické pravidlá sú všetky inverzné. Málokto čítal jeho prácu, ktorej výsledky boli namiesto toho sprístupnené prostredníctvom dlhej recenzie Paula Bernaysa.
Ketonenov kalkul je základom tabuľkovej metódy Everta Betha a sekvenčných kalkulov vo vplyvnej knihe {it Introduction to Metamathematics} Stephena Kleena. Druhým výsledkom bolo spresnenie strednej sekvenčnej vety, pomocou ktorej sa dal minimalizovať počet kvantifikačných inferencií s vlastnými premennými.
Nasledovala existencia najslabšieho možného midsekventu v tom zmysle, že ak je akýkoľvek midsekvent odvoditeľný, je odvoditeľný aj najslabší. Ak to Ketonen obrátil na protiklad, našiel čisto syntaktickú metódu na dôkazy nedovysloviteľnosti, ktorú aplikoval na afinnú rovinnú geometriu.
Jeho výsledkom, povedané moderným jazykom, bolo pozitívne riešenie slovného problému pre univerzálny fragment rovinnej afinnej geometrie so syntaktickým dôkazom nedostatočnej odvoditeľnosti paralelného postulátu od ostatných afinných axióm ako dôsledok.