Logique classique et déduction naturelle

[inviteab8f3a27]

Bonsoir,

Je viens d’apprendre aujourd’hui, qu’il existe des dérivées de la logique classique, apparemment plutôt des sous-ensembles (des interprétations volontairement restreintes), comme par exemple la déduction naturelle, qui par exemple ne connais pas le tiers-exclus (et à été conçus de cette manière).

Dans le même temps, il est dit sur Wikipédia, que la déduction naturelle à donné naissance à quelque chose qui s’appel «*isomorphisme de Curry-Howard*», qui si j’ai bien compris, traite de la correspondance entre preuve par la logique et preuve par l’algorithme.

Ma question n’est pas vraiment sur tous ces détails, mais simplement sur : comment une logique, qui est un sous ensemble d’une autre, peut-elle donner naissance à des choses qui n’ont pas put apparaître avec l’autre ?

J’espère ne pas être trop confus dans ma question.

Sinon, autre formulation assez équivalente : qu’est-ce qui rend la déduction naturelle nécessaire à certaine preuve si elle est un sous-ensemble de la logique classique ?

S’il apparait évident que je me méprend sur quelque chose, ça m’aiderait tout autant qu’on me le signale.

Marchi
-----

[Médiat]

Je viens d’apprendre aujourd’hui, qu’il existe des dérivées de la logique classique, apparemment plutôt des sous-ensembles (des interprétations volontairement restreintes), comme par exemple la déduction naturelle, qui par exemple ne connais pas le tiers-exclus (et à été conçus de cette manière).

Je n'ai pas souvenir que la déduction naturelle impose l'absence de tiers exclu (on peut le mettre ou non dans les règles), du coup, avec ce point de vue, vos autres questions ne sont plus pertinentes.

Ne confondez-vous pas avec l'intuitionnisme ?

La correspondance de Curry-Howard c'est d'ailleurs appliqué d'abord à la logique intuitionniste (moins de règles que la logique classique, donc "normal" de commencer par là), mais aujourd'hui elle s'applique parfaitement à la logique classique.

