syntaxic.tex

\subsection{Description syntaxique des morphismes de formules}

Étudions maintenant les morphismes de formules, qui sont ici des transformations
naturelles entre faisceaux. Regardons un peu plus précisément comment elles se
comportent. Soient $F,G\in\C_\psh(\Sigma)$ deux formules et $\theta:F\rightarrow F$
une transformation naturelle. Regardons comment elle doit se comporter~:

\[ \theta_\star : F\star \rightarrow G\star \]

L'existence de cette fonction nous dit que l'on renomme les variables de $F$ en des
variables de $G$, éventuellement en en contractant certaines. De plus, pour chaque
$R$ relation on a~:

\[ \theta_R : FR\rightarrow GR\]

Si on regarde comment $\phi_F$ et $\phi_G$ sont définies, cela signifie que chaque
instance de relation de $F$ est envoyée sur une instance de la même relation de $G$,
de nouveau en en contractant éventuellement certaines. Finalement, la contrainte
de naturalité est la suivante~:

\[\begin{tikzcd}
    F\star \arrow[d, "\theta_\star"] & FR_j \arrow[l, "Ff_i^j"]
                                            \arrow[d, "\theta_{R_j}"] \\
    G\star & GR_j \arrow[l, "Gf_i^j"] \\
\end{tikzcd}\]

Cela nous dit qu'après avoir renommé les variables de $F$ par $\theta_\star$, les
instance de relation sont envoyées sur des instances identiques dans $G$.

Ces différentes opérations nous rappellent un peu le calcul des séquents, et
c'est en effet le cas. Afin de le définir plus formellement, il va falloir décrire
les formules sous forme de séquents. On conseille donc de retourner voir la
définition \ref{formSeq}.

Nous rappelons maintenant les règles de déduction structurelle adaptées à nos séquents
(ce sont presque exactement celles du calcul des séquents intuitioniste).

\begin{defi}{Règles de déduction}
    Commençons par la règle de l'$\alpha$-renommage~:

    \[ \tproof{ \hypo{\Gamma, x\vdash \Delta}
         \infer1[$y\not\in\Gamma$]{\Gamma, y\vdash \Delta[x/y]} }\]

    Viennent ensuite les règles de commutation~:

    \[ \tproof{ \hypo{\Gamma, x, y, \Xi\vdash \Delta}
         \infer1{\Gamma, y, x, \Xi\vdash \Delta} }
       \qquad
       \tproof{ \hypo{\Gamma\vdash \Delta_1, R(\mathbf{x}), S(\mathbf{y}), \Delta_2}
         \infer1{\Gamma\vdash \Delta_1, S(\mathbf{y}), R(\mathbf{x}), \Delta_2} }
    \]

    Maintenant, les règles d'affaiblissement~:

    \[ \tproof{ \hypo{\Gamma\vdash\Delta}
         \infer1{\Gamma, x\vdash \Delta} }
       \qquad
       \tproof{ \hypo{\Gamma\vdash\Delta}
         \infer1{\Gamma\vdash\Delta,R(\mathbf{x})} }\]

    Enfin, les règles de contraction~:

    \[ \tproof{ \hypo{\Gamma,x,y\vdash\Delta}
         \infer1{\Gamma, x\vdash\Delta[y/x]} }
       \qquad
       \tproof{ \hypo{\Gamma\vdash\Delta, R(\mathbf{x}), R(\mathbf{x})}
         \infer1{\Gamma\vdash\Delta, R(\mathbf{x})} }\]

\end{defi}

On arrive maintenant au théorème de description syntaxique~:

