L'implication

Tu devrais te renseigner sur la règle du modus ponens, qui est à la base de toutes les maths. Si $A$ et $B$ sont des formules (et "$x=2$" est bien une formule, on s'autorise des formules non fermées, c'est-à-dire contenant des variables libres) alors si on dispose de $A \Rightarrow B$ et de $A$ alors on peut en déduire $B$ dans une démonstration formelle.

Tu sembles confondre beaucoup de choses.

Supposition : $a=2$

Déductions enchainées:

$a\times a = a\times 2$

puis $a\times 2 = 2\times 2$

donc $a\times a=2\times 2$

Je te laisse compléter, trouver les axiomes invoqués implicitement.

Je te rappelle la définition de $a=b$. C'est "tout ce qui arrive à $a$, arrive aussi à $b$.

De $a=2$, et du fait que $a$ peut dire sans mentir $a\times a = a\times moi $
tu as donc que $2$ peut aussi le dire sans mentir, ce qui donne $a\times a = a\times 2 $

etc, etc

Je ne t'ai pas mis tous les détails, car je pense que ton souci était l'ignorance de la règle linguistique suivante:

on peut commencer par "supposons X"

écrire "donc blablabla..., donc Y"

Puis récapituler en disant "msieurs-dames, je viens de vous prouver SANS SUPPOSER X que :

Non pas du tout.

est une phrase. Comme tu demandais une preuve de cette phrase dans l'environnement courant, je t'ai juste signalé que tu peux commencer par:

Autrement dit, rédiger comme suit:

"supposons $x=2$ blabla, plein de modus ponens, blabla,
donc $x^2=4$"

Quand tu mettras les quantificateurs tu n'auras plus de problème.

La tu appelles implication des énoncés qui commencent par "forall", normal que tu ressentes des demangeaisons.

La notion d'implication matérielle est bidon. C'est une sorte de concept philosopheux de la période pré scientifique. Elle se veut reliée aux notions de causes à effets temporelles, tout aussi vagues.

Si tu veux une aide pense à mettre une modalité. Par exemple "il est obligatoire que" devant ton implication. (Ou encore il est prouvable que)

Tu obtiendras un truc plus proche.

olaola7et10 a écrit:

Il y a d'autre implications comme l'implication stricte qui tentent de régler ce problème d'absence de causalité.

Non.

Soit $T$ un ensemble d'énoncés tels que, quels que soient les énoncés $x,y$
1°) tous les énoncés de la forme $((\neg y) \Rightarrow (\neg x)) \Rightarrow (x \Rightarrow y)$ appartiennent à $T$.
2°) tous les énoncés de la forme $x \Rightarrow (y \Rightarrow x)$
3°) si $x$ et $x \Rightarrow y$ appartiennent à $T$ alors $y$ aussi.

Alors si $a$ est un énoncé quelconque tel que $\neg a\in T$, $a \Rightarrow b \in T$ pour n'importe quel $b$. En effet:

(i) $(\neg a ) \Rightarrow ((\neg b) \Rightarrow (\neg a)) \in T$ d'après 2°
(ii) $\neg a\in T$ par hypothèse.
(iii) $(\neg b) \Rightarrow (\neg a)\in T$ d'après 3° appliqué à (ii) et (i)
(iv)$((\neg b) \Rightarrow (\neg a)) \Rightarrow (a \Rightarrow b)\in T$ d'après 1°
(v) $a \Rightarrow b \in T$ d'après 3°) appliqué à (iii) et (iv).

Pour être en désaccord avec ça, il faut rejeter 1°, 2° ou 3° ci-dessus. Préciser lequel.

NB: si on ajoute à la liste de ces axiomes ci-dessus l'axiome
4°: "pour tous énoncés $x,y,z$", $(x \Rightarrow (y \Rightarrow z)) \Rightarrow ((x \Rightarrow y) \Rightarrow (x \Rightarrow z))\in T$
alors toutes les tautologies de la logique classique propositionnelle sont dans $T$.

