Origines et buts d'une logique

[bardamu]

Personnellement je trouve ridicule, et sans fondement ses attaques contre les logiques modales (dont je ne suis pourtant pas un zélateur), de l'ironie là où l'on attend des arguments scientifiques, c'est pathétique et sans doute un aveu d'impuissance.

Sur les questions de style, c'est une affaire de goûts et de couleurs, donc bon...
Mais pourquoi "un aveu d'impuissance" ?
Girard a créé la logique linéaire, et c'est pas mal comme boulot.

Petit rajout : amusant, wikipedia met la logique linéaire parmi les logiques modales...

Discussion scindée à partir de Réfutation du théorème de Gödel

[Médiat]

Sur les questions de style, c'est une affaire de goûts et de couleurs, donc bon...

C'est pourquoi j'ai commencé mon post par "Personnellement".

Mais pourquoi "un aveu d'impuissance" ?

Parce que lorsque l'on a de bons arguments scientifiques contre une théorie scientifique on n'utilise pas l'ironie qui n'a rien de scientifique

Girard a créé la logique linéaire, et c'est pas mal comme boulot.

Quand bien même serait-il le meilleur logicien du monde, que je ne retirerais rien de ce que j'ai écrit. Je suis étonné de voir ce genre d'argument d'autorité sous ta signature .

[bardamu]

(...) Parce que lorsque l'on a de bons arguments scientifiques contre une théorie scientifique on n'utilise pas l'ironie qui n'a rien de scientifique (...) Je suis étonné de voir ce genre d'argument d'autorité sous ta signature .

Bonjour,
je précise ma pensée parce qu'au vu de ta réaction, il se pourrait qu'elle n'ait pas été très claire.

Les tentatives de Fondement (avec majuscule) logico-mathématique ont montré des limites et quand aujourd'hui on essaie de faire le tour des systèmes produits, on est un peu décontenancé. Pour ma part, j'ai le sentiment que chacun développant son propre langage, on peut en venir à réserver la logique à des spécialistes de... ce langage.

Je rejoindrais donc Girard sur 2 points :
- la recherche de Fondements logico-mathématiques est peut-être une de ces "illusions" nécessaires de la raison pure mais l'abus me semble nuisible
- la multiplication des systèmes formels tend à être stérile si ils ne s'ouvrent pas à d'autres activités que la logique

Si je m'interrogeais sur ton expression "aveu d'impuissance", c'est qu'à mon sens, Girard a justement produit un système qui a une puissance, c'est-à-dire des applications. Sans doute a-t-il eu la chance de faire son travail à l'heure du développement de l'informatique, et peut-être que 30 ans plus tôt n'aurait-il rien produit en logique qui ait un usage. Malgré tout, il a ce souci du rapport au concret, d'éviter de faire du formel pour du formel.

