<foo>
simply produces <foo>in the text).
<URL: http://somewhere.tld/ >
,
and it will be automatically made into a link.
(Do not try any other way or it might count as an attempt to spam.)mailto:
URI,
e.g. mailto:my.email@somewhere.tld
,
if you do not have a genuine Web site).
Ruxor (2005-01-24T14:14:31Z)
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 (2005-01-24T13:57:23Z)
Ok j'ai compris mon "erreur".
Après de (très rapides) recherches, il semblerait qu'en logique intuitionniste, on ait droit à "non(A et non(A))" mais pas à "(A ou non(A))". Ce qui me parait pas du tout intuitif, pour le coup ;)
(Je sors ça d'ici : <URL: http://fr.wikipedia.org/wiki/Principe_du_tiers_exclu/ >, et d'ailleurs ça serait pas mal d'avoir un article sur la logique intuitionniste… ;))
Ruxor (2005-01-24T12:22:29Z)
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.
julio (2005-01-24T10:52:58Z)
Hmmm, j'ai peut-être loupé un ou deux niveaux d'abstraction, mais à la première lecture il m'a semblé que la preuve par l'absurde marchait bien. Non ?
Ruxor (2005-01-23T17:18:08Z)
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).
Ruxor (2005-01-22T12:56:54Z)
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. » :-)
Decartes (2005-01-22T12:52:13Z)
Je pense donc je suis.