Indagini sul calcolo dei predicati

Titolo originale:

Investigations into the Predicate Calculus

Contenuto del libro:

Oiva Ketonen (1913-2000) è stato l'allievo più vicino al creatore della moderna teoria delle prove Gerhard Gentzen. Il loro incontro avvenne nel 1938-39 a Gottinga, con Ketonen che sperava di ricevere un argomento adatto per una tesi di dottorato e Gentzen invece profondamente immerso nei tentativi di dimostrare la coerenza dell'analisi.

La tesi di Ketonen del 1944, il suo unico lavoro di logica, introdusse quello che oggi viene chiamato il calcolo sequenziale G3. È la sua scoperta più nota, un calcolo sequenziale per la logica proposizionale classica le cui regole logiche sono tutte invertibili. Pochi hanno letto la sua tesi, i cui risultati sono stati invece resi disponibili attraverso una lunga recensione di Paul Bernays.

Il calcolo di Ketonen è alla base del metodo dei tableau di Evert Beth e dei calcoli sequenziali dell'influente {Istruzione alla metamatematica} di Stephen Kleene. Un secondo risultato è stato l'affinamento del teorema del midsequent, grazie al quale è stato possibile minimizzare il numero di inferenze di quantificatori con autovettori.

Ne è seguita l'esistenza di un seguito intermedio più debole possibile, nel senso che se qualsiasi seguito intermedio è derivabile, lo è anche il più debole. Trasformando questo principio in un contropositivo, Ketonen trovò un metodo puramente sintattico per la dimostrazione dell'inderogabilità, che applicò alla geometria del piano affine.

Il suo risultato, in termini moderni, era una soluzione positiva al problema delle parole per il frammento universale della geometria affine piana, con una prova sintattica dell'inderivabilità del postulato parallelo dal resto degli assiomi affini come corollario.