Investigații în calculul predicatelor

Titlul original:

Investigations into the Predicate Calculus

Conținutul cărții:

Oiva Ketonen (1913--2000) a fost cel mai apropiat student pe care l-a avut vreodată creatorul teoriei moderne a probelor, Gerhard Gentzen. Întâlnirea lor a avut loc în 1938--39 la Göttingen, Ketonen sperând să primească un subiect potrivit pentru o teză de doctorat, iar Gentzen, în schimb, era profund absorbit de încercările de a demonstra coerența analizei.

Teza lui Ketonen din 1944, singura sa lucrare în logică, a introdus ceea ce astăzi se numește calculul secvențial G3. Este cea mai cunoscută descoperire a sa, un calcul al secvențelor pentru logica propozițională clasică, ale cărui reguli logice sunt toate inversabile. Puțini i-au citit teza, ale cărei rezultate au fost în schimb puse la dispoziție printr-o lungă recenzie a lui Paul Bernays.

Calculul lui Ketonen este baza metodei tablourilor a lui Evert Beth și a calculelor secvențiale din influenta {it Introduction to Metamathematics} a lui Stephen Kleene. Un al doilea rezultat a fost o ascuțire a teoremei midsequent, prin care numărul de inferențe ale cuantificatorilor cu variabile proprii ar putea fi minimizat.

A urmat existența celei mai slabe jumătăți de secvență posibile, în sensul că, dacă orice jumătate de secvență este derivabilă, atunci și cea mai slabă este. Transformând acest lucru într-o contrapozitivă, Ketonen a găsit o metodă pur sintactică pentru demonstrarea subivabilității, pe care a aplicat-o geometriei plane afine.

Rezultatul său, în termeni moderni, a fost o soluție pozitivă la problema cuvântului pentru fragmentul universal al geometriei afine plane, cu o dovadă sintactică a subivabilității postulatului paralel din restul axiomelor afine ca un corolar.