Formules du premier ordre — Les-mathematiques.net The most powerful custom community solution in the world

Formules du premier ordre

Modifié (24 Nov) dans Fondements et Logique
Vu les questions récurrentes dans le sous-forum logique, je propose qu'on donne ici au moins deux constructions de l'ensemble des formules d'un langage du premier ordre $L$ donné.

Réponses

  • Modifié (24 Nov)
    Outre la définition de haut en bas, il y a celle, de bas en haut, que je préfère (issue ici du Cori-Lascar) :
    Les auteurs conviennent de noter $\mathrm{At}(L)$ l'ensemble des formules atomiques construites sur la langage $L$. Enfin, les auteurs utilisent l'ensemble $\mathscr{V}=\left\{\begin{array}{c|c}v_n&n\in\Bbb{N}\end{array}\right\}$ des symboles de variables formelles qu'il est possible d'enrichir. Un symbole de variable n'appartenant pas à $\mathscr{V}$, même enrichi, se nomme symbole de métavariable.
  • Comme pour les termes dudit langage, il possible de prouver qu'une formule de $\mathscr{F}(L)$ est équilibrée (au sens de Bourbaki) ou encore vérifie la règles des poids au sens de Cori-Lascar (les deux concepts étant équivalents, comme j'ai pu le montrer, moyennant une réactualisation du texte bourbachique). Bien entendu, le mieux est d'utiliser la notation polonaise gauche au lieu de la notation infixée qui nous contraint d'utiliser les parenthèses....
  • Un très bon moyen de comprendre ces choses est de les implémenter dans un langage informatique.
  • C'est-à-dire ? Écrire un programme qui engendre toutes les expressions dont la taille est bornée par tant ? un programme qui vérifie si une chaîne de caractères est une formule bien formée ? autre chose ?
  • Salut @Thierry Poma  : c'est quoi la notation polonaise gauche ?
  • Modifié (25 Nov)
    Merci @Thierry Poma, comme pour presque toutes mes interventions, j'écris depuis mon téléphone, donc je ne vais pas essayer d'écrire trop de LaTeX. Je compte procéder en plusieurs étapes.
    1) je donne ma construction du monoïde libre de base un ensemble donné
    2) je définis ce que j'appelle un langage fonctionnel
    3) un langage fonctionnel étant donné, je définis l'ensemble des termes de ce langage (ceci va formaliser en quelque sorte la notion d'arbres finis)
    4) je définis ce que j'appelle langage du premier ordre
    5) je définis l'ensemble des termes d'un langage du premier ordre
    6) je définis l'ensemble des formules atomiques d'un langage du premier ordre
    7) je définis l'ensemble des formules d'un langage du premier ordre

    En gros, je pars de 0. N'hésitez pas à proposer vos propres solutions pour chaque étape, j'ai une foule de choses à faire dont plusieurs projets en suspension là, donc je ne suis pas sûr d'écrire ceci en un temps raisonnable sans ressentir trop de culpabilité.
  • Modifié (24 Nov)
    1) soit $A$ un ensemble donné, on considère
    $A':=\bigcup \{ Hom_{\mathcal E ns}(n,A)\mid n\in \mathbb N \}$
    Et on considère $*:A'^2\to A'$ qui à $(u,v)\in A'^2$ associe l'application $w:(dom(u)+dom(v))\to A$ telle que pour tout $z\in dom(u)$, on a $w(z)=u(z)$ et pout tout $z\in (dom(u)+dom(v))\backslash(dom(u))$, on a $w(z)=v(z-(dom(u)))$.
    Alors $(A',*,(0;A;0))$ est le monoïde libre de base $A$.

    Édit.  J'avais oublié le $\bigcup$ dans la définition de $A'$.
    Edit2. Un symbole est sorti lors d'une modification automatique (ou peut-être une modification de la modération), j'avais mal écris le symbole. (C'est $\backslash$)
  • J'aurais spontanément introduit la réunion des ensembles de suites de longueur $n$ plutôt que cet ensemble qui contient un élément pour chaque entier, i.e. en bête bijection avec $\N$ (et ce, quel que soit $A$). Et je me serais passé de morphismes de la catégorie des ensembles au profit d'applications (c'est plus $\mathrm{Fun}$). M'enfin, c'est pas moi l'expert,  hein ?
  • Modifié (24 Nov)
    @Math Coss tes remarques sont très pertinentes, cependant j'ai corrigé mon erreur 3 minutes avant ta remarque, mais je te remercie quand même d'avoir observé l'erreur et d'avoir tenté de le signaler.
  • Modifié (24 Nov)
    Math Coss a dit :
    C'est-à-dire ? Écrire un programme qui engendre toutes les expressions dont la taille est bornée par tant ? un programme qui vérifie si une chaîne de caractères est une formule bien formée ? autre chose ?

    Par exemple; ou encore écrire des programmes qui traduisent des preuves dans un système en des preuves dans un autre système (ex: déduction naturelle vers système de Hilbert). rien que l'écriture d'une classe "formule du premier ordre" (suivi d'un programme qui substitue un terme à une variable proprement, avec gestion des variables libre du terme qui ont des occurrences liées dans la formule) est un défi et oblige à définir algorithmiquement ces objets à un moment où à un autre.
    Quelle est la (ou les) façon(s) intelligente(s) de représenter des formules de logique en machine?

    (avis personnel: c'est bien d'avoir un langage fonctionnel. Je ferais ça en ocaml ou carrément en coq, comme ça ça permet de prouver que le programme ne fait pas n'importe quoi au passage mais les courageux peuvent faire ça en python voire en C/C++).
  • Modifié (25 Nov)
    Notation. Pour tout ensemble $A$, on note $Mon(A)$ le monoïde libre de base $A$, et on note $\Pi _A$ la généralisation de la loi du monoïde $Mon(A)$.

    2) Ici, par langage fonctionnel, j'entends tout couple $(A,a)$ tel que $a$ est une application de $A$ dans $\mathbb N$ et l'image réciproque de $\{0\}$ par $a$  est non vide.
    (En gros je considère les éléments de $A$ comme des symboles de fonction dont l'arité est donnée par $a$)

    3) On se donne un langage fonctionnel $(A,a)$, soient $A',*$ tels que $Mon(A)=(A',*,(0;A;0))$, soit $B$ l'ensemble des $z\in \mathcal P (A')$ tels que pour tout $ f\in A$, pour tout $u\in Hom_{\mathcal Ens} (a(f),A')$, si $im(u)\subseteq z$ alors $*((1;A;\{(0;f)\}),\Pi _A (u))\in z$.
    On a $A'\in B$, donc on a $B\not = \emptyset$, donc $\bigcap B$ est défini.
    On dit que  $\bigcap B$ est l'ensemble des termes du langage fonctionnel $(A,a)$.
    (ici j'ai donné une définition par le haut 🙂)
    Édit. Pour éviter une possible ambiguïté, j'ai remplacé $A'^{a(f)}$ par $Hom_{\mathcal Ens} (a(f),A')$ et j'ai amélioré la rédaction.
  • @Martial : c’est un truc que Christophe affectionne ! Étant données des arités pour les symboles de fonction, et des symboles de constantes, alors tu définis par induction des termes. Si une chaîne $s$ commence par un symbole de constante, i.e. $s=aw$, alors $t(s) := (a,t(w))$. Si $s=fw$ avec $f$ symbole de fonction, $t(s):= f(t(w))$. Exemple : sur le langage avec $0$, $S$, $+$, $.$ et les arités dont tu te doutes, $.+0S0+SSS0SS0$ est bien formé, je crois, et ça devrait donner $(0+S(0)).(S(S(S(0)))+S(S(0)))$.
  • Modifié (25 Nov)
    4) Ici, j'ai une approche très personnelle, commençons par une petite remarque: "pour toute variable $x$, $\forall x$ est un quantificateur".

    a) on se donne un ensemble
    $c:=\{ \to, \wedge, \vee, \lnot, \leftrightarrow \}$ à 5 éléments. On suppose qu'aucun de ces éléments n'est une application.
    (On verra pourquoi après)
    b) on se donne une bijection $v$ de domaine $\mathbb N$
    (ici l'image de $v$ sera notre ensemble de variables)

    c) on se donne deux bijections $e$ et $u$ de domaine $\mathbb N$. 
    On suppose qu'aucun élément de $\bigcup \{im(e),im(u)\}$ n'est une application.
    (Ici les images respectifs de $e$ et $u$ sont respectivement les quantificateurs existentiels et universels)

    d) on se donne un objet mathématique $\sim$ 
    (Ici, $\sim$ jouera le rôle du symbole d'égalité)

    d') on se donne deux ensembles $F$ et $R$, on suppose que $\sim \in R$.
    (Ici $F$ et $R$ sont respectivement les ensembles des symboles de fonction et de relation)

    e) on se donne deux applications $a_F$ et $a_R$ respectivement de domaines $F$ et $R$ et chacun de but $\mathbb N$. On suppose que $a_R (\sim)= 2$.
    (Ici, les deux fonctions sont les fonctions arité)

    f) on suppose $\emptyset =\bigcap \{F,im(v)\}$ et on suppose $\emptyset =\bigcup \{ \bigcap \{a,b\} \vert a,b\in \{im(e),im(u),c\} \}$

    g) On dit que $(c,v,e,u,\sim,(F,a_F),(R,a_R))$ est un langage du premier ordre.

    5) On se donne un langage du premier ordre $L$, soient $c,v,e,u,\sim,F,a_F,R,a_R$ tels que $L=(c,v,e,u,\sim,(F,a_F),(R,a_R))$. On définit $F':=\bigcup \{F,im(v)\}$, on note $a_{F'}$ l'application de domaine $F'$ et de but $\mathbb N$ qui à tout élément $z\in F$ associe $a_F (z)$ et qui à tout élément de $im(v)$ associe $0$.
    $(F',a_{F'})$ est un langage fonctionnel.
    On appelle terme de $L$ tout élément de l'ensemble des termes du langage fonctionnel $(F',a_{F'})$, et on notera $\tau (L)$ l'ensemble des termes du langage fonctionnel $(F',a_{F'})$.

    Édit. J'ai modifié la remarque du début pour la rendre plus pédante. 🙂
  • Modifié (27 Nov)
    6) On se donne un langage du premier ordre $L$. Soient $c,v,e,u,\sim,F,a_F,R,a_R$ tels que $L=(c,v,e,u,\sim,(F,a_F),(R,a_R))$.
    Soient $A',*$ tels que $Mon(\bigcup \{R,\tau (L)\})=(A',*,(0;\bigcup \{R,\tau (L)\});0))$.
    On définit $At(L):=\{*(( 1;\bigcup \{R,\tau (L)\};\{(0;u')\}),\Pi _{\bigcup \{R,\tau (L)\}} (v'))\vert u'\in R \bigwedge v'\in Hom_{\mathcal E ns} (a_R (u'),A')\bigwedge im(v')\subseteq \{ (1; \bigcup \{R,\tau (L)\}; \{(0;t)\})\vert t\in \tau (L) \} \}$

    7) On se donne l'application $a_c$ de source $\bigcup \{c,im(e),im(u),At(L)\}$ et de but $\mathbb N$ qui à tout élément de $\bigcup \{ im(e),im(u)\}$ associe $1$ et à $\lnot$ associe $1$ et à tout élément de $c\backslash \{ \lnot \}$ associe $2$, et à tout élément de $At(L)$ associe $0$.
    $(\bigcup \{c,im(e),im(u),At(L)\},a_c)$ est un langage fonctionnel, on note $Formule(L)$ l'ensemble des termes du langage fonctionnel $(\bigcup \{c,im(e),im(u),At(L)\},a_c)$.

    Notation. Pour tout $i\in \mathbb N$, on note $\forall v(i):=u(i)$ et on note $\exists v(i):=e(i)$

    Remarque. La raison pour laquelle j'ai demandé que certains symboles ne soient pas des applications était pour m'assurer qu'aucun d'entre eux ne puisse appartenir à l'ensemble des formules atomiques.

    Édit. J'avais oublié $\bigcup$ à deux instances de $(\bigcup \{c,im(e),im(u),At(L)\},a_c)$, c'est corrigé. Si vous voyez une erreur, signalez le s'il vous plaît.
    Édit2. Encore un $\bigcup$ oublié, cette fois ci, c'était dans $\bigcup \{ im(e),im(u) \}$, c'est corrigé.
  • Modifié (25 Nov)
    Si les gens n'ont aucun complexe à utiliser le langage ensembliste, alors on peut procéder comme suit. Soit $V_0:=\emptyset$ et pour tout $n\in \N$ soit $V_{n+1}:= \bigcup_{i=0}^n \mathcal P (V_i)$. Soit $V_{\omega}:= \bigcup_{n\in \N} V_n$ (les initiés reconnaîtront les premiers termes de la hiérarchie de Von Neumann: les éléments de $V_{\omega}$ s'appellent "ensembles héréditairement finis". NB: on pourrait remplacer $\omega$ par n'importe quel ordinal limite dans ce qui va suivre).
    Si $x\in V_{\omega}$, le rang $rg(x)$ de $x$ est le plus petit entier $n$ tel que $x\in V_n$. Noter que pour tous $x,y\in V_{\omega}$ tels que $x\in y$, on a $rg(x) < rg(y)$.

    Noter que $V_{\omega}$ est stable par les opérations suivantes: $x,y \mapsto (x,y) (= \{\{x\},\{x,y\}\})$,$x \mapsto \bigcup x$ $x,y \mapsto x \times y$, $x,y\mapsto x^y$ etc. On note $(a,b,c):= (a,(b,c))$, $(a,b,c,d) := (a,(b,c,d))$ etc. $V_{\omega}$ contient $\N$ (mais $\N\notin V_{\omega}$)

    Pour tout $x\in V_{\omega}$ on pose $Succ(x):= x \cup \{x\}$ (aucun élément $y$ de $V_{\omega}$ n'est tel que $y\in y$ et donc $Succ$ ajoute exactement un élément à $x$). $Succ$ est injective ($x$ est l'unique élément de $Succ(x)$ dont le rang est le plus grand).

    I) Lambda-termes.
    Soit $L$ l'intersection de toutes les parties $P$ de $V_{\omega}$ telles que:
    -pour tous $c,x\in V_{\omega}$ tels que $x\in c$ , $(c,0,x) \in P$
    -pour tous $a,b,c\in V_{\omega}$, si $(c,a)\in P$ et $(c,b)\in P$ alors $(c,1,(c,a),(c,b)) \in P$
    -pour tous $f,c\in V_{\omega}$, si $(Succ(c),f)\in P$ alors $(c,2,(Succ(c),f))\in P$.

    $L$ est donc constitué des couples obtenus par application d'un nombre fini d'étapes suivantes:  $Var_c(x):= (c,0,x)\in L$, pour tous $a,b,c\in V_{\omega}$ tels que $(c,a), (c,b)\in L$, $App_c(a,b):= (c,1,(c,a),(c,b))\in L$ et enfin pour tous $c,f$ tels que $(Succ(c),f) \in L$, $Abs (c,f):= (c,2,(Succ(c),f)) \in L$ (NB: certaines redondances dans la définition sont faites pour assurer facilement que chaque terme a un rang strictement plus grand que ses sous-termes, ainsi des constructions par récurrence seront définies sans obstacle psychologique).

    Pour tout $c\in V_{\omega}$, on note $L_c$ l'ensemble des éléments de $L$ dont la première coordonnée vaut $c$.
    Les couples $(c,x)$ appartenant à $L$ (i.e. les éléments de $L_c$) s'appellent lambda-termes à variables libres dans $c$ (remarque: la lettre $c$ a été choisie pour "contexte").
     
    II) Changement d'ensemble de variables et substitutions.

    1°) Soient $c,d\in V_{\omega}$. Soit $e:  c\to d$ une fonction. alors $e$ se prolonge d'une unique manière en fonction $\hat e$ de $Succ(c)$ dans $Succ(d)$ en posant $\hat e (c):=d$.

    2°) Soient $c,d\in V_{\omega}$ et $e: c \to d$. On définit par induction sur le rang des objets une fonction $\Gamma_{c,d,e}: L_c \to L_d$ ("changement de contexte") en posant:
    $\Gamma_{c,d,e} (Var_c(x)) := Var_d(e(x))$,
    $\Gamma_{c,d,e} (App_c(a,b)):= App_d (\Gamma_{c,d,e}(a), \Gamma_{c,d,e} (b))$ et enfin,
    $\Gamma_{c,d,e} (Abs_c (f)):= Abs_d (\Gamma_{Succ(c), Succ(d), \hat e} (f))$.

    3°) (notation lambda) Etant donné $c\in L$ et $x\in C$, soit $u$ l'application de $c$ dans $Succ (c \backslash \{x\})$ définie par $u(x) = c \backslash \{x\}$ et $u(y) = y$ si $y \neq x$. Soit $f\in L_c$. Alors on note $\lambda x. f$ l'élément $Abs_{c \backslash \{x\}} \left (\Gamma_{c, Succ(c \backslash \{x\}, u)} (f)\right )$ de $L_{c \backslash \{x\}}$.
    (NB: noter que le problème d'alpha-renommage des variables liées est trivialisé: $\lambda a. \lambda b .(ab)b$ et $\lambda x \lambda y .(xy)y$ sont des éléments identiques de $L_{\emptyset}$ avec cette construction.)

    4°) (substitution) pour tout $x \in V_{\omega}$, on note $i_x: a\in x \mapsto a \in Succ(x) (= x \cup \{x\})$ l'injection canonique.
    Soient $c,d\in V_{\omega}$ et $\varepsilon: c \to L_d$ une fonction. Pour tout $x\in Succ(c)$ On pose $\tilde {\varepsilon} (x):=$
     $\Gamma_{d, Succ d, i_d} (\varepsilon (x))$ si $x\in c$;
    $\tilde {\varepsilon} (c) := Var_{Succ (d)} (d)$. $\tilde {\varepsilon}$ est une fonction de $Succ(c)$ dans $L_{Succ(d)}$.
    Ensuite on définit par induction sur le rang des objets, pour tous $c,d\in V_{\omega}$ et tout $\varepsilon: c \to L_d$,
    $\Sigma_{c,d,\varepsilon} (Var_c(x)):= \varepsilon (x)$,
    $\Sigma_{c,d,\varepsilon } (App_{c} (a,b)):= App_d (\Sigma_{c,d,\varepsilon}(a),\Sigma(c,d,\varepsilon) (b))$
    $\Sigma_{c,d,\varepsilon} (Abs_c(f)) := Abs_d (\Sigma_{Succ (c), Succ(d), \tilde{\varepsilon} (f)})$.

    Etant donnés $c,x_1,...,x_n\in V_{\omega}$ (avec les $x_i$ distincts mais n'appartenant pas forcément à $c$) et $t_1,...,t_n \in L_c$, on pose
    $v(y):=Var_c(y)$ si $y \in c \backslash \{x_1,...,x_n\}$ et pour tout $i$, $v(x_i):= t_i$. Alors $v$ est une fonction de $c \cup \{x_1,...,x_n\}$ dans $L_c$ et pour tout $f\in L_{c \cup \{x_1,...,x_n\}}$ on note $f[x_1:= t_1, x_2:= t_2, ... x_n := t_n] := \Sigma_{c \cup \{x_1,...,x_n\}, c , v} (f)$.

    Ceci réalise la substitution sans capture (i.e. sans problème vis-à-vis des variables liées).
     
    5°) Comment avoir un ensemble de variables infini?
    Comme dit en préambule, si $c$ est votre ensemble infini, remplacer $\omega$ par un ordinal limite $\theta$ tel que $c\in V_{\theta}$. TOUTE la construction précédente s'adapte mutatis mutandis dans $V_{\theta}$. Les rangs des objets sont des ordinaux. Ca ne fait pas de différence. Pour un ensemble dénombrable de variables on prendra $\theta := \omega + \omega$ etc.

    6°) Qu'est-ce qu'une formule du premier ordre sur une signature?
    C'est un cas particulier de lambda-terme. Le lecteur peut en donner une définition à partir de ce qui précède et de celle qu'il connaît déjà. Toutes les difficultés syntaxiques de ces notions sont déjà prises en charge plus haut. Il y aura des éléments dédiés dans $c$ notés $\forall, \exists$ et "$\forall x f$" abrège$\forall (\lambda x.f)$ par exemple.

    7°) Existe-t-il des implémentations informatiques de ce qui précède?

Connectez-vous ou Inscrivez-vous pour répondre.
Success message!