Investigations into the Predicate Calculus
Oiva Ketonen (1913-2000) był najbliższym uczniem twórcy nowoczesnej teorii dowodu Gerharda Gentzena. Ich spotkanie miało miejsce w latach 1938-39 w Getyndze, przy czym Ketonen miał nadzieję na otrzymanie odpowiedniego tematu rozprawy doktorskiej, a Gentzen zamiast tego był głęboko pogrążony w próbach udowodnienia spójności analizy.
Praca doktorska Ketonena z 1944 roku, jego jedyna praca w dziedzinie logiki, wprowadziła to, co dziś nazywa się rachunkiem następników G3. Jest to jego najbardziej znane odkrycie - rachunek sekwencyjny dla klasycznej logiki zdań, którego wszystkie reguły logiczne są odwracalne. Niewielu czytało jego pracę, której wyniki zostały udostępnione w długiej recenzji Paula Bernaysa.
Rachunek Ketonena jest podstawą metody tableau Everta Betha i rachunku sekwencyjnego we wpływowej książce Stephena Kleene'a {it Introduction to Metamathematics}. Drugim rezultatem było zaostrzenie twierdzenia o środkowej sekwencji, dzięki któremu można zminimalizować liczbę wnioskowań kwantyfikatorowych ze zmiennymi własnymi.
Wynikało z tego istnienie najsłabszej możliwej sekwencji środkowej, w tym sensie, że jeśli jakakolwiek sekwencja środkowa jest pochodna, to najsłabsza również. Przekształcając to w twierdzenie przeciwne, Ketonen znalazł czysto syntaktyczną metodę dowodzenia niedowartościowania, którą zastosował do geometrii płaszczyzny afinicznej.
Jego rezultat, w nowoczesnym ujęciu, był pozytywnym rozwiązaniem problemu słowa dla uniwersalnego fragmentu geometrii afinicznej płaszczyzny, z syntaktycznym dowodem niedowartościowania postulatu równoległego z reszty aksjomatów afinicznych jako następstwem.