Titre original :
Investigations into the Predicate Calculus
Contenu du livre :
Oiva Ketonen (1913--2000) est l'étudiant le plus proche du créateur de la théorie moderne de la preuve, Gerhard Gentzen. Leur rencontre a eu lieu en 1938-1939 à Göttingen, Ketonen espérant recevoir un sujet approprié pour une thèse de doctorat et Gentzen étant au contraire profondément plongé dans des tentatives pour prouver la cohérence de l'analyse.
La thèse de Ketonen de 1944, son seul travail en logique, introduit ce que l'on appelle aujourd'hui le calcul des séquences G3. Il s'agit de sa découverte la plus connue, un calcul séquentiel pour la logique propositionnelle classique dont les règles logiques sont toutes inversibles. Peu de gens ont lu sa thèse, dont les résultats ont été rendus accessibles par un long compte rendu de Paul Bernays.
Le calcul de Ketonen est à la base de la méthode des tableaux d'Evert Beth et des calculs séquentiels de l'influent ouvrage de Stephen Kleene intitulé « Introduction aux métamathématiques ». Un deuxième résultat a été l'affinement du théorème du séquent moyen, qui permet de minimiser le nombre d'inférences de quantificateurs avec des variables propres.
L'existence d'un médio-séquent le plus faible possible a suivi, dans le sens où si un médio-séquent quelconque est dérivable, un médio-séquent le plus faible l'est aussi. En transformant cela en contrapositive, Ketonen a trouvé une méthode purement syntaxique pour les preuves de sous-divisibilité qu'il a appliquée à la géométrie plane affine.
Son résultat, en termes modernes, était une solution positive au problème des mots pour le fragment universel de la géométrie affine plane, avec comme corollaire une preuve syntaxique de la sous-divisibilité du postulat parallèle à partir du reste des axiomes affines.
Autres informations sur le livre :
| ISBN : | 9781848904071 |
| Auteur : | |
| Éditeur : | |
| Langue : | anglais |
| Reliure : | Broché |
Achat:
Actuellement disponible, en stock.
