Définir et démontrer

Ltav

Bonjour,

Suite à un échange technique privé, je me permets de préciser la différence que je vois entre démontrer et définir une proposition B par une autre proposition A :

1) Je démontre B par A, i.e. A => B (preuve),
2) Je définis B par A, i.e. B := A (affectation de variable)

En général, on n'a pas 1) <=> 2).
Si B := A, alors A => B n'est plus une démonstration mais une tautologie : selon moi, je n'ai rien prouvé.

Est-ce l'avis de "tout le monde" ? Merci pour vos commentaires.

christophe c

Je te l'ai déjà dit il n'y a pas de définitions dans les vraies maths. Les définitions sont des ABREVIATIONS! Elles permettent de raccourcir le texte théorique. On peut appliquer au texte pratique un algorithme de remplacement brut pour obtenir le texte théorique (qui bouclera éventuellement mais qui a le devoir de ne pas boucler dans les maths concrètes disons).

Il suit que si tu ne précises pas un peu ta demande elle n'a pas vraiment de sens mathématique. Oui "appliquer" une définition donne une tautologie . Mais pas n'importe laquelle: ça donne X=X. C'est sans profondeur.

christophe c

Sinon pour info A=>B n'est JAMAIS une démonstration: c'est une phrase.

Ltav

Bonsoir,

Merci de ta réponse Cc. Tout à fait d'accord avec toi, en précisant bien que par "A => B" je n'entends pas la phrase elle-même mais "montrer A => B".

Il y a donc bien abus de langage de dire : "J'ai prouvé A => B" lorsque B := A ?

Tu vois où je veux en venir mais restons sur ce point théorique.
D'autres avis sont les bienvenus.

Blueberry

Ltav a écrit:

Il y a donc bien abus de langage de dire : "J'ai prouvé A => B" lorsque B := A ?

Non par forcément, tout dépend des axiomes dont tu pars. Chez Bourbaki, $A \Rightarrow A$ est un théorème par exemple.

Ltav

Merci de ta réponse Blueberry.
Et de quel(s) axiome(s) partent-ils pour démontrer A => A - si tu as cette information ?

Ltav

N.B. Je soupçonne qu'ils partent du tiers-exclu pour ne pas en arriver à démontrer A => non A.

Blueberry

