Comment la logique classique inclut-elle l'intuitionniste ?

[Exaptator]

.

En bleu la logique classique, en rouge la logique intuitionniste :


Avec "P(A)" qui signifie : "il est prouvé que A" ou plus simplement : "A est vraie" ou encore : "A : vraie"
Et A et ¬A : des propositions quelconques pouvant chacune être vraie ou fausse, mais pas l'une et l'autre vraies ou fausses en même temps.

(A et ¬A) : nécessairement faux __ Principe de non contradiction
(A ou ¬A) : nécessairement vrai __ Principe du tiers exclu


On a :

• P(A) <=> A ____________ => A : vraie
• P(¬A) <=> ¬A __________ => A : fausse
• ¬P(A) <=> ??? __________ => A : indéterminée 1
• ¬P(¬A) <=> ¬¬A ________ => A : indéterminée 2

On note que :

¬P(A) <≠> ¬P(¬A)

>>>>>>>>>>>>>>>> Démonstration par l'absurde

Afficher

Si on avait : ¬P(A) <=> ¬P(¬A), alors on aurait :

¬(¬¬A) <=> P(¬(¬P(¬A))) => P(P(¬A)) => P(¬A) => ¬ A

et :

¬(¬¬A) <=> P(¬(¬P(A))) => P(P(A)) => P(A) => A

Or c'est contradictoire.

Donc :

¬P(A) <≠> ¬P(¬A)

On retient donc :

• A <=> P(A)
• ¬A <=> P(¬A)
• ¬(¬A) <=> P(¬P(¬A)) <=> ¬P(¬A)

On retrouve bien 2 théorèmes de base de la Li :

• A <≠> ¬¬A

(étant donné que P(A) n'est pas davantage équivalent à ¬P(¬A) qu'à ¬P(A).)

et

• ¬A <=> ¬¬¬A

>>>>>>>>>>>>>>>> Preuve

Afficher

¬(¬¬A) <=> P(¬(¬P(¬A))) <=> P(P(¬A)) <=> P(¬A) <=> ¬A

Remarque 1 :

A <≠> ¬¬A
En revanche : A => ¬¬A



Remarque 2 :

Le fait que A <≠> ¬¬A, mais que ¬¬¬A <=> ¬A est tout à fait intéressant, car l'on peut en inférer ceci :
A, ¬A et ¬¬A

Tels que :
A <≠> ¬A <≠> ¬¬A <≠> A

Et que mis à part ces trois cas l'on a toujours des configurations comme :
¬A <=> (¬¬) ¬A
¬¬A <=> (¬¬) ¬¬A
(¬¬) ¬A <=> (¬¬) (¬¬) ¬A

Etc.

Ce qui revient à dire qu'en Li, on peut toujours supprimer un "¬¬" devant un ¬A ou un ¬¬A.

.

[Denis]

Salut Exaptator,

Penses-tu que nous devrions ajouter "la logique formelle" à la liste des thèmes canoniques du forum ?

Denis

[Dash]

Salut Denis,

C'est la meilleure question qui lui a été posée jusqu'ici!

[Exaptator]

Salut Exaptator,

Penses-tu que nous devrions ajouter "la logique formelle" à la liste des thèmes canoniques du forum ?

Denis

Vu le fait qu'elle suscite autant de débats contradictoires et de méprises, oui, surtout sur un forum comme celui-ci où il est question d'esprit critique. Car je vois mal comment un tel esprit pourrait se développer et être pertinent sans logique. Or, c'est un fait : la logique n'est pas naturelle à l'homme, la longue liste des biais cognitifs en témoigne. L'outil de la logique FORMELLE est donc indispensable et de nombreuses mises au point à ce sujet me semble plus que nécessaires, sans quoi il est vain d'espérer pouvoir développer un discours rationnel quelque soit le sujet abordé.

.

[Dash]

... la logique n'est pas naturelle à l'homme, la longue liste des biais cognitifs en témoigne.

Non.

