Fin

Ce n'est que la fin de l'école d'hiver. Pas la fin de l'hiver, pas la fin du monde, etc. Mais ça fait du bien, on bosse trop ici. J'ai commencé à coder un mode interactif rudimentaire pour Bedwyr. Rudimentaire au sens où il ne permet pas de définir ses propres tactiques, et pour l'instant si je permets ça ce sera au détriment de la sûreté des preuves. Mais bon ça a son côté joli et je vais pouvoir bientôt faire tourner quelques exemples. Cela m'aidera peut être à réfléchir à comment cette logique nous permettra de parler du monde, et quelles sont les choses que l'on n'aura pas le droit de dire.

Peut-on définir: "P vrai si P est faux", "P(x) vrai si ∀y. P(y) est faux", "P(λx.Mx) vrai si ∀y. P(y) ⇒ P(My)" ? Non, non et heu... Ces définitions qui se mordent la queue sont des casse-têtes du point de vue des modèles. Mais la consistence ne peut-elle pas se passer de modèle ? Entre en scène "P(λx.Mx) vrai si ∇y. P(y) ⇒ P(My)". Je me sens un peu démuni sur ces questions.

Tout cela est très autoritaire, froid, contraignant. Aucune course-poursuite héroique, aucun lever de soleil sur la Mongolie, aucun corps nu... Si on a pas de poste après la thèse, Etienne veut faire luthier-vent. Peut être qu'alors je me mettrai au dessin ? Ou j'irai coder pour manger, plus crédiblement. On ne devrait pas parler autant de ces choses là à table.