Non.
Ils partent des axiomes logiques:
(1) $(AouA) \Rightarrow A$
(2) $A \Rightarrow (AouB)$
(3) $(AouB) \Rightarrow (BouA)$
(4) $(A \Rightarrow \Rightarrow ((CouA) \Rightarrow (CouB)$

Leur 1ère déduction est que:

C1:De $A \Rightarrow B$ et $B \Rightarrow C$ on déduit $A \Rightarrow C$ (Transitivité de l'implication).

Puis ensuite $A \Rightarrow (AouA)$ et $(AouA) \Rightarrow A$ (axiomes (2) et (1) appliqués) donne par transitivité de l'implication $A \Rightarrow A$.

Le tiers exclu se déduit peu après.

GaBuZoMeu

Ltav ferait bien d'apprendre un petit peu de théorie de la démonstration, s'il veut savoir de quoi il parle.
En calcul des séquents (intuitionniste ou classique), $A\vdash A$ est un axiome de base. Par introduction du $\to$ à droite :
$$\begin{array}{rcl} A&\vdash& A\\\hline &\vdash&A\to A\end{array}\;.$$

christophe c

De mon téléphone je ne sais pas si je vois où tu veux en venir comme tu dis mais par contre tu te trompes de paragraphe. Il n'y a pas d'abus de langage ni de définition ajoutée quand quelqu'un prouve A=>Tout en 45219 lignes à un moment donné. Si tu veux dire qu'il annonce avoir prouvé nonA et non pas annonce qu'il a prouvé A=>Tout c'est juste une économie d'encre car non A est une abréviation de A=>Tout. La encore il n'y a pas d'abus de langage ni de loup caché.

Ltav

Merci à vous. Hmm...ça devient un peu "compliqué". Si j'ai bien compris :

- Pour Blueberry : A => A est un théorème (bourbakiste).

- Pour GaBuZoMeu : c'est une définition (du calcul des séquents intuitionniste ou classique).

- Pour Cc : c'est une tautologie (et "non A" au lieu de A => tout est une simple économie d'encre, je pourrais aussi bien écrire "nA" ou "Wow").

GaBuZoMeu

Tu n'as rien compris du tout, comme d'hab.

Dom

Ce dialogue de sourd est-il lié :
-à des "axiomes non dits" de chacun (comme dans des échanges politiques où l'on s'aperçoit en creuser très loin que chacun a un principe immuable qui était une évidence, non partagée)
-à une manière de chacun de dire à l'autre « c'est faux » sans argumenter en français mais avec des "lignes de code" incompréhensibles pour l'interlocuteur

Bizarre aussi @cc : « il n'y a pas de définition », puis « une définition c'est ... ».

christophe c

@dom: oui, mon impatience a peut-être conduit à une expressions trop condensée. Tu oublies de préciser que j'ai pris la peine de nuancer et il n'y a pas de contradiction:

<< il n'y a pas de définition dans les vraies maths, et une définition dans les maths pratiques c'est .....>>

Ce n'est pas spécifique aux maths. Tel texte documentaire dira

"............ société protectrice des animaux ......................."

mais le collègue qui était limité en octets et l'a envoyé par SMS a dit:

"............ SPA ......................."

Par exemple, $4=3+1$ est une abréviation de l'affirmation "vide" $3+1=3+1$ alors que $4 = 2+2$ est une affirmation non vide qui prétend que $3+1 = 2+2$, ie qui prétend que $(2+1)+1 = 2+(1+1)$ puisque $2$ est une abréviation de $1+1$ et pour laquelle, avant preuve, le doute est légitime.

Dom

Oui, bon, dans les vraies ou les fausses maths, les définitions sont des abréviations.
Ou alors je ne sais pas ce que sont les fausses (les vraies ?) maths.
Au lieu de dire "quadrilatère avec quatre angles droits" on dit "rectangle", par exemple.

Dans ton meta meta meta langage qui t'est propre, il faudrait définir les vraies maths, mais c'est un autre sujet.
C'est ta manière de voir, alors, on s'en fiche un peu (tu le dirais toi-même comme ça, je ne te dénigre pas, hein !).

Pour revenir au fond : c'est ce que je dénonce un peu dans mon propos.
Le lecteur qui passe par là lira bien un dialogue de sourd, et en sera conscient :
J'ai l'impression que personne ne dit clairement avec quoi il travaille, avec quelles définitions (pour le coup), avec quels axiomes (au sens général, disons les « présupposés »).

Attention, je ne critique pas du tout.
J'essaye d'expliquer pourquoi la précédente discussion a été fermée.

Bien sûr, il y a aussi une raison non encore évoquée : le troll, l'envie de faire durer pour le plaisir, le fait de ne pas savoir quoi foutre aujourd'hui, etc.
Mais, je peux être dupe, je ne crois pas que ce soit le cas.

GaBuZoMeu

Le lecteur qui passe par là lira bien un dialogue de sourd, et en sera conscient

C'est bizarre. Il arrive qu'un hurluberlu se pointe sur le forum et se mettre à raconter de grosses bêtises sur un domaine mathématique qu'il ne connaît pas. Je me souviens par exemple de dlz et des probas ou de la géométrie. Les intervenants qui s'y connaissent un tant soit peu lui montrent ses erreurs, mais il n'en démord pas. Il ne fait pas illusion et personne ne parle alors de "dialogue de sourds" en renvoyant les deux parties dos à dos.

Pourquoi un semblable hurluberlu peut-il faire illusion en logique et plus spécifiquement en théorie de la démonstration, alors que c'est un domaine tout aussi mathématique que les probas ou la géométrie ?

christophe c

dom a écrit:

Dans ton meta meta meta langage qui t'est propre, il faudrait définir les vraies maths, mais c'est un autre sujet.

:-D tu connais ma réponse, je l'ai faite 2687638136768763 fois.

<<vraie mathématique>> est une abréviation de <<recherche de certitudes absolues>>

Le mot "certitude absolue" est renommé en "théorème".

Un théorème de maths est un énoncé P tel qu'il existe une suite finie $u$ d'énoncés telle que:

si $u_0$ alors si $u_1$ alors si .... alors si $u_n$ alors $P$

est un axiome, ainsi que tous les $u_i$.

"axiome" veut dire "hypothèse pérenne admise par la théorie ambiante"

Les théorèmes de maths sont donc indépendants des théories, mais par abus de langage, comme les axiomes de la théorie ambiante, ne sont pas chaque fois rappelés, par économie d'encre, il apparait dans les archivages des commodités pour savoir qu'ils sont supposés sans qu'ils soient écrits. La théorie ambiante actuelle (depuis 100ans) est ZF (avec AF et AC en option parfois mal précisées).

Remarque: le mot "science" a la même définition, seule la théorie ambiante change, ainsi que la nature des hypothèses pérennes faites (en maths, elle est blanche, en science elle est engagée et se nourrit aux expériences et se négocie entre experts).

Les définitions sont des abréviations qui servent à raccourcir les textes lors de l'archivage.

christophe c

Je plussois la remarque de GBZM concernant la sociologie du forum, à ceci près que je précise que seul dom "renvoie dos à dos" (enfin s'est manifesté pour le faire) et est victime (consentante?) de l'illusion que la logique math serait obligée de se justifier face aux amateurs plusss que les autres spécialités scientifiques.

Je l'explique par le fait que 90% (au moins) des philosophes "combattent pour leurs salaires", ceci ayant introduit une "tradition" de respect (on veut nous aussi qu'ils aient un salaire, plutôt que d'aller nettoyer les WC des macdo, pour partie d'entre eux) de leurs propos (exemple: les gentillesses qu'on accorde à Ltav) ou de propos historiquement erronés, qui servent aujourd'hui de devinettes pour enfants, mais avec devoir de ne pas le dire trop fort (combien de collègues de lycées (à peu près tous ceux où je suis passé), j'ai dû "ménager" quand j'ai dû leur corriger leur erreur sur ce qu'ils appellent l'argument ontologique, car non ménagés, ils se seraient sacrément vexés de se voir "traités de pas au courant que c'est une blague").

Ca ne me parait pas "trop grave", à condition que ce ne soit pas "une petite partie visible d'un iceberg trop grand" (dont par exemple, une autre partie cachée consisterait , par exemple, à donner à un agent de 28ans des responsabilités sur un centre de calcul de dérivées sur un champ de travaux publics au prétexte qu'il aurait un bac ES et que dériver y est au programme). Pour l'heure ce phénomène ne se produit qu'avec des philosophes au prétexte qu'ils ont "un module de logique" à leur cursus universitaire (auquel ils ne captent que dalle), mais heureusement, ils ne font pas descendre des pelleteuses dans des cavités :-D

GaBuZoMeu

Je ne m'associe pas aux diatribes de Christophe sur les philosophes. Je ne crois pas par ailleurs que Ltav soit un philosophe sérieux (pas plus qu'un mathématicien sérieux).

Dom

Non, non, pas du tout ! :-?
Je ne renvoie pas dos à dos. C'est presqu'une insulte de me dire cela (oui, bon, toute proportion gardée :-D, je ne me sens pas offensé, loin de là, mais c'est totalement faux !).
Je cherche à savoir pourquoi ça perdure et j'ai bien expliqué ma démarche en "quelles en sont les raisons ?".

Si c'est un hurluberlu, thèse de @GBZM, alors oui, c'est une des raisons.
Elle est claire et limpide. Et d'ailleurs, tous les propos de @GBZM dans ladite discussion allaient dans ce sens.
(Pardon, @GaBuZoMeu de parler à la troisième personne, je réponds à @christophe c).

Edit : je n'avais pas lu le dernier message de @GBZM mais justement, je distingue les deux intervenants et surtout leurs interventions.

Mais, justement @cc, ton paragraphe : « ... il apparaît dans les archivages des commodités pour savoir qu'ils sont supposés sans qu'ils soient écrits. ». Va donc essayer de convaincre avec cette phrase.
Tu ne sembles pas du tout dire que «l'autre» raconte n'importe quoi.
Tu lui dis, au mieux, de "faire des maths". C'est certainement un bon conseil, mais je crois que c'est vain car complètement incompris. « Faire des maths » pour toi n'a pas la même signification que « Faire des maths » pour un écolier, vois-tu ?

Bon, du coup c'est moi qui vais passer pour le troll du WE...

christophe c

Looool ce n'étaient pas des "diatribes" (je googlerai ce mot). Juste une tentative d'explication sociologique (certes peu diplomate) : mais je pense sue les lecteurs tranquilles sauront traduire cette simplifications n en une éventualité réelle.

Dom

Oui, oui pas d'inquiétude.
J'm'énerve pas, j'explique ! ;-)

Allez, bon WE

christophe c

D'un pc, je reviens sur le mot "diatribe" que tu utilises GBZM:

<<diatribe>> abrège <<critique amère et violente>>

Il n'y a aucune amertume dans ma critique et d'ailleurs, ce n'est pas une critique, c'est une tentative d'explication qui dégrade l'image d'une partie des philosophes.

J'aurais pu ajouter une composante diplomate ou ne pas donner de pourcentage au doigt mouillé, j'en conviens. Mais attention: il n'y a rien de bien exagéré dans ce que j'ai dit. J'ai, en tant que représentant de P7 ( je ne me rappelle vraiment, mais vraiment plus du tout pourquoi ce titre), il y a une vingtaine d'années dû aller voir (pour rendre service) une conférence donnée par en gros l'un des patrons de la "philosophie française" (me rappelle plus non plus de quel institut il était le chef, mais je me rappelle PARFAITEMENT son nom, que je ne citerai pas) et revenir avec un eptit rapoprt écrit de quelques lignes. Et le sujet était... le lambda calcul.

Et bé.... toi-même tu aurais été plus sidéré que moi, par l'ampleur, non seulement des faussetés racontées, mais surtout par l'incapacité TOTALE du conférencier de répondre "je ne sais pas" face aux questions du public (dont une petite demi-douzaine s'y connaissait un peu et se marrait bien en posant des questions piéges et laissant l'orateur s'enfoncer). J'ai moi-même participé à la plaisanterie mais plus modérément que certains jeunots, bien plus "prédateurs" que moi (les jeunes tirent sur les ambulances).

Le conférencier était tellement traumatisé (intérieurement, il ne le montrait pas) que j'ai eu droit illico à la sortie à une invitation à diner (au cours de laquelle il n'a eu de cesse, de manière indirecte, d'essayer d'atténuer son ignorance du sujet qu'il venait d'exposer en se présentant comme un maitre, enfin plus précisément "sa faute" de s'être ainsi présenté) où j'ai ma foi très bien mangé (me rappelle pu des plats, mais bon souvenir).

Depuis lors (c'était la première fois que je découvrais qu'en dehors des sciences "on fait semblant" de charrier du concept), j'ai "subi" des dizaines d'événements du même acabit. Après, évidemment, je n'ai peut-être pas eu de chance, tout simplement. Je suis absolument persuadé qu'il existe des tonnes et des tonnes de philosophes honnêtes intellectuellement, là n'est pas la question, mais il y a des "traditions de politesse" qui font que...

Ca explique à mon avis que la logique est malmenée quand les équations aux dérivées partielles ne le sont pas. Un philosophe n'osera pas "l'ouvrir" devant une équation, mais s'il entend à la table d'à côté qu'on cause de RPA, évidemment, il "a envie" de venir faire l'intéressant. Et c'est là qu'en tant que scientifiques on a le devoir de ne pas trop le "casser" (du moins si c'est filmé). Sinon, bin c'est des pans entiers de programmes scolaires ou universitaires régulièrement vantés par lesdits qui s'en retrouveraient démasqués comme des erreurs enfantines et "ce serait déplaisant". L'argument ontologique comme "élément de pensée de la philosophie" sur lequel plein de "grands penseurs" :-D ont vidé leur bouteille d'encre, imagine si on "révélait au public" que c'est une erreur qu'on pourrait mettre au programme de sixième qu'il ne faut pas la faire, le malaise.

Mais je n'ai aucun aigreur contre ces traditions de politesse, j'y insiste. Ca me parait juste... un peu contingent disons.

Ltav

Bonsoir,

@Blueberry : sauf erreur, Bourbaki donne à A => B la définition B ou non A : grâce à cette définition, A => A n'est strictement rien d'autre que le tiers-exclu, A ou non A.

@GBZM : en effet, il m'arrive de faire de l'humour. Oui, tu as bien utilisé un théorème célèbre (le théorème de déduction de B par A appliqué trivialement à A = B), mais tu n'as pas compris ma démarche.

Je souhaiterais affiner encore plus la différence entre définition et démonstration : une définition doit être encore plus "forte" que la tautologie A => A, elle ne doit pas a priori être démontrable (même aussi trivialement que pour A => A). Je préfère donc traduire cette distinction par :

1) Je démontre B par A lorsque A $\vdash$ B (preuve ou déduction),
2) Je définis B par A lorsque B := A (affectation de variable)

Si B := A, alors A $\vdash$ A n'est plus une démonstration mais un axiome de déduction : on ne le "prouve" pas. Et l'abus de langage serait justement de parler de preuve ou de raisonnement pour A $\vdash$ A.

[small]Nota Bene :

@GBZM, Cc, voire Shah d'ock : essayez de ne plus vous enfoncer dans ces diatribes indignes de scientistes immatures. Si le dernier fil "RPA" a trop duré et été trop vite fermé à la fois, c'était en partie à cause de notre incapacité collective à nous accorder et surtout à nous respecter (j'essaie un peu de répondre par là au questionnement de Dom).

@Cc : je ne reviens pas sur tes insultes contre les philosophes : j'ai hélas vérifié par moi-même que tu ne connaissais pas grand-chose à la philosophie, ni à l'argument ontologique (tes critiques me rappellent les pseudos arguments de la "bande à Sokal et Bricmont", qui n'étaient finalement rien d'autre que deux cancres se "vengeant" de leurs cours incompris de "philo").

Revenons à notre sujet s'il vous plaît.[/small]

Bonne nuit.

Blueberry

Ltav a écrit:

sauf erreur, Bourbaki donne à A => B la définition B ou non A : grâce à cette définition, A => A n'est strictement rien d'autre que le tiers-exclu, A ou non A.

Oui, à une étape près. Tu prouves $A \Rightarrow A$ qui est $nonA~ou~A$ puis par application de l'axiome (3) $(nonA~ou~A) \Rightarrow (A~ou~nonA)$ tu déduis par modus ponens $(A~ou~nonA)$ qui est le tiers-exclu, qui est effectivement rapidement déduit dans Bourbaki.

Mais où veux-tu en venir?...

Shah d'Ock

Non mais heureusement qu'il n'y a pas besoin du tiers-exclu pour A implique A! Qu'en logique classique cet énoncé soit équivalent au tiers-exclu (plus généralement $(A \to \leftrightarrow (\neq A \lor $ est un théorème de logique classique. Bourbaki travaille d'office en logique classique) est une chose, mais ça ne l'empêche pas d'être vrai aussi en logique intuitionniste et même linéaire.

Ltav

Bonjour,

@Blueberry : merci pour tes précisions. Je m'intéresse particulièrement aux cas où on n'utilise pas le tiers-exclu (*). En fait, je recherche à exprimer plus formellement la différence entre définition et démonstration (au sens où Cc parle pertinemment d'une pure "abréviation" et d'"économie d'encre") et vos interventions me suggèrent que chercher cette différence dans A => A est insuffisant si cette formule n'est pas tout bonnement considérée comme un "axiome d'identité" (ce que le sens commun admet en général).

Je pense avoir trouvé cette formalisation dans l'écriture :

A $\vdash$ B

où $\vdash$ est le symbole de la démonstration syntaxique qui déduit B de A. Si je définis B := A, alors A $\vdash$ A n'est plus une démonstration mais un axiome logique.


(*) Rappelle-toi que l'ancien débat sur le raisonnement par l'absurde n'avait de sens qu'en logique intuitionniste, où j'insistais sur l'idée que, sans tiers-exclu, la "démonstration" de non P à partir de (P => faux) n'en était pas une : je démontre P => faux, mais je définis non P à partir de P => faux. On parle alors abusivement de "démontrer non P en prouvant P => faux". C'est encore plus clair en écrivant le raisonnement de manière syntaxique (au sens de la preuve formelle) et non plus sémantique (au sens des valeurs de vérité) : (P $\vdash$ tout) $\vdash$ non P. Pour non P := (P $\vdash$ tout), on retrouve bien un axiome (et non plus la "démonstration") : non P $\vdash$ non P.

Poirot

$A \vdash A$ n'est pas un axiome logique mais vient de la définition de démonstration syntaxique.

GaBuZoMeu

Bon, Ltav a découvert le symbole $\vdash$ et il l'emploie maintenant à tort et à travers :

> (P $\vdash$ tout) $\vdash$ non P.

Comme si cela allait donner de la cohérence à ce qu'il raconte. (:D

christophe c

Ltav a écrit:

tes critiques me rappellent les pseudos arguments de la "bande à Sokal et Bricmont", qui n'étaient finalement rien d'autre que deux cancres se "vengeant" de leurs cours incompris de "philo"

Ltav a écrit:

je ne reviens pas sur tes insultes contre les philosophes

Dans un cas tu appelles ça "des insultes", dans un autre pour les mêmes déclarations?), tu appelles ça des critiques. Le mot "critique" me parait plus approprié que le mot "insulte" qui est très fort et n'a, à mon avis, pas sa place ici.

Je te cite aussi (et surtout!!) pour ton évocation de Sokal et Brickmont écrite en petits caractères qui en méritait de plus gros, me semble-t-il. Tu me fais bien des compliments en déclarant que mes critiques sont à ranger dans la même cour que les leurs, qui ont tout de même nécessiter un livre, publié, bien vendu, pour être contenues. Moi, j'ai juste "témoigné" d'un ressenti, pas franchement argumenté.

Je ne comprends pas trop non plus, pourquoi tu penses être convaincant avec une sortie pareille (sur S et en petits caractères :-S Penses-tu juste que parce que tu les désapprouves et les traite de cancre, cela suffit pour que tes lecteurs "te croient sur parole"?

christophe c

J'ai fait l'effort d'aller sur ma messagerie jussieu, de cliquer sur un ancien MP des jours récents que je t'ai envoyé en réponse à un précédent MP de toi, et d'en extraire un passage qui me semble pertinent pour toi Ltav (bien que "purement intellectuel", je ne veux pas recopier ce MP trop long):

Ltav a écrit:

Le problème que tu as est que n'étant pas scientifique, tu ne sembles pas avoir compris que la science et les maths ne peuvent pas mentir, elles sont sérieuses, donc gèrent des suites de caractères avec précaution et minutie, en signalant tout ce qui est admis en hypothèse.

Quand on te lit, on voit bien que ton profil philosophico-littéraire souhaite donner une forme de transcendance un peu magique aux mots que ne peut pas se permettre la science.

Je te le répète, tant que tu ne comprends pas que dans les présents questionnements, tu refuses d'avoir le rôle du prouveur, il y a malentendu car c'est "forcément" le rôle que nous t'attribuons. Tes considérations ne sont "même pas fausses", elles sont juste non scientifiques. Je ne sais pas par quel bout prendre tes déclarations et les "calculs" que tu affiches dans tes posts, rien de plus. Essaie de te rendre compréhensible.

Je t'ai répondu le passage cité à propos de l'AO, mais je pourrais très bien te répondre la même chose à propos de ta déclaration suivante, ci-dessus: (mince, j'ai fait un aperçu, extrait à l'edit)

Ltav à blue a écrit:

Rappelle-toi que l'ancien débat sur le raisonnement par l'absurde n'avait de sens qu'en logique intuitionniste, où j'insistais sur l'idée que...

Ltav

Bonsoir,

@Poirot : merci pour la nuance, je pensais à l'axiome au sens d'une phrase évidente par elle-même et qui n'a pas à être prouvée. Mais "définition" me va très bien.

@GBZM ou la logique du "s'il enn parle que maint'nant, c'est qu'il vient de l'aaapprendre". Tu vois, c'est ça aussi le progrès, réutiliser des connaissances auxquelles on n'avait pas pensé (*). Tant que tes propos s'arrêteront à ce genre de "réaction nerveuse" entièrement agrippée à l'espoir d'une "chute de réputation" de l'interlocuteur en l'attaquant sur des miettes de phrases (méthode certifiée "S&B"), je ne vois pas en quoi tu peux remettre en cause la cohérence de ma position. Sa force n'a fait qu'augmenter, tant pis si tu ne veux pas le voir (je m'en remettrai).

@Cc : c'est un peu pareil, sauf que je suis un peu plus d'accord avec toi : quelque chose qu'on ne lit pas, qu'on se contente de survoler, qu'on ne sait même pas commencer...ne peut "même pas être faux" (au sens de Pauli), ni jamais "scientifique". Qui dirait le contraire ? Je ne m'attarderai pas sur S&B et ne faisais qu'indiquer une opinion certaine de ma part et bien étayée sur le sujet et l'esprit de leur livre, qui ne dépasse pas le niveau de la "plaisanterie" suivante : croire qu'on puisse juger un puissant système philosophique (**) auquel on n'a strictement rien compris, en sortant de petites phrases (dont l'allure "scientifique" donne à S&B l'illusion gourmande qu'ils peuvent les maîtriser) du bloc de leur contexte : en gros, "je crois comprendre un mot en anglais, alors je traduit Shakespeare". Ni plus, ni moins.

Je referme la parenthèse.

Pour en revenir au sujet, il semble donc bien qu'on ne puisse prétendre, une fois démontré A, avoir démontré (l'axiome ou la définition) A $\vdash$ A.

Bonne fin de nuit.

(*) Je répète l'idée : si non P := (P $\longrightarrow$ $\perp$), alors (P $\longrightarrow$ $\perp$) $\vdash$ non P n'est rien d'autre que : non P $\vdash$ non P. Il n'y a plus démonstration, à rigoureusement parler, mais une convention.

(**) jusqu'à celui de Hegel, philosophe admiré non sans raison par de nombreux grands scientifiques, dont les meilleurs mathématiciens allemands.

Shah d'Ock

Ltav a écrit:

réutiliser des connaissances auxquelles on n'avait pas pensé

C'est peut-être ça ton problème: tu utilises tous les "arguments" auxquels tu peux penser pour défendre une position. Autrement dit plutôt que de progresser, tu cherches à camper sur une position a priori, à avoir le dernier mot. On dirait que la seule raison que tu as de défendre ta position, c'est non pas que tu as de solide raison d'y croire (puisque tous tes "arguments" ont été successivement démontés et à chaque fois tu as dû en inventer de nouveaux), mais parce que c'est celle que tu as énoncé à un moment donné et que tu es incapable de revenir dessus.

Ltav

@Shah d'ock : pardon, mais là du coup, tu es disons plutôt "à côté de la plaque". As-tu compris le déroulement global des événements au moins ? Juste de loin ?

Tu me rappelles une conversation entre le capitaine Haddock et le professeur Tournesol sur la fusée qui les amène à la lune (le second explique au premier le fonctionnement de la fusée en phase d'alunissage et le premier comprend qu'il s'agirait d'une opération strictement inverse au décollage).

De même, ce que tu dis sur les arguments (qui aurait "démonté" qui), je te réponds que "c'est exactement ça, sauf que c'est exactement le contraire" (*).

Comme tout le monde fait en général, je suis parti d'une conviction originelle sur l'inexactitude de certaines thèses sur le raisonnement par l'absurde, que j'ai ensuite exprimée et développée tout au long du débat. Il y a eu deux "épisodes" : le premier a été bouclé durant le dernier fil sur le RPA (en gros, "sans TE, RPA = définition de non P [par P => tout]", "avec TE, RPA = démonstration de non P [par P => tout]"). L'épisode actuel, plus indépendant, consiste à traduire plus formellement et dans toutes les logiques la différence entre définir et démontrer. Bien sûr, mes positions n'engagent que moi et j'ai demandé à chacun de se faire une opinion par lui-même en relisant attentivement les échanges - ou en me faisant de nouvelles objections.

Bref, je ne dis pas ça pour t'offenser mais essayer d'expliquer ma démarche.

Bonne journée.

(*) Petites parenthèses : en fait, notre brave capitaine aurait dû dire "l'inverse". Je laisse au lecteur la liberté de réattribuer les deux rôles du professeur mal-entendant et du capitaine téméraire.

Shah d'Ock

Ltav a écrit:

Comme tout le monde fait en général, je suis parti d'une conviction originelle

C'est justement ce que je te reproche. Tout le monde ne fait pas ça, au contraire: la démarche scientifique consiste à partir d'un point où l'on ne sait pas et essayer d'acquérir un savoir à l'aide d'arguments rationnels. Et non, comme tu le fais, de partir d'une conviction et de chercher à la défendre par tous les moyens.

christophe c

Ltav a écrit:

je suis parti d'une conviction originelle sur l'inexactitude de certaines thèses sur le raisonnement par l'absurde, que j'ai ensuite exprimée et développée tout au long du débat. Il y a eu deux "épisodes" : le premier a été bouclé durant le dernier fil sur le RPA

(en gros, "sans TE, RPA = définition de non P [par P => tout]", "avec TE, RPA = démonstration de non P [par P => tout]").

Voilà pourquoi tu ne reçois plus de réponse. On pourrait mal le prendre. Ta phrase sous-entend que c'est ça qu'on t'a dit, nous et non ton slogan à toi (l'expression "a été bouclée" sous-entend qu'on a fini par rejoindre ta thèse bleue).

Non seulement ta thèse bleue "n'est pas vraie", mais en plus elle n'est "même pas fausse", elle ne veut juste rien dire du tout, ce ne sont pas des maths, tu n'énonces rien de mathématique. Je suis patient : je me répète!

<<sans TE, RPA = définition de non P [par P => tout]>>

n'a pas de sens!!! Tu es sur un forum de maths, ne te plains pas qu'on ne veuille pas forcément te donner un avis sur la poésie de ton expression, je ne prononce pas sur ladite poésie, peut-être as-tu des billes poétiques à faire valoir, je n'en sais rien.

Ltav

Bonjour,

Shah d'ock a écrit:

C'est justement ce que je te reproche. Tout le monde ne fait pas ça, au contraire: la démarche scientifique consiste à partir d'un point où l'on ne sait pas et essayer d'acquérir un savoir à l'aide d'arguments rationnels. Et non, comme tu le fais, de partir d'une conviction et de chercher à la défendre par tous les moyens.

Ton paragraphe conviendrait bien à un élève débutant en sciences. Je ne suis pas débutant en sciences. Ensuite, une conviction (celle du chercheur comme de l'élève) n'est pas forcément quelque chose d'irrationnel et d'ignorant. Ça peut être aussi à l'inverse un concentré de raison puissante, de créativité et d'expérience qu'il faut traduire en langage rationnel.

Cc a écrit:

Non seulement ta thèse bleue "n'est pas vraie", mais en plus elle n'est "même pas fausse", elle ne veut juste rien dire du tout, ce ne sont pas des maths, tu n'énonces rien de mathématique. Je suis patient : je me répète!

<<sans TE, RPA = définition de non P [par P => tout]>>

n'a pas de sens!!! [...]

On va arriver à une thèse bleue indécidable, c'est poétique aussi. Tu es assez mûr maintenant pour apprendre un grand secret Cc : tout ce que tu ne liras pas ou ne comprendras pas, n'aura pas de sens et ne voudra rien dire du tout. Telle est la dure loi de la connaissance. N'y vois pas qu'un "tautologisme" ou une simple remarque de bon sens (*).

(*) Je rappelle ce qui pour toi n'a toujours pas de sens :

Soit le raisonnement suivant ("RPA") : [Je veux montrer non P.] Je suppose P. Si j'arrive à l'absurde, alors j'en déduis non P.

Traduction en proposition logique :

(P => faux) $\vdash$ non P

En logique intuitionniste (sans tiers-exclu ou "TE"), on pose non P := (P => faux). Le "RPA" s'écrit donc aussi :

non P $\vdash$ non P.

C'est un axiome ou une définition, il n'y a plus déduction ou démonstration (avec ou sans "l'absurde").

Shah d'Ock

(...).
On peut soit considérer le symbole $\neg$ comme primitif et écrire les axiomes auxquels il est soumis, soit définir directement $\neg A$ comme $A \to \bot$.
Dans le premier cas, il découle des axiomes que $(\neg A ) \leftrightarrow (A \to \bot)$, et ce, tiers-exclu ou pas tiers-exclu.
J'ajouterai que le tiers-exclu est un axiome comme un autre, le fait de s'en servir ou pas ne change pas le reste du formalisme comme tu sembles le croire.

Shah d'Ock

Détail:
1) montrons que $\neg A$ implique $A \to \bot$.
Supposons $\neg A$. Supposons $A$. Alors $A \land \neg A$ donc $\bot$.
2) réciproquement montrons que $A \to \bot$ implique $\neg A$.
Supposons $A \to \bot$. Prenons la contraposée: $\top \to \neg A$. Donc $\neg A$.

Shah d'Ock

Et pour en revenir à la question initiale: la preuve que "$\sqrt{2}$ est rationnel" implique faux est une démonstration, je pense que tu ne vas pas nier cela?

Shah d'Ock

Ce qui semble te poser problème c'est l'application de la règle $\frac{A \vdash \bot}{\vdash A \to \bot}$, qui est un cas particulier de $\frac{A \vdash B}{\vdash A \to B}$, qui est une règle de déduction, ou si tu veux, "une convention".

Ltav

Bonsoir,

Merci de préciser comment tu montres 1) et 2) sans définir $\neg A$ par $A \longrightarrow \perp$ (donc hors logique intuitionniste).