Ca provient aussi de ce qu'on insiste pour prendre l'implication comme connecteur de base. Si on définit $a\Rightarrow b$ par $(\neg a) \vee b$ ou $\neg (a \wedge (\neg b))$ il n'y a plus ces problèmes.

Foys a écrit:

olaola7et10 a écrit:

Il y a d'autre implications comme l'implication stricte qui tentent de régler ce problème d'absence de causalité.

Non.

J'ai été précis : j'ai bien écrit "qui tentent", pas "qui réussissent" (car effectivement cela n'est qu'une tentative qui ne règle pas le problème).
Cordialement.

C'est vrai en logique mathématique, mais c'est faux dans le langage courant où l'implication a un lien de causalité.

Et l'implication matérielle (celle de la logique mathématique) est issue de l'implication du langage courant.

Comme a peu près tout en mathématiques, on part de l'aspect intuitif et courant, puis on généralise et formalise et on finit parfois par se détacher du sens initial.

Par contre faut pas confondre, c'est l'implication matérielle qui est une extension abusive de l'implication du langage courant, pas l'inverse.

Cordialement.

Allez, je m’ennuie cette après-midi, alors j’ajoute mon grain de sel à cet éternel marronnier (combien de fils là-dessus as-t-on déjà vu passer?), et peut-être (j’espère) faire un peu avancer la discussion.

J’aime bien l’interprétation « théorie des types » de l’implication (experts logiciens, si vous voyez que j’utilise de mauvais termes, ou que je dis des sottises, je serai ravi d’apprendre vos corrections, j’appelle ça de la « théorie des types » car j’ai pris conscience de cette interprétation en jouant avec des assistants de preuve fondés sur la théorie des types).

Si je comprends bien ce paradigme, une proposition est « identifiée » à l’ensemble de ses preuves (plutôt, c’est un type). La proposition $A \Rightarrow B$ est l’ensemble des fonctions de $A$ dans $B$.

Autrement dit une preuve de $A \Rightarrow B$, c’est une preuve qu’étant donné un élément de $A$ c’est-à-dire une preuve de (la proposition représentée par) $A$, je peux fournir un élément de $B$, c’est-à-dire une preuve de (la proposition représentée) par $B$.

Dit comme ça, ça semble quand même assez proche du sens « courant » de l’implication : à partir de $A$, je ponds $B$. Ca se conçoit même comme un jeu, mon adversaire me donne un élément de $A$ et il ne me lâche pas la grappe tant que je ne lui donne pas un élément de $B$.

Du coup, le « fameux » $A \Rightarrow (B \Rightarrow A)$ ne semble plus si déconnant (il ne l'a jamais été, mais je pense comme Christophe que pour certaines personne il n'est pas si clair): mon adversaire me donne $a \in A$, il attend en retour une preuve que s’il me donne un élément $b \in B$, je peux lui donner un élément de $A$. Ce à quoi je lui réponds juste que s'il me donne un $b \in B$, je peux toujours lui rendre le $a$ qu’il vient de me donner. J’ai donc prouvé $A \Rightarrow (B \Rightarrow A)$.

Dit autrement, étant donné un élément d’un ensemble, je peux toujours parler de la fonction constante égale à cet élément, partant de n’importe quel ensemble.


Ce qui doit gêner tant de gens avec cela, c’est que je n’ai pas « utilisé » le $b$ que mon adversaire me donnerait, une « utilisation » de ce $b$ formaliserait peut-être une forme de « causalité ».

Du coup, question à nos experts logiciens: j’ai déjà entendu parler (mais sans jamais avoir vu les détails) de « logique linéaire », où il y a une notion de « ressources utilisables » dans les preuves. Est-ce que dans ce cadre, on peut formaliser l’idée que je n’ai pas utilisé le $b$ de mon adversaire dans le $a$ que je lui ai rendu? J’intuite que, vu le message de Foys, ce que je fais reste valable en logique linéaire (j’ai le droit de ne pas utiliser une ressource, mais je n’ai pas le droit de « trop » l’utiliser). Cette intuition est-elle correcte ?