L'on pourrait tout aussi bien dire que les biais (et/ou les émotions/affects) ne sont pas naturels, la logique/raison/science en témoigne.
Les biais sont justement des process qui bypassent la logique sous certaines conditions/circonstances. Mais les biais et la logique sont tout aussi « naturel(le)s/non naturel(le)s » l'un que l'autre.

D'ailleurs (mais c'est un autre sujet), dans l'absolu, il n'existe rien qui ne soit pas naturel! ...à moins de croire au surnaturel.

[Nicolas78]

Je pense que Exaptator voulais juste dire qu'il vaut mieux être logique si on veut prétendre à un discours rationnel.
Ce qui me semble évident...personne ne le contredira la dessus. Sur le fond.

Ceci-dit, j'ai l'impression qu'il pense que seule la logique suffit...et/ou que celle-ci serait une vertus un peut spéciale.
Les arguments arbitraires qui propose le laisse croire en tout cas.

[Exaptator]

Bon, alors ? Aucune remarque sur ce que j'ai énoncé dans mon post introductif ? Tout est OK ?

[Cogite Stibon]

tel que formulé, ça n'a aucun sens.

[Exaptator]

tel que formulé, ça n'a aucun sens.

Euh... j'entendais une remarque ou une critique argumentées.... Ta remarque n'a donc pas plus de valeur que de la merde, celle-ci pouvant au moins servir d'engrais.

Merci d'appliquer des règles de politesses plus compatibles avec une discussion .... la logique ne doit pas être la seule à adopter un certain formalisme

Une remarque gratuite comme celle-ci ne présente donc aucune sorte d'intérêt.

.

[Cogite Stibon]

Bisous aussi

[Exaptator]

Bisous aussi

Donc tu n'as rien à redire d'intéressant ?

Sinon, c'est donc que tu n'as rien de pertinant à opposer à ce que j'ai mis plus haut.

Ça me va.
.

[Cogite Stibon]

[Exaptator]

Bon je vais faire des courses....

[Cogite Stibon]

Prends ton temps.

[Exaptator]

Non mais sérieux, t'es pas cap de fournir une critique intelligente de ce que j'ai écrit en post introductif ?

[Cogite Stibon]

Vu les efforts que tu as fais jusqu'à présent pour répondre à mes question, la quantité de non sens dans ton post introductif, et ton attitude odieuse sur ce forum, je n'ai pas envie de le faire.

[Exaptator]

Vu les efforts que tu as fais jusqu'à présent pour répondre à mes question, la quantité de non sens dans ton post introductif, et ton attitude odieuse sur ce forum, je n'ai pas envie de le faire.

C'est ce qu'on dit quand on à rien à dire d'intelligent.

Parle moi plutôt d'un de ces non-sens selon toi qu'on examine un peu cela.

Quant à l'ad hominem ça aussi ça ne vaut rien niveau argumentatif.
.

[Exaptator]

Merci d'appliquer des règles de politesses plus compatibles avec une discussion .... la logique ne doit pas être la seule à adopter un certain formalisme

Qui qui dit ça ?

Je suis poli et courtois avec les gens polis, courtois et ou qui ne se comportent pas comme des trolls.

Cela dit, je ne vois pas ce que j'aurais dit d'impoli plus haut. Je le répète : j'adapte le ton qui est le mien à celui de mes interlocuteurs.

Est-ce le mot "merde" ?

.

[Lulu Cypher]

Je suis poli et courtois avec les gens polis, courtois et ou qui ne se comportent pas comme des trolls.

C'est une remarque de cour d'école, si tu penses être courtois alors à chaque post essaye de l'être encore plus

Cela dit, je ne vois pas ce que j'aurais dit d'impoli plus haut.

Relis-toi

PS : ceci n'est pas un débat

[nikola]

À part ça, on m’a toujours dit que la logique intuitionniste contenait la logique classique pour une raison simple : les axiomes de la logique classique contiennent ceux de la logique intuitionniste en entier plus d’autres.

[Exaptator]

Certains diront que c'est abscons et con et que cela ne cache qu'une vacuité des propos...

[Exaptator]

.
[ EDIT : reprise avec petites corrections dans la formulation. ]