Pour autant, si je trouve amusante la verdeur de son langage, loin de moi l'idée qu'il s'agisse d'argument scientifique. Pour ma part, je trouve son expression assez claire pour qu'on distingue entre les contenus scientifiques et son style qui va parfois jusqu'à la blague de potache.
"Toujours dans la science à l’usage des débiles légers, mentionnons les 'logiques' non monotones" (pour moi, c'est plutôt , que ...), ne fonctionnera comme argument d'autorité que si on donne d'emblée ce statut d'autorité à l'auteur. Sinon, ça peut mener à s'interroger sur ce que sont ces choses si "affreuses" qu'il dénonce, à éveiller la curiosité, et accessoirement à se méfier des effets de "bluff" que provoque le formalisme.
C'est tout le paradoxe des critiques de la Vérité et du Réalisme : il faut malgré tout affirmer sa vérité et sa réalité, sans être pris pour un prophète d'une Vérité (comme disait Nietzsche : "Plutôt être pris pour un bouffon que pour un Saint").

[Médiat]

Les tentatives de Fondement (avec majuscule) logico-mathématique ont montré des limites et quand aujourd'hui on essaie de faire le tour des systèmes produits, on est un peu décontenancé. Pour ma part, j'ai le sentiment que chacun développant son propre langage, on peut en venir à réserver la logique à des spécialistes de... ce langage.

Toutes les activités humaines et les théories scientifiques en particulier ont des limites, donc je ne vois pas ce que tu veux dire en particulier, il est incontestable que la recherche, ne serait-ce que dans le domaine de la logique classique du premier ordre a donné de beaux et de très beaux enfants

Je rejoindrais donc Girard sur 2 points :

- la recherche de Fondements logico-mathématiques est peut-être une de ces "illusions" nécessaires de la raison pure mais l'abus me semble nuisible

C'est un peu prendre les logiciens pour des imbéciles que de penser qu'ils ne comprennent pas ce qu’ils font dans leurs propres recherches.

- la multiplication des systèmes formels tend à être stérile si ils ne s'ouvrent pas à d'autres activités que la logique

C'est ce que de nombreux physiciens disent des maths, et de nombreux mathématiciens de la logique, ne lisant pas dans l'avenir, je ne peux pas savoir d'avance ce qui se révélera indispensable aux autres connaissances dans x années, et quand bien même cela ne servirait pas, cela aurait quand même servi, ou alors il faut que tu me donnes ta grilles pour savoir quelles sont les recherches qui sont bien et celles qui sont mal (cela va nous renvoyer aux maths pleines et aux maths vides de tristes mémoires).

Si je m'interrogeais sur ton expression "aveu d'impuissance", c'est qu'à mon sens, Girard a justement produit un système qui a une puissance, c'est-à-dire des applications.

Avec ce genre d'arguments l'art est inutile

Malgré tout, il a ce souci du rapport au concret, d'éviter de faire du formel pour du formel.

Je revendique le droit et le bonheur qu'il y a à faire du formel pour le formel, surtout si celui-ci se révèle plus profond qu'il n'y paraît (j'ai déjà cité Badiou plusieurs fois ici)

Pour autant, si je trouve amusante la verdeur de son langage,

Moi, non, ce que tu trouves amusant, je le trouve insupportable de suffisance et d'auto-satisfaction, mais c'est une histoire de goût, bien sur..

C'est tout le paradoxe des critiques de la Vérité et du Réalisme : il faut malgré tout affirmer sa vérité et sa réalité, sans être pris pour un prophète d'une Vérité (comme disait Nietzsche : "Plutôt être pris pour un bouffon que pour un Saint").

La non plus je ne comprends pas l'argument, car la logique formelle n'est pas une critique de la Vérité et du Réalisme (je conserve tes majuscules), et n'affirme aucune vérité puisqu'elle redéfinit dans son propre cadre ce qu'est la "vérité" (qui n'a pas de sens en dehors d'elle-même), et si je mets des guillemets, c'est que je n'aime pas ce vocabulaire propre à induire en erreur sur la qualité de "faux" et "vrai"en logique, je préfère encore et , (d'ailleurs Girard utilise "vrai" et "faux" d'où une formulation ambiguë du théorème d'incomplétude de Gödel) ; quant à la "réalité", la logique en fabrique autant qu'elle veut, difficile dans ce cas d'être prophète d'une réalité, l'existence de plusieurs logiques en est justement un garant supplémentaire.

[Médiat]

Je viens de me relire ce matin, et il me semble que mon ton est un peu agressif, ce n'etait pas utile ; je maintiens néanmoins et avec force :

