Discussion:Calcul des propositions

Bonsoir

Si il y a un peu plus simple, je et sans doute beaucoup de non spécialiste seront preneurs !!

Pourtant je pensais connaitre pas trop mal l'électronique numérique. Mais là j'avoue que je suis complètement largué! Est ce les nouvelles bases ??

C'est un point de vue logicien et mathématicien sur la chose, il y a trois articles sur la même chose qu'il faudrait fusionner (va voir sur ma page perso). On pourrait rajouter des images (VF et VO) des portes logiques. ℓisllk 21 fév 2004 à 19:54 (CET)

Quatre avec Fonction logique ! ℓisllk 21 fév 2004 à 20:01 (CET)

Pour un point de vue de mathématicien, c'est du pur jus. Enfin de ce que connais des maths. Pour le reste, j'ai fouillé un peu et, j'ai trouvé quelques articles connexes plus en phase avec mes connaissances. Vous avez toute notre confiance pour arranger au mieux les relations inter-articles dans ce sujet. Utilisateur:Pulsar 21 fév 2004 à 22:58 (CET)

Je ne sais pas ou mettre ce lien, qui me semble intéréssant, mais peut-être un peu hosr sujet pour cete page. http://www.inria.fr/valorisation/applications/preuve.pdf

Au fait, c'est quoi le "problème de l'implication" dont il est fait mention dans l'article. Je veux bien que les stoïciens soient les premiers à y avoir répondu, mais j'ai beau chercher : il n'y a pas une seule fois le mot "implication" dans la page stoïcisme.

Soit dit en passant, je n'aime pas cet article. C'est une bonne chose de voir la logique prépositionnelle sous une forme épistémologique, mais ça ne suffit pas à se faire une idée (idée simple et concise, je veux dire) sur la question. Par exemple, il manque une définition formelle par une grammaire des propositions, un système de déduction et une sémantique formelle (donnée d'une relation d'équivalence sémantique ... en fait une manière de faire serait de dire que la sémantique d'une proposition c'est sa table de vérité), qui permettraient une compréhension immédiate à tout lecteur de culture scientifique. De plus la moitié de cet article n'est constitué que de considérations générales sur la logique qui seraient par exemple aussi bien valables pour le calcul des prédicats que pour le calcul des propositions. Non décidément ... quelque chose me dérange, sans que j'arrive à vraiment mettre le doigt dessus.

Sinon, y a-t-il une raison d'utiliser le terme "foncteur" pour parler des opérateurs logiques ? Je n'ai jamais vu utiliser ce terme dans le contexte de la logique en dehors de cet article.

Fin de gueulante, merci ;-) --Aldoo / ✉ 31 déc 2004 à 12:02 (CET)

L'article Stoïcisme est cours de rédaction, merci de patienter. Cet article est issu d'un cours de logique, fait par un professeur reconnu dans son domaine. Les considérations générales permettent d'introduire la formalisation ; un lecteur non scientifique peut ainsi comprendre plus facilement de quoi il retourne. D'autres part, il ne suffit pas de donner des définitions : les considérations "générales" sont une interprétation de la logique, un méta langage. On ne peut établir la sémantique de ces symboles sans produire une explication de leurs utilisations (par exemple, pour l'implication). Cela ne peut donc être réduit simplement à l'épistémologie, puisque tout cela fait partie de la logique. Sinon, toutes les sections ne sont pas encore développées et le terme foncteur existe. Caton 31 déc 2004 à 12:21 (CET)

Je partage le point de vue de Aldoo. L'article souligne qu'en calcul des propositions, il y a un aspect syntaxique et un aspect sémantique. Or ces deux aspects ne ressortent pas. Il conviendrait donc de rédiger :

• un paragraphe sur la syntaxe et sur un aspect axiomatique du calcul des propositions
• un paragraphe sur la sémantique (en gros les tables de vérité). Il suffit de déplacer certains passage du paragraphe Foncteurs.
• un paragraphe sur l'équivalence entre les deux aspects et sur la complétude du calcul des propositions.

Theon 5 janvier 2006 à 09:41 (CET)

Et la logique intuitionniste?

Je ne pas sûr que, en 2006, on puisse faire l'impasse sur la logique intuitionniste (sans parler de la logique linéaire) quand on parle de calcul des propositions. En effet à travers la correspondance de Curry-Howard son lien avec l'informatique est si fort qu'on ne peut pas l'ignorer. Je vous invite pour cela à voir l'article logique mathématique. Or cet article (calcul des propositions) se place d'emblée en logique classique, sans états d'âme. Je pense qu'il faudrait avoir une attitude moins péremptooire.

D'autre part, je pense qu'une coordination avec les articles logique mathématique, logique intuitionniste et logique classique (et pourquoi pas logique linéaire?) serait plus constructive :-). Je n'ai aucune idée préconçue sur le sujet et je ne suis pas opposé à plusieurs niveaux de lecture, bien au contraire, mais s'il me semble qu'il faille se coordonner.

Pierre de Lyon 6 janvier 2006 à 09:02 (CET)

Je suis tout à fait d'accord sur le fait de signaler que l'article se place dans le cadre de la logique classique en ajoutant un paragraphe précisant qu'il existe d'autres logiques avec un lien vers la logique intuitionniste, mais je ne pense pas qu'on puisse développer les aspects de la logique intuitionniste à l'intérieur du présent article car il y a beaucoup de choses à dire sur la logique intuitionniste qui dépasse le calcul propositionnel, par exemple, le sens à donner au symbole d'existence. Theon 6 janvier 2006 à 09:23 (CET)

C'est aussi mon point de vue bien sûr. Ceci l'existence fait partie du calcul des prédicats, on pourrait ne parler déjà que du rejet du tiers exclus qui n'est pas rien.Pierre de Lyon 6 janvier 2006 à 09:29 (CET)

Bibliographie

Je pense que ça n'est pas judicieux de citer comme livres de référence le livre de Robert Blanché Introduction à la logique contemporaine - 1957, ed. Armand Colin, coll Cursus, 205p. et celui de Quine 1980 (1941). Elementary Logic; Harvard University Press. (ISBN 0674244516). An introductory text. soit un livre de 1957 et un livre de 1941 à un moment où la logique est en train de vivre l'une de ses plus fantastiques révolutions depuis Aristote, sauf à indiquer leur intérêt historique et à citer un vrai livre de «logique contemporaine» comme par exemple R. David, K. Nour et C. Raffalli Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés (2001).

