Version sans JavaScript, en lecture seule : les ateliers, les quiz et l’exécution du code n’y sont pas. Version complète · Catalogue · Se connecter

Feuille d'exercices 7

Premier ordre : le langage

Termes et formules, variables libres et liées, renommage et substitution sans capture. Chapitre 7.

Corrigé
  1. Terme.
  2. Formule atomique.
  3. Ni l'un ni l'autre : $P$ attend un terme, et $R(x, y)$ est une formule.
  4. Formule, close.
  5. Ni l'un ni l'autre : $f$ attend un terme.
  6. Ni l'un ni l'autre : on ne quantifie que des variables, et $a$ est une constante.
Corrigé
  1. Une occurrence de $x$ est libre si elle n'est dans la portée d'aucun quantificateur sur $x$. Une variable est libre dans une formule si elle y a au moins une occurrence libre.
  2. Dans $R(y, x)$, $y$ et $x$ sont libres : hors de la portée de $\forall x$, et le $\exists y$ ne porte que sur $R(x, y)$. Variables libres : $\{x, y\}$.
  3. Seul $z$ est libre ; le $x$ de $R(x, z)$ est lié par le $\forall x$ intérieur, le plus proche. Variables libres : $\{z\}$.
  4. Aucune : la formule est close.
Corrigé
  1. $x$ est libre : ses occurrences dans $R(x, z)$ et $S(x)$ sont hors de la portée de $\forall x$. Elle est aussi liée dans la première partie. $y$ n'est pas libre : sa seule occurrence est liée par $\exists y$.
  2. On renomme le $x$ lié : $(\forall u\, \exists y\, R(f(u), f(y))) \land ((\forall z\, R(x, z)) \to S(x))$.
  3. On ne remplace que les occurrences libres : $(\forall x\, \exists y\, R(f(x), f(y))) \land ((\forall z\, R(t, z)) \to S(t))$. Il faut que $t$ ne contienne pas $z$, sinon il serait capturé par $\forall z$. Si $t = g(z)$ par exemple, on renomme d'abord $z$ en $w$ : $(\forall x\, \exists y\, R(f(x), f(y))) \land ((\forall w\, R(g(z), w)) \to S(g(z)))$.
Corrigé
  1. $y$ apparaît dans $f(y)$ et serait capturé. On renomme : $\exists z\, R(x, z)$, puis on substitue : $\exists z\, R(f(y), z)$.
  2. $\exists y\, (x < y)$ est vraie pour tout $x$. La substitution naïve donne $\exists y\, (f(y) < y)$ : avec $f$ interprété par « plus un », elle dit qu'un entier est plus grand que son successeur, ce qui est faux. La substitution correcte, $\exists z\, (f(y) < z)$, est vraie pour tout $y$, comme la formule de départ l'était pour tout $x$.