est de montrer que si Fermat est indécidable  dans Peano, il est vrai dans N, vu que c'est un énoncé Pi_0^1, ce qui donne une idée de ce que pourrait être une preuve d'indécidabilité ! Par contre, je suis assez d'accord avec le fait de mettre en avant le caractère fini des démonstrations (en insistant sur la récurrence), fautil le faire ne intro ?