Modèles, dérivabilité et formules

Bonjour,

Le dernier chapitre chapitre de mon cours d'épistémologie est consacré à la logique. Il y a pas mal de notions, et de notations, que j'ai du mal comprendre.

1) Tout d'abord, je souhaiterais poser une question à propos d'un livre que je me suis procuré : "Introduction à la logique" de F. Rivenc.

Lorsqu'il introduit le métalangage permettant de parler du langage formel (langage-objet), il écrit qu'il va adopter la convention suivante dans son ouvrage :

" Les symboles primitifs du langage-objet seront utilisés comme noms d'eux-mêmes dans le métalangage ; et la juxtaposition des noms sera utilisée comme nom pour la juxtaposition. "

J'ai bien compris la première partie de la phrase (les symboles seront autonymes), par contre je ne comprends pas du tout ce qu'il veut dire par :

"la juxtaposition des noms sera utilisée comme nom pour la juxtaposition." ??

Qu'est-ce que ça veut dire ? Si vous aviez un exemple...


2) J'en viens à ma question relative à mon cours.

On se place dans un système formel $S$ sémantiquement complet pour la logique du premier ordre. La prof nous dit alors que :

" le théorème de Gödel affirme que une formule $\varphi$ de $S$ de premier ordre est formellement démontrable si et seulement si elle est vraie dans tous les modèles, autrement dit :

Pour tout ensemble $\Gamma$ de formules et pour toute formule $\varphi$, on a : $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi $.

J'avoue que je m'y perds pas mal...

a) Tout d'abord, qu'est-ce qu'un modèle exactement ? Est-ce que, par exemple, le plan, avec ses points, droites et courbes est un "modèle" pour la géométrie euclidienne plane ?

b) Que signifie le symbole $\vdash$ ? Dans mon cours, on dit que c'est le symbole de la relation syntaxique de la dérivabilité. Mais qu'est-ce que la dérivabilité ? Pourriez-vous me donner un exemple concret : par exemple en géométrie euclidienne plane, que serait une formule $\varphi$ ? et que voudrait dire que $\Gamma \vdash \varphi$ ?

c) Mêmes questions pour le symbole $\models$. Dans mon cours, il est dit que ce symbole signifie "être vrai dans un modèle". Là aussi, pourriez-vous me donner un exemple concret ?

Merci d'avance pour vos réponses.