1. Aimer ou non le style de Girard est affaire de goût et donc n'a aucune importance.
2. Affirmer, comme Girard, que les logiques modales sont sans intérêt puisqu'il y en a plusieurs n'est pas un argument scientifique et n'est donc pas recevable dans ce cadre.
3. L'utilitarisme me paraît un mauvais critère pour juger un champ de recherche.
4. Le formalisme pour le plaisir du formel s'est révélé très fécond, même si aucun industriel n'y a encore trouvé son compte (certains philosophes, l'y ont trouvé).
5. Utiliser le vocabulaire "vrai", "faux" pour la logique est un piège qui finit par se retourner contre le logicien que l'on accuse de se méler de ce qui ne le regarde pas (et en logique modale on parle facilement de "mondes possibles" au lieu de modèle, ce qui là aussi peut induire en erreur ceux qui voudraient interpréter ces "mondes").

Bonne année.

[Sephi]

(et en logique modale on parle facilement de "mondes possibles" au lieu de modèle, ce qui là aussi peut induire en erreur ceux qui voudraient interpréter ces "mondes")

Justement je suis tombé, à travers des lectures de philo, sur la logique modale et la sémantique des mondes possibles. Ces "mondes" sont-ils ni plus ni moins que des "modèles" pour une théorie de logique modale ?

[Médiat]

Ces "mondes" sont-ils ni plus ni moins que des "modèles" pour une théorie de logique modale ?

Oui, a un détail près : il faut une famille de modèles au sens habituel du terme, pour faire un modèle au sens d'une logique modale. Si tu veux en savoir plus, une recherche sur le net de "Modèle de Kripke" devrait te donner des dizaines de liens pertinents.

[Matmat]

Personnellement je trouve ridicule, et sans fondement ses attaques contre les logiques modales (dont je ne suis pourtant pas un zélateur), de l'ironie là où l'on attend des arguments scientifiques, c'est pathétique et sans doute un aveu d'impuissance.

Les arguments de JYG ne sont peut etre pas d'ordre scientifiques (mais ce n'est pas parce qu'ils ne sont pas scientifiques qu'ils sont sans fondement), mais un scientifique peut (et doit) utiliser des arguments non scientifiques pour dire ce qui est du domaine d'une science et ce qui ne l'est pas...

Ici , une question importante n'a pas été posée : Est ce que la logique est une activité purement mathématique ? Autrement dit peut on réellement considérer qu'un travail en logique est abouti lorsqu'on ne s'est borné à ne faire que des mathématiques !

Je remarque que traditionnellement les logiciens ne se privaient pas d'exprimer leurs considérations philosophiques, et c'était seulement aprés maintes considérations "extra-mathématiques" qu'ils s'attelaient à rechercher un système logique, l'un n'allait pas sans l'autre , le système logique était une conséquence des réflexions philosophiques qu'ils avaient faite.

Le logicien "moderne" qui produit une logique modale en quelques jours, et laisse aux autres le soin d'y trouver un quelconque rapport avec quoique ce soit, fait clairement l'impasse de considérations "extra-mathématiques" que s'imposaient le logicien "classique".

Il n'y a pas que la cohérence internes des systèmes qui compte... Demandons nous si on peut valider les logiques uniquement à l'intérieur des mathématiques alors meme que la logique n'est pas, et n'a jamais été, une activité purement et seulement mathématiques...

Cordialement,
Matmat

[Médiat]

Ici , une question importante n'a pas été posée : Est ce que la logique est une activité purement mathématique ?

C'est mon droit de logicien que de n'y voir qu'une activité mathématique et de considérer que ceux qui y voient autre chose lui font dire ce qu'elle ne prétend en aucun cas dire ; mais tant mieux si cela peut les aider ne serait-ce qu'à exprimer un problème (les lois de la thermodynamique resteraient valides même si l'on n'avait jamais inventé le moteur à explosion). Est-ce que la théorie des groupes est purement mathématique ? Que les physiciens l'utilisent, tant mieux, mais s'ils ne le faisaient pas la théorie des groupes continuerait d'exister.

la logique n'est pas, et n'a jamais été, une activité purement et seulement mathématiques...

Affirmation bien péremptoire qui rend caduque l'interrogation précédente que tu trouves importante, et dont je me moque complètement en tant que logicien (et comme ma personnalité ne se réduit pas à cela, je m'accorde le droit de réfléchir, au delà de ma pratique des mathématiques).

[invite431]

Demandons nous si on peut valider les logiques uniquement à l'intérieur des mathématiques alors meme que la logique n'est pas, et n'a jamais été, une activité purement et seulement mathématiques...

