Essai sur la genèse de la méthode des tableaux de Beth

Nous relatons comment, entre 1951 et 1955, et sans savoir, avant la fin 1954, où il va aboutir, Beth élabore la méthode des tableaux sémantiques classiques. Nos conclusions sont étayées par des correspondances et des ébauches de travaux, retrouvées dans les papiers de Beth. Nous appuyant sur des documents de même nature, nous étudions ensuite l’élaboration, consciente de sa fin cette fois, et surtout technique, des tableaux sémantiques intuitionnistes, achevée dès 1956, mais qui suscite des objections. Nous notons, au passage, que dès la fin 1955, Beth écrit qu’une formule niée est valide dans un arbre, si cette formule n’est valide dans aucun de ses sous-arbres. Nous disons enfin comment, substituant l’étude intuitive de la déductibilité à celle de modèles, et esquivant ainsi les discussions précédemment évoquées, Beth requalifie ses tableaux sémantiques intuitionnistes en tableaux déductifs, et en reconsidère la méthode de justification.