Vizsgálatok a predikátumszámításról

Eredeti címe:

Investigations into the Predicate Calculus

Könyv tartalma:

Oiva Ketonen (1913--2000) volt a modern bizonyításelmélet megalkotójának, Gerhard Gentzennek a legközelebbi tanítványa. Találkozásukra 1938--39-ben került sor Göttingenben, Ketonen abban reménykedett, hogy megfelelő témát kap doktori disszertációjához, Gentzen ehelyett mélyen elmerült az analízis konzisztenciájának bizonyítási kísérleteiben.

Ketonen 1944-es disszertációja, egyetlen logikai munkája, bevezette azt, amit ma G3-szekvencia-kalkulusnak nevezünk. Ez a legismertebb felfedezése, egy szekvencia-kalkulus a klasszikus mondattani logikához, amelynek logikai szabályai mind invertálhatók. Dolgozatát kevesen olvasták, az eredményeket inkább Paul Bernays hosszú recenziója tette hozzáférhetővé.

Ketonen kalkulusa az alapja Evert Beth táblakép-módszerének és Stephen Kleene befolyásos {Egy bevezetés a metamatematikába} című művében szereplő szekvencia-kalkulusoknak. Egy másik eredménye a középszekvencia-tétel élesítése volt, amellyel minimalizálható a sajátváltozós kvantifikációs következtetések száma.

Ezt követte a lehető leggyengébb középszekvencia létezése, abban az értelemben, hogy ha bármelyik középszekvencia levezethető, akkor a leggyengébb is az. Ezt kontrapozitívvá alakítva Ketonen talált egy tisztán szintaktikai módszert az alulkövethetőség bizonyítására, amelyet az affin síkgeometriára alkalmazott.

Eredménye, modern kifejezéssel élve, a síkbeli affin geometria univerzális töredékére vonatkozó szóprobléma pozitív megoldása volt, és ennek folyományaként a párhuzamos posztulátumnak a többi affin axiómából való alulbocsáthatóságának szintaktikai bizonyítása.