Discussion:Règle d'inférence

Règle d'inférence et axiomes

La phrase « Si l'ensemble des prémisses est vide, alors la conclusion est appelée un « théorème » ou un « axiome » de la logique. » est en contradiction avec ce qui est dit dans la section: Règles d'inférence et axiomes. Pierre de Lyon 27 octobre 2007 à 14:38 (CEST)

Ceci dit, cette section me parait faire des mélanges de niveaux qu'un lecteur non averti ne peut pas comprendre. Pour éviter de rentrer dans les détails un renvoi au théorème d'incomplétude de Gödel me paraitrait suffisant. A noter que la notation $\vdash$ $p$ n'a pas été introduite.Pierre de Lyon 27 octobre 2007 à 16:49 (CEST)

c'est peut-être la différence axiome logique / axiome de la théorie qui est en jeu, mais ça n'est franchement pas clair.

D'accord pour l'exemple de toute façon hors de propos (il peut être recasé dans règle admissible versus démontrable (la règle de |-p on déduit |-provable(p) est admissible pas dérivable). Proz 27 octobre 2007 à 17:42 (CEST)

Ca risque d'être un truisme alors. En effet, on va définir provable par induction, en gros on disant que p est « provable » (ou provable(p)) s'il a une démonstration. Mais c'est bien le théorème p $\vdash$ provable(p) qui le nœud du problème. Il faut « internaliser » la démonstration. Pierre de Lyon 27 octobre 2007 à 18:18 (CEST)

Oui, ça n'est pas autre chose, truisme est un peu fort, c'est une partie de la démonstration du th. de Gödel (coder la prouvabilité, l'une des étapes est justement de montrer que l'on peut "faire" des définitions par induction). C'est un exemple de règle admissible que l'on trouve. Par contre, je ne sais pas ce que tu entends par p $\vdash$ provable(p), mais $\vdash p\to provable(p)$ est bien faux en général (tu peux "internaliser" si p est Sigma_1, par ex. la prouvabilité, c'est le second th. mais là je crois qu'on est carrément hors sujet). Proz 27 octobre 2007 à 18:43 (CEST)

Preuve et démonstration

C'est l'usage sur WP d'utiliser l'un plutôt que l'autre ? Il y a une nuance ? - Eusebius ^[causons] 27 octobre 2007 à 15:05 (CEST)

Il y a encore dix ans, personne n'aurait parlé de « théorie de la preuve » car on disait seulement « théorie de la démonstration ». Depuis l'anglais a fait ses ravages et la première expression est de plus en plus utilisée, mais c'est à tort. Comme le montre un petit tour vers le dictionnaire du TLF, une preuve n'est pas une démonstration. Je cite « Math: Calcul permettant de vérifier le résultat d'une opération en faisant l'opération inverse ». Il me paraît donc approprié de remplacer « preuve » par « démonstration », car nous devons apprendre à nos lecteurs à utiliser le mot juste, même si c'est un peu à contre courant. Pierre de Lyon 27 octobre 2007 à 16:06 (CEST)

Mille excuses, j'ai fait mes études de logique dans la perfide Albion... - Eusebius ^[causons] 27 octobre 2007 à 16:11 (CEST)

Nobody's perfect. Continuons à améliorer ce « papier » (ou peut-être cet « article »). Et merci pour ton travail. Pierre de Lyon 27 octobre 2007 à 16:50 (CEST)

Tu m'as mis le doute, je viens de relire ma dernière publi en français pour vérifier que j'avais pas écrit « papier » ! - Eusebius ^[causons] 27 octobre 2007 à 17:14 (CEST)

Disons peut-être 20 ans plutôt que 10. Pierre a très probablement raison sur l'usage antérieur, et très certainement sur le rôle de l'anglais (d'après le TLF je comprends quand même qu'une démonstration peut-être une preuve mais pas forcément l'inverse, au moins hors math.). Il reste que ça me fait bizarre de lire "omega-démonstration" (la construction avec "-", que n'avait pas chosie eusebius, doit déjà être un anglicisme d'ailleurs). Proz 27 octobre 2007 à 17:55 (CEST) J'ai réécrit.

Effectivité et algorithme

Il me semble qu'effectif veut dire qu'il y une méthode de décision. Dans ce cas, je préfère le mot « algorithme » à celui de « procédure ». Donc je dirais qu'il y a un « algorithme effectif qui ... ». Pierre de Lyon 27 octobre 2007 à 18:27 (CEST)

"algorithme" suffirait alors ? Proz 27 octobre 2007 à 18:47 (CEST)