Par où commencer la logique ?

Merci samok pour le résume !!

Wesh,

Je réponds demain mais vraiment merci pour les pavés, ça doit prendre je sais pas combien de paquets de minutes de pondre un truc comme ça.

Juste, pour la preuve en photo, non c’est pas écrit très gros mais c’est pas le résultat que j’utilise, j’aurais pu détailler plus mais c’est : si a est non-nul alors si ab est nul alors c’est b qui est nul (qui se justifie par le fait que je compose par l’inverse qui du coup existe puis associativité puis inverse fois a fait 1 puis 1 est neutre donc reste b puis truc fois 0 egal 0 ...)

Sachant que j’ai bien compris qu’on peut toujours vider une liste d’axiomes en les rajoutant avec une implication dans la racine mais ma question est pas là, c’est vraiment la phrase « prouver blabla » sans contexte est-ce que c’est montrer si liste vide alors blabla ? Càd trouver l’arbre correspondant

Christophe c:
Ton texte est très dense pour moi, j’ai mis du temps à essayer de comprendre et je suis naturellement lent à la détente, en plus j’ai beaucoup de questions sur ce que t’as dit donc du coup je propose la chose suivante: est-ce que tu pourrais confirmer ou reprendre en détaillant simplement (sans perdre d’information si possible mais quand tu dis illusion platonicienne que tu détailles ce que t’entends par ça par exemple bon pour le coup je vois de quoi tu parles je crois mais ça demande quand même un gros effort d’interprétation et au final je suis pas sûr qu’on parle des mêmes trucs) quasiment tout ce que je vais dire. Je sais que c’est une demande un peu égoïste parce que ça demande du temps mais t’as l’air d’accepter d’en consacrer. En gros essayer de passer sur chacun des points que j’essaie d’aborder même si c’est de la bouillie infâme à tes yeux parce que comme j’essaie d’interpréter un peu tout à ma sauce et que j’ai aucune expérience en logique et tout ça va être très brouillon ce que je vais te demander ou essayer de reformuler... bref vraiment merci si c’est possible de faire ça.

Point 1

En particulier, chaque fois que tu fais un modus ponens, la procédure de recensement te signale que tu as utilisé l'axiome "(A=>B)=>(A=>B)" qui est de la forme X=>X

(C’était dans un de tes premiers messages)

Mettons qu’on me demande de démontrer $(1+1)+1=2+1$.
En français je dirais: on sait que $1+1=2$ et que $1+1=2 \Rightarrow (1+1)+1=2+1$ donc $(1+1)+1=2+1$.
Pour moi c’est ça le modus ponens de ce que j’ai appris parce que j’ai comme hypothèse $A == 1+1=2$ et $1+1=2 (== A)\Rightarrow (1+1)+1=2+1 (==B)$ en gros comme j’ai $A$ et $A\Rightarrow B$ j’ai le droit d’écrire et de prononcer la phrase « alors ça démontre que » $B$, je sais pas comment je le vois dans ma tête quel est le statut du modus ponens par rapport aux phrases que j’écris pour moi c’est un truc un peu « hors maths » qui m’autorise à écrire un truc qui sera « vrai » si on me dit que $A$ et $A\Rightarrow B$ le sont. Ça veut dire quoi vrai quelle différence de statut y a entre le modus ponens et les phrases que j’écris tout ça vraiment j’en sais rien du tout, je suis d’ailleurs très paumé là-dessus. Bref du coup avec ton arbre et ton algo ce qui serait modus ponens serait le nom qu’on donne  « au plus petit arbre » avec un sens que je ne saurais pas expliciter mieux sans me perdre qui aurait une fois l’algo preuve appliqué comme axiomes $A$ et $A\Rightarrow B$ et comme conclusion si ça s’appelle comme ça $B$. Donc ce serait l’arbre (et je pense qu’il n’y aurait que lui):
0)A
1)B (0)
(Je suppose que A c’est pas de la fameuse forme qui vire les axiomes)
Là j’ai bien comme axiome $A$ et $A\Rightarrow B$