Comme je l'ai déjà dit en long et en large, oui la preuve de "$\sqrt{2}$ rationnel implique faux" est une démonstration (en logique classique et intuitionniste), mais "$\sqrt{2}$ rationnel implique faux, donc $\sqrt{2}$ non rationnel" n'a pas de preuve en logique intuitionniste, où ce n'est ni un raisonnement, ni une argumentation, ni une démonstration, ni une déduction, mais une définition. On l'écrit :

$\sqrt{2}$ non rationnel := ($\sqrt{2}$ rationnel implique faux)

ou

$\sqrt{2}$ non rationnel $\vdash$ $\sqrt{2}$ non rationnel

La subtilité que plusieurs d'entre vous n'avez pas saisie est que la proposition :

Je prouve non P en supposant P et en en déduisant tout

est vraie en logique classique (il y a bien raisonnement et preuve), mais pas en logique intuitionniste où elle équivaut à :

Je prouve non P à partir de non P

puisque : J'ai défini non P par "supposer P et en en déduire tout"

Il faudrait dire tout simplement (toujours en L.I.) :

Je prouve non P

...et rien de plus.

N.B. Ce qui "m'embête" n'est donc pas exactement l'application de la règle $\frac{A \vdash \bot}{\vdash A \to \bot}$, mais de dire faussement que si j'en "déduis" non A au sens de la logique intuitionniste alors j'ai une preuve de non A.

Bonne nuit.

Shah d'Ock

Ltav a écrit:

Merci de préciser comment tu montres 1) et 2) sans définir $\neq A$ par $A \to \bot$

M'enfin?! J'ai tout détaillé. Pour 1) j'utilise que de $A \land \neq A$ je peux déduire $bot$, pour 2) le fait qu'une implication implique sa contraposée.

Ltav a écrit:

Comme je l'ai déjà dit en long et en large, oui la preuve de "$\sqrt{2}$ rationnel implique faux" est une démonstration (en logique classique et intuitionniste), mais "$\sqrt{2}$ rationnel implique faux, donc $\sqrt{2}$ non rationnel" n'a pas de preuve en logique intuitionniste,

Aussi long, aussi large que tu aies pu l'écrire, ça reste faux.

AD

Ltav
L'ouverture de la présente discussion ressemble fort à la réouverture d'une discussion fermée par la modération. http://www.les-mathematiques.net/phorum/read.php?16,1598534,1607628#msg-1607628
Cela est normalement passible de bannissement.
Je ferme donc ce fil. Toute tentative de réouverture d'une discussion semblable amènera à la sanction précitée.
AD.