Eh ben, étant prof de logique formelle (floue aussi), il va falloir, apparemment, que je me recycle

La logique à pour seul but de vérifier la validité et non pas la véracité d'un raisonnement, indépendamment de son contenu.

Vérifier un raisonnement est une opération mathématique; pour les digressions sur le contenu je laisse libre cours aux philosophes.

P.S. Pour le formalisme logique, on est au XXIème siècle, plus chez les Grecs !

Amicalement

[bardamu]

Bonjour,

Je viens de me relire ce matin, et il me semble que mon ton est un peu agressif, ce n'etait pas utile

Je viens de me relire et il me semble que ce que j'ai dit est un peu léger...
Pour l'agressivité, pas d'inquiétude, tant que c'est pour la bonne cause, il est utile de s'entendre dire qu'on dit des choses débiles...

; je maintiens néanmoins et avec force :[*]Affirmer, comme Girard, que les logiques modales sont sans intérêt puisqu'il y en a plusieurs n'est pas un argument scientifique et n'est donc pas recevable dans ce cadre.

Le fond de sa critique ne me semble pas porter sur les logiques modales en général (lui-même conservant 2 modalités) mais sur la manière dont on fait de la logique.
Il y a sans doute à redire sur ses jugements à l'emporte-pièce mais, à mon sens, il a le mérite d'évoquer des questions épistémologiques sur la pratique des logiciens, la valeur/intérêt de tel ou tel système formel selon ce qu'on attend généralement d'une logique (cohérence, clarté, "scientificité", usage...).
C'est une critique de l'intérieur du milieu des logiciens et c'est selon moi à méditer.
Extraits de http://iml.univ-mrs.fr/~girard/cours/envoi.pdf

Il y une dizaine d’années, je n’aurais pas donné un sou des fondements. (...) J’ai été amené à changer d’avis lors de la rédaction de la seconde partie
de Locus Solum [34] ; il y avait des pistes à explorer, à condition de distinguer fondements et préjugés.
(...)
La logique s’est attiré le cordial mépris — assez justifié, dans l’ensemble — des mathématiciens pour son manque de :

Technicité : globalement faible, ce qui explique la prolifération des logiques jetables. Avec un minimum de compétitivité, la sélection naturelle nous aurait évité les logiques paraconsistantes et autres bidouillages.

Conceptualité : de rares sous-domaines cultivent la technicité, souvent pour elle-même. Ainsi, les degrés d’indécidabilité déclinent à n’en plus finir des variantes tordues d’un vrai théorème (Friedberg-Muchnik, 1956) : " les problèmes r.e. indécidables ne sont pas tous équivalents ". C’est difficile
sans être profond : une prouesse technique jamais n’abolira le concept.

Standards : rappeler que la logique non monotone contredit l’incomplétude est, paraît-il, mesquin ; exiger qu’un calcul des séquents vérifie le Hauptsatz serait, de même, dogmatique ; refuser un article aux formulations volontairement ambiguës passe pour le comble de l’élitisme. Pourtant, un mathématicien qui compléterait des opérateurs non bornés se ferait "jeter" ; et, dans la vie courante, personne n’achèterait une voiture sans freins ; pas plus, d’ailleurs, qu’un médicament aux propriétés incertaines.

