From madore@news.ens.fr
Path: eleves!not-for-mail
From: madore@news.ens.fr (GroTeXdieck)
Newsgroups: ens.forum.lettres
Subject: Re: L'aquarium
Date: 6 Nov 1999 02:39:32 GMT
Lines: 295
Sender: madore@clipper.ens.fr
Message-ID: <8004d4$p8k$1@clipper.ens.fr>
References: <7vtbjl$65m$1@clipper.ens.fr> <7vvill$1si$1@clipper.ens.fr> <7vvjkt$406$3@clipper.ens.fr> <7vvk9f$1si$3@clipper.ens.fr> <7vvrqh$ebq$1@clipper.ens.fr> <7vvubu$ft4$1@clipper.ens.fr>
NNTP-Posting-Host: clipper.ens.fr
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: clipper.ens.fr 941855972 25876 129.199.129.1 (6 Nov 1999 02:39:32 GMT)
X-Complaints-To: forum@clipper.ens.fr
NNTP-Posting-Date: 6 Nov 1999 02:39:32 GMT
X-Newsreader: Flrn (0.4.0 - 07/99)
X-Wisdom-Of-The-Day: I believe discord doesn't help avoid regularity. 
X-Troll: Ben il en redemande, je suis bien oblige de lui en redonner.
Xref: eleves ens.forum.lettres:73

Frederic Chateigner in litteris (lettres:72) scripsit :
> Comment ça, ça veut rien dire ? Au sens large, syllogismos, c'est un
> raisonnement ; au sens restreint, c'est une forme de raisonnement, certes
> dépassée (ie intégrée), mais assez bien définie, non ? Ça n'annonce pas

Non, pas bien définie - ou plutôt, passablement arbitraire.  Disons
que si on cherche à décortiquer le raisonnement au point d'en
descendre à un niveau aussi élémentaire, il faut vraiment faire
l'effort de préciser exactement quelles manipulations on peut faire.

On peut sauver l'intérêt du syllogisme en l'assimilant à la loi très
précise appelée « modus ponens » (ou « application ») dans la
terminologie « actuelle » : si on a A=>B et qu'on a A alors on a B.
Le modus ponens forme la moitié du raisonnement (en logique
classique), l'autre moitié étant fournie soit par le théorème de
déduction (ou « abstraction » : si j'ai montré B en faisant
l'hypothèse, temporairement admise, que A, alors en fait j'ai montré
A=>B sans aucune hypothèse), soit (en éliminant le théorème de
déduction par « élimination d'abstraction ») par un jeu d'axiomes dits
de Hilbert, dont les deux plus importants sont K : A=>B=>A et S :
(A=>B=>C)=>(A=>B)=>A=>C.  Dans ce cas le syllogisme est bien une étape
importante du raisonnement, mais ce n'est pas vraiment le sens
classique.

Mais classiquement le syllogisme c'est un peu plus que ça.  Ce serait
plutôt une forme de transitivité de l'implication : si tout ce qui
possède la propriété P possède la propriété Q et que tout ce qui
possède la propriété Q possède la propriété R, alors tout ce qui
possède la propriété P possède la propriété R.  (Exemple : tous les
chats sont des animaux, tous les animaux sont mortels, donc tous les
chats sont mortels.)  Mais sous cette forme ce n'est plus du tout un
raisonnement atomique, c'est une succession d'étapes, et pas plus
intéressante qu'une autre, ni particulièrement associée à la règle de
« modus ponens » citée plus haut (certes, on l'utilise - mais on
l'utilise partout, aussi).  Décortiquons avec Coq :

| Welcome to Coq V6.3 (July 1999)
| No .coqrc or .coqrc.6.3 found. Skipping rcfile loading.
| 
| Coq < Parameter U (* Universe of discourse *) : Type.
| U is assumed

U sera mon Univers de discours, contenant toutes les choses dont je
peux parler.

| 
| Coq < Parameters cat, animal, mortal : U->Prop.
| cat is assumed
| animal is assumed
| mortal is assumed

« Chat », « Animal » et « Mortel » sont définies comme des propriétés
sur cet univers de discours, i.e. des fonctions P qui prennent un
individu x et lui donnent une propriété (P x) (« x est un chat »,...),
(P x) étant une affirmation (Prop est le type des propositions en
Coq).  Donc ce sont des fonctions de U vers Propr, notation U->Prop.

| 
| Coq < Axiom first : (x:U)((cat x)->(animal x)).
| first is assumed

Cet axiome dit que pour tout x, si x est un chat, alors x est un
animal.

| 
| Coq < Axiom second : (x:U)((animal x)->(mortal x)).
| second is assumed

Cet axiome dit que pour tout x, si x est un animal, alors x est
mortel.

| 
| Coq < Theorem syllogism : (x:U)((cat x)->(mortal x)).
| 1 subgoal

J'annonce que je vais démontrer le théorème suivant : pour tout x, si
x est un chat, alors x est mortel.

|   
|   ============================
|    (x:U)(cat x)->(mortal x)

Coq m'écrit ce que je dois démontrer.  Au-dessus de la ligne figurent
mes hypothèses.  Pour l'instant, je n'en ai pas.

| 
| syllogism < Intro x.

Ce que je veux démontrer commence par « pour tout x ».  J'annonce donc
que j'instancie ce x.  Philosophiquement, je ne peux pas raisonner
directement sur tout l'Univers, il faut que je choisisse un élément de
cet Univers, que je raisonne dessus, et je pourrai ensuite tirer des
conclusions générales parce que le choix était arbitraire.

C'est important (et c'est le fait de ne pas avoir réalisé ça plus tôt
qui a, à mon humble avis, causé des complications aux logiciens
classiques).  Parce que sinon, on est obligé de faire des
raisonnements « à l'intérieur » des quantificateurs universels : pour
dire le moins, c'est malcommode.  Pis que ça : ça dénote un manque de
compréhension de l'unité de la logique (distinguer le « particulier »
du « général » est absurde, le général n'est autre que le raisonnement
particulier appliqué à chaque instance).

