Discussion:Correction (logique)

	Tâches à accomplir pour Correction (logique)	aide
	Votre aide est la bienvenue pour corriger les liens, présents dans l'article, vers les pages d'homonymie Chimère , Complétude ⇒ Quelques explications pour effectuer ces corrections. -- 12 avril 2023 à 03:36 (CEST)

Bonjour, je suis assez gêné avec cet article, qui s'il parle bien du théorème de correction (appelé aussi adéquation en français et soundness en anglais), me semble dès l'introduction parler de je ne sais quoi d'autre. Il ne me semble pas sûr qu'il fallait traduire l'article anglais.

Je pense qu'il faudrait reprendre quasi à zéro l'article :

En le renommant théorème de correction ou théorème d'adéquation (l'un étant le redirect vers l'autre) et en disant en gros :

• le thm dit : si A |- B, alors A|= B,
• soit en mots : si la théorie B se déduit (syntaxiquement) de la théorie A, alors tous les structures d'interprétations modèles de A sont modèles de B.
• Ce thm est relatif à une logique (celle de référence étant le calcul des prédicats du premier ordre) et est considéré comme le minimum pour une logique.
• Sa réciproque, soit si A |= B, alors A|- B est appelé théorème de complétude pour la logique considérée et est souvent plus dure à établir ... lorsque c'est possible cf le en:Lindström's theorem
• Autres développements récupérables de l'article actuel.

--Epsilon0 ε₀ 4 juillet 2012 à 19:53 (CEST)

Non ça parle pas d'un théorème, mais d'une propriété d'un système logique. On peut ensuite prouver ou pas qu'un système a cette propriété, mais théorème n'est pas définition, ou alors j'ai raté un truc TomT0m (d) 4 juillet 2012 à 20:53 (CEST)

Salut, merci pour tes commentaires. Je reprend actuellement, sur mon temps libre, mes études de logique formelle en repassant par les base pour assainir tout le fatra qui constitue ma vision du domaine. J’ai suivi des cours d’ingénierie de la preuve sans avoir ces bases bien solidement fixés, et j’y reviens maintenant car je souhaite bien comprendre tout cela, notamment en raison de mon attrait pour la philosophie. Je me suis mis à la traduction de soundness parce que c’est un terme sur lequel je suis retombé pratiquement dès le début de ma lecture de Logic de Paul Tomassi. Il y est défini comme une inférence valide à laquelle on fourni des prémisses vrais. C’est également ce qu’on trouve comme définition sur Internet Encyclopedia of Philosophy. Tu pourras constater que j’ai ajouté un certain nombre de sources qui ne sont pas présentes dans l’article originale, comme mon idée est effectivement plus de l’utiliser comme matériel d’où débuter que comme référence mordicus. Bref, si tu as plus de sources à me conseiller, je suis preneur, pour ce que je peux en juger par mes lecture, la correction ne se limite pas au théorème que tu présentes, mais qui est bien présent dans l’article dans les sections sur les systèmes déductifs. --Psychoslave (d) 4 juillet 2012 à 21:00 (CEST)

@Tomtom je ne comprends pas précisément ce que tu dis. Sinon c'est clairement un thm pour la logique usuelle.

@Psychoslave, bon je serai absent 10/15 jours, mais reviendrai sans doute sur ce sujet (relance moi si rien n'a bougé). Laisse p.-e. tes références (pas bien regardé) sur le sujet le temps que les notions essentielles (je crois ce que j'ai mis ci-dessus) concernant cet article soient mises. Sinon j'ai mis ce mot à ta suite sur le Thé. D'autres réactions peuvent venir.

Cordialement à vous 2. --Epsilon0 ε₀ 4 juillet 2012 à 21:28 (CEST)

Et si je formulais ainsi : "la correction est la propriété d'un système de déduction ou d'une logique formelle telle qu'on puisse y démontrer le théorème de la correction" ? Si on prend la première phrase de l'article en on ça {{citation[en|In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics.}}. Un système est correct si il possède cette propriété, mais ce n'est pas le cas de tous les système possibles. TomT0m (d) 4 juillet 2012 à 21:47 (CEST)

Correction d'un argument ou d'un système logique ?

Je me suis attelé à travailler sur l'article, mais les bases ne sont pas très saines (not sound). Tout d'abord il y a une confusion: traite-on de la correction d'un argument ou d la correction d'un système logique? --Pierre de Lyon (d) 15 novembre 2012 à 18:28 (CET)

Il faudrait choisir, effectivement. Parmi les choses qui ne vont pas :

• le paragraphe étymologie ressemble fort à ce qui est appelé ici du travail inédit
• parler de correction sans référence à une sémantique n'a pas de sens (ex. "Ainsi le calcul des prédicats ou la logique intuitionniste ont été démontré corrects", vis-à-vis de quoi ?).
• correction faible/forte : j'ai des doutes sur la pertinence (c'est pertinent pour la complétude), s'agit-il de parler de règles infinitaires ? Une référence serait bienvenue
• Arithmétique de correction : à reprendre
• beaucoup de liens rouges ont déjà des équivalents

Mais c'est effectivement bien délicat de faire quelque chose tant que l'on ne décide pas du sujet traité. Pour la correction des arguments : la seule source http://www.iep.utm.edu/val-snd/ n'est pas assurée selon cette page même, voir le bas de page. Donc mieux vaudrait probablement choisir la correction des systèmes logiques. Proz (d) 15 novembre 2012 à 19:43 (CET)