Pierre de Lyon 6 janvier 2006 à 09:25 (CET)

tout à fait d'accord. Theon 6 janvier 2006 à 12:53 (CET)

Logique intuitionniste

J'ai rajouté le paragraphe de logique intuitionniste. Bien que succinct, j'espère qu'il fait bien comprendre le problème posé par le tiers exclu et pourquoi une mathématique constructiviste a ses raisons d'être. Theon 7 janvier 2006 à 12:04 (CET)

C'est très bien. J'ai fait quelques corrections. Dis-moi si tu es d'accord. De toute façon le renvoi à l'article logique intuitionniste permet (ou permettra quand il sera complet) de trouver les compléments attendus.

Pierre de Lyon 10 janvier 2006 à 09:13 (CET)

---

Bonjour,

Je suis très d'accord avec les remarques de Aldoo ci-dessus. Cet article manque de concision et est plutôt confus. Par exemple on y introduit les logiques plurivalentes dans la section vocabulaire fondamental pour n'en plus jamais faire mention, un peu bizarre pour un concept présenté comme fondamental. De plus il y manque un certain nombre de points clefs : lien avec les algèbres de Boole, théorème de compacité, NP-complétude de la satisfiabilité.

Enfin bref, je vais y faire des modifs.

Laurent de Marseille 11 janvier 2006 à 22:22 (CET)

Le paragraphe Vocabulaire fondamental devrait en effet être repris, en éliminant les notions qui ne sont pas utilisées dans l'article, par exemple, logique monovalente, logique plurivalente. S'il s'agit de créer des liens vers l'algèbre de Boole, ou le théorème de compacité, pourquoi pas. S'il s'agit de développer ces notions l'intérieur de cet article, je ne suis pas sûr que cela le rende plus concis :-). Un lien vers la NP-complétude existe dans le paragraphe Méthodes de calcul. Theon 12 janvier 2006 à 08:12 (CET)

Le lien sur la NP-compétude m'avait en effet échappé, mais il est trop discret s'agissant de l'un des résultats fondamentaux autour du calcul propositionnel et en théorie de la complexité. Je ne tiens pas à allonger l'article, plutôt à le raccourcir, mais il faut quand même ajouter une section sur les résultats principaux avec des liens (à la réflexion je ne suis pas très sûr que le théorème de compacité soit vraiment important à mentionner).

Il y a également un paragraphe à faire sur l'historique du calcul des propositions, peut-être même un article ; c'est très joli de dire que le CP hérite de la logique stoïcienne mais il faudrait expliciter un peu (je suis incompétent sur le sujet).

Laurent de Marseille 12 janvier 2006 à 11:22 (CET)

Moi aussi. Se pose d'ailleurs la question de savoir s'il convient de laisser le paragraphe sur l'implication dans la logique stoïcienne, qui pointe vers un article sur le stoïcisme, lequel possède un paragraphe vide sur la dite implication. L'auteur de ce passage avait probablement une idée en tête, mais laquelle ? Theon 12 janvier 2006 à 13:31 (CET)

Pour une méthodologie

Nous sommes trois à vouloir refondre cet article: Theon, Laurent de Marseille et moi Pierre de Lyon. Je propose que nous entendions dans un premier temps sur une structure et que dans un deuxième temps nous nous partagions les sections à (ré)écrire.

A moins qu'il y ait d'autres volontaires.

Pierre de Lyon 25 janvier 2006 à 15:50 (CET)

Je trouve que l'introduction générale devrait être réécrite, axée plutôt sur l'aspect mathématique. L'aspect philosophique me paraît mieux placé dans un article logique en général que dans calcul des propositions. En particulier, je proposerais volontiers la suppression de la partie la question de l'implication.

Le paragraphe vocabulaire fondamental est-il nécessaire ? Les notions utilisées ne peuvent-elle être définies au moment où on les introduit ?

La partie méthode de calcul ne me paraît pas soulever assez la difficulté à évaluer une formule du calcul propositionnel. Peut-être peut-on le réécrire en développant davantage l'aspect NP-complet.

La partie foncteur logique apporte-t-elle vraiment grand chose ? Ne peut-on l'abréger ?

