Aller au contenu

Discussion utilisateur:ByteMe666

Le contenu de la page n’est pas pris en charge dans d’autres langues.
Une page de Wikipédia, l'encyclopédie libre.

Bienvenue sur Wikipédia, ByteMe666 !


Bonjour, je suis Bastenbas, et je vous accueille en tant que wikipédien bénévole.

Wikipédia est une formidable aventure collective, toujours en construction. La version francophone comporte aujourd'hui 2 646 989 articles, rédigés et maintenus par des bénévoles comme vous et moi. Vous allez y effectuer vos premiers pas : n’hésitez pas à me contacter si vous avez besoin de conseils ou d'aide pour cela, ou à laisser un message sur le forum des nouveaux. Une réponse vous sera apportée avec plaisir !

Wikipédia repose sur des principes fondateurs respectés par tous :

  1. Encyclopédisme et vérifiabilité (s'appuyer sur des sources reconnues) ;
  2. Neutralité de point de vue (pas de promotion) ;
  3. Licence libre et respect des droits d'auteurs (pas de copie ou plagiat) ;
  4. Savoir-vivre (politesse et consensus) ;
  5. N'hésitez pas à modifier (l'historique conserve tout).

Vous êtes invité(s) à découvrir tout cela plus en détail en consultant les liens ci-contre

Un livret d'aide à télécharger, reprenant l’essentiel à savoir, est également à votre disposition.

Je vous souhaite de prendre plaisir à lire ou à contribuer à Wikipédia.

À bientôt !

P.S. Vos nouveaux messages seront affichés en bas de cette page et signés par leur expéditeur. Pour lui répondre, cliquez sur sa signature (aide).
Bastenbas (discuter) 22 novembre 2017 à 10:04 (CET)[répondre]

Modus Ponens suite

[modifier le code]

Je vois vos interrogations. Le lien entre déduction et table de vérité est donné par le Théorème de complétude (calcul des propositions), soit : équivalence entre :

  • Aspect sémantique :
    • 1/ |= A --> B , "A -->B" est une tautologie = est une formule dont la table de vérité donne toujours le vrai.
    • 2/ A |= B, autre formulation : Toute distribution de valeur de vérité qui satisfait A, satisfait B.
  • Aspect syntaxique :
    • 3/ A |- B , De A on peut déduire B, par exemple par les règles de la déduction naturelle (2/ et 3/ sont équivalents par thm de complétude)
    • 4/ |- A --> B (équivalent à 3/ par le thm de la déduction déjà évoqué)