PS. Christophe, j'ai cru comprendre que tu as une sainte horreur des types et du typage, mais ne tape pas trop fort sur moi s'il te plaît.

Dreamer écrivait : http://www.les-mathematiques.net/phorum/read.php?16,2091694,2257270#msg-2257270
[Inutile de recopier un message présent sur le forum. Un lien suffit. AD]
À toutes fins utiles l'implication en logique classique est appelée "l'implication matérielle", et dans ce fil on cherche à expliquer et pas à construire une nouvelle théorie mathématique, et enfin à toutes fin utiles la très grande majorité disons 90% des gens qui font des maths n'ont pas de formation en logique et raisonnent avec l'implication du langage courant ce qui permet de faire la très grande majorité des maths rigoureusement.

Salut Christophe,

J'ai compris le warning que tu mets quand à l'utilisation de "trucs classiques" comme le choix, le tiers exclu (sacrément moins fort que choix) etc dans la "construction" des objets.

Du coup, pour voir si j'ai compris ce que tu dis à la fin de ton post concernant les logiques linéaires, affines et intuitionnistes, la construction (que j'ai donné dans mon post précédent), pour tout $A, B$ d'un $\Phi(A, \in (A \to (B \to A))$ (et donc la preuve de $A \to (B \to A)$) est valable en logique affine, mais pas en logique linéaire (puisque j'ai donné $a \mapsto (b \mapsto a)$, qui n'est pas linéaire.).

Mais $(A \to (B \to A))$ est aussi non vide (on dit aussi "habité" dans ce genre de contextes, non?) en logique affine linéaire, puisque je peux toujours construire $a \mapsto (b \mapsto 0)$, n'est-ce pas?

Tu n'as pas commenté le slogan de la logique linéaire que j'ai évoqué, qui évoque la possibilité d'avoir des "ressources en nombres limités" (ou quelque chose comme ça) dans une preuve. Comment le fait de raisonner en terme de "fonctions linéaires" permet-il de formaliser cette idée?

D'ailleurs, tu parles de fonctions linéaires, est-ce-à-dire qu'il y a un corps/anneau de base caché derrière, et que je n'obtiens pas la même "logique" si je prends des fonctions $\mathbb{Z}/2\mathbb{Z}$-linéaires, ou $\mathbb{Q}(\sqrt{29})$-linéaire?

Ou bien au contraire, ce qu'on appelle "logique linéaire" va plutôt désigner (la logique régissant) les formules vraies dans tout ces "modèles" (j'imagine alors que le "modèle universel" sera les groupes abéliens, et qu'on prendra des fonctions $\mathbb{Z}$-linéaires), je mets des guillemets à modèles car je sais que ça a un sens précis en logique, alors que je parle là de la notion intuitive. Cela ressemble plus à ce que tu dis quand tu mentionnes le fait de donner des constructions uniformes, indépendantes des lettres, mais j’extrapole peut-être trop.

PS: Je me souviens d'un fil ou tu expliquais des trucs d'algèbre linéaire à quelqu'un en utilisant du langage logique (la personne avait un peu du mal à suivre, malheureusement), par exemple, tu disais (je crois, pardonne moi si c'est faux) que le dual d'un espace vectoriel V pouvait se penser comme $\neg V$, (j'imagine que le corps de base $k$ est alors "le faux", ou $\bot$, et que $\mathcal{L}(V, k)$, est alors $V \to \bot$, c'est-à-dire $\neg V$), j'imagine qu'on est en plein dans le paradigme de la logique linéaire que tu décris?

Edits: des boulettes aux pires endroits.

