Preuves, réfutations et contre-exemples

L'analyse du rôle des preuves et des réfutations, due à Lakatos, est examinée d'un point de vue logique. On se propose de montrer tout d'abord que, dès que des énoncés de complexité arbitrairement grande sont pris en compte, le processus dialectique ne peut plus mettre en jeu, pour une conjecture proposée, une "démonstration informelle" d'une part, et une réfutation qui résulterait de la seule donnée d'un contre-exemple, d'autre part ; mais plutôt deux conjectures incompatibles, chacune étant accompagnée d'une "démonstration informelle", d'une "expérience de pensée". Privilégier celle appuyant le contre-exemple allégué n'est possible qu'en s'appuyant sur la conception "euclidienne" de la démonstration qui est donc présupposée dans l'analyse de Lakatos. Celui-ci semble admettre d'ailleurs que le processus dialectique s'achève lorsque la conjecture modifiée prend la forme d'un énoncé "logiquement valide" et plus seulement "mathématiquement vrai" et sa démonstration celle d'une preuve formelle. Ensuite, on s'intéresse aux mécanismes qui font d'une preuve formelle un instrument permettant d'écarter effectivement les contre-exemples en s'appuyant sur l'interprétation sans contre-exemple introduite indépendamment par Gödel et Kreisel. L'enjeu de ces résultats est apprécié dans la perspective de donner une proof-theoretic semantics des mathématiques classiques qui puisse être l'analogue de celle obtenue pour les mathématiques intuitionnistes