Maintenant, les tables de vérité sont la sémantique de la logique classique (avec tiers exclu et raisonnement par l'absurde), tandis que la sémantique de Kripke est la sémantique de la logique intuitionniste (dont parle plutôt Notification PIerre.Lescanne :), qui a donc aussi un théorème de complétude avec cette sémantique. En espérant avoir clarifié des choses. --Epsilon0 (discuter) 23 mars 2018 à 10:15 (CET)[répondre]

Notification Epsilon0 : Bonjour, merci pour votre réponse. Je suis allé voir un peu le cours de Pierre Lescanne , il m'a redirigé vers ses notes de cours. J'ai lu les deux premiers powerpoints, alors à force de relectures les choses s'éclaircissent, mais je suis encore en train de patauger. Je vous remercie en tous cas de bien souligner qu'il faut savoir distinguer sémantique et syntaxique, car, bien que je n'ai pas tout de suite compris ce que cela voulait dire, j'ai poursuivi mes lectures avec bien en tête comme objectif d'apprendre à distinguer ces deux choses. Là, je vais regarder votre lien sur la complétude. Dans l'état où je vous écris, je crois comprendre que la logique classique, édifiée par exemple avec une approche à la Hilbert, avec suffisamment d'axiomes, de connecteurs, et de règles de déduction, permet de prouver de manière syntaxique que ¬¬A⇒A (ou on peut quasiment le poser en axiome aussi, je crois qu'il y a plusieurs façons de faire), ce qui impose la sémantique {0,1} (ou encore {Vrai,Faux})?... J'ai l'impression que syntaxique et sémantique sont liées mais pas complètement. Par exemple je crois qu'un des résultats remarquables des notes du deuxième cours de Pierre Lescanne est qu'en logique minimale (seulement modus ponens et axiomes K et S), la loi de Pierce est valide classiquement (dans la sémantique {0,1} avec l'interprétation habituelle de ⇒), mais n'est pas un théorème de la logique minimale. De ce résultat je comprends qu'il est possible d'utiliser la sémantique {0,1} en logique minimale, mais alors elle est incomplète. La logique classique et la sémantique {0,1} sont compatibles et (je crois mais je vais lire pour en être sûr) la logique classique est complète pour ce modèle. Et enfin, la logique intuitionniste et la sémantique {0,1} sont incompatibles, car d'après l'article wikipédia sur l'implication, la logique intuitionniste donnerait à ⇒ une infinité de valeur de vérité (je ne sais pas ce que ça veut réellement dire, mais en tous cas j'en comprends qu'on ne peut pas faire de la logique intuitionniste avec la sémantique {0,1}). Il y a donc des sémantiques qui «fonctionnent» ou non avec différentes logiques, et si elles fonctionnent, il faut ensuite voir si on a complétude.
Maintenant, j'essaye de dépiauter tout ce que je viens de raconter pour voir si je n'ai pas dit de bêtises, et je vais surtout essayer de savoir exactement comment la syntaxe de la logique classique conduit à figer la sémantique sur {0,1}, et enfin essayer de vraiment comprendre s'il y a un sens profond entre ce que je ressens intuitivement dans mon esprit et que j'appelle la «causalité», et la table de vérité de ⇒.

Notification Epsilon0 :Notification PIerre.Lescanne :Bonjour, Je voulais vous remercier pour vos aides et indications ces derniers temps. J'ai fait pas mal de lectures encore hier, mais je n'arrive pas aboutir à une vue d'ensemble satisfaisante et bien distinguer les choses. J'ai notamment essayé de comprendre ce qu'était un modèle (d'où provenait {0,1}, ou la sémantique de Kripke), comment savoir si un système de déduction a un modèle qui vérifie ses axiomes (théorème de complétude), et si le théorème de complétude assure qu'un tel modèle existe, alors quel est il ? etc etc. Et je me suis retrouvé à me perdre dans des notions de plus en plus complexes que je comprenais de moins en moins. D'ailleurs, les articles liés à la notion de modèle avaient recours à des ensembles dénombrables de symboles, notions qui me semblent avoir du sens en théorie des ensembles, or j'ai cru comprendre que la théorie des ensemble est édifiée à partir de logique, donc je me suis retrouvé à me sentir comme perdu dans une histoire de serpent qui se mord la queue, et ne comprenais plus comment on peut parler de système de déduction, modèles, langages, en manipulant des notions de théorie des ensembles, quand on essaye de poser la logique même sur laquelle repose la théorie des ensembles. Il doit y avoir une subtilité de distinction de méta-mathématiques et de mathématiques qui m'échappe. En bref, je renonce pour l'instant, sinon il faut que je mette une halte à ma vie et me consacre à trouver la vérité sur ces notions, mais comme j'ai d'autres projets, ne suis pas chercheur dans le domaine et n'ai pas de mécène, ni ne suis pas un riche hériter, je dois accepter momentanément de faire l'impasse. Éventuellement je consulterai à l'occasion un des bouquins de référence recommandés dans les slides de M. Lescanne. J'ai tout de même eu la satisfaction momentanée d'avoir l'impression de très bien comprendre que (A⇒B)⇒(¬B⇒¬A) et (¬B⇒¬A)⇒(A⇒¬¬B) en logique intuitionniste et minimale, et que cette affirmation très utile (A⇒B)⇔(¬B⇒¬A) que je manipule tout le temps dans mes modestes activités mathématiques n'est valable qu'en logique classique, c'est à dire avec réduction à l'absurde. Autre satisfaction de ces moments d'errements à travers wikipedia: comprendre que dans un contexte intuitionniste, tiers exclu, annulation de la double négation et loi de Pierce sont équivalents, et se déduisent toutes de la réduction à l'absurde. Je suis donc un peu content de ressortir de cette aventure en ayant compris que ces différents modes de raisonnements que j'utilise depuis longtemps sont liés, de savoir aussi qu'ils sont indépendant du modus ponens. En gros, j'ai effleuré la compréhension de certaines choses qui me permettent maintenant de distinguer un peu mieux les mécanismes du raisonnement. Je vous remercie en tous cas pour vos réponses et aiguillages, et je vous recontacterai peut-être vers la fin de l'année, lorsque je me pencherai à nouveau sur ce genre de questions, pour l'heure, j'ai des priorités et échéances de la vie qui m'obligent à suspendre mes réflexions ! Salutations.

Petit remarque préliminaire: savoir si un système de déduction a un modèle qui vérifie ses axiomes n'est pas la complétude mais la correction. --Pierre de Lyon (discuter) 2 avril 2018 à 15:39 (CEST)[répondre]
Je suis en tout cas très satisfait de voir que vous avez compris beaucoup de choses comme vous le démontrez: modèle -- déduction, logique classique -- logique intuitionniste. Vous êtes sur la bonne piste. Dès que vous serez à nouveau disponible, je vous expliquerai comment sortir de cet apparent cercle vicieux que vous décrivez très bien, il n'y a pas un longue étape à franchir, quoique ce problème ait perturbé les logiciens du XIXe siècle. --Pierre de Lyon (discuter) 2 avril 2018 à 15:47 (CEST)[répondre]