Universalité : la logique développe des concepts à usage purement interne, un peu comme les devises non convertibles des ci-devant "démocraties populaires ". Un topologue peut-il entendre parler sans sourire des domaines de Scott, cette topologie "non convertible" ?
(...)
la logique est pour moi — et beaucoup d’autres — une discipline fascinante, une fenêtre magique sur le monde : à la fois science et regard sur la science.
Ce regard sur la science suppose des interlocuteurs ; autrefois, le regard décapant d’un Kreisel palliait, tant bien que mal, le manque d’épistémologues
compétents.
(...) une fée maligne a changé les épistémologues — dont la science a cruellement besoin — en " logiciens " épistémiques — dont elle n’a rien à faire. D’où l’idée un peu utopique de recréer le milieu détruit, de restaurer un dialogue interrompu, quitte à pécher parfois par naïveté : tentons-nous (LIGC, infra) de réinstaller le loup (l’épistémologue) dans les montagnes (la science vivante) ? (...)
Le groupe de réflexion pluridisciplinaire (mathématiques, physique, informatique, biologie, logique et épistémologie) LIGC "Logique et Interaction :
pour une Géométrie de la Cognition" ( http://www-philo.univ-paris1.fr/Joinet/ligc.html ) est tout, sauf un lieu de pensée unique, encore moins une secte. S’il fallait condenser en une ligne l’"esprit LIGC", ce serait : Subjectif, mais pas subjectiviste.
Ce slogan — kantien sinon dans la forme, du moins dans l’esprit — réfère à la constitution du sujet ; un sujet auquel il importe de restituer sa place si l’on veut éviter de prendre pour un absolu ce qui n’est qu’un attribut du miroir.

Au-delà de la forme du discours, il me semble que Girard et le LIGC sont dans une réflexion particulièrement pertinente sur l'évolution possible de la logique à partir d'un paradigme "opérationaliste".

Baguette dit : "La logique à pour seul but de vérifier la validité et non pas la véracité d'un raisonnement, indépendamment de son contenu" et c'est sans doute le souci d'une logique classique, dont le formalisme serait établi de toute éternité, mais qu'en est-il pour ceux qui créent des logiques ?
Pourquoi tenterait-on une nouvelle logique si tout était entendu qu'il ne s'agissait que de vérifier l'application de règles de cohérence ? Lorsqu'on essaie autre chose, c'est avec quels objectifs, quelles règles ?
A mon sens, l'approche de Girard tend à une logique aux prémisses stables, gérant le dynamisme procédural, constructive (utilisation d'une preuve dans un processus suivant, complexification), susceptible d'auto-validation "sémantique" (jeu entre processus) et adaptée à nos outils informatiques.

L'abandon d'une mentalité où l'on rechercherait une sorte de forme éternelle du Discours-Vrai peut se faire au bénéfice d'une modestie "kantienne" où la logique s'efforce de partir de quelques acquis pour éviter une remise en cause perpétuelle et avance en liaison avec l'environnement techno-philosophico-scientifique (physique, informatique, neurobiologie, mathématiques...).
J'ai l'impression que Girard considère que dans sa discipline on ne cherche pas de tronc commun, que chacun fait sa doctrine avec une rigueur aléatoire et qu'au final la recherche en logique n'apporte pas tout ce qu'elle pourrait.

[invite431]

Baguette dit : "La logique à pour seul but de vérifier la validité et non pas la véracité d'un raisonnement, indépendamment de son contenu" et c'est sans doute le souci d'une logique classique, dont le formalisme serait établi de toute éternité, mais qu'en est-il pour ceux qui créent des logiques ?

Bonsoir,

Qu'est-ce qu'une logique "classique" ? Qui a dit que le formalisme d'une logique quelconque soit établi de toute éternité ?

La logique floue à abandonné le principe du tiers-exclu. Est-ce par opposition à la logique formelle ? Non, mais pour obtenir d'autres résultats ou plus exactement une autre "gamme" de résultats, l'une n'exclut pas l'autre, elles ne sont pas antagonistes mais complémentaires.
En quoi la logique floue ne répond elle pas au principe "La logique à pour seul but de vérifier la validité et non pas la véracité d'un raisonnement, indépendamment de son contenu" ?

Pourquoi tenterait-on une nouvelle logique si tout était entendu qu'il ne s'agissait que de vérifier l'application de règles de cohérence ? Lorsqu'on essaie autre chose, c'est avec quels objectifs, quelles règles ?

Qui a jamais dit que "tout était entendu" ?

Et pourtant, toute logique ne peut être consistante sans vérifier l'application de SES règles de cohérences, sous peine de faire tout sauf de la logique.

Les oppositions me paraissent toujours, dans ce domaine, porter plus sur la sémantique que sur la ... logique !

