La rigueur informelle

Overview & Synopsis

Si la rigueur formelle consiste à présenter des règles formelles puis à s’assurer qu’un raisonnement donné s’y conforme, il est clair que le travail qui précède la mise en forme n’en est pas pour autant livré à l’arbitraire et il semble donc qu’il y ait place pour une autre variété de rigueur, cette fois informelle. L’idée de rigueur informelle est associée au nom de Georg Kreisel et au combat qu’il a mené contre le formalisme hilbertien. Le texte vise un double objectif. Présenter plus en détail les idées de Kreisel; en déplacer légèrement le point d’application, afin de pouvoir proposer comme exemple de rigueur informelle la façon dont chez Martin-Löf les explications de sens servent à justifier les lois logiques.