Preuve et alpha-équivalence

Congru
Modifié (2 May) dans Fondements et Logique
Soient $L$ un langage (du premier ordre), soient $A,B \in \mathcal F L$ tels que $A$ et $B$ sont $\alpha$ équivalents.
Quelqu'un sait-il si on a $\vdash (A\iff B )$ ou si pour toute $L$-théorie $T$, on a $(T\vdash A )\iff (T\vdash B )$ ? (Attention ! Il ne faut pas passer par le théorème de complétude!)

Ma notion de preuve est celle du Cori/Lascar. Je me demande si je ne vais pas devoir rajouter aux axiomes les $ A\iff B $ où $A$ et $B$ sont $\alpha$-équivalents.

Réponses

  • Désolé il manque des .dll pour comprendre le sens de la demande.

    (Bisous AD, repose-toi un peu, je vais veiller pour toi aux photos de syntaxes et de syntagmes dans ce fil)


  • Que veut dire $\alpha$-équivalents ? 
  • @Cyrano $\alpha$-équivalence comme en $\lambda$-calcul. Intuitivement, les deux formules sont égales à renommage des variables liées près.
  • Cyrano
    Modifié (2 May)
    Ah d'accord. On a un théorème de réalphabétisation des variables liées en logique du premier ordre qui dit que $$\vdash \forall x \varphi \Leftrightarrow \forall y \varphi (x \mapsto y),$$ si $y$ n'a aucune occurrence dans $\varphi.$
  • Merci @Cyrano, est-ce que tu peux m'envoyer vers la littérature là dessus ?
  • Cori-Lascar, tome 1, page 233. :)
  • Foys
    Modifié (3 May)
    Pour la métathéorie il faut vraiment bosser avec des représentations des formules (ou lambda-termes) où il n'y a pas d'alpha-équivalence, sinon vous allez devenir fou.

    Solutions possibles:
    -indices de De Bruijn
    -Niveaux de De Bruijn: étant donné le langage du premier ordre $\mathcal L$ fixé, et $(\mathbf x_k)_{k\in \N}$ une suite de lettres distinctes ne figurant pas dans $L$ et $d\in \N$ on appelle $d$-terme un terme dont les variables libres sont toutes dans $\{\mathbf x_k, k \leq d\}$, et $d$ formule une formule définie par induction de la façon suivante:
    -les expressions de la forme $R(t_1,...,t_n)$ où chaque $t_i$ est un $d$-terme sont des $d$-formules
    -$\neg F$ et $F * G$ sont des $d$-formules lorsque $F$ et $G$ en sont ($*$ désignant un des connecteurs ligiques)
    -$Q_{\mathbf x_{d+1}} H$ est une $d$-formule si $H$ est une $d+1$-formule et $Q$ un quantificateur.

    -les $0$-formules sont aussi appelées formules closes.

    Moralité: il ne sert strictement à rien (au niveau méta) d'être "libre" de choisir les variables liées d'une formule. Ce système les impose pour vous.

    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 @Cyrano tu me sauve la vie.
    Merci @Foys pour les informations supplémantaires.
  • Congru
    Modifié (2 May)
    J'explique, ce qu'il y a dans le Cori/Lascar ne donne pas une réponse à ma question initiale, mais ça répond à un problème qui m'avait conduit à ma question. Donc c'est super.
    La réponse de @Foys est plus dans le sens de ma question initiale.
    Donc normalement c'est @Cyrano qui m'a donné une information supplémentaire  :D

    Comment formalise-t-on cette histoire de "aucune occurrence libre de la variable $x$ n'est dans le scope d'un quantificateur liant une variable du terme $t$" ? J'avais tendance à remplacer cette condition par "aucune variable du terme $t$ n'est liée".
  • Je recommande ce très bon article (en anglais) qui aborde conceptuellement les indices de De Bruijn, sous une forme générale: https://golem.ph.utexas.edu/category/2021/08/you_could_have_invented_de_bru.html

    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, je vais consulter le lien.
  • En fait, le Cori-Lascar utilise une syntaxe très laxiste sur les variables liées, qui autorise les conflits de notation. Par exemple, on peut se permettre d'écrire, $$\forall x (P(x) \Rightarrow \exists x Q(x)).$$ En soi, les conventions sur la portée des quantificateurs entraine la non-ambiguïté d'une telle formule. (Le pour tout ne concerne que le premier x et le il existe que le second.) C'est ce qui fait aussi qu'un analyste peut parfois avoir envie d'écrire $\int_0^t f(t) dt.$ En soi, il sait ce qu'il fait, cela ne créera aucun problème majeur.

    Cela dit, pour éviter de telles écritures, on peut appliquer systématiquement le théorème de réalphabétisation des variables liées de telle sorte à ce que toutes les lettres liées soient différentes et, bien sûr, soient différentes des variables libres déjà en place.
  • Congru
    Modifié (3 May)
    Merci @Cyrano. Mais j'avais vraiment un problème pour formaliser "aucune occurrence libre de la variable $x$ n'est dans le scope d'un quantificateur liant une variable du terme $t$". Un problème qui date d'une époque où je n'avais pas les outils et depuis cette époque j'avais trouvé refuge dans le fait de remplacer cette condition par "aucune variable du terme $t$ n'est liée". En gros j'évitais le problème de capture de cette façon, quitte à renommer les variables liées.
    Je me suis rendu compte hier que j'ai maintenant des outils pour formaliser "aucune occurrence libre de la variable $x$ n'est dans le scope d'un quantificateur liant une variable du terme $t$". C'est juste une définition par récursion transfinie dont j'ai une très grande habitude.


  • Solution pour formaliser "aucune occurrence libre de la variable x n'est dans le scope d'un quantificateur liant une variable du terme t" :


Connectez-vous ou Inscrivez-vous pour répondre.