Par contre je serais d'avis de maintenir une structure de l'article basée sur aspect syntaxique, aspect sémantique (dans un ordre ou dans l'autre), équivalence entre les deux, NP-complétude, logiques non classiques.

Theon 26 janvier 2006 à 09:52 (CET)

Je suis d'accord avec les propositions (sur le calcul des propositions, hi, hi !) de Theon. Une fois que l'on s'est mis d'accord sur la structure je pense qu'il est mieux que un seul d'entre nous agisse sur l'article (sans contrainte temporelle), plutôt que de se partager les sections, ça assurera plus facilement la cohérence d'ensemble. J'ajoute que je préférerais ne pas être l'acteur en question (j'aime mieux faire l'inspecteur des travaux finis, hi, hi !) mais que je le ferai si personne d'autre ne s'y colle.

En ce qui concerne le plan je vous soumets la proposition (encore une proposition, décidément...) suivante qui détaille celle de Theon. Ça serait bien que nous nous mettions d'accord car une fois qu'on aura un beau plan bien propre on pourra l'appliquer à d'autres articles (par exemple calcul des prédicats) :

• chapeau introductif court
• historique (optionnel)
• définition du système
  • les formules
  • la prouvabilité (on n'est pas obligé de mettre ici un système formel complet, on peut renvoyer à un article existant comme déduction naturelle ; par contre on peut faire apparaître ici certaines des formules prouvables caractéristiques du système logique considéré (par exemple le tiers-exclus pour le calcul propositionnel)
  • la sémantique
• variantes : par exemple la variante intuitionniste du calcul propositionnel
• résultats principaux (avec sous-sections si nécessaire, par ex pour calcul des propositions une sous-section pour la complétude relativement aux algèbres de Boole, une autre pour la NP-complétude)
• références

Laurent de Marseille 27 janvier 2006 à 12:51 (CET)

Je suis d'accord avec les «déclarations» de Théon et Laurent et donc le plan proposé. Je proposerais qu'on montre aussi que la logique (comment s'appelle-t-elle?) qui est l'intuitionniste plus $(p\Rightarrow q)\vee (q\Rightarrow p)$ se trouve strictement incluse entre l'intuitionniste et la classique.

Elle n'a pas de nom que je sache ; en fait je crois (à vérifier quand même avant de le mentionner) qu'il y a une suite infinie T_1, ... T_n, ... de tautologies classiques de ce genre telle que T_{i+1} est conséquence intuitionniste de T_i pour tout i mais par la réciproque. Ce qui entraîne qu'il y a une infinité de logiques de plus en plus fortes comprises entre les logiques intuitionniste et classique. Étonnant non ?

Il s'agit, me semble-t-il des logiques $(p_{1}\Rightarrow p_{2})\vee (p_{2}\Rightarrow p_{3})...\vee (p_{n}\Rightarrow p_{1})$ et on les caractérise par leurs modèles de Kripke: linéaire (-: pas au sens de Girard) pour les premiers et de plus en plus «large». Comme ça on montre qu'il n'y a pas que la logique intuitionniste et la logique classique.Pierre de Lyon 28 janvier 2006 à 12:17 (CET)

Je peux poursuivre la remise en forme de l'article entreprise depuis quelques temps pour approcher du modèle ci-dessus défini. Par contre, je ne suis pas compétent pour rédiger une partie historique. Theon 30 janvier 2006 à 13:34 (CET)

Logique bivalente

A proprement parler, ça n'est pas logique qui est bivalente, mais la sémantique. Je pense qu'il faut bien différencier ce qui

1. syntaxe,
2. système de déduction (règles),
3. sémantique.

{0,1} est un modèle ou une sémantique. On peut aussi considérer des modèles de Kripke comme sémantique.Pierre de Lyon 30 janvier 2006 à 15:58 (CET)

Pierre, dans l'intro, tu mets qu'il y a trois points de vue (syntaxique, déductif ou sémantique), et non plus deux. Je crois qu'il y a deux sens du mot syntaxique dans l'article, la syntaxe au sens de formation des formules, et syntaxe au sens de déduction. Le premier sens n'est pas vraiment un aspect du calcul propositionnel. Ce n'est que la définition de l'orthographe qui est utilisée, que ce soit d'ailleurs en logique classique ou intuitionniste. Pour le deuxième sens, je suis d'accord de lui substituer le mot aspect déductif et de faire disparaître le mot syntaxique lorsqu'il est pris au sens de déductif. Par contre, à l'intérieur de l'aspect déductif, il y a deux sous-aspects, celui des systèmes de Hilbert (concis mais peu praticables) et celui de la déduction naturelle, qui, comme son nom l'indique, et plus naturelle. Je pense qu'il conviendrait donc :

• dans l'intro, de revenir aux deux points de vue, le déductif et le sémantique.
• de déplacer la phrase «Cependant à la suite, par exemple, de Christopher Strachey ironisant sur le sucre syntaxique, les logiciens accordent de moins en moins d'attention à la syntaxe pour se consacrer au fond des choses: la déduction et la sémantique» dans le paragraphe sur les systèmes de déduction, après le mot concis. Que penses-tu d'une reformulation telle que :

«On donne ici une définition inspirée des systèmes à la Hilbert qui a l'intérêt d'être concise. Ces systèmes sont cependant d'une manipulation peu aisée. Aussi, à la suite par exemple de Christopher Strachey qui ironise sur le sucre syntaxique, les logiciens accordent de moins en moins d'attention à ce type de traitement purement symbolique pour se consacrer au fond des choses : la déduction proprement dite et la sémantique. Pour un système de déduction plus proche des raisonnements habituels, on se reportera à l'article dédié à la déduction naturelle.» ?

Je suis d'accord. Mon souci était de ne pas enlever du texte, j'ai donc été conduit à en ajouter. Mais dans le fond, je suis parfaitement d'accord il y a deux aspects: le déductif (théorie de la démonstration) et le sémantique (théorie des modèles) et nous n'avons pas à trop nous intéresser à la syntaxe, sinon à son strict minimum pour savoir de quoi on parle.

En revanche, je ne suis pas sûr que ta formulation me va. Quand Strachey ironisait sur la syntaxe, il visait le fait de savoir si on mettait une virgule ici, une parenthèse là. Hilbert vs deduction naturelle vs calcul des séquents, ça relève de la déduction, ou si on préfère de la théorie de la démonstration, et pas de la syntaxe. Pierre de Lyon 1 février 2006 à 13:04 (CET)

Mais dans ce cas, je ne saisis pas bien l'ironie de Strachey. La syntaxe du calcul propositionnel dans l'article se borne à définir ce qu'est une formule. Je ne vois pas comment on peut se passer d'une telle définition, ou alors, on ne fait plus de calcul propositionnel. Ou alors, la phrase fait allusion à des développements qui ne sont pas dans l'article. Le fait d'ailleurs que j'ai mal interprété la phrase de Strachey montre qu'on ne voit pas très bien ce qu'elle veut dire.Theon 1 février 2006 à 15:11 (CET)

La référence à la formule de Strachey vise le fait qu'il n'est pas très intéressant de savoir si on note les formules avec des opérateurs infixes et des parenthèses ou si on utilise une notation polonaise. L'un ou l'autre choix sont différentes manières de sucrer sa syntaxe ;les uns préféreront la première, les autres la seconde, sans que cela ne change grand chose au calcul propositionnel. Il est beaucoup plus intéressant de dire que les formules ont une structure d'arbre, quelle que soit la façon dont on les note. Mais si tu trouves la phrase pas assez claire tu as raison il faut la corriger.

D'autre part je suis d'accord avec Pierre, ça n'a rien à voir avec l'opposition système de Hilbert/déduction naturelle : il s'agit là de deux systèmes ayant des structures très différentes. Et à ce propos j'ajoute qu'il ne faudrait pas laisser le lecteur croire que ce sont les deux seuls systèmes : il y en a bien d'autres à commencer par le calcul des séquents.

Laurent de Marseille 2 février 2006 à 00:42 (CET)

Effectivement, que l'on présente telle ou telle syntaxe, cela n'est pas très intéressant. Dans ce cas, ne faut-il pas supprimer le passage sur la notation préfixée, en le déplaçant dans un article spécifique (par exemple un article sur Lukasiewicz) ? Sur les systèmes de déduction, l'article ne fait pas référence à deux systèmes, mais bien à trois : les systèmes de Hilbert, la déduction naturelle, le calcul des séquents. A ce propos, je me demande si le paragraphe "autres axiomes possibles" est d'un grand intérêt ici, et ne serait pas mieux placé précisément dans l'article système de Hilbert qui, d'ailleurs, n'existe pas encore. Theon 2 février 2006 à 08:12 (CET)

Oui c'est parmi mes projets de le créer mais en ce moment je suis un peu surchargé.

Laurent de Marseille 2 février 2006 à 23:08 (CET)

Je suis d'accord avec la discussion ci-dessus. Pierre de Lyon 3 février 2006 à 10:08 (CET)

J'ai essayé de m'approcher du mieux possible du plan défini plus haut, et je pense le moment venu de passer la main. Les points suivants pourraient être améliorés.

• L'introduction générale 1- est un peu verbeuse. Il faudrait la remanier, peut-être introduire un paragraphe historique.
• Le paragraphe 2-6 "foncteurs logiques", provenant de l'article initial est là comme un cheveu sur la soupe. Je ne sais pas trop qu'en faire : le supprimer ? le déplacer dans le paragraphe algèbre de Boole de cette page ? le déplacer dans l'article algèbre de Boole ?
• Les paragraphes 3-3 compacité et 3-4 algèbre de Boole sont squelettiques. Il faudrait ou bien les développer, ou bien les supprimer.
• Autres logiques 4-. A développer également ou pas ?

Theon 3 février 2006 à 18:52 (CET)

Je vais reprendre un peu la main. Pierre de Lyon 3 février 2006 à 19:34 (CET)

Merci Theon, c'est du super boulot. Désolé de n'être pas très actif en ce moment, ça va revenir d'ici un mois j'espère.

Laurent de Marseille 4 février 2006 à 13:22 (CET)

Bilan provisoire

Je clos le fil précédent qui commençait à s'allonger inconsidérément. Après le travail de Theon qui a considérablement fait progresser le schmilblik, voici quelques remarques en guise de bilan.

• Je pense que Theon est trop scrupuleux et que l'on peut supprimer les foncteurs logiques. Si je comprends bien, le terme foncteur logique est un nom pompeux pour ce qu'on appelle d'habitude une fonction booléenne ; le sujet a déjà un article et n'entretient qu'un rapport indirect avec le calcul propositionnel donc n'a pas sa place ici. Les cinq premiers paragraphes de l'introduction générale ne me semblent pas essentiels non plus, je n'aime en général pas les explications de nature linguistique de la logique mathématique, mais j'admets que ce point de vue est discutable.

Je vais le faire. Pierre de Lyon 4 février 2006 à 16:48 (CET)

• Et puisque nous en sommes à l'introduction, j'en profite pour revenir à la question au début du fil précédent à propos de la phrase « il est possible de considérer le calcul des propositions de trois points de vue syntaxique, déductif ou sémantique » ; je ne formulerais pas les choses exactement comme ça, je dirais plutôt, en suivant la section Logique mathématique#Système logique, que le calcul propositionnel est formé de trois composantes : 2 syntaxiques (formules et déductions) et 1 sémantique.

Ca me convient. Pierre de Lyon 4 février 2006 à 16:48 (CET)

• Enfin je n'aime pas (mais là aussi j'admets que mon point de vue est discutable) que l'on présente la sémantique comme le fait de définir le sens d'une formule, car cela ne fait que déplacer le problème du sens. Je préfère en général parler d'interprétation des formules dans des structures mathématiques préservant certains invariants (voir encore la section Logique mathématique#Système logique).

Je partage ce point de vue. Mais je pense que l'on explique souvent de cette manière dans une introduction parce que le mot «sémantique» fait savant et fait peur alors que le mot «sens» est plus facilement accepté. Mais en fin de compte c'est bien d'une représentation dans un structure mathématique «connue» qu'il s'agit.Pierre de Lyon 4 février 2006 à 16:48 (CET)

Laurent de Marseille 4 février 2006 à 13:47 (CET)

Hilbert vs déduction naturelle

C'est amusant, nous écrivons

On donne ici une définition inspirée des systèmes à la Hilbert qui a l'intérêt d'être concise.

tandis que la version anglaise écrit:

For simplicity, we will use a natural deduction system.

Pour des raisons de simplicité, nous utilisons un système de déduction naturelle.

Pierre de Lyon 6 février 2006 à 09:17 (CET)

Correct vs cohérent

Il fallait bien mettre correct. J'ai donc rétabli correct à la place de cohérence. En effet, la cohérence n'est pas la correction et la correction est une propriété importante. En anglais on dit sound et soundness donc sain et santé, mais je me vois pas parler de la santé d'un système. Donc comme beaucoup j'ai adopté correction Pierre de Lyon 22 février 2006 à 09:29 (CET)

ensemble de symboles _dénombrable_

J'ai rajouté que l'ensemble des symboles est supposé dénombrable, généralement. --Johanneshuisman 24 février 2006 à 10:11 (CET)

prouvabilité

La définition de preuve se mordait un peu la queue. J'ai remodelé un peu ce paragraphe. Par contre, je ne suis pas sûr si le français est impec. Johannes Huisman 27 février 2006 à 11:20 (CET)

Exemples de théorème

Ajout du lien vers la page "lois de De Morgan" que je rédige actuellement Léna 10 mai 2006 à 10:40 (CEST)

Modifications diverses

J´ai tenté d´apporter quelques modifications à l´article:

1. j´ai modifié la définition d´une proposition;
2. j´ai donné une définition du terme calcul car un article sur le calcul des propositions doit au moins donner une définition à peu près satisfaisante;
3. j´ai mentionné Frege dans l´introduction car c´est tout de même lui qui a refondé la logique propositionnelle et j´ai introduit un hyperlien vers l´article Frege;
4. J´ai déplacé le passage sur les "jeux des connecteurs" car il n´avait pas sa place dans "Principales propriétés du calcul propositionnel";
5. Dans "Structure du calcul des propositions" j´ai refait le passage sur la syntaxe.

J´espère que mes apports seront utiles.

Apierrot 26 juin 2006 à 20:48 (CEST)

Encore deux mots:

1. Au cours de mes modifications j´ai été amené (de rares fois) à supprimer une version précédente. Non pas que je les tenais pour fautifs mais je voulais éviter les répétitions.
2. J´ai pratiqué de nombreux déplacements afin de donner un peu plus de cohérence au tout.
3. J´aurais une demande: est-ce qu´on ne pourrait pas ajouter un passage montrant l´importance du calcul des propositions (pour la philosophie et pour les maths tout particulièrement)? En ce qui concerne la philosophie j´ai pensé intégrer ceci

L'importance du calcul des propositions

"L´importance du calcul des propositions pour les différentes sciences (humaines ou sciences « dures ») est immense. C´est en effet lui qui détermine les règles d´induction d´une propositions à partir d´une autre. Il est donc essentiel pour celui qui dans n´importe quel domaine théorique veut déduire correctement une proposition à partir de certaines prémisses. Dans le domaine des sciences humaines, c´est néanmoins la philosophie et tout particulièrement la philosophie analytique qui semble avoir accordé le plus d´importance au calcul des propositions et à la logique mathématique.".

J´attends votre avis.

Apierrot 27 juin 2006 à 16:46 (CEST)

Ça me parait pertinent et semble refléter mes cours rasoir d'IA :) Manproc 28 juin 2006 à 13:21 (CEST)

ca veut dire quoi? on garde ou on jette ce nouveau paragraphe? Apierrot 28 juin 2006 à 14:48 (CEST)

Je constate que la partie sur les "formes normales" a disparu. Ça ne me choque pas plus que ça (je n'avais pas passé mon après-midi dessus) mais c'est une information que je n'avais pas trouvé ailleurs et qui est indispensable dans un autre article (Théorème de Cook), ce pourquoi je l'avais ajouté ici, l'article me paraissant l'endroit le plus apte à recevoir cette information. A-t-elle été déplacé sur un autre article ? Manproc 28 juin 2006 à 13:31 (CEST)

C´est bien que tu mentionnes la passage sur les formes normales. En fait je l´ai effacé mais je voulais le réintégrer dans un chapitre sur l´évaluation des lois à part plus tard, lequel chapitre mériterait un approfondissement. Si tu veux réintégrer tes remarques sur les formes normales (dont il faut effectivement parler dans cet article), tu peux le faire, je suis tout à d´accord avec toi. J´espère que tu n´as pas mal pris mon effacement (un peu rapide, je l´admets). Amicalement

Pierre

Apierrot 28 juin 2006 à 14:48 (CEST)

PS: puis-je t´indiquer qu´il existe désormais un Portail de logique si cela t´intéresse.

Non non, je ne suis pas vexé :). Je vais tâcher de réintégrer ça dans la partie "Syntaxe du calcul des propositions".

oui, mais le procédé d´évaluation de Helbrand mérite lui aussi qu´on explique ce qu´est qu´une forme normale: tu pourrais y travailler? Apierrot 28 juin 2006 à 15:42 (CEST)

À ce propos, je me demande s'il ne faudrait pas découper un peu tout ça dans l'objectif de rendre l'information plus accessible.

d´accord: je viens de le faire même. Apierrot 28 juin 2006 à 15:42 (CEST)

J'entends par exemple faire une sous-partie pour les opérateurs, une pour les variables, une pour les expressions histoire de les faire apparaitre dans le sommaire. Ainsi il sera plus facile de faire référence à un « mot clé » dans un autre article. L'article en l'état est très bon mais nécessite de tout lire pour acquérir des notions élémentaires. J'avoue également que je n'ai pas tout relu, cette remarque concerne donc essentiellement la partie "Syntaxe du calcul des propositions". Pour le portail logique c'est une bonne idée, je vais jetter un oeil. Manproc 28 juin 2006 à 15:14 (CEST)

Je ne suis pas pour cette phrase

Je suis réticent à l'ajout d'une phrase sur l'importance du calcul des propositions pour deux raisons.

• Je l'ai déjà mentionné, cet article insiste trop sur la logique classique, or on sait que le calcul des propositions classique n'est qu'un calcul de propositions parmi d'autres, il y a, en effet, le calcul des propositions minimal, le calcul des propositions intuitionniste, les calculs de propositions modaux, sans oublier la calcul des propositions linéaire.
• Le calcul des prédicats (les calculs des prédicats) est (sont) probablement plus important(s) pour les différentes sciences que le calcul des propositions.

En fait c'est bien la logique, toute la logique, qui est importante pour les différentes sciences.

Pierre de Lyon 28 juin 2006 à 18:15 (CEST)

Je vous suis. Vous ne pourriez pas retravailler le petit paragraphe que je propose afin d´intégrer

vos remarques?

Apierrot 28 juin 2006 à 18:31 (CEST)

Voici une proposition sans prétention.

Le calcul des propositions occupe une place clé dans les différentes sciences qu'elles soient sciences humaines ou sciences « dures ». C´est en effet lui qui identifie des règles correctes de déduction d'une proposition à partir d'autres. Il est donc essentiel pour celui qui dans n´importe quel domaine théorique veut assoir ses raisonnements déductifs sur des bases saines et solides. Dans le domaine des sciences humaines, c´est la philosophie et tout particulièrement la philosophie analytique qui semble avoir accordé le plus d´importance au calcul des propositions et à la logique mathématique.

Pierre de Lyon 29 juin 2006 à 09:54 (CEST)

Refonte partielle de l´article?

Est-ce qu´on pourrait pas retravailler l´article afin d´intégrer les remarques de Pierre de Lyon sur le fait que l´article se concentre sur la logique des propositions traditionnelle? cette demande s´adressant naturellement tout particulièrement à Pierre de Lyon.

Apierrot 28 juin 2006 à 18:42 (CEST)

Dans une discussion précédente, nous avions convenu que cet article introduisait sommairement au calcul des propositions en se focalisant sur le calcul des propositions classique avec des renvois sur les autres articles pour ceux qui voudraient en savoir plus.

En revanche, il faut éviter dans ce texte de prêcher pour la primauté absolue de la logique classique.

(-: A noter que je baigne en pleine contraction, car dans un autre contexte, je m'intéresse actuellement à une certaine réhabilitation de la logique classique, qui ne peut se comprendre que si on connaît la logique linéaire et la logique intuitionniste.

Pierre de Lyon 28 juin 2006 à 19:08 (CEST)

J'ai terminé une refonte de l'article (modulo la suppression d'une section à voir ci-dessus) et j'aimerais avoir votre avis. Pierre de Lyon (d) 23 novembre 2007 à 22:21 (CET)

modification mineure pour lisibilité

Je débarque sur le sujet via une recherche sur pierce (loi de pierce) via Commons JR (économiste) bref totalement ignare en logique. Par contre je sais lire. La page loi de pierce renvoie ici pour l'explication des symboles logiques.

Sauf erreur je n ai pas vu de définition de ces deux termes \land, ou \lor,

Super !!! je ne sais pas si ca va s afficher, bref le V et le V inversé. Je ne sais pas ce qu il veut dire. Et je trouverais bien que vous fassiez un tableau récapitulatif avec le sens des différents termes. Juste ça, ça serait utile pour le néophyte qui tombe sur un signe logique et qui ne le connait pas, du genre j ai déja appris a lire non A (l espece de crochet horizontal, ca veut dire non) je suppose que V et V inversé c est union et intersection pour l instant mais je suis pas sur du tout

Bonjour, voyez le tableau en bas à droite ici --Epsilon0 15 mai 2007 à 21:12 (CEST)

Axiomes

Dans l'exposé du système de Lukasiewicz (en fait il faudrait dire Frege - Lukasiewicz - Tarski), le 3e axiome me semble bizarre. Chez metamath ainsi que dans mes divers textbooks, c'est (¬g → ¬f) → (f → g) - Michel421 29 octobre 2007 à 23:49 (CET)

Bizarre ne me parait pas le bon adjectif, mais je dirais qu'il est inattendu ou non orthodoxe et que l'axiome que tu cites est plus courant. En effet, les deux axiomes (¬g → ¬f) → (f → g) et (¬g → f) → (¬g → ¬f) → g sont équivalents si je ne me trompe. Pierre de Lyon 30 octobre 2007 à 00:10 (CET)

Logique minimale

Si cette formule :

$f\to (f\lor g)$

est bien un axiome, alors remplaçons $g$ par $\lnot f$ et nous avons :

$f\to (f\lor \lnot f)$

ce qui, apparemment, signifie que de n'importe quelle formule $f$ on peut déduire $f\lor \lnot f$ ou, si vous voulez, que dès que l'on peut construire la formule $f$, on peut construire $f\lor \lnot f$. Quelle différence avec le tiers exclu ? - Michel421 1 novembre 2007 à 14:34 (CET)

La différence est que dans la première proposition ne figure pas le signe $\lnot$.Pierre de Lyon

Donc "$f$" n'est pas une méta-variable, en logique minimale ou intuitionniste il y a des restrictions sur la structure des formules qui peuvent être substituées aux lettres, c'est ça ? - Michel421 1 novembre 2007 à 23:24 (CET)

Non. De f on déduit bien (f ou non f) en logique minimale, mais ça n'a rien à voir avec le tiers-exclu : f ou non f sans aucune hypothèse. Proz 1 novembre 2007 à 23:45 (CET)

La logique classique et le tiers exclu

Je ne pense pas que la discussion qui se situe dans cette section soit à sa place ici. De plus, je ne la comprends pas. Je propose de l'enlever. Pierre de Lyon (d) 23 novembre 2007 à 21:56 (CET)

Je suis d'accord, je ne comprends pas non plus, je ne vois pas trop comment on peut expliquer ce genre de choses sans beaucoup plus s'étendre, parler de l'infini ... hors sujet. On peut se contenter de mentionner la propriété de disjonction. Proz (d) 23 novembre 2007 à 22:25 (CET)

FNC ?

C'est le seul article Fr à utiliser le sigle FNC ... on pourrait envisager

• de supprimer l'abréviation dans le texte ?
• de lui donner un article à part entière ? (on peut traduire en:Conjunctive normal form
• d'utiliser l'abréviation en anglais CNF ?

Qu'en pensez-vous? Ripounet 2 décembre 2007 à 20:45 (CET)

Bonjour,

1. Concernant les abréviations FNC et FND c'est moi (je me dénonce) qui les ai introduites dans l'article, essentiellement dans un but d'abréviation et car elles me semblent courantes. Mais on peut préférer la forme longue. Maintenant abréger par les acronymes anglophones CNF et DNF me semble peu pertinent, car on est sur fr: pas sur en: .

2. Sur le fond, j'avoue que cette section dans l'article (que je n'ai pas initiée) me semble un peu dissonante car trop peu générale pour un article introductif et aussi peu théorique. Via un article autonome peut se révéler utile. Mais je ne sais pas trop :

Créer Forme normale ou Forme normale disjonctive et Forme normale conjonctive (les liens bleus sont des redirects + page d'homonymie)?

Mais pour Forme normale conjonctive il y a sans doute bcp plus de choses à dire lié à la notion de clause + le problème SAT voire la règle de coupure.

Donc crée t-on un nouvel article, disons Forme normale, ou étoffe t-on cette section du présent article de manière à ce qu'il serve d'introduction (par des renvois) à des notions plus fines liées au pb SAT (ou à d'autres chose que j'ignore) ?

Je crois que sur ce sujet l'avis de Pierre de Lyon qui vient d'améliorer fortement l'article et est spécialiste en théorie de la démonstration devrait résoudre la question (@ Pierre, n'est-ce pas?).

Question en passant : le cut (noté "!") du langage Prolog, c'est bien la règle de coupure, ou rien à voir?

--Epsilon0 3 décembre 2007 à 19:50 (CET)

J'aime bien l'idée de créer un vrai article autonome Forme normale conjonctive. Mais je n'ai pas les connaissances pour le faire moi-même. Ripounet (d) 7 décembre 2007 à 16:22 (CET)

modus barbara (implicatif) à corriger

Cela me parait pas valide, cf avec A, non B et non C. J'ai pas vérifié mais distribuer les parenthèses dans l'autre sens me parait mieux. En passant, on pourrait peut-être rajouter la commutativité et l'associativité du "et", "ou" ? Outs (d) 9 mars 2010 à 20:44 (CET)

Effectivement, ne pas hésiter à corriger. Pour les exemples supplémentaires je ne sais pas, peut-être mais ce ne sont plus que des exemples (déjà là ...). Il faut voir ce qui existe dans les articles liés ... L'associativité et la commutativité devraient être mentionnés en tant que telles pas comme exemples me semble-t-il. Proz (d) 9 mars 2010 à 21:30 (CET)

Un peu de relecture

J'ai fait un peu de relecture (je ne prétends pas avoir terminé, loin de là). Je déplace ceci ici : c'est à récupérer probablement ailleurs, mais je ne vois pas trop le rapport direct avec le calcul prop. (cet article est bien lourd).

Les algèbres de Boole peuvent être formalisées avec un seul axiome :

(P | (Q | R)) | ((T | (T | T)) | ((S | Q) | ((P | S) | (P | S))))

autrement dit, il suffit de dire que cette proposition vaut 1 pour que toutes les autres identités des algèbres de Boole en découlent.

Veroff et McCune ont démontré en 2000 en utilisant leur système de démonstration automatique de théorèmes Otter que l'on peut formaliser les algèbres de Boole par la seule équation

((P | R) | Q) | ((P | (P | Q)) | P) = Q.

Proz (d) 9 mars 2010 à 22:41 (CET)

Tables de vérité

J'ai peur qu'on confonde à la lecture de cet article table de vérité, et table des lois binaires associées aux connecteurs (les seules représentées). L'article table de vérité est à réécrire (écrit actuellement d'un point de vue d'électronicien, bien présenté dans son contexte ailleurs). Proz (d) 9 mars 2010 à 23:51 (CET)

J'ai corrigé pour ici Outs (d) 10 mars 2010 à 14:00 (CET)

Théorie des fonctions de vérité

Je me demande si nous devons garder théorie des fonctions de vérité comme homonyme de calcul des propositions. --Pierre de Lyon (discuter) 16 septembre 2015 à 10:04 (CEST)

Au mieux ça ne fait référence qu'à l'aspect sémantique. J'enlève ("calcul des énoncés" est lui clairement utilisé. Proz (discuter) 27 janvier 2020 à 13:15 (CET)

Calcul des séquent (CS)

Dans CS, il est dit que gamma et delta sont des multi-ensembles, ce ne sont pas des suites plutôt ? Outs (d) 11 mars 2010 à 07:17 (CET)

Je me répond à moi même : il n'y a pas les règles d'échanges dans la section, donc ok.Outs (d) 11 mars 2010 à 10:00 (CET)

Par ailleurs il y a un article dédié et il n'est probablement pas nécessaire de donner toutes les règles (à comparer quand même soigneusement avec l'article), mais juste le principe. Proz (d) 11 mars 2010 à 10:06 (CET)

Ah ben justement j'étais justement en train de m'interroger sur la pertinence de cette section dans un article sur le calcul des propositions. Je serai pour supprimer toutes les règles, en plus ce n'est pas très bien expliqué.

En parlant des règles : "introduction du faux à droite" et "Introduction du faux à gauche" me paraissent être de simples conséquences de la règle d'affaiblissement et de l'axiome. Par contre il manque les règles pour la négation, j'imagine que l'auteur de ce texte voulait poser non A = a -> faux, mais ce n'est pas expliqué. Outs (d)

A droite oui, mais à gauche comment déduirais-tu Abs |- A ? Ceci dit la formulation symétrique, avec négation, qui est celle de l'article dédié, est plus usuelle au moins pour la logique classique. Proz (d) 11 mars 2010 à 20:47 (CET)

Hey bien : $\quad \perp \ \vdash$ c'est pareil que $\quad \perp \ \vdash \bot$, non ? D'ailleur pourquoi il n'y a pas la barre de déduction au dessus de l'axiome ? Outs (d) 11 mars 2010 à 21:10 (CET)

C'est pareil intuitivement, mais quelle déduction formelle ? Si l'absurde n'avait pas de règle particulière, on pourrait démontrer les formules le contenant en le remplaçant par n'importe quelle variable propositionnelle. Or Abs |- A, mais pas B |- A.

Heu non, il n'existe pas de règle dans le calcul des séquents qui permet de rempalcer $\bot$ par une autre proposition . De toute façon ces règles ne sont pas complètes, elles ne disent pas comment gérer la négation.

(la barre au dessus de l'axiome c'est une affaire de convention). et de renvoyerProz (d) 11 mars 2010 à 21:56 (CET)

Je pense plutôt qu'elle est importante car c'est elle qui dénote l'absence de prémisse à cette règle. Évidement c'est sous entendu quand on dit que c'est un axiome, mais cela me parait nécessaire d'uniformiser la présentation entre les axiomes et les règles. Outs (d) 12 mars 2010 à 09:36 (CET)

1. Ce serait une propriété d'un système qui justement n'a pas de règle pour Abs (propriété classique de substitution qui est une "meta" propriété). La négation se définit. Mais à on avis il suffit d'expliquer le principe sur un connecteur et de renvoyer à l'article dédié ce qui règle le problème.

2. Les deux se font, c'est sans importance. Proz (d) 12 mars 2010 à 23:40 (CET)

section "Les systèmes déductifs"

J'ai l'impression qu'il manque dans la wikipedia française dédié à la description des "Systèmes déductifs" (SD), c'est à la Hilbert, la déduction naturelle, le calcul des séquent, etc. J'ai cherché et le seul endroit que j'ai trouvé où il y une explication sur les SD c'est dans cette page. Or les SD s'applique pas uniquement à la logique propositionnelle. D'ailleurs il y a une chose assez révélatrice : dans la section SD de cette page, il y a un lien "article détaillé : Théorie de la démonstration", or l'article détaillé en question est presque vide. Ce qui m'amène à la proposition suivante : pourrait-on prendre le section SD de cette article et la déplacer dans l'article Théorie de la démonstration ? Cela fournirait un début pour avoir une page correcte parlant de ce sujet. Outs (d) 11 mars 2010 à 11:17 (CET)

Je partage ton souci, je ne pense pas que l'on ait besoin de donner tous les détails des systèmes de déduction dans cet article. Mais l'article théorie de la démonstration devrait plutôt traiter du domaine de la logique que ça recouvre, donc ce n'est pas vraiment l'endroit ou recopier cette section. Il me semble que cet article devrait renvoyer plutôt sur des articles dédiés sur chacun de ses systèmes, mais les présenter quand même donc ça n'est pas un simple déplacement, et il y faut un petit texte de présentation, expliquant aussi ce qui se passe de particulier en propositionnel. Bref c'est quand même du travail. Pour le calcul des séquents ou les systèmes à la Hilbert, les articles dédiés font déjà à peu près la même chose (les règles pour l'absurde, les multi-ensembles c'est du détail). Pour la déduction naturelle c'est une autre représentation, et les deux sont intéressantes. Proz (d) 11 mars 2010 à 21:49 (CET)

D'accord, donc tu pense que Théorie de la démonstration ne serait pas un bon endroit pour accueillir un contenu qui serait similaire (dans un premier temps) à la section SD. Dans ce cas que pense-tu (enfin je pose la question à tous le monde évidement) de créer un article système déductif ? Y'a-t-il déjà un endroit dans les pages consacrées à la logique qui pourrait être dédié à cela ? Outs (d) 12 mars 2010 à 09:16 (CET)

Il y a une section Système logique contenant une sous-section Systèmes de déduction dans l'article Logique mathématique et qui remplit en gros les objectifs décrits par Proz ci-dessus. Laurent de Marseille (d) 13 mars 2010 à 00:52 (CET)

Ah ben voilà, elle est très bien cette section, je ne l'avais pas vue. Elle est bien mieux rédigée que ce qui se trouve dans l'article ici. Outs (d) 13 mars 2010 à 12:59 (CET)

Il y a aussi un article Système formel ; ça n'est pas exactement les systèmes déductifs mais ça s'en rapproche. Cela étant rien n'empêche de créer un article Système déductif si quelqu'un en ressent la nécessité. Laurent de Marseille (d) 19 mars 2010 à 09:15 (CET)

premier ordre et calcul des propositions

Le calcul propositionnel du second ordre est défini ici par l'utilisation des quantificateurs universel et existentiel, mais le calcul du premier ordre est défini comme utilisant ces mêmes prédicats pour les propositions voir Wikipédia ?--Lmeléo (discuter) 17 juin 2014 à 11:16 (CEST)

On ne dit pas « calcul des propositions du premier ordre » et « calcul des propositions du second ordre » mais « calcul des prédicats du premier ordre » et « calcul des prédicats du second ordre ». L'expression « calculs des propositions » est réservé à l'étude des expressions sans quantificateurs et sans variables. --Pierre de Lyon (discuter) 17 juin 2014 à 16:33 (CEST)

Merci pour cette précision, hélas elle me semble incompatible avec le texte de cet article, je cite:“On peut introduire les quantificateurs ∃ (il existe) et ∀ (quel que soit) pour quantifier les propositions (ce qui est à distinguer de la quantification du calcul des prédicats). Ainsi pour exemples on aura comme formules valides du calcul propositionnel quantifié, appelé aussi calcul propositionnel du second ordre (C'est moi qui souligne) :” (in Paragraphe : Calcul propositionnel quantifié).

Mais vous pourriez peut-être répondre aux questions que je me posais : 1 Gödel ayant démontré la complétude du calcul des prédicats du premier ordre (soit la logique classique, sans quantificateurs ?), il existe un système formel notablement puissant pour lequel la cohérence est établie. D'accord ?

2 En 1926 Paul Bernays a prouvé la complétude du calcul des propositions, 3 ans plus tard Gödel a prouvé autre chose : la complétude du calcul des prédicats du premier ordre, soit le calcul des propositions + les quantificateurs, mais pas les relations. Est-ce exact ? --Lmeléo (discuter) 18 juin 2014 à 18:39 (CEST)

J'avais mal lu ce qui était écrit dans l'article. En effet, dans l'article (calcul des propositions) on parle de quantifications sur les propositions alors que dans l'article sur le calcul des prédicats la quantification dont il est question est sur une classe d'objets spécifiques que l'on appelle les éléments. Les quantifications sont donc différentes.

1. Gödel a démontré la complétude du calcul des prédicats avec quantifications sur les éléments. Il s'agit d'une quantification du premier ordre. Gentzen a démontré la cohérence du calcul des prédicats du premier ordre comme conséquence de son Hauptsatz.

2. Oui.

Ceci dit on parle de calcul du second d'ordre dans deux cas: soit sans parler d'éléments on quantifie sur les propositions, soit on considère des éléments et en plus d'une quantification sur les éléments on ajoute une quantification sur les prédicats (ou sur les relations).

--Pierre de Lyon (discuter) 19 juin 2014 à 11:19 (CEST)

Merci pour votre réponse parfaitement claire.--Lmeléo (discuter) 26 juin 2014 à 10:23 (CEST)

Antilogie

Bonjour, ↳ Antilogie (h · j · ↵) redirigeait ici. Même si le terme apparaît effectivement dans l’article, je ne pense pas que la redirection se justifie. J'ai donc modifié vers Antilogie (rhétorique) (d · h · j · ↵) qui me paraît plus judicieux, d’autant qu’il s’agit de la seule entrée Antilogie de Wikipédia. Les trois liens de l’espace principal qui pointaient vers la page de redirection me semblent également destinés à la page Antilogie (rhétorique). La prochaine étape sera, sauf avis contraire, de demander le renommage de cette dernière page sans parenthèse avec éventuellement (quelle forme ?) un renvoi vers Calcul des propositions (d · h · j · ↵). En cas de désaccord, on pourrait transformer Antilogie en page d’homonymie. ❖ Luciofr ✎ 12 janvier 2018 à 14:11 (CET)