Substitution

Congru
Modifié (1 Jan) dans Fondements et Logique
Bonjour
Voilà une question qui vaut la peine, je crois.
Comment substituer un terme à une constante dans une formule ?
Bien cordialement.

Réponses

  • Bonsoir,
    Où est le problème ?
  • Congru
    Modifié (1 Jan)
    Bonsoir
    Il s'agit d'utiliser une occurrence de la fonction substitution $subst(F;a;b)$ définie par récursion transfinie, mais dans $(F;a;b)$, $F$ est une formule, $a$ est une suite finie injective de variables et $b$ est une suite de termes de même longueur que $a$.
    Il faut utiliser une occurrence d'une telle fonction.
  • Je ne comprends rien à ce que tu écris. Pourquoi parles-tu de récursion transfinie ???
  • Je parle de récursion transfinie, car la définition de la fonction de substitution utilise le théorème de récursion transfinie.
  • Congru
    Modifié (1 Jan)
    Mais, ce n'était peut-être pas utile de rappeler quel théorème est utilisé pour définir cette fonction. Je ne sais juste pas s'il y a d'autres façons de définir cette fonction, donc j'ai précisé ce détail.
  • "la définition de la fonction de substitution utilise le théorème de récursion transfinie."
    ??????????????????
  • Je pense que congru voulait parler des récurrences qui définissent des objets informatiques comme des arbres (dont les formules sont des cas particuliers).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • @Congru Oui, la question en vaut la peine, la substitution est vraiment un objet non trivial...
    De souvenir, il y a un certain nombre de manière de définir la substitution. De mon côté, j'ai appris la définition de substitution en utilisant l'alpha-renommage. On peut également le faire avec les indices de de Bruijn. Il me semble que tu t'étais penché sur le lambda-calcul : la substitution que tu as vue en lambda-calcul et celles en logique du premier ordre vont beaucoup se ressembler. Je te conseille donc de regarder directement comment cette question est traité dans le poly ou le livre que tu utilisais.
  • Congru
    Modifié (1 Jan)
    Désolé, voici un lien vers un texte qui parle du théorème :
    https://acrobat.adobe.com/id/urn:aaid:sc:EU:95634bc5-0c66-440b-8145-84c34b6687d3
    Ce théorème est pour moi comme le dual du théorème d'induction. Avec ce théorème, on définit des fonctions sur les bienfondés-setlike.
  • Congru
    Modifié (1 Jan)
    @Heuristique, merci pour le conseil. J'ai commenté avant de voir ton message.
    J'ai appris à construire la fonction substitution sur les formules avant de l'apprendre sur les lambda-termes.
    Mais, je suis en train de travailler sur la théorie de la démonstration en ce moment (oui, je reviendrai sur le lambda-calcule après cela et ensuite je reviendrai sur la théorie des ensembles... j'ai des tas de trucs en suspension) du coup je suis revenu sur une démonstration d'un théorème de la théorie de la démonstration où tous les auteurs substituent un terme à un symbole de constante dans une formule. Mais le problème est que la fonction de substitution ne s'applique qu'aux symboles de variables et non aux symboles de constante.
  • @Foys, merci. Au fait j'ai peut-être fait un anglicisme, en anglais ils disent transfinite recursion. Toi et @GaBuZoMeu connaissez peut-être le théorème sous un autre nom, je crois qu'on le nomme aussi de "définition par induction".
  • Cela me semble bizarre de substituer un terme à une constante plutôt qu'à une variable mais, en soi, cela doit pouvoir se définir...
    Pour le quiproquo, il y a bien une différence entre le théorème de récurrence/induction et le théorème de définition par récurrence/induction.
    Le premier te permet de prouver une propriété par induction, le second te permet de définir un objet/une fonction par induction.
    Le premier est équivalent au caractère bien fondé d'un ordre, le second nécessite effectivement des arguments non triviaux.
  • Voilà ! C’est quand même mieux d’engager une discussion pour comprendre où ça bloque plutôt que d’aligner 18 ou 19 points d’interrogation pour toute réponse !
  • GaBuZoMeu
    Modifié (2 Jan)
    Si je mets des points d'interrogation, c'est parce que je ne comprends toujours pas le problème.
    Dans une formule d'un langage du premier ordre, on remplace chaque occurrence de la constante par le terme, pourvu que cette occurrence ne soit pas dans le champ d'une quantification sur une variable ayant le même nom qu'une variable du terme. Pour éviter les ennuis, on peut renommer les variables liées .
    Qu'y a-t-il de transfini là-dedans ?
  • Foys
    Modifié (2 Jan)
    Contrairement à une légende tenace il n'y a pas besoin de se baser sur un théorème d'induction non trivial pour définir et manipuler des objets syntaxiques (arborescents) et des preuves formelles. On peut s'arranger pour dans la règle, obliger le prouveur à lui même livrer les objets en plus des démonstrations formelles elles mêmes (i.e.: à prouver qu'un texte est une formule, à prouver qu'une lettre est une variable libre d'une formule donnée, ou à prouver que ladite lettre est liée dans la formule en question, à prouver qu'une formule donnée est obtenue à partir d'une autre formule donnée par substitution sans capture d'une variable donnée par une autre etc.).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Congru
    Modifié (2 Jan)
    @GaBuZoMeu, moi dans ma démonstration, je substitue dans la formule $F$ en appliquant la fonction $subst$ à $(F;u;v)$, $u$ étant une suite finie et injective de varibles et $v$ étant une suite finie de termes dont la longueur est égale à celle de $u$. La fonction $subst$ est définie par récursion tranfinie. J'utilise des objets mathématiques tels que la fonction $subst$ et non des instructions.
  • Bof bof.
    Pourquoi parlais-tu au début de constante pour en arriver maintenant à des variables ?
  • Congru
    Modifié (2 Jan)
    C'est justement le cœur du problème.
    Je crois qu'il faut utiliser la substitution dans un langage où la constante considérée serait un symbole de variable et non un symbole de constante.
    Donc, il faut créer un autre langage que celui de départ.
  • Foys
    Modifié (3 Jan)
    je substitue dans la formule 𝐹 en appliquant la fonction 𝑠𝑢𝑏𝑠𝑡 à (𝐹;𝑢;𝑣), 𝑢 étant une suite finie et injective de varibles et 𝑣 étant une suite finie de termes dont la longueur est égale à celle de 𝑢. La fonction 𝑠𝑢𝑏𝑠𝑡 est définie par récursion tranfinie.

    @Congru
    Il est possible de remplacer tout ça par un méta énoncé $subst' (v,w,F,G)$ qui peut a posteriori s'interpréter comme "$G$ est obtenu en substituant $w$ à $v$ dans $F$" ($subst'$ est un nouveau symbole de prédicat qui n'apparaît pas dans les formules) avec des règles d'inférence spécifiques:

    0°) formules: 

    0.i) Pour toutes variables $a,b$, $a\notin b$ est une formule

    0.II) Pour toutes formules $F,G$, $(F \to G)$ est une formule

    0.iii): Pour toute formule $F$ et toute variable $x$, $\forall x F$ est une formule.

    1°) Liberté:

    1.i) si $x$ est différente de $y$ et de $z$ alors $x$ n'est pas libre dans $y \notin z$

    1.ii) si $x$ n'est pas libre dans $F$ et n'est pas libre dans $G$ alors $x$ n'est pas libre dans $F \to G$.

    1.iii) si $x$ n'est pas libre dans $F$ alors $x$ n'est pas libre dans $\forall y F$ quelle que soit la variable $y$.

    1.IV) $x$ n'est pas libre dans $\forall x G$ quelle que soit la formule $G$

    2°) Substitutions:

    2.i) $subst'(v,w,(x \notin y), (x \notin y))$, $subst'(v,w,(x \notin v), (x \notin w))$, $subst'(v,w,(v \notin x), (w \notin x))$ et $subst'(v,w,(v \notin v), (w \notin w))$ où $x$ et $y$ sont des variables différentes de $v$ (on définit dans la suite $\perp:= \forall x \forall y, x \notin y$; "$x \in y:= x \notin y \to \perp$" etc)

    2.ii) "si $subst'(v,w,X_1,X_2)$ et $subst'(v,w,Y_1,Y_2)$ alors  $subst'(v,w,(X_1 \to Y_1),(X_2 \to Y_2)$"

    2.iii) si $x$ est différent de $v$ et de $w$ et si $subst'(v,w,P,Q)$ alors $subst'(v,w,\forall x P, \forall x Q)$

    2.iv) $subst'(v,w, \forall v F, \forall v F)$ pour toute formule $F$ et toute variable $v$

    2.v) si $subst' (w,a,F,G)$, $a$ n'est pas libre dans $F$ et différente de $w$, et si $subst'(v,w, \forall a G,H)$" alors $subst' (v,w, \forall w F, H)$


    3°) Définition d'un système de preuves
    On appelle axiome du calcul des prédicats
    3.1°) toute formule de l'une des formes suivantes: i) $(X \to (Y \to Z)) \to ((X \to Y) \to (X \to Z))$, ii) $X \to (Y \to X)$ (avec preuve que les divers X,Y,Z sont bien des formules; cette remarque s'applique aussi aux points suivants)
    3.2°) toute formule de la forme $\forall x F \to G$ telle qu'il existe une variable $t$ et une preuve de $subst'(x,t,F,G)$
    3.3°) $(\forall x (A \to B )) \to ((\forall x A) \to (\forall x B ))$ où $A,B$ sont des formules quelconques et $x$
     une variable quelconque (EDIT: ajout tardif)

    4°) On appelle théorème (de calcul des prédicats)
    4.1°) un axiome du calcul des prédicats
    4.2°) une formule $G$ telle qu'il existe une formule $F$ telle que $F \to G$ et $F$ sont des théorèmes
    4.3°) une formule $F\to \forall x G$ telle que $F\to G$ est un théorème et qu'il existe une preuve de ce que $x$ n'est pas libre dans $F$.

    #####################

    Le prouveur échoue à établir qu'un élément syntaxique est une formule ou bien à prouver une substitution? Pas grave: le résultat final n'est pas démontré, c'est tout.


    Le laïus précédent ne contient AUCUNE croyance sur de prétendus théorèmes d'induction cachés (il ne suppose que connue une notion opérante de variable...): toutes les décompositions de formules sont à la charge du prouveur.

    (Bien évidemment qu'en pratique, toutes les étapes de preuves abordées dans 1 et 2 sont considérées comme superflues, intuitivement évidentes quoique fastidieuses et totalement laissées sous silence et implicites. Nous les mettons sous cette forme pour combattre cet insupportable mythe anti-formaliste qui prétend que les définitions de la logique formelle de base contiennent des références cachées à des théorèmes d'induction/récurrence).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Merci @Foys, ce que tu exposes ne fais pas partie de mes connaissances. Mais ça me fait plaisir d'apprendre de nouvelles choses, je n'ai pas encore tout compris sur ce que tu as dit, mais je vais relire cela dans le but justement de mieux comprendre.
Connectez-vous ou Inscrivez-vous pour répondre.