Sinon, autre formulation assez équivalente : qu’est-ce qui rend l['intuitionnisme] nécessaire à certaine preuve si elle est un sous-ensemble de la logique classique ?

Mauvais point vue, c'est exactement le contraire.

[inviteab8f3a27]

Re-Bonsoir

Je n'ai pas souvenir que la déduction naturelle impose l'absence de tiers exclu

Pourtant, cette règle est bien une tierce partie qu’elle exclus.

(on peut le mettre ou non dans les règles)

C’est ce que j’ai cru lire, oui, mais j’ai aussi cru lire aussi que l’on pouvait y ajouter encore d’autres règles, ce qui ne m’a pas aidé à comprendre de quoi il en retourne, bien au contraire.

Ne confondez-vous pas avec l'intuitionnisme ?

Bonne question. J’ai supposé que les deux était la même chose. Donc si ça n’est pas le cas, je vais me re-pencher sur la question.

La correspondance de Curry-Howard c'est d'ailleurs appliqué d'abord à la logique intuitionniste (moins de règles que la logique classique, donc "normal" de commencer par là), mais aujourd'hui elle s'applique parfaitement à la logique classique.

Confirmation qu’elle inclus moins de règles donc.

Mauvais point vue, c'est exactement le contraire.

Je vais revoir ce qu’est cette logique intuitionniste, parce que semble que je me suis complétement mépris à ce sujet.

Merci pour ces éclaircissements.

[inviteab8f3a27]

Si cela peut aider les autres personnes également intéressées par ce sujet, je viens de découvrir un document d’un enseignant de la CNAM, un certain Franck Wynen, qui me semble prometteur, rien que par sa phrase d’introduction :

Lorsque pour la première fois on entend parler de logique intuitionniste, on découvre que la
logique enseignée dans nos écoles n’est pas la seule existante. [...]

Pour le lire, ici : La logique intuitionniste (format PDF).

(je n’ai pas terminé de lire)

[A voir en vidéo sur Futura]

[pelkin]

Si cela peut aider les autres personnes également intéressées par ce sujet, je viens de découvrir un document d’un enseignant de la CNAM, un certain Franck Wynen, qui me semble prometteur, rien que par sa phrase d’introduction :
[/I]

Qui vous semble prometteur pourquoi ? (je viens de le lire ... et c'est fatigant de voir réinventer la roue)
Parce que la logique formelle vous dérange ?
Personne ne nie la logique des prédicats, ni la linéaire, même pas la logique floue malgré son absence de formalisme.

En bref, quelle est votre question ou ... vous essayez de prouver quoi ?

[inviteab8f3a27]

Qui vous semble prometteur pourquoi ?

Prometteur d’une présentation plus pédagogique (ce sont les termes et la tournure qui me l’ont fait sentir) ; et effectivement, la présentation historique était assez pédagogique.

(je viens de le lire ... et c'est fatigant de voir réinventer la roue)

En même temps, apprendre, c’est un peu ré-inventé, et quand on sait, on doit être capable de ré-inventer. Ce serait alarmant de devoir exclure la ré-invention de la roue et ça empêcherait même d’en faire évoluer le concept. De plus, la logique intuitionniste, d’après le précédent document, n’est pas une ré-invention de la roue, et même au contraire, puisqu’elle prend un contre courant par rapport à la logique classique (elle suppose du la logique découle des mathématique et non l’inverse).

Parce que la logique formelle vous dérange ?

Ce que l’esprit humain peut être fragile alors, et s’effrayer pour si peu ....

Personne ne nie la logique des prédicats, ni la linéaire, même pas la logique floue malgré son absence de formalisme.

Les prédicats et les clauses de Horn sont formalisés (les clauses de Horn portent d’ailleurs le nom de celui qui les a formalisé). La logique floue l’est aussi (elle a d’ailleurs des applications dans les systèmes de contrôles)

En bref, quelle est votre question ou ... vous essayez de prouver quoi ?

La question était dans le titre : quest-ce qui distingue la logique classique et la logique intuitionniste (j’ai confondu naturelle et intuitioniste, je ne savais pas).

vous essayez de prouver quoi ?

Rien.

[Médiat]

quest-ce qui distingue la logique classique et la logique intuitionniste

A question simple et claire, réponse simple et claire (j'espère) : le tiers exclu ne fait pas partie des axiomes de la logique intiutionniste (donc cela exclu le raisonnement pas l'absurde (attention à ne pas trop interpréter cette formulation simple, mais je n'ai pas le temps d'être exhaustif maintenant)).

C'est à dire qu'en logique intuitionniste, on peut prouver , mais pas l'inverse.

Résultat important : tout théorème d'une théorie T en logique intuitionniste est un théorème de logique classique (trivial).
Tout théorème d'une théorie T en logique classique peut se traduire en un théorème de logique intuitionniste (encore un coup du grand Gödel)

[inviteab8f3a27]

A question simple et claire, réponse simple et claire (j'espère) : le tiers exclu ne fait pas partie des axiomes de la logique intiutionniste (donc cela exclu le raisonnement pas l'absurde (attention à ne pas trop interpréter cette formulation simple, mais je n'ai pas le temps d'être exhaustif maintenant)).

C'est à dire qu'en logique intuitionniste, on peut prouver , mais pas l'inverse.

À ce sujet, j’ai vu sur un autre forum (perdu l’adresse, désolé), qu’il y a une similitude entre ce une forme de logique qui est connue en topologie. Quelque chose à voir avec l’intérieur et l’extérieure d’un volume…

Résultat important : tout théorème d'une théorie T en logique intuitionniste est un théorème de logique classique (trivial).
Tout théorème d'une théorie T en logique classique peut se traduire en un théorème de logique intuitionniste (encore un coup du grand Gödel)

D’accord, c’est important ça, cette question qu’il est possible d’exprimer un théorème dans l’une ou l’autre logique. Parce que si je ne me trompe pas, j’ai lu sur Wikipédia que la loi de Peirce ne peut pas être démontrée en déduction naturelle, tandis que la page sur la loi de Peirce (Wikipédia) propose une démonstration en logique intuitionniste de cette loi (juste pour montrer que effectivement, les deux ne doivent pas être confondues comme je l’avais fait).

Je pense qu’il faut aussi conclure de ce message que le théorème de Goëdel s’applique aussi à la logique intuitionniste, et que les deux sont à égalité devant le grand Goëdel (un point sur lequel elle ne serait pas différente).

[Médiat]

D’accord, c’est important ça, cette question qu’il est possible d’exprimer un théorème dans l’une ou l’autre logique.

Attention j'ai bien écrit, dans un sens "est un théorème", et dans l'autre "peut se traduire en un théorème"

[Matmat]

Je pense qu’il faut aussi conclure de ce message que le théorème de Goëdel s’applique aussi à la logique intuitionniste, et que les deux sont à égalité devant le grand Goëdel (un point sur lequel elle ne serait pas différente).

Je crois que vous avez mal compris car :
Médiat parlait de la non-non traduction de Gödel-Kolmogorov qui n'a rien à voir avec les théorèmes de Gödel.
Par ailleurs le théorème d'incomplétude est démontré par l'absurde ... (en dehors du cadre de validité de la logique intuitioniste justement ).

[invite7863222222222]

Par ailleurs le théorème d'incomplétude est démontré par l'absurde ... (en dehors du cadre de validité de la logique intuitioniste justement ).

Grr... non, je m'inscris en faux sur le fait que la démonstration par l'absurde du théorème d'incomplétude s'inscrit en dehors du cadre de la validité de la logique intuitionniste.

Le rejet du tiers exclus de l'intuitionnisme est valable concernant la logique qui quantifient les objets mathématiques courant, les démonstrations étant des choses différentes des objets mathématiques habituels, les raisons d'être intuitionniste n'ont tout simplement pas de sens quand on raisonne sur des démonstrations.

Ce qui serait résumé par le fait, qu'il n'y aucune raison de dire que les théorèmes d'incomplétude qui s'appliquent à la logique classique ne s'appliquent pas aussi à la logique intuitionniste.

[Médiat]

(donc cela exclu le raisonnement pas l'absurde (attention à ne pas trop interpréter cette formulation simple, mais je n'ai pas le temps d'être exhaustif maintenant)).

Je précise ce que je voulais dire :
Lorsque l'on parle de tiers exclu, on parle de deux choses différentes (sous un seul nom ) du point de vue intuitionniste, qui n'en font qu'une du point de vue logique classique (ceci expliquant cela).

En effet du point vue intuitionniste les deux types de raisonnements suivants ne sont pas de même nature :
1) Démontrer non p en (supposant p et en démontrant le faux)
2) Démontrer p en (supposant non p et en démontrant le faux)

La première est valide en logique intuitionniste, pas la deuxième.

[Matmat]

Grr... non, je m'inscris en faux sur le fait que la démonstration par l'absurde du théorème d'incomplétude s'inscrit en dehors du cadre de la validité de la logique intuitionniste.

Le rejet du tiers exclus de l'intuitionnisme est valable concernant la logique qui quantifient les objets mathématiques courant, les démonstrations étant des choses différentes des objets mathématiques habituels, les raisons d'être intuitionniste n'ont tout simplement pas de sens quand on raisonne sur des démonstrations.

A moins que vous ayez voulu parlé des raisons philosophiques de l'intuitionisme je n'ai pas compris votre argument sur "les objets mathématiques habituels" ... Pour moi,et puisque c'est précisement une démonstration métamathématiques nous sommes justement monté d'un niveau de langage où les énoncés mathématiques sont les objets mathématiques, et puis de toute façon une règle d'inférence d'une logique n'inclut pas une sélection préalable d'objets mathématique pour lesquels elle est valide...(a moins d'une raison philosophique ?)

Ce qui serait résumé par le fait, qu'il n'y aucune raison de dire que les théorèmes d'incomplétude qui s'appliquent à la logique classique ne s'appliquent pas aussi à la logique intuitionniste.

Il y a cette raison là : la démonstration du théorème d'incomplétude de Godel n'est pas valide avec les seules règles d'inférences de la logique intuitionniste.

[invite7863222222222]

A moins que vous ayez voulu parlé des raisons philosophiques de l'intuitionisme je n'ai pas compris votre argument sur "les objets mathématiques habituels" ... Pour moi,et puisque c'est précisement une démonstration métamathématiques nous sommes justement monté d'un niveau de langage où les énoncés mathématiques sont les objets mathématiques, et puis de toute façon une règle d'inférence d'une logique n'inclut pas une sélection préalable d'objets mathématique pour lesquels elle est valide...(a moins d'une raison philosophique ?)

Appliquer les règles d'inférences quelque soit ce sur quoi elles portent est aussi justifié par une raison philosophique par ceux qui n'acceptent pas le principe.

Il y a cette raison là : la démonstration du théorème d'incomplétude de Godel n'est pas valide avec les seules règles d'inférences de la logique intuitionniste.

Si car appliquer les règles d'inférence de la logique intuitionniste aux énoncés mathématiques et aux objets mathématiques, ce n'est pas équivalent.

Mais au délà de cela, le message de Médiat, me laisse penser que, de toute façon, le théorème d'incomplétude n'a pas besoin de la règle du tiers exclu (celle qui n'est pas valide en logique intuitionniste) pour être démontré.

[Médiat]

Mais au délà de cela, le message de Médiat, me laisse penser que, de toute façon, le théorème d'incomplétude n'a pas besoin de la règle du tiers exclu (celle qui n'est pas valide en logique intuitionniste) pour être démontré.

Mon message sur la traduction n'est pas tout à fait suffisant pour l'affirmer, mais il est exact que la démonstrtion de Gödel est "constructive" (en tout cas dans mon souvenir), donc valide en logique intuitionniste.

[Matmat]

Mais au délà de cela, le message de Médiat, me laisse penser que, de toute façon, le théorème d'incomplétude n'a pas besoin de la règle du tiers exclu (celle qui n'est pas valide en logique intuitionniste) pour être démontré.

Mais si, regardez la fin, pour conclure à la vérité de l'expression "L'expression de nombre de Godel N n'est pas démontrable", il suppose qu'elle est fausse d'où il déduit qu'elle est démontrable , or c'est en contradiction avec le fait que le système soit consistant (fausse et démontrable) et "donc" (mais pour ce donc il faut appliquer le tiers exclus) elle est vraie .

Bref il dit que l'expression est vraie avec comme seul argument que sa négation engendre une contradiction, on est dans le cas 2 de Médiat.

[invite7863222222222]

Mais si, regardez la fin, pour démontrer l'expression "L'expression de nombre de Godel N n'est pas démontrable", il suppose qu'elle est fausse d'où il déduit qu'elle est démontrable , or c'est en contradiction avec le fait que le système soit consistant (fausse et démontrable) et "donc" (mais pour ce donc il faut appliquer le tiers exclus) elle est vraie .

Bref il dit que l'expression est vraie avec comme seul argument que sa négation engendre une contradiction, on est dans le cas 2 de Médiat.

Attention, la logique intuitionniste ne refuse pas tout le temps la règle du tiers exclus, elle l'accepte dans certains cas, quand elle est démontrée pour certains types d'objets.

Autrement dit, l'intuitionnisme ne dit pas que la règle du tiers exclus n'est jamais valable, il dit simplement qu'on ne peut pas la considérer comme toujours valable.

[invite7863222222222]

Mais si, regardez la fin, pour conclure à la vérité de l'expression "L'expression de nombre de Godel N n'est pas démontrable", il suppose qu'elle est fausse d'où il déduit qu'elle est démontrable , or c'est en contradiction avec le fait que le système soit consistant (fausse et démontrable) et "donc" (mais pour ce donc il faut appliquer le tiers exclus) elle est vraie .

On peut le faire de façon constructiviste (cas 1 de Médiat) : "supposons que L'expression de nombre de Godel N est démontrable" est vraie alors on en déduirait qu'elle est indémontrable ce qui est absurde donc "L'expression de nombre de Godel N est démontrable" est fausse c'est à dire L'expression de nombre de Godel N n'est pas démontrable.

[Matmat]

... est vraie alors on en déduirait qu'elle est indémontrable ce qui est absurde ...

C'est pas absurde c'est l'incomplétude , c'est justement cela l'incomplétude !

[invite7863222222222]

C'est pas absurde c'est l'incomplétude , c'est justement cela l'incomplétude !

Non c'est contraire à l'hypothèse de départ, donc on arrive à une absurdité.


De tous les cas, j'avoue ne pas très bien comprendre où vous voulez en venir : la logique intuitionniste se justifie et s'applique d'abord pour les nombres, les ensembles. A vrai dire, pour les démonstrations, on en a un peu rien à faire du tiers exclus et de la logique intuitionniste.

[invite7863222222222]

De tous les cas, j'avoue ne pas très bien comprendre où vous voulez en venir : la logique intuitionniste se justifie et s'applique d'abord pour les nombres, les ensembles. A vrai dire, pour les démonstrations, on en a un peu rien à faire du tiers exclus et de la logique intuitionniste

et de la logique classique.

[Matmat]

Non c'est contraire à l'hypothèse de départ, donc on arrive à une absurdité.


De tous les cas, j'avoue ne pas très bien comprendre où vous voulez en venir : la logique intuitionniste se justifie et s'applique d'abord pour les nombres, les ensembles. A vrai dire, pour les démonstrations, on en a un peu rien à faire du tiers exclus et de la logique intuitionniste.

C'est pas contraire à l'hypothèse de départ , c'est même ce qu'on veut conclure : on cherche un énoncé vrai et indémontrable et on le trouve ! Ce n'est vraiment pas le moment de dire que c'est absurde !

Je ne voulais pas en venir quelquepart, je clarifiais un point confus pour hibou et la discussion a deviée

[invite7863222222222]

C'est pas contraire à l'hypothèse de départ , c'est même ce qu'on veut conclure : on cherche un énoncé vrai et indémontrable et on le trouve ! Ce n'est vraiment pas le moment de dire que c'est absurde !

Ha d'accord, c'est pas absurde, c'est contradictoire avec l'hypothèse de départ, donc l'hypothèse de départ est fausse et on arrive au même résultat.

Bref, je continue à dire que l'intuitionnisme appliqué aux raisonnements, je ne vois toujours pas ce que ca veut dire.

[inviteab8f3a27]

Je crois que vous avez mal compris car :
Médiat parlait de la non-non traduction de Gödel-Kolmogorov qui n'a rien à voir avec les théorèmes de Gödel.
Par ailleurs le théorème d'incomplétude est démontré par l'absurde ... (en dehors du cadre de validité de la logique intuitioniste justement ).

Je ne vais même pas penser à me pencher sur les preuves apportées par Gödel à sa démonstration qui n’est pour moi qu’un théorème en lequel j’ai confiance ; cependant, merci pour le «*non-non traduction de Gödel-Kolmogorov *», parce que ce truc amène des choses intéressantes quand on le tappe dans Google. De la lecture en vue (pas pour maintenant).

[inviteab8f3a27]

[...]

Le rejet du tiers exclus de l'intuitionnisme est valable concernant la logique qui quantifient les objets mathématiques courant, les démonstrations étant des choses différentes des objets mathématiques habituels, les raisons d'être intuitionniste n'ont tout simplement pas de sens quand on raisonne sur des démonstrations.

[...]

Oops, il va falloir éclaircir, parce que je me noie. Ou alors il y a démonstrations et démonstrations ?

[inviteab8f3a27]

Je précise ce que je voulais dire :
Lorsque l'on parle de tiers exclu, on parle de deux choses différentes (sous un seul nom ) du point de vue intuitionniste, qui n'en font qu'une du point de vue logique classique (ceci expliquant cela).

En effet du point vue intuitionniste les deux types de raisonnements suivants ne sont pas de même nature :
1) Démontrer non p en (supposant p et en démontrant le faux)
2) Démontrer p en (supposant non p et en démontrant le faux)

La première est valide en logique intuitionniste, pas la deuxième.

Oui, voilà, c’est d’aboutir à «*quelque chose*» qui n’est finalement que «*pas grand chose*» ou même concrêtement rien, car on est parti d’une hypothèse fausse (je donne quelque chose à ce propos dans un message plus tard, pour les autres non-spécialistes, comme moi, qui liraient ce sujet).

Vrai que de partir d’une hypothèse fausse, ça n’est ni-intuitif, ni-constructif aux sens logique comme aux sens courants de ces termes.

[inviteab8f3a27]

A moins que vous ayez voulu parlé des raisons philosophiques de l'intuitionisme je n'ai pas compris votre argument sur "les objets mathématiques habituels" ... Pour moi,et puisque c'est précisement une démonstration métamathématiques nous sommes justement monté d'un niveau de langage où les énoncés mathématiques sont les objets mathématiques, et puis de toute façon une règle d'inférence d'une logique n'inclut pas une sélection préalable d'objets mathématique pour lesquels elle est valide...

Sous réserve que j’ai bien compris (je ne suis pas matheux), il me semble que même à ce niveau de langage, il existe une différence : par exemple un énnoncé peut tout à fait caché un infini quelque part, qui n’apparait pas explicitement (ça arrive, si je ne me trompe pas), mais l’infini, n’est pas un objet mathématique pour la logique intuitionniste (en tous cas, elle rejète l’appel à l’infini tout autant que l’appel au tiers-exclus).

(a moins d'une raison philosophique ?)

Je ne sais pas si «*philosophique*» est ici connoté, mais en tous les cas, même la logique classique dépend elle-même d’une philosophique (qu’elle soit la seule courament admise, n’enlève rien à son origine philosophique).

[inviteab8f3a27]

Attention, la logique intuitionniste ne refuse pas tout le temps la règle du tiers exclus, elle l'accepte dans certains cas, quand elle est démontrée pour certains types d'objets.

Elle l’accepte ou on peut lui ajouter ? (c’est différent)

Autrement dit, l'intuitionnisme ne dit pas que la règle du tiers exclus n'est jamais valable, il dit simplement qu'on ne peut pas la considérer comme toujours valable.

Soit. Sous quelles conditions ?

[inviteab8f3a27]

[...]

Je ne voulais pas en venir quelquepart, je clarifiais un point confus pour hibou et la discussion a deviée

Non, non, pas du tout déviée, on est même les deux pieds dedans continuez, ça m’intéresse beaucoup.

[invite7863222222222]

Elle l’accepte ou on peut lui ajouter ? (c’est différent)

C'est plutôt qu'on peut démontrer.

Soit. Sous quelles conditions ?

Je ne me suis jamais vraiment posé la question plus que cela, mais par exemple, quand on quantifie sur un ensemble fini de valeur, il me semble qu'on peut toujours savoir si une propriété A(x) est démontrable pour tout x d'un ensemble fini, simplement faisant parcourir à x toutes les valeurs possibles puisqu'il y en a un nombre fini.