En bleu la logique classique, en rouge la logique intuitionniste :


Avec "P(A)" qui signifie : "il est prouvé que A" ou plus exactement : "A est démontrée dans le système formel" ou encore, plus simplement cette fois : "A : vraie"
Et A et ¬A : des propositions quelconques pouvant chacune être contradictoire ou non, mais pas l'une et l'autre contradictoire ou non contradictoire en même temps.

(A et ¬A) => ⊥ : contradictoire __ PRINCIPE DE NON CONTRADICTION
(A ou ¬A) => ⊤ : tautologique ___ Principe du tiers exclu


On a :

• P(A) <=> A ____________ => A : démontrée dans le système formel
• P(¬A) <=> ¬A __________ => A : démontrée contradictoire
• ¬P(A) <=> ??? __________ => A : indéterminée 1
• ¬P(¬A) <=> ¬¬A ________ => A : indéterminée 2

(⊤ : toujours vraie)
(¬⊤ : pas toujours vraie)



On note que :

(P(A) => ¬P(¬A)) => ⊤


Mais que :

(¬P(¬A) => P(A)) => ¬⊤


Et que :

(¬P(A) <=> ¬P(¬A)) => ¬⊤

>>>>>>>>>>>>>>>> Démonstration par l'absurde

Afficher

Si on avait : ¬P(A) <=> ¬P(¬A), alors on aurait :

¬(¬¬A) <=> P(¬(¬P(¬A))) => P(P(¬A)) => P(¬A) => ¬ A

et :

¬(¬¬A) <=> P(¬(¬P(A))) => P(P(A)) => P(A) => A

Or c'est contradictoire.


Donc :

(¬P(A) <=> ¬P(¬A)) => ¬⊤

On retient donc :

• A <=> P(A)
• ¬A <=> P(¬A)
• ¬(¬A) <=> P(¬P(¬A)) <=> ¬P(¬A)

Et qu'on retrouve bien 2 théorèmes de base de la Li :

• A => ¬¬A, sachant que : (A <=> ¬¬A) => ¬⊤

et

• ¬A <=> ¬¬¬A

>>>>>>>>>>>>>>>> Preuve

Afficher

¬(¬¬A) <=> P(¬(¬P(¬A))) <=> P(P(¬A)) <=> P(¬A) <=> ¬A

Remarque :

Le fait que (A <=> ¬¬A) => ¬⊤, mais que ¬¬¬A <=> ¬A est tout à fait intéressant, car l'on peut en inférer ceci :
A, ¬A et ¬¬A

Tels que :
(A <=> ¬A) => ¬⊤, (¬A <=> ¬¬A) => ¬⊤ et (¬¬A <=> A) => ¬⊤

Et que mis à part ces trois cas l'on a toujours des configurations comme :
¬A <=> (¬¬) ¬A
¬¬A <=> (¬¬) ¬¬A
(¬¬) ¬A <=> (¬¬) (¬¬) ¬A

Etc.

Ce qui revient à dire qu'en Li, on peut toujours supprimer un "¬¬" devant un ¬A ou un ¬¬A.



.

[Exaptator]

.

En fait, en français ça donne :

• A
  P(A)
  • A prouvée non contradictoire (1).

• ¬A
  P(¬A)
  • A prouvée contradictoire (1).

• ¬¬A
  ¬P(¬A)
  • "A prouvée contradictoire" (1), non prouvée.

• ¬¬¬A
  ¬(¬P(¬A))
  • A prouvée contradictoire (1).
  ¬A
  P(¬A)

____


P(A) <=> A

P(¬A) <=> ¬A

¬P(A) <=> ?

¬P(¬A) <=> ¬¬A



-----------> Soit : ¬P(A) : une expression en Lc qui n'a pas d'équivalent en Li.



C'est-à-dire :

• ¬P(A)
  • "A prouvée non contradictoire" (1), non prouvée.

_____


Note :

(1) : ".... à partir du système formel"



.

[Exaptator]

.
Bon... Il semblerait que ça marche pas mon truc...

Faut dire que je ne maîtrise pas des masses la Li....

