Discuter:Calcul des prédicats

Un article de Wikipédia, l'encyclopédie libre.

Je ne comprends pas le bien-fondé du changement de catégorie de cet article. Ou alors, je voudrais qu'on m'explique la différence entre les catégories logique et logique informatique. Pour moi la seconde était le développement formel de la première, accompagné des développements théoriques relatifs à la complétude et à la calculabilité, alors que la première reste dans un langage assez général et traite de la logique d'un point de vue plus épistémologique. --Ąļḋøø 30 aoû 2004 à 12:43 (CEST)

J'ai supprimé le passage «Il n’y a pas de sens à dire qu’une formule qui contient des variables libres est vraie ou fausse. Il faut substituer des constantes à toutes les variables libres pour obtenir une formule susceptible d’être vraie ou fausse.» du paragraphe Précicats, variables libres, variables liées, car il n'est pas correct. Si P est un prédicat unaire, la formule Px \to Px, dans laquelle apparaît la variable libre x, est un théorème du calcul des prédicats, que ce soit du point de vue syntaxique (il résulte du remplacement de f par Px dans la tautologie du calcul des propositions f \to f) que sémantique (dans tout modèle M, si P est représenté par une partie A de M et si on attribue à x une valeur a dans l'ensemble, alors on obtient une formule vraie, à savoir : si a appartient à A, alors a appartient à A).Theon 16 janvier 2006 à 13:44 (CET)

J'ai abrégé le paragraphe sur les résultats d'incomplétude qui ont peu de rapports avec le sujet de l'article. Un lien suffit pour renvoyer le lecteur intéressé sur les résultats d'incomplétude. Theon 17 janvier 2006 à 10:47 (CET)

je me trompe peut-être, mais le "théorème" cité par theon dit quelque chose comme P(x) \to P(x) est satisfait pour tout x. Donc la formule complète est en fait \forall x (P(x) \to P(x)), formule dans laquelle x n'est pas une variable libre, contrairement à ce que prétend theon. Personnellement, je trouve qu'il n'y avait pas lieu de supprimer le passage cité: chercher à évaluer une formule non close n'a pas de sens. Tout au mieux, on lie implicitement les variables libres en utilisant des quantificateurs sans s'en rendre compte (c'est ce que Theon semble avoir fait).

Il existe une différence entre prouver Q(x), et prouver \forall x, Q(x). D'ailleurs, l'équivalence entre ces deux formulations repose sur des axiomes du calcul des prédicats. L'axiome de généralisation par exemple, énonce que, pour prouver \forall x, Q(x), il suffit de prouver Q(x), avec x variable libre. Cela a donc un sens de s'intéresser à la validité d'une formule telle que Q(x), avec x variable libre. La rédaction initiale de l'article était trop restrictive. La preuve de \forall x (P(x) \to P(x)) se fait par exemple en trois étapes.
1) Preuve de f \to f en calcul propositionnel
2) Preuve de P(x) \to P(x) par substitution de f par P(x)
3) Preuve de \forall x (P(x) \to P(x)) par application de l'axiome de généralisation. Theon 4 mai 2006 à 18:03 (CEST)

La généralisation est une règle, et pas un axiome (Q x → ∀x Q x est manifestement fausse en général). Pour définir inductivement la sémantique du calcul des prédicats classique, on est bien obligé d'une façon ou d'un autre de remplacer les variables libres par des "constantes" (éléments du modèle). Donc la phrase supprimée est correcte au sens strict, mais demande des explications. L'usage est d'interpréter la vérité d'une formule avec des variables libres par celle de sa clôture universelle. Je ne propose pas le rétablissement, sinon dans un contexte ou la sémantique est mieux expliquée.

Au passage l'article théorie des modèles est imprécis à ce sujet (pas de définition vraiment correcte de la sémantique). L'article Théorème de complétude passe en calcul propositionnel quand la question se pose... Proz 22 juillet 2006 à 17:34 (CEST)

Sommaire

[modifier] Kant dans cet article

Je suis pas un défenseur de Kant, mais si on le cite, dire que "critique de la raison pure" avait pour propos de dire que la logique était complète et définitive... me semble un peu fort (relisez ne serait-ce que le titre du livre). Voici la phrase que je critique : 'Emmanuel Kant croyait à tort que la logique de son temps, celle d’Aristote, était une science complète et définitivement achevée (préface de la seconde édition de la critique de la raison pure, 1787).'. Il y a probablement pas mal d'interprétation qu'on peut faire, mais kant a été souvent présenté comme "précurseur" de godel car il souligne (il est proche d'une démonstration philosophique si on peut dire ca) l'incapacité du "raisonnement pur" à être complet et qu'il est toujours dépendant de l'expérience (des axiomes). En bref, cette phrase, c'est vouloir faire dire à kant quelque chose qu'il a dit mais hors de son contexte, ca n'est pas correct et peut être mal interprété et est trop simplificateur (a mon avis). Et pire, aguicheur. (ca fait toujours classe de sortir quelques grand noms autour d'une anecdote plus ou moins vraie).

