Comments on Gödel was here

Il vaut mieux penser à ¬P comme P⇒⊥ : à ce moment-là, il devient clair que de P et ¬P on déduit ⊥ (c'est un simple modus ponens, donc certainement valable en logique intuitionniste), c'est-à-dire (P∧¬P)⇒⊥, bref, ¬(P∧¬P). En revanche, P∨¬P, en termes brouweriens, ce serait quelque chose comme la possibilité d'avoir P ou ¬P de façon constructive, et ce n'est certainement pas vrai en général (en logique intuitionniste).

On peut aussi penser à ça à travers l'isomorphisme de Curry-Howard : si P est un type d'un langage fonctionnel, et ⊥ (“Bottom”) le type vide, trouver un objet de type (P∧(P⇒⊥))⇒⊥, c'est facile (une fonction qui prend un argument qui est un couple formé d'un élément de type P et d'un de type P⇒⊥ et qui applique ce dernier au premier), alors que trouver un élément de type P∨(P⇒⊥) (c'est-à-dire un élément d'un type qui a un constructeur depuis P et un depuis P⇒⊥), c'est plus technique (mais avec la loi de Pierce, c'est-à-dire avec le call/cc, ça se fait, donc, quand on abandonne la logique intuitionniste pour passer en logique classique).

Ceci étant la logique intuitionniste n'est pas très très importante : trouver une démonstration de T en logique classique, c'est bien. Mais attention ! il peut y avoir des choses qui ressemblent très subtilement à une preuve vraie et qui, en fait, sont incorrectes, car elles utilisent d'une façon ou d'une autre quelque chose d'injustifié (comme la consistance de la théorie ou bien une forme de complétude).

julio → On peut faire par l'absurde, effectivement, mais pas de la façon la plus naïve qui soit. En gros, il faut dire : si on suppose ¬T (par l'absurde), par définition de T, T n'est pas prouvable, c'est-à-dire que ¬T n'est pas réfutable, bref, la théorie prouve (enfin, postule) sa propre consistance, et ça, par le théorème de Gödel, ce n'est possible qu'à moins qu'elle soit contradictoire, donc ¬T est contradictoire, bref, ceci prouve T. Mais cette preuve ne marche pas en logique intuitionniste, alors que celle que j'ai donnée, si.

Bon, voici quand même une preuve du théorème T. Je note ◻A pour l'affirmation « A est un théorème » (il faut parenthéser ◻A⇒B comme « (◻A)⇒B » et non « ◻(A⇒B) »). On a T⇔◻T par définition de T. Par ailleurs, une autre diagonalisation / Quineification du même style permet de construire G tel que G⇔(◻G⇒T). Alors on a les résultats suivants :
G⇒◻G⇒T (par définition de G)
◻(G⇒◻G⇒T) (en reflétant la preuve de ce qui précède)
◻G⇒◻(◻G⇒T) (par modus ponens interne)
◻G⇒◻◻G⇒◻T (idem)
or ◻G⇒◻◻G (par réflexion interne)
du coup, ◻G⇒◻T (découle des deux précédents)
mais ◻T⇒T (par définition de T)
ainsi, ◻G⇒T (découle des deux précédents),
c'est-à-dire G (c'est exactement la définition de G),
et aussi ◻G (en reflétant),
ce qui prouve T (on a prouvé ◻G et ◻G⇒T).

Tiens, il y a des normaliens même pas capables d'écrire « Descartes » sans faute d'orthographe…

« “I don't think so,” said René Descartes. Just then, he vanished. » :-)