De la lecture

Un peu risqué de laisser ça ici avant la soutenance, non? En tous cas je vais lire ça m'intéresse, il y a longtemps que je tourne autour de ce qu'a initié Girard sans avoir vraiment eu le courage de m'y mettre à fond.

Ben si tu postules MDC ou CNRS j'imagine qu'il vaut mieux faire circuler un produit fini, c'est-à-dire une thèse acceptée qui inclus les corrections suites aux rapports de jury (tu parles de possibles grosses bêtises restantes).

J'ai rien compris (le seul endroit où je comprends les mots, c'est les algèbres d'opérateurs !), mais c'est très joli. Sinon, méfie-toi quand même : suppose que TF1 s'en empare pour en faire un jeu de télé-réalité ! Qui récupérera les royalties ??? :P

> leon : en quoi est-ce risqué ?

risqué, pas vraiment mais c'est un peu maladroit. Tu mets le nom des rapporteurs sur un document qu'ils n'ont pas validé, disons que ça se fait pas trop. Evidemment en pratique ça ne pose pas de problème parce que le directeur s'est assuré avant que le manuscrit sera accepté par les rapporteurs.

C'est un peu le même problème, dans une moindre mesure, que les gens qui mettent sur leur page web un article avec marqué "soumis à Annals of Mathematics".

Je te souhaite effectivement un meilleur destin scientifique que celui des deux zozos... et je t'imagine plus honnête!

Pour l'histoire des papiers soumis, je vois ça souvent et étant en phase de candidature MdC ça m'énerve prodigieusement. Bon, faut pas être parano non plus, c'est fait honnêtement en général mais je souhaite bien du courage aux membres des commissions pour juger tout ça sereinement...

Bonne chance pour ta soutenance de thèse, Deufeufeu. Je dois avouer, j'ai parcourut ta thèse en diagonale, mais la logique ne me passionne pas vraiment.

J.

{\it l'éminent jury m'ayant délivré le grade de docteur en mathématiques cette après-midi}

Toutes mes félicitations.


Borde.

Mes plus sincères congratulations, docteur.
Faut-il dire deudeufeufeu désormais ?

e.v.

(tu)

Félicitations ! Tu as eu une ceinture noire ? http://abstrusegoose.com/143

Bravo deufeufeu ! Par contre, la deufeufatation se traîne toujours sur Google, il faut que tu fasses quelque chose !

Ne t'en fais pas Kito, je ne dézingue que les méchants.

Félicitations et bon courage pour la suite

FD, si ça t'intéresse de mélanger les 2 lignes (forcing et correspondance de Curry Howard) voici un résumé d'un principe unificateur Krivinien:

pour passer de l'univers classique à l'univers "forcing", on remplace l'ensemble de vérité à 2 éléments vrai,faux par une algèbre de Boole complète. Les seules difficultés étant:

1) d'avoir le courage de s'émanciper des constructions techniques initialisantes: ie définir proprement quand l'énoncé "nomA appartient à nomB" a la valeur v de l'algèbre de Boole. Mais une fois ça fait, la valeur de l'énoncé:

$A\to B$ est naturellement la borne sup de valeur de nonA et de valeur de B

et celle de l'énoncé

$\forall xR(x)$ est naturellement la borne inf quand $x$ parcourt tous les noms, des valeurs de $R(x)$

2) De créer des algèbres de Boole exotiques pour obtenir, par exemple, que la valeur de vérité de "non hypothèse du continu" soit non nulle (etc)

Mais initialement, Cohen ne l'avait inventé de cette façon simple: il avait défini "p force A" par récurrence sur la construction de l'énoncé.

"p force $A\to B$" signifie " pour tout $q\leq p$ qui force A, on a que $q$ force aussi B"

"p force $\forall xR(x)$" signifie "pour tout nom a, p force R(a)"

JLK a remarqué un truc très naturel:


il se passe la même chose avec la "réalisation" des énoncés:

un programme qui force $A\to B$ est un programme p tel que pour tout programme q qui force A, le programme "p.q" force B

(l'autre cas est trivial avec quelque soit)

Il s'ensuit qu'en regardant le "." comme l'opération "borne inf", on retombe sur du forcing.

Ou plus précisément: le forcing est un cas particulier de "réalisation abstraite" où on définit:

une structure "réalisante" ou "froçante" ou "garantissante" comme étant de la forme E=(P,T,F,.,force) une structure avec P considéré comme un ensemble de "programmes", T un ensemble de phrases, et "force" une partie de $P\times T$, F un ensemble d'environnement et . une application de P² dans P et vérifiant:

p force $A\to B$ ssi pour tout q: q force A implique p.q force B

p force $\forall xR(x)$ ssi: pour tout a, p force R(a)

Dans ce cas, le forcing est un exemple, et les travaux de CorCuHo en donne un autre. Dans le cas du forcing, les programmes sont les valeurs de vérité d'une algèbre de Boole et le "." est l'opération borne inf

Dans la CorCuHo, le . est l''application du lambda calcul et les programmes sont les habituels programmes de l'informatique (écrits en camL par exemple, mais ça n'est pas très important)


Edit: je n'ai pas utilisé F, pour pas compliquer, mais voilà comment il s'utilise:


p force A quand p ne buggue dans aucun environnement qui résiste à A.

Un environnement e (un élément de F), résiste à $A\to B$ quand il "offre" un $p\in P$ qui force $A$ et un environnement e' qui résiste) à B

Et ce n'est pas le mot "force" qui est "primitif", mais les mots "résiste"; "buggue"

Au fait Marco, la dédicace de ta thèse n'est plus à jour??? :-) :-) :-)

Bon courage pour la rentrée,

F.D.