Apparemment, la philosophie ne se console pas de ne plus contenir la mathématique, et la mathématique n'arrive pas à se consoler de ne plus pouvoir faire de philosophie.

Amicalement

[Médiat]

Je veux d'abord préciser que je n'ai jamais dit que Girard était le pire logicien du monde (j'ai juste laissé entendre qu'il n'était pas le meilleur ; outre qu'une telle remarque n’est que rhétorique, mes révérences vont à Shelah ), j’ai juste dit que je n’aimais pas sa suffisance, et dans ce domaine les extraits que tu cites me confortent dans cette attitude, et qu’il utilisait des arguments n’ayant rien de scientifiques contre les logiques modales ; néanmoins je vais jouer ton jeu et reprendre les arguments de Girard :

• Manque de technicité : j’ignorais que la technicité (clairement associé à la difficulté dans le paragraphe suivant) fut un critère de jugement d’une théorie scientifique (ici manque de technicité et dans le paragraphe comceptualité il y en a trop, bizarre).
• Manque de conceptualité : la catégoricité, la stabilité, les rangs de Morley, tous les travaux de Shelah etc. tout cela se ferait sans " concept " (ici, pas de concept, dans le paragraphe universalité il y en a, bizarre) ?
• Manque de standards : encore une fois, dans quelle plaque de marbre est-il gravé qu’une théorie scientifique doit être monolithique et figée à tout jamais ? Je suis étonné, que l’on puisse reprocher à un domaine scientifique d’explorer les possibles (c’est le cas des différentes logiques modales), ne serait-ce que pour en dresser la taxonomie, et ainsi en extraire la cinquième essence.
• Manque d’universalité : une science ne se développerait que dans son propre cadre ? Mais c’est un critère obligatoire pour qu’une théorie scientifique soit crédible : qu’elle ne s’occupe que d’elle-même, laissant les interprétations hors cadre à d’autres (que dirait-on si la logique était inféodée à d’autres théories, scientifiques ou non ?). Bien sur pour les sciences expérimentales, il y a toujours, à un moment ou à un autre, une confrontation avec le " réel ", mais cela n’a pas de sens pour les maths en général et la logique en particulier.

Pour le reste, j’approuve totalement la dernière intervention de baguette.

[bardamu]

Bonsoir,
Qu'est-ce qu'une logique "classique" ? Qui a dit que le formalisme d'une logique quelconque soit établi de toute éternité ?
(...)Qui a jamais dit que "tout était entendu" ?
(...)

(...) je vais jouer ton jeu et reprendre les arguments de Girard : (...)

Bonjour à vous deux,
je redis là où je vois la question (celle du théorème de Gödel est réglée ?).
Girard fait des jugements sur des voies qui lui semble épuisées ou moins prometteuses que la sienne. On peut certes contester sa perception mais, à mon sens, elle indique une possible évolution (révolution ?) de la logique et c'est là le point qui me semble le plus intéressant.

Quand il dit "manque de technicité, conceptualité etc.", c'est par rapport au regard des mathématiciens, leur "cordial mépris" envers la logique selon lui. Il me semble que le contre-argument devrait être que les mathématiciens n'ont pas ce mépris envers la logique, qu'ils s'y intéressent, en font quelque chose. Est-ce le cas ? Et si ils ne s'y intéressent pas, pourquoi ? Il n'y a aucun lien entre math et logique ? Est-ce que les relations pourraient changer (logique/informatique => logiciel Coq pour la vérification de preuves) ?

Pour Baguette : quand je parle de logique "classique", c'est celle qui dit qu'il s'agit seulement de "vérifier la validité d'un raisonnement, indépendamment de son contenu". Girard estime que la logique peut être autre chose.
Extrait de http://www.anr-prelude.fr/IMG/pdf/LudAppPrag.pdf