\begin{theo}{Description syntaxique d'un morphisme de formule}
    Soient $F,G\in\C_\Sigma$ deux formules. Alors il existe une transformation
    naturelle $\theta:F\rightarrow G$ si et seulement si $\ml{\phi_F}$ peut être réécrit
    en $\ml{\phi_G}$ selon les règles de déduction ci-dessus.
\end{theo}

\begin{pv}
    Admis
\end{pv}

Pour des raisons de temps, on n'a pas essayé de prouver ce théorème. Il pourrait
cependant être intéressant de le faire, voir d'essayer de le généraliser aux nouveau
type de séquents introduit un peu plus loin, en \ref{commaSeq}.

\begin{rem}
    On pourrait même tenter d'établir une bijection entre des arbres de preuve
    et des transformations naturelles, mais certains arbres donnent les mêmes
    transformations, donc il faudrait quotienter par la bonne relation, ce qui
    n'est pas trivial.
\end{rem}

On peut maintenant se demander ce que donnent les constructions classiques en terme
de séquent.

\begin{lem}\label{seqStandarts}
    Soient $\phi_1$, $\phi_2$ deux formules telles que $\ml{\phi_1} = \Gamma\vdash\Delta$
    et $\ml{\phi_2} = \Xi\vdash\Omega$ (on suppose $\Gamma\cap\Xi=\emptyset$), alors~:

    \begin{align*}
        \ml{\phi_\mathbf{0}} &=~\vdash \\
        \ml{\phi_\mathbf{1}} &= x\vdash R_1(x,\dots, x),\dots R_n(x, \dots, x) \\
        \ml{\phi_1\wedge\phi_1} &= \Gamma,\Xi\vdash\Delta,\Omega \\
        \ml{\phi_{y\star}} &= x\vdash
    \end{align*}
\end{lem}

\subsection{Représentation en séquents de $\tsigma$}\label{seqTSigma}

\begin{defi}{Représentation en séquents de $\tsigma$}\label{commaSeq}
    Soit $f : n\ast\rightarrow X$ un objet de $\tsigma$. On note
    $\ml{\phi_X} = \Xi\vdash\Phi$. $f$ induit une fonction de $x_1,\dots x_n$ vers $\Xi$.
    On note le séquent associé à $f$ de la façon suivante~:

    \[ \ml{f} := x_1, \dots x_n; \Xi - \im f\vdash \Phi',\mathcal{E} \]

    Où $\Phi'$ est $\Phi$ où l'on a remplacé chaque variable par une de ses préimage
    par $f$ si elle est dans l'image de $f$. De plus, $\mathcal{E}$ est une suite
    d'égalités~: $x_i=x_j\in\mathcal{E}$ si $f(x_i) = f(x_j)$ et $i\neq j$.

    Une formule de la forme $\Xi;\Gamma\vdash \Phi$ représente une formule ayant comme
    variables libre $\Xi$ et comme variables liées $\Gamma$. De plus on a toujours
    $\Xi\cap\Gamma=\emptyset$.
\end{defi}

\begin{exs}
    \item $\ml{\iota\ast} = x;\vdash$
    \item $\ml{\iota yR} = x_1,\dots x_{\ar(R)};\vdash R(x_1, \dots, x_{\ar(R)})$
    \item Si on note $\tilde{0} : 2\rightarrow 2$ la fonction constante égale à
        zéro, on peut prendre $\theta : 2\ast\rightarrow X$ où $X$ est une formule
        vide à deux variables telle que $\theta_\star = \tilde{0}$. Dans ce cas, on
        a $\ml{\theta} = x,y;\vdash x = y$~: c'est la diagonale ! On remarque donc
        qu'avec ces conventions, il est possible de définir la diagonale même en
        l'absence de relation. Cela revient à dire que l'égalité fait toujours
        partie des relations autorisées, ce qui est une convention commune.
\end{exs}

\begin{lem}
    Soient $X,Y\in\tsigma$. On note $X+Y$ leur coproduit. Notons aussi
    $\ml{X} = \Xi;\Gamma\vdash\Phi$ et $\ml{Y} = \Xi';\Gamma'\vdash\Phi'$ (on suppose
    tous les ensembles de variables disjoints).
    
    Alors $\ml{X+Y} = \Xi,\Xi';\Gamma,\Gamma'\vdash\Phi,\Phi'$.
\end{lem}

\begin{lem}
    Notons $\mathbf{0}$ l'élément initial de $\tsigma$.
    
    Alors $\ml{\mathbf{0}} = ;\vdash$.
\end{lem}

\begin{lem}
    Soient $X,Y\in\tsigma$. On note $<X> = \Xi,x;\Gamma\vdash\Phi$ et
    $\ml{Y} = \Xi',y;\Gamma'\vdash\Phi'$. On considère de plus les flèches allant de
    $\ml{Z} = x;\vdash$ vers $X$ (resp $Y$) qui sélectionnent la variable $x$ (resp $y$).

    Alors $\ml{X +_Z Y} = \Xi,\Xi',x;\Gamma,\Gamma'\vdash\Phi,\Phi'[y/x]$.
\end{lem}

\begin{pv}
    Tous ces lemmes sont des conséquences directes du théorème \ref{commaCL}.
\end{pv}