Compte tenu de la remarque ci-dessus, je propose de supprimer le paragraphe relatif à Kant, à moins que quelqu'un se sente assez compétent pour le modifier. Theon 2 juin 2006 à 15:39 (CEST)
je suis d'accord : on peut supprimer si personne n'est capable de corriger. Proz 22 juillet 2006 à 17:04 (CEST)


[modifier] Calcul des relations

Je ne suis pas d'accord avec la redirection de « calcul des relations » vers « calcul des prédicats ». Je propose de supprimer cette redirection et de commencer un article sur les calcul des relations comme l'avait initié Alfred Tarski. Pierre de Lyon 1 avril 2007 à 15:33 (CEST)

[modifier] Consistance

Après avoir présenté le calcul des prédicats d'un point de vue syntaxique et sémantique, l'article s'intéresse au rapport entre ces points de vue. Bonne présentation de la complétude, mais qu'en est-il de la cohérence\consistance ? Cela revient, à mon avis, à s'intéresser uniquement à l'implication suivante : Si la formule est valide, alors c'est un théorème. En oubliant l'implication dans l'autre sens... Qu'en pensez-vous ? Jérémie

Il y a deux problèmes dans l'article : disons la fidélité, ce qui est démontrable est valide dans tout modèle : juste mentionné pas vraiment traité ; une théorie (éventuellement infinie) est syntaxiquement cohérente ssi elle a un modèle : pas traité du tout (ni fidélité, ni complétude). Proz (d) 5 mars 2008 à 00:50 (CET)

Bonjour Jérémie et bien venu en logicie,

  • Comme vous le remarquez bien les liens syntaxe-sémantique ont 2 sens :
    • 1. "Si la formule est valide, alors c'est un théorème", c'est le thm de complétude. Qui nous dit donc que les règles syntaxiques nous donnent toutes les formules valides (mais potentiellement d'autres).
    • 2. Dans l'autre sens ont a : "Toute formule qui est théorème est valide". C'est le thm de fiabilité/correction (soundness en anglais) Qui nous dit que les règles ne nous donne que des formules valides (mais potentiellement pas toutes).
  • Maintenant : La question de la cohèrence découle du thm de fiabilité (Toute formule qui est théorème est valide) donc contrairement à ce qui vous semble.

Explication : 1. être cohèrent = ne pas pouvoir dériver (syntaxiquement) le faux = La formule fausse n'est pas un théorème. 2. (constat) : le faux n'est pas une formule valide donc 3. si on a le résultat "Toute formule qui est théorème est valide", on a que la formule fausse n'est pas dérivable des règles, ce qui établit donc la consistance.

  • Concernant l'article :
    • La consistance d'une logique (il y en a plusieurs selons les règles syntaxiques que l'on se donne) est un peu le service minimal demandé et il est souvent plus facile à démontrer que la complétude de cette logique face à une interprétation sémantique. Aussi bien souvent, comme il en est dans cet article, on en parle moins. Mais vous avez raison de souligner, que ce point n'est pas assez mis en avant dans l'article, car tout de même, oui, pour répondre tout de même à votre interrogation, le calcul des prédicat est bien démontré cohérent; rassurez vous :-); [mais il n'est que semi-decidable :-( , mais c'est une autre question].
    • ... mais c'est loin d'être un résultat si trivial car pour des théories (théorie = règles d'inférences logiques+axiomes spécifiques) intuitivement simples comme l'arithmétique, on sait que si elle sont cohèrentes on ne peut le démontrer (cf Théorème d'incomplétude )!
    • Bref qu'un lecteur vigilant et soucieux comme vous de bien comprendre ce qui est dit s'interroge sur la question de la consistance du calcul des prédicats (en se trompant de sens sur l'implication; donc moins vrotre faute que l'incomplètude :-))) de l'article) , permet de voir qu'il y a encore du boulot à faire sur cet article. Au fait a t-on un article sur le théorème de fiabilité (enfin "soundness", tant je crois qu'on en parle si peu en français que la terminologie n'est pas établie) ?

--Epsilon0 ε0 5 mars 2008 à 11:33 (CET)

Ce que je voulais dire :

  • Point de vue sémantique : Toute formule valide est un théorème. Il s'agit de la complétude, correctement abordée dans l'article.
  • Point de vue syntaxique : Tout théorème est une formule valide. Il s'agit de la consistance, que je jugeai un peu passée sous silence.