| 1 subgoal
|   
|   x : U
|   ============================
|    (cat x)->(mortal x)

J'ai pris un x arbitraire, qui rentre dans mes hypothèses (c'est un
membre de l'Univers).  Puisqu'il est arbitraire, il suffit que je
prouve mon assertion (« si x est un chat alors x est mortel ») sur ce
x-là.

| 
| syllogism < Intro H.
| 1 subgoal

Mon affirmation commence par un « si ».  J'applique le théorème de
déduction (tactique « Intro » de Coq) : je vais donc supposer que x
est un chat.

Au niveau mathématique, l'étape consistant à prendre un chat x dans
l'Univers, ou à prendre une hypothèse H que x est un chat, sont
exactement de même nature (Coq utilise « Intro » pour les deux), avec
juste un « méta » qui flote.  Une implication ou une quantification
universelle sont la même chose (si ce n'est que dans l'implication le
terme de droite ne dépend pas du paramètre alors que dans la
quantification il le peut).

|   
|   x : U
|   H : (cat x)
|   ============================
|    (mortal x)

À ce moment-là, j'ai l'hypothèse supplémentaire (notée H) que x est un
chat, et je dois montrer que x est mortel.

| 
| syllogism < Apply (second x).
| 1 subgoal

J'applique mon second axiome, instancié à l'individu x.  Il y a là une
règle de modus ponens (tactique « Apply » de Coq).

|   
|   x : U
|   H : (cat x)
|   ============================
|    (animal x)

Je sais que x est un chat, et je dois maintenant montrer que c'est un
animal.

| 
| syllogism < Apply (first x).
| 1 subgoal

J'applique le premier axiome, instancié à x.

|   
|   x : U
|   H : (cat x)
|   ============================
|    (cat x)

Maintenant je dois prouver que x est un chat sachant que x est un
chat.

| 
| syllogism < Exact H.

Or c'est exactement une hypothèse (H).

| Subtree proved!

Donc j'ai fini la démonstration.  Coq s'en émerveille.

| 
| syllogism < Qed.

Ce qu'il fallait démontrer.

| Intro x.
| Intro H.
| Apply (second x).
| Apply (first x).
| Exact H.

Coq récapitule les étapes de la démonstration.  On voit au passage que
ce n'était pas une raisonnement atomique : il y avait bien plusieurs
étapes distinctes.

| 
| syllogism is defined
| 
| Coq < Print syllogism.

Je demande de réécrire la preuve sous forme symbolique.

| syllogism = 
| [x:U; H:(cat x)](second x (first x H))