Olaola7et10, si tu restes au niveau de l'explication valable à 90%, libre à toi de croire que tu fais des mathématiques.

Bonne continuation.

olaola7et10 a écrit:

et enfin à toutes fin utiles la très grande majorité disons 90% des gens qui font des maths n'ont pas de formation en logique et raisonnent avec l'implication du langage courant ce qui permet de faire la très grande majorité des maths rigoureusement.

:-D
Non!

La majorité des mathématiciens utilisent l'implication des logiciens et n'ont pas ce problème. Tu ne devrais pas parler de ce que tu ne connais pas.

Bonjour

Foys a écrit:

La majorité des mathématiciens utilisent l'implication des logiciens et n'ont pas ce problème. Tu ne devrais pas parler de ce que tu ne connais pas.

Euh.... non je ne crois pas non.

Demande à un mathématicien lambda sans formation logique de démontrer/justifier que 2>3 => pi=12 et tu verras sa réponse.

Jean-Louis montre s'il le fallait que tu te trompes lourdement.

Je pense que c'est toi qui ne connais pas grand chose, il vaut mieux éviter d'intervenir dans ce cas.

Bonne journée.


Edit : On voit même certains pseudo-logiciens qui vont jusqu'à utiliser Faux => P (croyant que c'est vraiment établi ! et que c'est pas juste un axiome abusif) dans la vie courante sans se rendre compte que c'est ridicule.

Bonjour,

Je ne suis pas très compétent en logique, mais entre croire Foys ou CC dans ce domaine ou croire un inconnu vindicatif, mon choix est tout fait, mon axiome personnel est de croire Foys ou CC qui ont fait leurs preuves;

Cordialement,

Rescassol

Bonjour,

Ben, c'est comme toi, tu débarques avec tes gros sabots et tu balances des affirmations d'autorité sur un ton déplaisant. Tu n'as aucune crédibilité.

Cordialement,

Rescassol

Ce qui est étonnant de la part de Kenshiroolaola, c'est qu'il écrit des choses comme :

On voit même certains pseudo-logiciens qui vont jusqu'à utiliser Faux => P (croyant que c'est vraiment établi ! et que c'est pas juste un axiome abusif)

alors même que:

