Les théorèmes d'incomplétude de Goedel ne disent bien évidemment rien sur la
preuve de l'enoncé indécidable en Arithmétique (la cohérence). On analysera
brièvement quelques théorèmes "concrèts" d'incomplétude (Paris-Harrington et,
surtout, la forme finie de Friedman du théorème de Kruskal) pour mettre en
évidence un des points de la preuve qui echappent à la formalisation
arithmétique. Le lien sera alors établi avec l'idée de preuve prototype,
notion très simple en Théorie des Types, et discutera de son utilisation pour
analyser, dans leur preuve, le "lieu" de l'indémontrabilite' arithmétique
de ces théorèmes.