Sans doute me suis-je mal exprimé précédemment mais j'ai bien compris le sens des implications contrairement à ce que vous pensez, et ma question "qu'en est-il de la cohérence ?" se rapportait à l'explication qui en ai faite dans l'article, pas au calcul des prédicats lui-même, dont je sais qu'il est (heureusement) prouvé cohérent.

Vous avez surement raison sur le fait qu'il s'agit d'un "service minimal" et donc sans doute, il n'est point besoin de s'étendre sur la chose.

Merci pour votre réponse très complète (et pour votre acceuil, je suis ravi de participer ne serait-ce qu'en m'interrogeant :-) , personnellement je n'ai jamais entendue parler du théorème de fiabilité et serais curieux de lire un article sur le sujet.

Jérémie

L'article est à améliorer et vous aviez raison de soulever ce problème, mais ce n'est pas le seul. La complétude du calcul des prédicats n'est pas abordée dans le cadre le plus général et le plus intéressant, celui d'une théorie (si tout modèle d'une théorie T est modèle d'une formule F, alors F se déduit syntaxiquement de T), donc je ne trouve pas que l'article soit satisfaisant de ce point de vue. Ce que vous appelez consistance est parfois appelé fidélité, adéquation, ..., c'est ce qu'Epsilon0 appelle fiabilité, je ne l'ai jamais vu appelée consistance. La consistance d'une théorie, en général c'est plus ou moins synonyme de sa cohérence, avec des variations dans les ouvrages introductifs : soit la théorie a un modèle, soit la théorie ne permet pas de déduire syntaxiquement toutes les formules, l'équivalence étant justement un autre énoncé du théorème de complétude (+fidélité), le "vrai". Proz (d) 6 mars 2008 à 01:40 (CET)
En relisant l'article autre trou : il ne parle pas de calcul des prédicats égalitaire, or on a un théorème de complétude pour le calcul des prédicats avec égalité, ce qui est intéressant et très utile. Proz (d) 6 mars 2008 à 02:08 (CET)
Une petite remarque pour Jérémie: la consistance (ou cohérence) n'est pas « Tout théorème est une formule valide ». Ce concept s'appelle la correction (ou la fiabilité ou Sourire la « santé » ou la soundness en anglais). La cohérence (ou consistance) c'est l'absence de contradiction et c'est donc autre chose. Je crois que ces concepts sont bien présentés dans l'article Calcul des propositions section Décidabilité, cohérence, complétude, compacité. Pierre de Lyon (d) 6 mars 2008 à 22:55 (CET)

[modifier] Question aux spécialistes sur le lien entre prédicat et atome propositionnel

Bonjour, je me permets de polluer légèrement cette page de discussion pour poser une question sur la notion de prédicat, histoire de bien finir de vous convaincre que je ne suis pas un logicien :-) Je considère un prédicat p(X), où X prend ses valeurs dans un domaine dénombrable. Je décide de considérer que p(1) représente un atome propositionnel p1, p(6) l'atome p6, et que p(X) est un schéma correspondant à tout un ensemble d'atomes propositionnels. La question est, est-ce que cette "transformation" (dans un sens ou dans l'autre) a un nom ? D'autre part si vous avez des critiques ou des infos sur le concept, je suis preneur. Merci d'avance ! - Eusebius [causons] 31 mai 2008 à 17:42 (CEST)

Tu peux choisir tes "atomes propositionnels" comme tu veux, rien ne t'empêche de les appeler directement p(1), p(2), ..., p(n), ... Ca se fait, voir par ex. les applications du th. de compacité du calcul propositionnel (dans par ex. Cori-Lascar ? à vérifier). Il n'y a pas vraiment de transformation. Sinon prendre les formules atomiques closes du langage à paramètres dans le modèle, c'est je crois le diagramme positif du modèle (ce que tu fais pour N, langage de signature p), ça sert en théorie des modèles (voir Chang et Keisler par ex.). Proz (d) 31 mai 2008 à 19:02 (CEST)
Pour le nom des propositions c'était un exemple évidemment. Sinon merci beaucoup, je vais essayer de regarder tout ça... - Eusebius [causons] 31 mai 2008 à 19:14 (CEST)
Je ne sais si cela répond à la question, mais un atome propositionnel peut être vu comme un prédicat 0-aire, càd sans paramêtre. Aussi tout énoncé (formule sans variable libre), voire toute formule (?) peut être représenté comme un atome propositionnel, que l'on peut d'ailleurs intuitivement définir comme un énoncé inanalysé. --Epsilon0 ε0 31 mai 2008 à 22:32 (CEST)