Je me suis rendu compte tout seul comme un grand que ce que l'on prouve en Lc n'est pas toujours valide comme preuve en Li...

C'est dingue que je suis passé à coté d'un truc aussi énorme, alors que c'est pourtant, - bien évidemment ! -, ce qui fait toute la différence entre la Lc et la Li, et aussi l'intérêt de l'une et de l'autre, de l'une par rapport à l'autre.

Je ne le comprenais simplement pas.


En fait le truc c'est que contrairement à ce que j'ai écrit précédemment dans ce fil, on a pas :

P(A) <=> A
P(¬A) <=> ¬A
¬P(A) <=> ?
¬P(¬A) <=> ¬¬A

Mais en modifiant un peu la définition de la fonction P comme suit :

• P : "Il est prouvable ou il est prouvé en Lc" *

on a bien ceci :

• A ⇒ P(A)

• ¬A ⇒ P(¬A)

• ¬¬A ⇒ ¬P(¬A)

Rien dans la Li n'impliquant ¬P(A).


____

* note : il faudrait que je change de lettre car dans l'autre fil je définis cette fonction encore autrement.....


.

[Exaptator]

Ancien article Wiki (?) :

L'intuitionnisme est une position philosophique vis-à-vis des mathématiques proposée par le mathématicien hollandais Luitzen Egbertus Jan Brouwer comme une alternative à l'approche dite classique. Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko et Arend Heyting. Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste et ceci bien que l'ensemble des formules valides de la logique intuitionniste soit strictement inclus dans l'ensemble des formules valides de la logique classique. Gerhard Gentzen en a formulé les règles de déduction dans le cadre de la déduction naturelle.

Les travaux récents, notamment la correspondance de Curry-Howard, lui ont donné un statut central dans la logique et dans l'informatique, en faisant d'elle historiquement la première des logiques constructives. Des travaux la concernant, effectués par Gödel et Andreï Kolmogorov au sujet de la « Non-non interprétation » (interprétation de la double négation) ont ouvert la porte de l’interprétation de la logique classique dans les termes de la logique intuitionniste. L'étude de la logique intuitionniste est la clé pour bien comprendre la logique classique et ses subtilités.


Article Wikipédia :

L'intuitionnisme est une philosophie des mathématiques que L. E. J. Brouwer a élaborée au début du xxe siècle. Pour Brouwer, les mathématiques sont une libre création de l'esprit humain et tous les objets qu'elles manipulent doivent être accessibles à l'intuition. L'intuitionnisme a pour conséquence une profonde remise en cause des mathématiques, notamment en refusant l'infini actuel : un nombre réel ne peut être représenté comme une suite infinie de décimales qu'à la condition de disposer d'un moyen effectif de calculer chacune de ces décimales ; on parle alors de réel constructif.

Sur le plan logique l'intuitionnisme n'accepte pas le raisonnement par l'absurde ou le tiers exclu pour la raison que ces principes permettent de démontrer des propriétés de façon non constructive : par exemple si on veut démontrer l'existence d'un nombre réel satisfaisant une certaine propriété, on peut raisonner par l'absurde, supposer qu'un tel réel n'existe pas, en déduire une contradiction et conclure que donc un tel réel existe, mais cette démonstration ne donne aucune indication sur la façon dont on pourrait calculer ce réel. Pour un intuitionniste on a juste démontré que l'existence d'un tel réel n'est pas contradictoire, mais pas que ce réel existe.

La logique intuitionniste a été développée par V. Glivenko1 et Arend Heyting, Kurt Gödel2 et Andreï Kolmogorov3 et formalise les principes logiques sur lesquels s'appuie l'intuitionnisme.

L'intuitionnisme est souvent considéré comme une forme de constructivisme, avec lequel il a beaucoup en commun, mais il s'en écarte quand, comme c'est le cas pour l'intuitionnisme originel de Brouwer, il conduit à des énoncés mathématiques valides qui ne le sont pas classiquement. La logique intuitionniste ne permet, elle, de démontrer que des énoncés valides en logique classique.
.