Voici cette réécriture.

|      : (x:U)(cat x)->(mortal x)

Et voici le théorème démontré.

| 
| 
| Coq < Quit.

Fin de la session.

> plus de pipo que tout autre terme logique, généralement. Il y a plein
> d'exemples sur forum. Je préfère pipoter avec de la logique bien ringarde,

Bien sûr.  Ce que je veux dire c'est que le syllogisme donne
l'impression d'avoir fait une étape minimale et universelle, donc
inattaquable, du raisonnement.  Or cette étape n'est ni minimale (il
faut bien voir cette idée d'instanciation et de généralisation
successive) ni universelle, ni inattaquable.  Certes, quand quelqu'un
fait un syllogisme, c'est tout de même plus souvent une des prémisse
qui est foireuse que le syllogisme lui-même.  Mais le pipo est
néanmoins fréquent.

> ça a un côté scolastique assez plaisant.

Mais faire de la logique scolastique moyen-âgeuse avec un programme de
la fin du XXe siècle, c'est un plaisir délectable, assurément.

> Par ailleurs, tu prends l'exemple "Socrate est mortel" dans Coq. Mais cet
> exemple canonique n'est pas un syllogisme. Le syllogisme n'admet que des
> propositions générales. Pas d'individus, donc. Je ne saurais pas très bien
> te dire pourquoi, je crois que c'est lié à la question de l'existence, et
> tout le gouspin, mais il est trop tard pour y réfléchir. Enfin, c'est un
> détail. À confirmer, d'ailleurs.

Si je me rappelle bien, les logiciens considéraient plusieurs types de
syllogismes selon que les prémisses fussent générales ou
particulières, positives ou négatives.  Ainsi, une prémisse générale
et positive était désignée par la lettre A ; si les deux prémisses
étaient « A », la conclusion l'était ; cette forme de syllogisme
(comme celui avec mes chats) était notée A-A-A, où « BARBARA » pour le
moyen mnémotechnique.  Si la prémisse mineure est particulière
(« Socrate est un homme »), c'est « E », et le syllogisme est (sur la
mortalité de Socrate) est « E-A-E » ou « CELARENT ».  Il y avait aussi
des possibilités de prémisses négatives (lettres « I » et « O ») et
tout un tas de mots idiots pour retenir ça.

De toute façon, la distinction est oiseuse : les formes réputées
« particulières » peuvent se ramener aux formes « générales » par
introduction d'une propriété qui n'est vérifiée que par l'individu
considéré « être Socrate » est au même niveau que « être un chat », et
inversement les formes « générales » peuvent se ramener aux
« particulières » par l'utilisation de la généralisation comme je l'ai
fait.

Si j'ose me hasarder à émettre une opinion, c'est que la logique doit
être confiée aux logiciens (et aux informaticiens).  Les philosophes
n'ont pas à regarder la logique elle-même, on la comprend déjà
parfaitement.  Eux doivent nous expliquer, par exemple, ses relations
avec la pensée humaine (qui est tout sauf logique), avec le langage
humain, ou peut-être avec le monde réel.  Malheureusement, la logique
elle-même est trop souvent mal comprise, y compris des
mathématiciens.  Sous prétexte que c'est un truc trivial (ce l'est),
on lui fait dire des bêtises.

> + Ça a l'air marrant, Coq, c'est quoi exactement ?

C'est un programme développé par une équipe de l'INRIA qui a pour but
de permettre la vérification mécanique de preuves mathématiques.
C'est surtout utiliser pour de la certification de programmes (on
prouve qu'un programme fait bien ce qu'on attend de lui, et Coq
vérifie que cette preuve est correcte).  Je m'étais amusé, dans le
temps, à lui faire vérifier tout un tas de théorèmes de base de la
théorie des ensembles.  Ça peut aussi servir à barboter comme un fou
(le fait de dire des choses garanties correctes par le programme
n'empêche pas qu'elles puissent quand même être idiotes ou sans
intérêt) ou à épater la galerie.

>> Faut pas, faut pas.  J'aime bien les littéraires.  (Surtout quand ils
>> sont bl...  non, rien.)
> 
> Tu veux dire B/L ?

Non.  Pas spécialement.

>                    Ou blond(e)s ? Ou les deux ?
                             ^^^
                             Non

Oui.