Réponses

  • Je ne suis pas un expert en logique, mais je me lance.

    1) Ca ca n'a pas l'air sorcier, ca veut juste dire que le nom d'une juxtaposition de symoble sera la juxtaposition des noms des symboles, si je comprends bien.

    a) Oui, en gros c'est ca l'idée. Un bon "jouet" pour s'essayer a cette notion de modèle est la théorie des groupes. Tu prends une operation binaire $\cdot$, une operation unaire ${}^{-1}$, une constante $e$, et 3 variables libres $x,y,z$ et les axiomes :

    1- $\forall x, x\cdot e=e\cdot x=x$
    2- $\forall x, x^{-1}\cdot x=x\cdot x^{-1}=e$
    3- $\forall x, \forall y, \forall z, x \cdot (y \cdot z)=(x \cdot y) \cdot z$

    Dans ce cas n'importe quel groupe ($\mathbb{Z}$, $S_n$, ...) est un modèle de cette théorie. Donc informellement un modèle est une manière d'attribuer un "sens" aux symboles, de les "incarner" concretement par des objets qui satisfont aux axiomes.

    b)La dérivabilité, il me semble que c'est simplement le fait de déduire une proposition à partir des axiomes en utilisant les règles de la logique du premier ordre. Par exemple, à partir des axiomes ci dessus, on peut prouver la propriété de simplification à droite : $\forall x,y,z, (x \cdot y = z \cdot y ) \Rightarrow (x=z)$. En effet :
    $(x \cdot y) \cdot y^{-1} = (z \cdot y ) \cdot y^{-1}$ (propriété d'une opération binaire
    $x \cdot (y \cdot y^{-1}) = z \cdot (y \cdot y^{-1})$ axiome 3
    $x \cdot e = z \cdot e$ axiome 2
    $x = z $ axiome 1

    c) Ca veut dire que si je prends n'importe quel modèle (en l'occurence un groupe, mettons $\mathbb{Z}$ ), alors pour tout triplet d'entiers $(a,b,c)$, l'implication $a+b=c+b \Rightarrow a=c$ est vraie. Par exemple, les implications :
    - $1+2=4+2 \Rightarrow 1=4$
    - $1+2=1+2 \Rightarrow 1=1$

    sont vraie.
  • Au passage, jouer avec la théorie des groupes permet de "demystifier" la notion de proposition indécidable qui donne souvent lieu a pas mal de fantasmes. Par exemple, la proposition $\forall x,y,\ x \cdot y = y \cdot x$ est indecidable dans la theorie des groupes, en ce sens qu'il existe des groupes (donc des modèles) commutatifs, et d'autres qui ne le sont pas.
  • 1) ne te formalise pas sur ce genre de phrases, ce sont des archaïsmes bureaucrates.
    2) a) un modèle d'une théorie, i.e. un ensemble d'axiomes, c'est un ensemble qui vérifie les axiomes de la théorie. Plus précisément on note $M \models \varphi$ pour dire que $M$ modélise la formule $\varphi$. Cette relation est définie inductivement en deux temps. Tout d'abord on se donne une interpretation du langage dans $M$, c'est-à-dire qu'on associe à chaque symbole de constante un element de $M$, pour chaque symbole on se donne une vraie fonction de $M$, idem pour les symboles de relations. On note $f : \mathcal{L} \rightarrow M$ cette fonction d'interprétation. A ce stade on est capable d'affirmer $M \models R t_1 ... t_n$, pour un symbole de relation d'arité $n$ et des termes sans variables $t_i$, puisqu'il suffit de vérifier que $(f(t_1), ..., f(t_n)) \in f(R)$. Ensuite pour passer aux formules générales on définit inductivement $\models$ avec des définitions du style : $M \models \varphi \wedge \varphi'$ ssi $M\models \varphi$ et $M \models \varphi'$, ou encore, $M \models \forall x. \varphi$ si pour tout element $e\in M$ on a $M \models \varphi$ où on a étendu $f$ par $f(x) = e$. Ainsi de suite...
    On a $M \models T$ si $\forall \varphi \in T, M \models \varphi$.
    b) La relation $\vdash$ est définie par la notion de prouvabilité syntaxique. En général, on se place dans le calcul des séquents de la logique classique du premier ordre. Tu trouveras les règles ici http://fr.wikipedia.org/wiki/Calcul_des_sequents . La notation $\Gamma \vdash \varphi$ signifie que tu peux construire un arbre de preuve où les noeuds sont des règles logiques et les feuilles sont de la forme $\Gamma \vdash A$ avec $A \in \Gamma$, c'est-à-dire l'application d'un axiome.
    c) Alors il y a également une notation qui est $T \models \varphi$ qui signifie pour tout modèle $M$ de $T$, ie $M\models T$, on a $M\models \varphi$.
    Le premier théorème de Godel dit que $T \models \varphi$ ssi $T \vdash \varphi$.
  • jobhertz a écrit:
    Au passage, jouer avec la théorie des groupes permet de "demystifier" la notion de proposition indécidable qui donne souvent lieu a pas mal de fantasmes. Par exemple, la proposition $ \forall x,y,\ x \cdot y = y \cdot x$ est indecidable dans la theorie des groupes, en ce sens qu'il existe des groupes (donc des modèles) commutatifs, et d'autres qui ne le sont pas.
    En fait une propriété indécidable ne fait pas vraiment sens. C'est d'un problème dont on peut dire si il est décidable ou indécidable. Par exemple, pour rester dans les groupes le problème du mot est indécidables. Savoir si une formule de l'arithmétique est prouvable est indécidable, mais si on ne prend que l'addition (Presburger) le sous-problème est décidable.
    Ta notion est en fait une notion d'indépendance. La propriété de commutation est indépendante de la théorie des groupes car il existe des modèles qui la valide et des modèles qui ne la valide pas.
  • deufeufeu, il me semble que le mot indécidable a un sens algorithmique (celui, je crois, que tu donnes) et un sens logique (synonyme de indépendant, comme écrivait jobherzt).

    En tout cas wikipedia pense comme moi (ce qui ne prouve pas grand-chose...).

    [Edit : pardon, je fais sauter la majuscule :)]
  • Oui le barbu rasé, mea culpa, il me semble me rappeler maintenant que j'ai fait mettre cette définition dans le cours de logique que j'ai donné à l'automne... Mais je n'aime pas trop appeler du même nom deux choses relativement différentes.
  • Merci beaucoup pour vos réponses.

    Je vais reprendre en détail ma question 2-a), avec la réponse de deufeufeu.

    Defeufeu> Un modèle d'une théorie, i.e. un ensemble d'axiomes, c'est un ensemble qui vérifie les axiomes de la théorie.

    => Si je comprends bien, en prenant l'exemple que donne jobhertz, la "théorie" peut être la théorie des groupes définie par les axiomes que donne jobhertz dans son post :

    1- $\forall x, x\cdot e=e\cdot x=x$
    2- $\forall x, x^{-1}\cdot x=x\cdot x^{-1}=e$
    3- $\forall x, \forall y, \forall z, x \cdot (y \cdot z)=(x \cdot y) \cdot z$

    Alors, par exemple, l'ensemble $(\Z, +)$ est un modèle de cette théorie ?


    ---


    Defeufeu> Plus précisément on note $M \models \varphi$ pour dire que $M$ modélise la formule $\varphi$.

    => Je ne saisis pas bien ce qu'est une formule exactement. Par exemple, en prenant toujours le même exemple : $M = (\Z, +)$, est-ce :

    - $1 + 2 = 3$

    -$\forall a,b,c \in \Z$, $a +b = c + b \Rightarrow a = c$

    sont des formules ?


    ---

    Defeufeu> Tout d'abord on se donne une interpretation du langage dans $M$, c'est-à-dire qu'on associe à chaque symbole de constante un element de $M$, pour chaque symbole on se donne une vraie fonction de $M$, idem pour les symboles de relations. On note $f : \mathcal{L} \rightarrow M$ cette fonction d'interprétation.

    => Ici, je n'arrive plus à suivre... Toujours, en prenant $M = (\Z, +)$, où $M$ modélise la théorie des groupes, pourrais-tu me donner un exemple d'une fonction $f : \mathcal{L} \to M$ ? ($\mathcal{L}$ est un "alphabet" si je comprends bien) ?
  • On va reprendre depuis le départ si tu le veux bien.
    On appelle langage un quadruplet $\mathcal{L} = (C, F, R, a)$ avec $C,F,R$ des ensembles disjoints appelés respectivements symboles de constantes, fonctions et relations; et $a : F \cup R \rightarrow \mathbb{N}$ est appelée fonction arité. On note en général implicitement l'arité par $f^{(n)}$ pour dire que $f$ est un symbole d'arité $n$.
    On se donne un ensemble dénombrable $V$ dont les éléments sont appelés variables, et on supposera toujours que les symboles des langages sont distincts de $V$.

    On appelle termes sur le langage $\mathcal{L}$ les éléments du plus petit ensemble $T$ tel que 1) $\forall c\in C, c \in T$; 2) $\forall x \in V, x \in T$; 3) $\forall f^{(n)} \in F, \forall t_1, ..., t_n \in T, f(t_1,...,t_n)\in T$.

    On appelle formule atomique de $\mathcal{L}$ les éléments de l'ensemble $A = \{ r(t_1,...,t_n), \forall r^{(n)} \in R, \forall t_1, ..., t_n \in T\}$.
    On appelle formule de $\mathcal{L}$ les éléments du plus petite ensemble $\mathcal{F}$ tel que 1) $\forall \varphi \in A, \varphi \in \mathcal{F}$ 2) $\forall \varphi_1,\varphi_2 \in \mathcal{F}, \varphi_1 \wedge \varphi_2 \in \mathcal{F}$, $\varphi_1 \vee \varphi_2 \in \mathcal{F}$ et $\neg \varphi_1 \in \mathcal{F}$ 3) $\forall x \in V, \forall \varphi \in \mathcal{F}, "\forall x. \varphi" \in \mathcal{F}$ et $"\exists x. \varphi" \in \mathcal{F}$.

    Le langage de la théorie des groupes c'est $(\{e\}, \{inv^{(1)}, \times^{(2)}\}, \{=^{(2)}\})$ on note en général $inv(t) = t^{-1}$ et $\times(t,t') = t t'$. Et la théorie des groupes correspond bien aux axiomes que tu donnes. Mais attention tu peux également présenter la théorie des groupes dans le langage des monoïdes $(\{e\}, \{\times^{(2)}\}, \{=^{(2)}\})$
    en rendant implicite l'inverse : $\forall x \exists y . x y = y x = e$.

    La suite pour plus tard...
  • Merci pour tes explications, deufeufeu. C'est beaucoup plus clair, surtout avec l'exemple de la théorie des groupes.

    Dans le 3) de ta définition des formules de $\mathcal {L}$, je ne comprends pas bien la phrase :

    $\forall x \in V, \forall \varphi \in \mathcal{F}, "\forall x. \varphi" \in \mathcal{F}$ et $"\exists x. \varphi" \in \mathcal{F}$.

    Comment faut-il lire/interpréter le point $.$ dans $"\forall x. \varphi"$ et $"\exists x. \varphi"$ ? Ca veut dire quoi ?

    ---

    Sinon, pour poursuivre mon investigation, peux-tu, une fois qu'on s'est donné un langage, me dire qu'elle est la définition exacte d'un "théorème" ?
  • J'ai mis des guillemets parce qu'il y a deux niveau de $\forall$ undans les formules définies et un dans le langage mathématique que j'utilise.
  • " J'ai mis des guillemets parce qu'il y a deux niveau de $\forall$ undans les formules définies et un dans le langage mathématique que j'utilise. "

    Euhh... J'ai pas compris ce que tu m'écris :S...

    Par exemple,

    $\forall x \in V, \forall \varphi \in \mathcal{F}, "\forall x. \varphi" \in \mathcal{F}$ doit se lire comment ? Normalement, quand j'utilise $\forall$, ça se dit : "pour tout" $\diamond$ "tel que" ... Je ne vois pas où placer le "tel que" dans ta phrase $"\forall x. \varphi" \in \mathcal{F}$.

    Sinon, un théorème, si je comprends bien, est un énoncé construit à partir des axiomes d'une théorie ? Et on dit qu'on a prouvé un théorème si on a pu construire une suite finie d'opérations logiques aboutissant à une tautologie ? Dans ce cas, si on note $T$ une théorie (un ensemble d'axiomes), $t$ un théorème, on note $ T \vdash t$ pour dire qu'on a prouvé le théorème ? C'est bien ça ("en gros") ?
  • Salut Bruno,

    Je ne suis pas spécialiste mais voilà une manière de voir les choses : $\mathcal{F}$ est un ensemble de formules. La phrase de deufeufeu signifie que si $x$ est n'importe quelle variable et $\varphi$ n'importe quelle formule, alors la proposition $\forall x, \, \varphi$ est encore une formule. C'est un énoncé de stabilité, un peu comme lorsqu'on dit que si $F$ est un sous-espace vectoriel de $E$ alors pour tout scalaire $\lambda$ et tout $u \in F$, le produit $\lambda u $ est encore dans $F$. Stabilité par multiplication dans le cas des e.v. ; stabilité par quantification dans le cas des tes formules.

    Alors effectivement lorsqu'on écrit mathématiquement "pour toute variable $x$ et pour toute formule $\varphi$" ça devient compliqué car on veut écrire $\forall x \in V, \, \forall \varphi \in \mathcal{F}, \, \forall x, \, \varphi \in \mathcal{F}$ mais là on n'y comprend rien. Pour faire comprendre que le but de l'assertion est d'expliquer que la proposition $\forall x, \varphi$ est encore une formule, on l'encadre par des guillemets, on aurait aussi pu mettre des parenthèses ou des crochets ou que sais-je.
  • Cela veut dire que la formule $\forall x.\varphi$ est dans l’ensemble des fonctions quels que soient $x$ variable et $\varphi$ fonction.
    Algebraic symbols are used when you do not know what you are talking about.
            -- Schnoebelen, Philippe
  • egoroff a tout à fait raison. En fait, la manière la plus compacte de définir cela c'est par une grammaire.
    L'ensemble F des formules est donnée par la grammaire suivante :
    $$F ::= A\ |\ \neg F\ |\ F \wedge F\ |\ F \vee F\ |\ \forall V. F\ |\ \exists V. F$$
    Où chaque élément entre $|$ est appelée une production. Si une production est de la forme $f(E_1,...,E_n)$ où les $E_i$ sont soit l'ensemble $F$ soit des ensembles précedemment définis, il faut lire cela comme la définition suivante :
    $$\forall e_1\in E_1, ..., \forall e_n\in E_n, f(e_1,...,e_n)\in F$$
    Quand je fais ce cours à des informaticiens, c'est la syntaxe que j'utilise.
  • Merci pour vos réponses, egoroff et deufeufeu.

    Deufeufeu, est-ce que tu pourrais m'indiquer quelques éléments bibliographiques au sujet de ces questions ? (langage, grammaire, etc.)

    Sinon, pouvez-vous me donner votre avis sur la question concernant ma question sur les théorèmes. Je la rappelle ici :

    1) Un théorème, si je comprends bien, est un énoncé construit à partir des axiomes d'une théorie, par exemple : "la somme des angles d'un triangle dessiné dans le plan, est égale à deux droits" est un thorème pour la géométrie euclidienne ?

    2) Et on dit qu'on a prouvé un théorème si on a pu construire une suite finie d'opérations logiques aboutissant à une tautologie ?

    3) Dans ce cas, si on note $T$ une théorie (un ensemble d'axiomes), $t$ un théorème, on note $ T \vdash t$ pour dire qu'on a prouvé le théorème ? C'est bien ça ("en gros") ?

    Merci d'avance pour vos réponses.
  • Bruno_1 écrivait:
    > 1) Un théorème, si je comprends bien, est un énoncé construit à partir des axiomes d'une théorie

    Je ne dirais pas les choses ainsi, c'est le mot "construit" qui me gêne, je pourrais dire sans problème :

    Un théorème est un énoncé démontré à partir d'un jeu d'axiomes et de règles d'inférences (la logique utilisée)


    > 2) Et on dit qu'on a prouvé un théorème si on a pu construire une suite finie d'opérations logiques aboutissant à une tautologie ?

    Là encore je ne dirais pas les choses ainsi :

    On a prouvé un énoncé P (ce qui lui attribue le titre de théorème) si on a pu construire une suite finie d'énoncés commençant par des axiomes, se terminant par P, et dont chaque étape est l'application d'une règle d'inférence (on peut voir cela comme un graphe orienté plutôt que comme une suite (ne serait-ce que parce qu'il y a plusieurs débuts à cette "suite")).

    ou encore

    On a prouvé un énoncé P (ce qui lui attribue le titre de théorème) si on a pu construire une suite finie d'étapes (boîte noire) dont une sortie est P, telle que les entrées sont
      [1] soit des axiomes [2] soit des théorèmes déjà démontrés
    la sortie est un nouveau théorème obtenu par l'application d'une règle d'inférence aux entrées.


    > 3) Dans ce cas, si on note $T$ une théorie (un ensemble d'axiomes), $t$ un théorème, on note $ T \vdash t$ pour dire qu'on a prouvé le théorème ?

    Une théorie n'est pas un ensemble d'axiomes, mais un ensemble d'énoncés clos par inférence. La propriété d'être un axiome n'est pas intrinsèque à un énoncé, il faut comprendre la notion d'axiome comme une notion de "générateur" d'une théorie

    Je dirais donc, plutôt :
    Dans ce cas, si on note $T$ un ensemble d'énoncés, $t$ un théorème, on note $ T \vdash t$ pour dire que $T$ permet de démontrer $t$ (que $t$ est une conséquence de $T$).
    Si on prend comme définition de "théorie", celle que j'ai donnée ci-dessus, et si on dit que $T$ est une théorie, alors $ T \vdash t$ ne veut dire que $t \in T$
Connectez-vous ou Inscrivez-vous pour répondre.