Or t’as l’air de dire que le modus ponens c’est l’arbre:
0)$A\Rightarrow B$
1)$A$
2)$B$ (0,1)
Et du coup on a bien l’axiome supplémentaire qu’apparemment les mathématiciens enlèvent après le programme preuve qui est $(A\Rightarrow \Rightarrow (A\Rightarrow $.
Pourquoi cette différence, est-ce que c’est moi qui connais une mauvaise définition ?
Donc pour toi j’insiste lourdement un modus ponens c’est (c’est quoi d’ailleurs c’est le nom qu’on donne à un arbre ?) ça aboutit (?) à trois axiomes et pas deux.

Point 2

si $A_1$ alors si $A_2$
> alors si ..... alors si $A_8$ alors
> $P$

Quand tu avais décrit l’algo tu n’avais pas fini sur la partie « qu’est ce qu’on prouve » je sais juste qu’il y avait une liste d’axiomes puis un « alors » puis la phrase en racine. Pourquoi je peux interchanger les axiomes entre les Si et les alors si ?
Imaginons que je puisse pas et qu’on donne un sens d’écriture dans les listes et dans leur concaténation et qu’à la fin l’algo fait un PRINT Si blablab alors bloublou en reprenant les axiomes dans l’ordre donné dans la liste en lisant mettons de gauche à droite les axiomes, est-ce que cet algo est « équivalent » à l’algo qui dirait la chose suivante, il sort une liste d’axiomes puis fait une liste de PRINT chaque PRINT donnant un si axiomes alors racine et au final les PRINT donnent toutes les combinaisons possibles en interchangeant les axiomes. On appèlerait phrase prouvée par l’arbre bidule une des phrases après l’un des PRINT, est-ce que c’est un peu dans ce sens là que je suis censé comprendre ? En gros un arbre ne prouve pas une seule chose mais prouve plusieurs phrases qui sont la même en changeant l’ordre des axiomes et ça a été décidé comme ça point ? Qu’est ce que ça voudrait dire que ces deux algos sont équivalents si jamais c’est le cas ? Est-ce que le fait de prouver: $(A\to (B\to C))\to (B\to (A\to C))$ permet de justifier par exemple le fait d’interchanger les axiomes dans la phrase « preuve » ? Si oui comment ?
ATTENTION si jamais les questions sont évidentes dans le sens où tu penses que je peux trouver tout seul la réponse sans y passer 1 an, merci de me le dire et j’essaierai de chercher, là je commence à fatiguer aussi.

Autre chose c’est quoi le statut de la phrase Preuve ? Est-ce que le « si A alors B » que tu utilises dans la phrase preuve est « quelque part de même nature » de que la phrase « $A\to B$ »? Moi tout ce que je vois c’est que c’est si j’ai un arbre qui me donne « si A alors B » alors l’arbre qui reprend le même et rajoute à la racine un fil vers la nouvelle racine « $A\to B$ » alors la phrase preuve du nouvel arbre est « si alors $A\to B$ ». T’as l’air de parler de ça un peu après notamment pour justifier cette règle qui permet de virer un axiome sous condition mais ca me parait toujours pas clair, les arbres sont pas les mêmes, les phrases preuves sont pas les mêmes d’accord on a une liste d’axiome vide mais ensuite ? Tout ce que je sais c’est que le symbole implication se prononce « si alors » à voix haute après je sais pas si y a un lien avec le si alors de ta phrase preuve et qu’est ce qui le justifie (et pour le justifier d’ailleurs faudrait que je le fasse avec un arbre mais la justification serait une nouvelle phrase preuve mais ... et alors ? Y a pas un cercle vicieux quelque part ?)

JE SAIS QUE C’EST SAOULANT de me lire et tu dois peut-être avoir envie de m’égorger mais si c’est possible j’adorerais que tu puisses répondre dans le détail à toutes ces interrogations :-D


Point 3

Mais in fine globalement, tu peux toujours dire
> que tu as prouvé :

si $A_1$ alors si $A_2$
> alors si ..... alors si $A_7$ alors si $[A_8$
> alors $P]$

De ce que je comprends de l’algo j’ai prouvé plutôt si $A_1$ alors si $A_2$
alors si ..... alors si $A_7$ alors $A_8\to P$ ce qui n’est pas censé être pareil, si oui je ne vois pas pourquoi et je ne vois pas comment le montrer parce que pour le montrer faudrait utiliser l’algo preuve sur un arbre avec cette phrase dedans (on est d’accord je peux mettre n’importe quoi comme phrase dans l’arbre pas forcément un truc « conventionnellement » mathématiques ?) qui me sortira une preuve avec son format mais je vois pas quoi en faire.

Point 4

Mais les logiciens par exemple ne présenteraient
> pas le choses comme ça même s'ils voulaient
> coller le plus possible au format utilisé. Ils
> diraient que tu n'as droit qu'au modus ponens et
> quand moi je dis que tu ajoute l'axiome $H_1\to
> (H_2\to (H_3\to C))$ au moment du recensement
> quand tu passes sur le noeud étiqueté $C$ qui a
> 3 fils étiquetés respectivement $H_1,H_2,H_3$,
> eux ne font pas, ça, ils rajoutent un QUATRIEME
> fils au noeud $C$ qui est JUSTEMENT $H_1\to
> (H_2\to (H_3\to C))$, puis ils appliquent un
> premier modus ponens qui va donner $(H_2\to
> (H_3\to C))$, puis un deuxième modus ponens qui
> va donner $H_3\to P$ et enfin un troisième modus
> ponens qui va donner $P$.

Voilà on commence à rentrer dans ce que je trouve plus dur à comprendre.
Donc si je comprends ce que tu veux dire, pour toi tout arbre est une preuve, les logiciens eux d’une part ils disent que tous les arbres ne sont pas des preuves il faut que pour chaque « arbre élémentaire » il y ait une feuille $A$ une feuille $A\to B$ et une racine $B$ ou alors une feuille A une feuille B une feuille $A\to (B\to C)$ une feuille $B\to C$ et une racine $C$ ou alors etc etc ET EN PLUS dans l’algo preuve on enlève le passage qui rajoute automatiquement une succession d’implication entre les fils dans la liste d’axiomes c’est ça ?

Point 5

Toute la partie où tu parles de pointeur et tu utilises le terme illusion platonicienne

De ce que je sais un pointeur est un emplacement mémoire qui contient l’adresse d’un autre emplacement mémoire. Tu as l’air de dire qu’une variable (ou je sais pas quel nom on donne d’ailleurs j’ai du mal avec le statut de ces choses) c’est un pointeur. Mais du coup en maths c’est quoi un pointeur ? En info un pointeur est un objet physique en maths pour filer la métaphore de l’illusion platonicienne, c’est en quelque sorte un pointeur dans l’emplacement mémoire abstrait (ensemble ?) des caractères abstraits appelés symboles de constantes dont la valeur est l’objet mathématiques abstrait platonicien pur :-D
Je veux bien d’ailleurs dans l’absolu y a pas plus de sensation de concret dans ma tête j’ai l’impression quand je me fais croire à la persistance « réelle » du pointeur physique et ce truc là dans tous les cas c’est un sentiment global de cohérence une sensation bizarre de « je parle d’un truc » c’est vrai que pour le pointeur physique le truc est renforcé par la sensation « image visuelle des sens » mais bon...

Tu as l’air de dire que donc si je dis « a » dans une phrase mathématique et qu’à la ligne d’après je redis « a » rien me garantit que c’est le même mais le problème c’est que j’ai vraiment l’impression que justement c’est censé faire partie des « non-dits » des trucs on y croit tous de même qu’on croit que le symbole est vraiment un vrai « symbole platonicien » etc etc dans ce cas jusqu’où je suis censé pousser la « barre platonicienne » des trucs que j’écris en maths ? Apparemment je dois me mettre en mode les symboles sont pas « sensation d’être des taches d’encre toutes différentes » mais « sensation d’être la représentation d’un objet symbole abstrait » bon ça ok de toute façon la « sensation de tache d’encre » est elle-aussi l’objet platonicien de «représentation de l’objet réel tâche d’encre » et je pourrais boucler comme ça longtemps et c’est flou dans ma tête ça me perd et c’est très très frustrant.

Point 6

Le modus ponens est par contre tout à fait
> LEGITIME et HONNETE à la condition (qui est
> d'ailleurs la vraie et bonne incarnation des
> preuves de maths/sciences) que ce soit dans le jeu
> prouveur-sceptique, car, là, c'est aussi et
> uniquement un jeu de pointeurs: Lea propose A et
> Bob choisit entre continuer avec "prouve-moi A=>B"
> et continuer avec "prouve-moi A".

J’ai rien compris, c’est quoi le prouveur sceptique ?

Point 7

Donc les listes sont tout
> bêtement vues comme des ensembles (dans mon post,
> je modifierai si tu veux, mais demain)

Non d’ailleurs dans un message au dessus t’as dit: A; A; A=>B; A=>(B=>C).
En listant les axiomes de ton premier exemple d’algo preuve. Et en vérifiant je trouve pareil.

Bon j’ai pris une liste d’exos de topo simples genre les premiers exos de TDs de topo d’une fac qui « mettent en jambe ». Je vais essayer de les mettre sous forme d’arbre et si j’ai la foi je les posterai ici au moins quelques uns avec la démo française et la version arbre.

Christophe c: Si tu peux pense à répondre à mon gros pavé avec les points en gras là, merci pour toutes les réponses que je peux avoir d’ailleurs,même si j’ai peur que ça finisse encore en clash ( vous adorez ça sur ce forum :-D (je plaisante osef personnellement))