Dans la conception traditionnelle, une formule, pour être validée, doit faire l’objet d’une preuve (...), mais pour être invalidée, il suffit de lui fournir un contre-modèle, c’est-à-dire un modèle dans laquelle elle est fausse.
Ainsi peut-on dire que les preuves s’opposent aux contre-modèles, conception un peu curieuse qui oblige le logicien à constamment faire le grand écart entre le monde de la SYNTAXE et celui de la SEMANTIQUE.

Girard, depuis au moins son article On the meaning of logical rules ([5]), tente d’abolir cette conception dualiste pour la remplacer par une conception moniste au terme de laquelle les preuves ne s’opposent plus à des contre-modèles mais à des contre-preuves (ou, si on veut, à des réfutations), autrement dit des objets de même nature. Une telle entreprise ressemble beaucoup à la Théorie des Jeux puisque cette dernière est justement
basée sur la confrontation de deux joueurs (un proposant et un opposant), l’un qui propose une formule et la défend face aux attaques de l’autre jusqu’à ce que l’un des deux n’ait plus de coup à jouer (en ce cas, il est le perdant).
(...)
pour Girard, une sémantique séparée de la syntaxe n’a pas lieu d’être. La signification des règles de la logique est dans les règles de la logique elles-mêmes, par exemple dans leurs symétries.
Dans On the meaning etc., Girard dit :
My thesis is that the meaning of logical rules is to be found in the well-hidden geometrical structure of the rules themselves

Il donne comme illustration la négation, qui ne saurait être interprétée par ”NO” (par une simple inversion des valeurs de vérité) mais par l’échange des positions entre proposant et opposant.
La position défendue par Girard peut ainsi être dite immanentiste par opposition à la conception tarskienne qui conduit à une perpétuelle fuite en avant dans les niveaux méta dès qu’il s’agit de fonder la notion de vérité comme étant aux racines mêmes de la sémantique, conception que l’on peut qualifier alors de transcendantale (il faut croire en la vérité aux niveaux méta pour fonder la sémantique d’une formule).
Avec cette perspective, le logicien peut envisager de vivre dans un univers homogène (plus la peine de faire le grand écart !).
(...)

En matière d'application, il y a quelques exemples simples de dialogues dans le document, et à la limite, on pourrait formaliser les échanges de forum avec ce système.
On verrait apparaître des divergences, convergences, paralogismes, abandons de l'échange etc. et, exceptionnellement (d'après mon expérience...), des consensus. On pourrait peut-être aussi faire apparaître la logique des uns et des autres, c'est-à-dire leur comportement dans l'échange.
Au lieu de chercher des règles gérant des modalités d'échanges rationnel et de vérifier ensuite que ça marche sur les modèles, on constaterait la structure de ces échanges et les règles qui les régissent.

[Médiat]

Ainsi peut-on dire que les preuves s’opposent aux contre-modèles, conception un peu curieuse qui oblige le logicien à constamment faire le grand écart entre le monde de la SYNTAXE et celui de la SEMANTIQUE.

Grand écart ? Non, juste l'application du théorème de complétude d'un certain Gödel. Cette façon, une fois de plus, de présenter les choses est biaisé, en effet pour montrer qu'une formule (du premier ordre) est "vraie" dans le cadre d'une théorie complète, il suffit de montrer qu'elle est vraie dans un seul modèle, à l'opposé trouver un contre-modèle ne montre pas que la proposition est "fausse" (car cela il faut encore le prouver), mais seulement qu'elle n'est pas "vraie".

Encore une fois je n'ai jamais dit que toutes les idées de Girard étaient mauvaises ou inintéressantes, seulement que sa façon de présenter les choses serait modérée rapidement sur FSG (n'avons nous pas assez vu de "ce que font les autres est nul, la seule façon de faire un tant soit peu intelligente est la mienne" non ?). Je me sentirais beaucoup plus attiré par la lecture de ses textes s'ils étaient sur un autre ton (j'ai lu les 30 premières pages du "Point aveugle", mais j'ai fini par me lasser de ses lazzis).

PS : il est possible que ma formation de danseuse m'est préparé au grand écart (je voulais dire, formation de théoricien des modèles).