1/ le premier fil où il est intervenu donne PLUSIEURS PREUVES que faux => P (rappelant ainsi que ce n'est pas un axiome, encore moins un axiome "abusif")

2/ Ailleurs, c'est peut-être peu développé, mais j'ai en tout bénévolat donné des centaines de fois sur le forum et un peu partout, une preuve de ce fait.

3/ Que quand des personnes sont intervenus pour demander des compléments, autant dans le fil en lien que dans les autres fils, il est arrivé la plupart du temps que je ne sois pas loin et réponde.

S'il voulait (kenshiolaola) contester, il semblerait du coup "obligatoire" qu'il se reporte aux endroits où ça a été démontré, ou à tout le moins qu'il les mette en lien.

Il y a donc deux possibilités:

- ou bien il n'a rien lu et dans ce cas, quelles intentions président sa militance ces jours-ci contatée

- ou bien il a lu, a été convaincu (sinon il aurait pointé les endroits), et s'énerve tout seul en écrivant (en plus en gras) que "c'est faux quand-même nananinanère"

:-S :-S j'avoue ne pas intuiter qui l'emporte entre (1) et (2) :-S :-S

Aller juste pour rigoler démontre-nous que 2>3 => Théorème de Pythagore, que je puisse le poster ailleurs, please, please. J'ai envie de m'amuser un peu.

http://www.les-mathematiques.net/phorum/read.php?16,2091694,2257652#msg-2257652

Je serais très très très tenté de le faire. Mais plusieurs intrevenants l'ont fait pour s'amuser dans l'autre fil. Je dois donc lutter contre ma mini-vanité et ne pas te faire plaisir afin de ne pas encourager ton attitude irrespecteuse envers les autres et ta tendance inexpliquée à ne pas avoir lu les fils entiers où tu as débarqué pour "attaquer direct".

Désolé, ça m'aurait fait .... tellement plaisir :-D

Bon aller, je file. Inutile de me remercier, ça ira. Bye !

(aaahh j'aime beaucoup Raoh c'est clair, mais n'oublions pas les fondamentaux, Kenshiro est plus fort au final obligeant Raoh à abdiquer, et en terme de classe aussi.

Image 1

Image 2

C'est pas pour rien que j'ai choisi ce pseudo.)

Je vais quand même faire un post sérieux et un peu plus technique pour rebondir sur

christophe c a écrit:

"mais en fait, je m'aperçois que je refuse A=>(B=>A)"

En fait la logique linéaire et la loi de Peirce entraînent la logique classique à elles seules pour les phrases construites avec l'implication.

Plus précisément soient respectivement $L_1,L_2$ et $P$ les ensembles d'énoncés de la forme suivante ($A,B,C$ étant des énoncés quelconques):

$(L1): A \to ((A \to \to $
$(L2): (A \to \to ((B \to C) \to (A \to C))$
$(P): ((A\to \to A) \to A$

Alors le plus petit ensemble d'énoncés contenant $L_1,L_2$ et $P$ et stable par modus ponens contient toutes les tautologies classiques (celles écrites uniquement avec "$\to$").

$L_1$ et $L_2$ sont d'innocentes tautologies linéaires, si vous les refusez bah je sais pas comment vous convaincre. Par contre il est vrai que l'axiome de Peirce "$P$" est un peu spécial.

Pour le voir (l'énoncé bleu ci-dessus) il suffit de montrer que cet ensemble contient les énoncés de la forme $(X \to (X \to Y)) \to (X \to Y)$ et $X \to (Y \to X)$ pour tous énoncés $X,Y$ (les fameux "droit de copier une hypothèse" et "droit d'ignorer une hypothèse" qui redescendent un peu de leur piédestal), à partir de quoi la littérature classique sur les systèmes de Hilbert permet de compléter la preuve. Cette page wikipédia https://fr.wikipedia.org/wiki/Liste_de_systèmes_logiques contient une liste de tels systèmes. Espérons qu'elle ne sera pas vandalisée...

Merci au logiciel "prover9" d'avoir fait ça pour moi :-D (je note "$C$" l'implication; "$T$" voulant dire "est un théorème" ). Il y a aussi une preuve gratuite de $X\to X$.

============================== PROOF =================================

% Proof 1 at 0.02 (+ 0.00) seconds.
% Length of proof is 14.
% Level of proof is 4.
% Maximum clause weight is 16.000.
% Given clauses 16.

1 (all x all y T(C(C(C(x,y),x),x))) # label(non_clause).  [assumption].
2 (all x all y all z T(C(C(x,y),C(C(y,z),C(x,z))))) # label(non_clause).  [assumption].
3 (all x all y T(C(x,C(C(x,y),y)))) # label(non_clause).  [assumption].
4 (all x all y (T(C(x,y)) & T(x) -> T(y))) # label(non_clause).  [assumption].
5 (all x all y T(C(C(x,C(x,y)),C(x,y)))) # label(non_clause) # label(goal).  [goal].
6 T(C(C(C(x,y),x),x)).  [clausify(1)].
7 T(C(C(x,y),C(C(y,z),C(x,z)))).  [clausify(2)].
8 T(C(x,C(C(x,y),y))).  [clausify(3)].
9 -T(C(x,y)) | -T(x) | T(y).  [clausify(4)].
10 -T(C(C(c1,C(c1,c2)),C(c1,c2))).  [deny(5)].
13 T(C(C(C(C(C(x,y),x),x),z),z)).  [hyper(9,a,8,a,b,6,a)].
15 T(C(C(C(C(x,y),C(z,y)),u),C(C(z,x),u))).  [hyper(9,a,7,a,b,7,a)].
[color=#FF0000]76 T(C(C(x,C(x,y)),C(x,y))).  [hyper(9,a,13,a,b,15,a)].[/color]
77 $F.  [resolve(76,a,10,a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=16. Generated=175. Kept=71. proofs=1.
Usable=16. Sos=48. Demods=0. Limbo=5, Disabled=6. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=104. Back_subsumed=1.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
Demod_attempts=0. Demod_rewrites=0.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=1.
Megabytes=0.19.
User_CPU=0.02, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 3080 exit (max_proofs) Sat Jun  5 16:04:13 2021

============================== PROOF =================================

% Proof 1 at 0.03 (+ 0.00) seconds.
% Length of proof is 22.
% Level of proof is 9.
% Maximum clause weight is 16.000.
% Given clauses 28.

1 (all x all y T(C(C(C(x,y),x),x))) # label(non_clause).  [assumption].
2 (all x all y all z T(C(C(x,y),C(C(y,z),C(x,z))))) # label(non_clause).  [assumption].
3 (all x all y T(C(x,C(C(x,y),y)))) # label(non_clause).  [assumption].
4 (all x all y (T(C(x,y)) & T(x) -> T(y))) # label(non_clause).  [assumption].
5 (all x all y T(C(x,C(y,x)))) # label(non_clause) # label(goal).  [goal].
6 T(C(C(C(x,y),x),x)).  [clausify(1)].
7 T(C(C(x,y),C(C(y,z),C(x,z)))).  [clausify(2)].
8 T(C(x,C(C(x,y),y))).  [clausify(3)].
9 -T(C(x,y)) | -T(x) | T(y).  [clausify(4)].
10 -T(C(c1,C(c2,c1))).  [deny(5)].
13 T(C(C(C(C(C(x,y),x),x),z),z)).  [hyper(9,a,8,a,b,6,a)].
14 T(C(C(C(C(x,y),y),z),C(x,z))).  [hyper(9,a,7,a,b,8,a)].
15 T(C(C(C(C(x,y),C(z,y)),u),C(C(z,x),u))).  [hyper(9,a,7,a,b,7,a)].
[color=#FF0000]22 T(C(x,x)).  [hyper(9,a,13,a,b,14,a)].[/color]
27 T(C(C(C(x,x),y),y)).  [hyper(9,a,8,a,b,22,a)].
29 T(C(C(x,y),C(C(C(z,z),x),y))).  [hyper(9,a,7,a,b,27,a)].
85 T(C(C(x,C(y,z)),C(y,C(x,z)))).  [hyper(9,a,15,a,b,14,a)].
86 T(C(C(x,C(C(y,z),y)),C(x,y))).  [hyper(9,a,15,a,b,13,a)].
221 T(C(C(x,C(y,y)),C(y,y))).  [hyper(9,a,86,a,b,29,a)].
269 T(C(x,C(y,y))).  [hyper(9,a,14,a,b,221,a)].
[color=#FF0000]273 T(C(x,C(y,x))).  [hyper(9,a,85,a,b,269,a)].[/color]
274 $F.  [resolve(273,a,10,a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=28. Generated=567. Kept=268. proofs=1.
Usable=27. Sos=231. Demods=0. Limbo=1, Disabled=13. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=299. Back_subsumed=8.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
Demod_attempts=0. Demod_rewrites=0.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=1.
Megabytes=0.52.
User_CPU=0.03, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 2735 exit (max_proofs) Sat Jun  5 15:15:33 2021

(Merci pour ce cadeau.
Aller et un de plus qui n'a rien compris et qui ne sait pas ce qu'il fait.
Je vais l'ajouter à une compilation que je posterai peut-être sur un site dédié.
Au suivant, à qui le tour? il me reste encore un peu de place.

Prochain challenge : 2=0 => deux droites perpendiculaires à une même droite sont parallèles.)