3_structures.tex

\section{Estructuras}

  % Lemma 133. Con prueba. Lemma 43.
  \begin{lemma} \label{lemma_43}
    \PN Sea $\mathbf{A}$ una estructura de tipo $\tau$ y sea $t \in \TAU$. Supongamos que $\vec{a}, \vec{b}$ son
    asignaciones tales que $a_{i} = b_{i}$ cada vez que $x_{i}$ ocurra en $t$, entonces $t^{\mathbf{A}}[\vec{a}] =
    t^{\mathbf{A}}[\vec{b}]$.
  \end{lemma}
  \begin{proof}
    \PN Sea
    \begin{center}
      Teo$_{k}$: El lema vale para $t \in T_{k}^{\tau}$
    \end{center}
    \PN Probaremos este lema por inducción en $k$.

    \vspace{3mm}
    \PN \underline{Caso Base:} \begin{tabular}{|c|} \hline Teo$_{0}$ \\\hline \end{tabular} Sea $t \in T_{0}^{\tau}$ y
    sean $\vec{a}, \vec{b}$ asignaciones tales que $a_{i} = b_{i}$ cada vez que $x_{i}$ ocurra en $t$, entonces
    \[
      t \in Var \cup \mathcal{C}
    \]
    \PN es decir, sucede una de las siguientes:
    \begin{itemize}
      \item $t = x_{i}$, con $x_{i} \in Var$:
        \[
          t^{\mathbf{A}}[\vec{a}] = a_{i} = b_{i} = t^{\mathbf{A}}[\vec{b}]
        \]
      \item $t = c$, con $c \in \mathcal{C}$:
        \[
          t^{\mathbf{A}}[\vec{a}] = i(c) = t^{\mathbf{A}}[\vec{b}]
        \]
    \end{itemize}

		\PN \underline{Caso Inductivo:} \begin{tabular}{|c|} \hline Teo$_{k} \Rightarrow$ Teo$_{k + 1}$ \\\hline
    \end{tabular} Sea $t \in T_{k+1}^{\tau}$ y sean $\vec{a}, \vec{b}$ asignaciones tales que $a_{i} = b_{i}$ cada vez
    que $x_{i}$ ocurra en $t$, entonces
    \[
      t \in T_{k}^{\tau} \cup \{f(t_{1}, \dotsc, t_{n}): f \in \mathcal{F}_{n},n\geq 1,t_{1}, \dotsc, t_{n} \in
      T_{k}^{\tau}\}
    \]
    \PN es decir, sucede una de las siguientes:
    \begin{itemize}
      \item $t \in T_{k}^{\tau}$: Aplicando HI y utilizando el hecho de que $T_{k}^{\tau} \subseteq T_{k+1}^{\tau}$,
      obtenemos que Teo$_{k+1}$ vale.
      \item $t = f(t_{1}, \dotsc, t_{n})$, con $f \in \mathcal{F}_{n} \ n \geq 1 \ \text{y} \ t_{1}, \dotsc, t_{n} \in
      T_{k}^{\tau}$: Notar que para cada $j = 1, \dotsc, n$, tenemos que $a_{i} = b_{i}$ cada vez que $x_{i}$ ocurra en
      $t_{j}$, lo cual por Teo$_{k}$ nos dice que:
      \[
        t_{j}^{\mathbf{A}}[\vec{a}] = t_{j}^{\mathbf{A}}[\vec{b}] \qquad \text{para} \ j = 1, \dotsc, n
      \]
      \PN Se tiene entonces que
      \begin{eqnarray*}
        t^{\mathbf{A}}[\vec{a}] &=& i(f)(t_{1}^{\mathbf{A}}[\vec{a}], \dotsc, t_{n}^{\mathbf{A}}[\vec{a}]) \\
        &=& i(f)(t_{1}^{\mathbf{A}}[\vec{b}], \dotsc, t_{n}^{\mathbf{A}}[\vec{b}]) \\
        &=& t^{\mathbf{A}}[\vec{b}]
      \end{eqnarray*}
    \end{itemize}
  \end{proof}

  % TODO
  % Lemma 134. Con prueba. Lemma 44.
  \begin{lemma} \label{lemma_44}
    \PN \newline
    \begin{enumerate}[(a)]
      \item $Li((t \equiv s)) = \{v \in Var: v$ ocurre en $t$ ó $v$ ocurre en $s\}$
      \item $Li(r(t_{1}, \dotsc, ,t_{n})) = \{v \in Var: v$ ocurre en algún $t_{i}\}$
      \item $Li(\lnot \varphi) = Li(\varphi)$
      \item $Li((\varphi \eta \psi)) = Li(\varphi) \cup Li(\psi)$
      \item $Li(Qx_{j}\varphi) = Li(\varphi)-\{x_{j}\}$
    \end{enumerate}
  \end{lemma}
  \begin{proof}
    \PN \newline
    \begin{enumerate}[(a)]
      \item son triviales de las definiciones, teniendo en cuenta que si una variable $v$ ocurre en $(t\equiv s)$ (resp. en $r(t_{1}, \dotsc, t_{n})$) entonces $v$ ocurre en $t \ \text{o} \ v$ ocurre en $s$ (resp.$v$ ocurre en algun $ t_{i}$)
      \item son triviales de las definiciones, teniendo en cuenta que si una variable $v$ ocurre en $(t\equiv s)$ (resp. en $r(t_{1}, \dotsc, t_{n})$) entonces $v$ ocurre en $t \ \text{o} \ v$ ocurre en $s$ (resp.$v$ ocurre en algun $ t_{i}$)
      \item es similar a (d)
      \item Supongamos $v \in Li((\varphi \eta \psi))$, entonces hay un $i$ tal que $ v$ ocurre libremente en $(\varphi
        \eta \psi )$ a partir de $i$. Por definición tenemos que ya sea $v$ ocurre libremente en $\varphi$ a partir de
        $i-1$ ó $v$ ocurre libremente en $\psi$ a partir de $i-\left\vert (\varphi \eta \right\vert$, con lo cual $v \in
        Li(\varphi) \cup Li(\psi)$.

        \PN Supongamos ahora que $v \in Li(\varphi) \cup Li(\psi)$. Supongamos $v \in Li(\psi)$. Por definición tenemos
        que hay un $i$ tal que $v$ ocurre libremente en $\psi$ a partir de $i$. Pero notese que esto nos dice por definicion que $v$ ocurre libremente en $(\varphi \eta \psi )$ a partir de $ i+\left\vert (\varphi \eta \right\vert $ con lo cual $v\in Li((\varphi \eta \psi ))$.
      \item Supongamos $v\in Li(Qx_{j}\varphi )$, entonces hay un $i$ tal que $v$ ocurre libremente en $Qx_{j}\varphi $ a partir de $i$. Por definicion tenemos que $v\neq x_{j} \ \text{y} \ v$ ocurre libremente en $\varphi $ a partir de $ i-\left\vert Qx_{j}\right\vert $, con lo cual $v\in Li(\varphi )-\{x_{j}\}$
      Supongamos ahora que $v\in Li(\varphi )-\{x_{j}\}$. Por definicion tenemos que hay un $i$ tal que $v$ ocurre libremente en $\varphi $ a partir de $i$. Ya que $v\neq x_{j}$ esto nos dice por definicion que $v$ ocurre libremente en $Qx_{j}\varphi $ a partir de $i+\left\vert Qx_{j}\right\vert $, con lo cual $v\in Li(Qx_{j}\varphi )$.
    \end{enumerate}
  \end{proof}

  % Lemma 135. Con prueba. Lemma 45.
  \begin{lemma} \label{lemma_45}
    \PN Supongamos que $\vec{a}, \vec{b}$ son asignaciones tales que si $x_{i} \in Li(\varphi)$, entonces $a_{i} =
    b_{i}$, entonces $\mathbf{A} \models \varphi \lbrack \vec{a}] \Leftrightarrow \mathbf{A} \models \varphi \lbrack
    \vec{b}]$.
  \end{lemma}
  \begin{proof}
    \PN Sea
      \begin{center}
        Teo$_{k}$: El lema vale para $\varphi \in F_{k}^{\tau}$
      \end{center}
      \PN Probaremos este lema por inducción en $k$.

      \vspace{3mm}
      \PN \underline{Caso Base:} \begin{tabular}{|c|} \hline Teo$_{0}$ \\\hline \end{tabular} Sea $\varphi \in
      F_{0}^{\tau}$ y sean $\vec{a}, \vec{b}$ asignaciones tales que si $x_{i} \in Li(\varphi)$ entonces $a_{i} = b_{i}$
      entonces
      \[
        \varphi \in \{(t \equiv s): t, s \in T^{\tau}\} \cup \{r(t_{1}, \dotsc, t_{n}): r \in \mathcal{R}_{n}, n \geq 1,
        t_{1}, \dotsc, t_{n} \in T^{\tau}\}
      \]
      \PN es decir, sucede una de las siguientes:
      \begin{itemize}
        \item $\varphi = (t \equiv s)$ con $t, s \in T^{\tau}$:
          \begin{eqnarray*}
            \mathbf{A} \models \varphi[\vec{a}] &\Leftrightarrow& \mathbf{A} \models (t \equiv s)[\vec{a}] \\
            &\Leftrightarrow& t^{\mathbf{A}}[\vec{a}] = s^{\mathbf{A}}[\vec{a}] \\
            &\Leftrightarrow& t^{\mathbf{A}}[\vec{b}] = s^{\mathbf{A}}[\vec{b}] \qquad
              (\text{Por} \ \textbf{Lemma~\ref{lemma_43}}) \\
            &\Leftrightarrow& \mathbf{A} \models (t \equiv s)[\vec{b}] \\
            &\Leftrightarrow& \mathbf{A} \models \varphi[\vec{b}]
          \end{eqnarray*}

        \item $\varphi = r(t_{1}, \dotsc, t_{n})$ con $r \in \mathcal{R}_{n}, n \geq 1, t_{1}, \dotsc, t_{n} \in
          T^{\tau}$:
          \begin{eqnarray*}
            \mathbf{A} \models \varphi[\vec{a}] &\Leftrightarrow& \mathbf{A} \models r(t_{1}, \dotsc, t_{n})[\vec{a}] \\
            &\Leftrightarrow& r(t_{1}^{\mathbf{A}}[\vec{a}], \dotsc t_{n}^{\mathbf{A}}[\vec{a}]) \in i(r) \\
            &\Leftrightarrow& r(t_{1}^{\mathbf{A}}[\vec{b}], \dotsc t_{n}^{\mathbf{A}}[\vec{b}]) \in i(r) \qquad
              (\text{Por} \ \textbf{Lemma~\ref{lemma_43}}) \\
            &\Leftrightarrow& \mathbf{A} \models r(t_{1}, \dotsc, t_{n})[\vec{b}] \\
            &\Leftrightarrow& \mathbf{A} \models \varphi[\vec{b}]
          \end{eqnarray*}
      \end{itemize}

  		\PN \underline{Caso Inductivo:} \begin{tabular}{|c|} \hline Teo$_{k} \Rightarrow$ Teo$_{k + 1}$ \\\hline
      \end{tabular} Sea $\varphi \in F_{k+1}^{\tau}$ y sean $\vec{a}, \vec{b}$ asignaciones tales que si $x_{i} \in
      Li(\varphi)$ entonces $a_{i} = b_{i}$ entonces si $\varphi \in F_{k}^{\tau}$, aplicando HI y utilizando el hecho
      de que $F_{k}^{\tau} \subseteq F_{k+1}^{\tau}$, obtenemos que Teo$_{k+1}$ vale. Por el contrario, tenemos los
      siguientes casos:
      \begin{itemize}
        \item $\varphi = (\varphi_{1} \eta \varphi_{2})$, con $\eta \in \{\wedge, \vee, \rightarrow, \leftrightarrow\}$.
        Probaremos $(\varphi_{1} \wedge \varphi_{2})$ ya que los demás casos son análogos. Ya que $Li(\varphi_{1}),
        Li(\varphi_{2}) \subseteq Li(\varphi)$, Teo$_{k}$ nos dice que:
        \[
          \mathbf{A} \models \varphi_{1}[\vec{a}] \ \text{sii} \ \mathbf{A} \models \varphi_{1}[\vec{b}] \ \text{y} \
          \mathbf{A} \models \varphi_{2}[\vec{a}] \ \text{sii} \ \mathbf{A} \models \varphi_{2}[\vec{b}]
        \]
        \PN Se tiene entonces que
        \begin{eqnarray*}
          \mathbf{A} \models \varphi[\vec{a}] &\Leftrightarrow& \mathbf{A} \models \varphi_{1}[\vec{a}] \ \text{y} \
            \mathbf{A} \models \varphi_{2}[\vec{a}] \\
          &\Leftrightarrow& \mathbf{A} \models \varphi_{1}[\vec{b}] \ \text{y} \ \mathbf{A} \models \varphi_{2}[\vec{b}]
            \qquad (\text{Por Teo}_{k}) \\
          &\Leftrightarrow& \mathbf{A} \models \varphi \lbrack \vec{b}]
        \end{eqnarray*}

        \item $\varphi = \lnot \varphi_{1}$: Ya que $Li(\varphi_{1}) \subseteq Li(\varphi)$, Teo$_{k}$ nos dice que
        $\mathbf{A} \models \varphi_{1}[\vec{a}] \ \text{sii} \ \mathbf{A} \models \varphi_{1}[\vec{b}]$. Se tiene
        entonces que
        \begin{eqnarray*}
          \mathbf{A} \models \varphi[\vec{a}] &\Leftrightarrow& \mathbf{A} \models \lnot \varphi_{1}[\vec{a}] \\
          &\Leftrightarrow& \mathbf{A} \models \lnot \varphi_{1}[\vec{b}] \qquad (\text{Por Teo}_{k}) \\
          &\Leftrightarrow& \mathbf{A} \models \varphi[\vec{b}]
        \end{eqnarray*}

        \item $\varphi = Qx_{j}\varphi_{1}$, con $Q \in \{\forall, \exists\}$: Probaremos $\varphi = \forall x_{j}
        \varphi_{1}$ ya que el otro caso es análogo. Notar que $\downarrow_{j}^{a}(\vec{a})$ y $\downarrow_{j}^{a}
        (\vec{b})$ coinciden en toda $x_{i} \in Li(\varphi_{1}) \subseteq Li(\varphi_{1}) \cup \{x_{j}\}$, con lo cual
        por Teo$_{k}$ nos dice que $\mathbf{A} \models \varphi_{1}[\downarrow_{j}^{a}(\vec{a})]$ sii $\mathbf{A} \models
        \varphi_{1}[\downarrow_{j}^{a}(\vec{b})]$ para todo $a \in A$. Por lo tanto
        \begin{eqnarray*}
          \mathbf{A} \models \varphi[\vec{a}] &\Leftrightarrow& \mathbf{A} \models \varphi_{1}[\downarrow_{j}^{a}
            (\vec{a})] \ \ \text{para cada} \ a \in A \\
          &\Leftrightarrow& \mathbf{A} \models \varphi_{1}[\downarrow_{j}^{a}(\vec{b})] \ \ \text{para cada} \ a \in A
            \qquad (\text{Por Teo}_{k}) \\
          &\Leftrightarrow& \mathbf{A} \models \varphi[\vec{b}]
        \end{eqnarray*}
      \end{itemize}
  \end{proof}

  % Corollary 136. Sin prueba. Lemma 46.
  \begin{corollary} \label{corollary_46}
    \PN Si $\varphi$ es una sentencia, entonces $\mathbf{A} \models \varphi \lbrack \vec{a}] \Leftrightarrow \mathbf{A}
    \models \varphi \lbrack \vec{b}]$, cualesquiera sean las asignaciones $\vec{a}, \vec{b}$.
  \end{corollary}

  % TODO
  % Lemma 137. Con prueba. Lemma 47.
  \begin{lemma} \label{lemma_47}
    \PN \newline
    \begin{enumerate}[(a)]
      \item Si $Li(\varphi) \cup Li(\psi) \subseteq \{x_{i_{1}}, \dotsc, x_{i_{n}}\}$, entonces $\varphi \thicksim \psi$
      si y solo si la sentencia $\forall x_{i_{1}} \dotsc \forall x_{i_{n}}(\varphi \leftrightarrow \psi)$ es
      universalmente válida.
      \item Si $\varphi_{i} \thicksim \psi_{i}, i = 1, 2$, entonces $\lnot \varphi_{1} \thicksim \lnot \psi_{1},
      (\varphi_{1} \eta \varphi_{2}) \thicksim (\psi_{1} \eta \psi_{2}) \ \text{y} \ Qv\varphi_{1} \thicksim Qv \psi_{1}$.
      \item Si $\varphi \thicksim \psi \ \text{y} \ \alpha^{\prime}$ es el resultado de reemplazar en una fórmula $\alpha$
      algunas (posiblemente $0$) ocurrencias de $\varphi$ por $\psi$, entonces $\alpha \thicksim \alpha^{\prime}$.
    \end{enumerate}
  \end{lemma}
  \begin{proof}
    \begin{enumerate}[(a)]
      \item Tenemos que
        \[
          \begin{array}{l}
            \varphi \thicksim \psi \\
            \ \ \Updownarrow \text{ (por (6) de la def de}\models \text{)} \\
            \mathbf{A} \models (\varphi \leftrightarrow \psi )[\vec{a}]\text{, para todo } \mathbf{A}\text{ y toda }\vec{a}\in A^{\mathbb{N}} \\
            \ \ \Updownarrow \\
            \mathbf{A} \models (\varphi \leftrightarrow \psi )[\downarrow _{i_{n}}^{a}(\vec{a })]\text{, para todo }\mathbf{A}\text{, }a\in A\text{ y toda }\vec{a}\in A^{ \mathbb{N}} \\ \ \ \Updownarrow (\text{por (8) de la def de}\models ) \\ \mathbf{A} \models \forall x_{i_{n}}(\varphi \leftrightarrow \psi )[\vec{a}] \text{, para todo }\mathbf{A}\text{ y toda }\vec{a}\in A^{\mathbb{N}} \\ \ \ \Updownarrow \\ \mathbf{A} \models \forall x_{i_{n}}(\varphi \leftrightarrow \psi )[\downarrow _{i_{n-1}}^{a}(\vec{a})]\text{, para todo }\mathbf{A}\text{, }a\in A\text{ y toda }\vec{a}\in A^{\mathbb{N}} \\ \ \ \Updownarrow \text{ (por (8) de la def de}\models \text{)} \\ \mathbf{A} \models \forall x_{i_{n-1}}\forall x_{i_{n}}(\varphi \leftrightarrow \psi )[\vec{a}]\text{, para todo }\mathbf{A}\text{ y toda }\vec{a}\in A^{ \mathbb{N}} \\ \ \ \Updownarrow \\ \ \ \ \ \vdots \\ \ \ \Updownarrow \\ \mathbf{A} \models \forall x_{i_{1}}...\forall x_{i_{n}}(\varphi \leftrightarrow \psi )[\vec{a}]\text{, para todo }\mathbf{A}\text{ y toda }\vec{a}\in A^{ \mathbb{N}} \\ \ \ \Updownarrow \\ \forall x_{i_{1}}...\forall x_{i_{n}}(\varphi \leftrightarrow \psi )\text{ es universalmente valida}
          \end{array}
        \]
      \item Es dejado al lector.
      \item Por induccion en el $k$ tal que $\alpha \in F_{k}^{\tau }$.
    \end{enumerate}
  \end{proof}

  % TODO: detalle
  % Lemma 138. Con prueba. Lemma 48.
  \begin{lemma} \label{lemma_48}
    \PN Sea $F: \mathbf{A} \rightarrow \mathbf{B}$ un homomorfismo, entonces:
    \[
      F(t^{\mathbf{A}}[(a_{1}, a_{2}, \dotsc)] = t^{\mathbf{B}}[F(a_{1}), F(a_{2}), \dotsc)]
    \]
    \PN para cada $t \in \TAU, (a_{1}, a_{2}, \dotsc) \in A^{\mathbb{N}}$.
  \end{lemma}
  \begin{proof}
    \PN Sea
    \begin{center}
      Teo$_{k}$: El lema vale para $t \in T_{k}^{\tau}$
    \end{center}
    \PN Probaremos este lema por inducción en $k$. Denotemos $(F(a_{1}), F(a_{2}), \dotsc)$ con $F(\vec{a})$.

    \vspace{3mm}
    \PN \underline{Caso Base:} \begin{tabular}{|c|} \hline Teo$_{0}$ \\\hline \end{tabular} Sea $t \in T_{0}^{\tau}$ y
    sea $F: \mathbf{A} \rightarrow \mathbf{B}$ un homomorfismo, entonces
    \[
      t \in Var \cup \mathcal{C}
    \]
    \PN es decir, sucede una de las siguientes:
    \begin{itemize}
      \item $t = x_{i}$, con $x_{i} \in Var$:
      \begin{eqnarray*}
        F(t^{\mathbf{A}}[\vec{a}]) &=& F(a_{i}) \\
        &=& t^{\mathbf{B}}[F(\vec{a})]
      \end{eqnarray*}
      \item $t = c$, con $c \in \mathcal{C}$:
      \begin{eqnarray*}
        F(t^{\mathbf{A}}[\vec{a}]) &=& F(c^{\mathbf{A}}) \\
        &=& c^{\mathbf{B}} \\
        &=& t^{\mathbf{B}}[F(\vec{a})]
      \end{eqnarray*}
    \end{itemize}

		\PN \underline{Caso Inductivo:} \begin{tabular}{|c|} \hline Teo$_{k} \Rightarrow$ Teo$_{k + 1}$ \\\hline
    \end{tabular} Supongamos que vale Teo$_{k}$ y supongamos $F: \mathbf{A} \rightarrow \mathbf{B}$ es un homomorfismo,
    $\vec{a} = (a_{1}, a_{2}, \dotsc) \in A^{\mathbb{N}}$, entonces:
    \[
      t \in T_{k}^{\tau} \cup \{f(t_{1}, \dotsc, t_{n}): f \in \mathcal{F}_{n},n\geq 1,t_{1}, \dotsc, t_{n} \in
      T_{k}^{\tau}\}
    \]
    \PN es decir, sucede una de las siguientes:
    \begin{itemize}
      \item $t \in T_{k}^{\tau}$: Aplicando HI y utilizando el hecho de que $T_{k}^{\tau} \subseteq T_{k+1}^{\tau}$,
      obtenemos que Teo$_{k+1}$ vale.
      \item $t = f(t_{1}, \dotsc, t_{n})$, con $f \in \mathcal{F}_{n} \ n \geq 1 \ \text{y} \ t_{1}, \dotsc, t_{n} \in
      T_{k}^{\tau}$, tenemos entonces
      \begin{eqnarray*}
        F(t^{\mathbf{A}}[\vec{a}]) &=& F(f(t_{1}, \dotsc, t_{n})^{\mathbf{A}}[\vec{a}]) \\
        &=& F(f^{\mathbf{A}}(t_{1}^{\mathbf{A}}[\vec{a}], \dotsc, t_{n}^{\mathbf{A}}[ \vec{a}])) \\
        &=& f^{\mathbf{B}}(F(t_{1}^{\mathbf{A}}[\vec{a}]), \dotsc, F(t_{n}^{\mathbf{A}}[ \vec{a}])) \\
        &=& f^{\mathbf{B}}(t_{1}^{\mathbf{B}}[F(\vec{a})], \dotsc, t_{n}^{\mathbf{B}}[F( \vec{a})])) \\
        &=& f(t_{1}, \dotsc, t_{n})^{\mathbf{B}}[F(\vec{a})] \\
        &=& t^{\mathbf{B}}[F(\vec{a})]
      \end{eqnarray*}
    \end{itemize}
  \end{proof}

  % Lemma 139. Con prueba. Lemma 49.
  \begin{lemma} \label{lemma_49}
    \PN Supongamos que $F: \mathbf{A} \rightarrow \mathbf{B}$ es un isomorfismo. Sea $\varphi \in F^{\tau}$, entonces:
    \[
      \mathbf{A} \models \varphi \lbrack (a_{1}, a_{2}, \dotsc)] \Leftrightarrow \mathbf{B} \models \varphi \lbrack
      (F(a_{1}), F(a_{2}), \dotsc)]
    \]
    \PN para cada $(a_{1}, a_{2}, \dotsc) \in A^{\mathbb{N}}$. En particular $\mathbf{A} \ \text{y} \ \mathbf{B}$ satisfacen las
    mismas sentencias de tipo $\tau$.
  \end{lemma}
  \begin{proof}
    %TODO
  \end{proof}

  % Lemma 140. Con prueba. Lemma 50.
  \begin{lemma} \label{lemma_50}
    \PN Supongamos que $\tau$ es algebraico, si $F: \mathbf{A} \rightarrow \mathbf{B}$ es un homomorfismo biyectivo,
    entonces $F$ es un isomorfismo.
  \end{lemma}
  \begin{proof}
    \PN Debemos probar que $F^{-1}$ es un homomorfismo, es decir, debemos ver
    \begin{itemize}
      \item $F^{-1}(c^{\mathbf{B}}) = c^{\mathbf{A}}$, para todo $c \in \mathcal{C}$: Ya que $F(c^{\mathbf{A}}) =
        c^{\mathbf{B}}$, tenemos que $F^{-1}(c^{\mathbf{B}}) = c^{\mathbf{A}}$
      \item $F^{-1}(f^{\mathbf{B}}(b_{1}, \dotsc, b_{n})) = f^{\mathbf{A}}(F^{-1}(b_{1}), \dotsc, F^{-1}(b_{n}))$ para
        cada $f \in \mathcal{F}_{n}, b_{1}, \dotsc, b_{n} \in B$: Sean $a_{1}, \dotsc, a_{n} \in A$ tales que
        $F(a_{i}) = b_{i}, i = 1, \dotsc, n$. Tenemos que
        \begin{eqnarray*}
          F^{-1}(f^{\mathbf{B}}(b_{1}, \dotsc, b_{n})) &=& F^{-1}(f^{\mathbf{B}}(F(a_{1}), \dotsc, F(a_{n}))) \\
          &=& F^{-1}(F(f^{\mathbf{A}}(a_{1}, \dotsc, a_{n}))) \\
          &=& f^{\mathbf{A}}(a_{1}, \dotsc, a_{n}) \\
          &=& f^{\mathbf{A}}(F^{-1}(b_{1}), \dotsc, F^{-1}(b_{n}))
        \end{eqnarray*}
    \end{itemize}
    \PN Luego, $F^{-1}$ es homomorfismo y por lo tanto $F$ es isomorfismo.
  \end{proof}

  % Lemma 141. Con prueba. Lemma 51.
  \begin{lemma} \label{lemma_51}
    \PN Supongamos que $\tau$ es algebraico, si $F: \mathbf{A} \rightarrow \mathbf{B}$ es un homomorfismo, entonces
    $I_{F}$ es un subuniverso de $\mathbf{B}$.
  \end{lemma}
  \begin{proof}
    \PN Para probar que $I_{F}$ es un subuniverso de $\mathbf{B}$, debemos ver:
    \begin{itemize}
      \item $I_{F} \neq \emptyset$: Ya que $A \neq \emptyset$, tenemos que $I_{F} \neq \emptyset$.
      \item $c^{\mathbf{B}} \in I_{F}$, para cada $c \in \mathcal{C}$: Es claro que $c^{\mathbf{B}} = F(c^{\mathbf{A}})
        \in I_{F}$ para cada $c \in \mathcal{C}$, pues F es homomorfismo.
      \item $f^{\mathbf{B}}(b_{1}, \dotsc, b_{n}) \in I_{F}$, para cada $b_{1}, \dotsc, b_{n} \in I_{F}$ y $f \in
        \mathcal{F}$: Sean $a_{1}, \dotsc, a_{n}$ tales que $F(a_{i}) = b_{i}, i = 1, \dotsc, n$. Tenemos que
        \[
          f^{\mathbf{B}}(b_{1}, \dotsc, b_{n}) = f^{\mathbf{B}}(F(a_{1}), \dotsc, F(a_{n})) = F(f^{\mathbf{A}}(a_{1},
          \dotsc, a_{n})) \in I_{F}
        \]
        \PN por lo cual $I_{F}$ es cerrada bajo $f^{\mathbf{B}}$.
    \end{itemize}
  \end{proof}

  % Lemma 142. Con prueba. Lemma 52.
  \begin{lemma} \label{lemma_52}
    \PN Supongamos que $\tau$ es algebraico, si $F: \mathbf{A} \rightarrow \mathbf{B}$ es un homomorfismo, entonces
    $\ker F$ es una congruencia sobre $\mathbf{A}$.
  \end{lemma}
  \begin{proof}
    \PN Sea $f \in \mathcal{F}_{n}$. Supongamos que $a_{1}, \dotsc, a_{n}, b_{1}, \dotsc, b_{n} \in A$ son tales que
    $a_{1} \ker F \ b_{1}, \dotsc, \linebreak a_{n} \ker F \ b_{n}$. Tenemos entonces que
    \begin{eqnarray*}
      F(f^{\mathbf{A}}(a_{1}, \dotsc, a_{n})) &=& f^{\mathbf{B}}(F(a_{1}), \dotsc, F(a_{n})) \\
      &=& f^{\mathbf{B}}(F(b_{1}), \dotsc, F(b_{n})) \\
      &=& F(f^{\mathbf{B}}(b_{1}, \dotsc, b_{n}))
    \end{eqnarray*}

    \PN lo cual nos dice que $f^{\mathbf{A}}(a_{1}, \dotsc, a_{n}) \ker F \ f^{\mathbf{B}}(b_{1}, \dotsc, b_{n})$.
  \end{proof}

  % Lemma 143. Con prueba. Lemma 53.
  \begin{lemma} \label{lemma_53}
    \PN $\pi_{\theta}: \mathbf{A} \rightarrow \mathbf{A}/\theta$ es un homomorfismo cuyo núcleo es $\theta$.
  \end{lemma}
  \begin{proof}
    \PN Debemos ver que $\pi_{\theta}$ satisface
    \begin{itemize}
      \item $\pi_{\theta}(c^{\mathbf{A}}) = c^{\mathbf{A}/\theta}$, para cada $c \in \mathcal{C}$: Tenemos que
        \[
          \pi_{\theta}(c^{\mathbf{A}}) = c^{\mathbf{A}}/\theta = c^{\mathbf{A}/\theta}
        \]
      \item $\pi_{\theta}(f^{\mathbf{A}}(a_{1}, \dotsc, a_{n})) = f^{\mathbf{A}/\theta}(\pi_{\theta}(a_{1}), \dotsc,
        \pi_{\theta}(a_{n}))$, para cada $f \in \mathcal{F}_{n}$ y $a_{1}, \dotsc, a_{n} \in A$: \linebreak Tenemos que
        \begin{eqnarray*}
          \pi_{\theta}(f^{\mathbf{A}}(a_{1}, \dotsc, a_{n})) &=& f^{\mathbf{A}}(a_{1}, \dotsc, a_{n})/\theta \\
          &=& f^{\mathbf{A}/\theta}(a_{1}/\theta, \dotsc, a_{n}/\theta) \\
          &=& f^{\mathbf{A}/\theta}(\pi_{\theta}(a_{1}), \dotsc, \pi_{\theta}(a_{n}))
        \end{eqnarray*}

      \item $(a_{1}, \dotsc, a_{n}) \in r^{\mathbf{A}}$ implica $(\pi_{\theta}(a_{1}), \dotsc, \pi_{\theta}(a_{n})) \in
        r^{\mathbf{A}/\theta}$, para todo $r \in \mathcal{R}_{n}, a_{1}, \dotsc, a_{n} \in A$: Lo cual vale, dado que
        $\pi_{\theta}(a_{1}) = a_{1}/\theta, \dotsc, \pi_{\theta}(a_{n}) = a_{n}/\theta$.
    \end{itemize}
    \PN por lo tanto, $\pi_{\theta}$ es un homomorfismo.
  \end{proof}

  % Corollary 144. Con prueba. Lemma 54.
  \begin{corollary} \label{corollary_54}
    \PN Para cada $t \in \TAU, \vec{a} \in A^{\mathbb{N}}$, se tiene que $t^{\mathbf{A}/\theta}[(a_{1}/\theta,
    a_{2}/\theta, \dotsc)] = t^{\mathbf{A}}[(a_{1}, a_{2}, \dotsc)]/\theta$.
  \end{corollary}
  \begin{proof}
    \PN Ya que $\pi_{\theta}$ es un homomorfismo, utilizando el \textbf{Lemma~\ref{lemma_48}} tenemos que
    \[
      \pi_{\theta}(t^{\mathbf{A}}[(a_{1}, a_{2}, \dotsc)] = t^{\mathbf{A}/\theta}[\pi_{\theta}(a_{1}),
        \pi_{\theta}(a_{2}), \dotsc)] \\
    \]
    \PN lo cual, por definición de $\pi_{\theta}$ es igual a
    \[
      t^{\mathbf{A}}[(a_{1}, a_{2}, \dotsc)]/\theta = t^{\mathbf{A}/\theta}[(a_{1}/\theta, a_{2}/\theta, \dotsc)]
    \]
  \end{proof}

  % TODO: detalle
  % Theorem 145. Con prueba. Lemma 55.
  \begin{theorem} \label{theorem_55}
    \PN Sea $F: \mathbf{A} \rightarrow \mathbf{B}$ un homomorfismo sobreyectivo. Definimos sin ambiguedad la siguiente
    función:
    \begin{eqnarray*}
      \bar{F}: A/\ker F &\rightarrow& B \\
      a/\ker F &\rightarrow& F(a)
    \end{eqnarray*}
    \PN la cual es un isomorfismo de $\mathbf{A}/\ker F$ en $\mathbf{B}$.
  \end{theorem}
  \begin{proof}
    \PN Notese que la definición de $\bar{F}$ es inambigua ya que si $a/\ker F = a^{\prime}/\ker F$, entonces $F(a) =
    F(a^{\prime})$. Veamos que $\bar{F}$ es biyectiva, es decir:
    \begin{itemize}
      \item $\bar{F}$ es sobreyectiva: Ya que $F$ es sobre, tenemos que $\bar{F}$ lo es.
      \item $\bar{F}$ es inyectiva: Supongamos que $\bar{F}(a/\ker F) = \bar{F}(a^{\prime}/\ker F)$, tenemos entonces
        que $F(a) = F(a^{\prime})$, lo cual nos dice que $a/\ker F = a^{\prime}/\ker F$, es decir, $\bar{F}$ es
        inyectiva.
    \end{itemize}
    \PN Luego, $\bar{F}$ es biyectiva, por lo que el \textbf{Lemma~\ref{lemma_50}} no dice que para ver que $\bar{F}$ es
    un isomorfismo, basta con ver que $\bar{F}$ es un homomorfismo. Veamos esto.
    \begin{itemize}
      \item $\bar{F}(c^{\mathbf{A}/\ker F}) = c^{\mathbf{B}}$, para cada $c \in \mathcal{C}$: Tenemos que
        \[
          \bar{F}(c^{\mathbf{A}/\ker F}) = \bar{F}(c^{\mathbf{A}}/\ker F) = F(c^{\mathbf{A} }) = c^{\mathbf{B}}
        \]
      \item $\bar{F}(f^{\mathbf{A}/\ker F}(a_{1}/\ker F, \dotsc, a_{n}/\ker F)) = f^{\mathbf{B}}(\bar{F}(a_{1}/\ker F), \dotsc,
        \bar{F}(a_{n}/\ker F))$, para cada $f \in \mathcal{F}_{n}$ y $a_{1}, \dotsc, a_{n} \in A$: Tenemos que
        \begin{eqnarray*}
          \bar{F}(f^{\mathbf{A}/\ker F}(a_{1}/\ker F, \dotsc, a_{n}/\ker F)) &=& \bar{F}(f^{\mathbf{A}}(a_{1}, \dotsc,
          a_{n})/\ker F) \\
          &=& F(f^{\mathbf{A}}(a_{1}, \dotsc, a_{n})) \\
          &=& f^{\mathbf{B}}(F(a_{1}), \dotsc, F(a_{n})) \\
          &=& f^{\mathbf{B}}(\bar{F}(a_{1}/\ker F), \dotsc, \bar{F}(a_{n}/\ker F))
        \end{eqnarray*}

      \item $(a_{1}/\ker F, \dotsc, a_{n}/\ker F) \in r^{\mathbf{A}/\ker F}$ implica $(\bar{F}(a_{1}/\ker F), \dotsc,
        \bar{F}(a_{n}/\ker F)) \in r^{\mathbf{A}/\ker F}$, para todo $r \in \mathcal{R}_{n}, a_{1}, \dotsc, a_{n} \in A$:
    \end{itemize}
  \end{proof}

  % Lemma 146. Nada. Lemma 56.
  \begin{lemma}
    \PN Este lema no se evalua.
  \end{lemma}

  % Lemma 147. Nada. Lemma 57.
  \begin{lemma}
    \PN Este lema no se evalua.
  \end{lemma}

  % TODO: de aca en adelante...
  % Lemma 148. Con prueba. Lemma 58.
  \begin{lemma} \label{lemma_58}
    \PN Sea $\tau$ un tipo cualquiera y supongamos $t \in \TAU$. Si $t =_{d} t(v_{1}, \dotsc, v_{n})$ entonces se da
    alguna de las siguientes:
    \begin{enumerate}
      \item $t = c$ para algún $c \in \mathcal{C}$.
      \item $t = v_{j}$ para algún j.
      \item $t = f(t_{1}, \dotsc, t_{m})$, con $f \in \mathcal{F}_{m} \ \text{y} \ t_{1}, \dotsc, t_{m} \in T_{k-1}^{\tau}$ tales
      que las variables que ocurren en cada uno de ellos están en $\{v_{1}, \dotsc, v_{n}\}$.
    \end{enumerate}
  \end{lemma}
  \begin{proof}
  \end{proof}

  % Lemma 149. Con prueba. Lemma 59.
  \begin{lemma} \label{lemma_59}
    \PN Sea $\tau$ un tipo cualquiera y supongamos $t \in \TAU$. Si $t =_{d} t(v_{1}, \dotsc, v_{n})$. Sea $\mathbf{A}$
    un modelo de tipo $\tau$. Sean $a_{1}, \dotsc, a_{n} \in A$. Se tiene que:
    \begin{enumerate}
      \item Si $t = c$ entonces $t^{\mathbf{A}}[a_{1}, \dotsc, a_{n}]= c^{\mathbf{A}}$.
      \item Si $t = v_{j}$ entonces $t^{\mathbf{A}}[a_{1}, \dotsc, a_{n}]= a_{j}$.
      \item Si $t = f(t_{1}, \dotsc, t_{m})$, con $f \in \mathcal{F}_{m} \ \text{y} \ t_{1}, \dotsc, t_{m} \in \TAU$, entonces:
      \[
        t^{\mathbf{A}}[a_{1}, \dotsc, a_{n}]= f^{\mathbf{A}}(t_{1}^{\mathbf{A}}[a_{1}, \dotsc, a_{n}], \dotsc,
        t_{m}^{\mathbf{A}}[a_{1}, \dotsc, a_{n}])
      \]
    \end{enumerate}
  \end{lemma}
  \begin{proof}
    \begin{enumerate}[(1)]
      \item trivial
      \item trivial
      \item Sea $\vec{b}$ una asignación tal que a cada $v_{i}$le asigna el valor $a_{i}$. Por definición tenemos EquivElim
      \begin{eqnarray*}
        t^{\mathbf{A}}[a_{1}, \dotsc, a_{n}] &=& t^{\mathbf{A}}[\vec{b}] \\
        &=& f^{\mathbf{A}}(t_{1}^{\mathbf{A}}[\vec{b}], \dotsc, t_{m}^{\mathbf{A}}[\vec{b}]) \\
        &=& f^{\mathbf{A}}(t_{1}^{\mathbf{A}}[a_{1}, \dotsc, a_{n}], \dotsc, t_{m}^{\mathbf{A}}[a_{1}, \dotsc, a_{n}])
      \end{eqnarray*}
    \end{enumerate}
  \end{proof}

  % Lemma 150. Con prueba. Lemma 60.
  \begin{lemma} \label{lemma_60}
    \PN \textbf{(De reemplazo para términos)}. Supongamos $t =_{d} t(w_{1}, \dotsc, w_{k}), s_{1} =_{d} s_{1}(v_{1},
    \dotsc, v_{n}), \dotsc, s_{k} =_{d} s_{k}(v_{1}, \dotsc, v_{n})$. Todas las variables de $t(s_{1}, \dotsc, s_{k})$
    están en $\{v_{1}, \dotsc, v_{n}\}$ y si declaramos $t(s_{1}, \dotsc, s_{k}) =_{d} t(s_{1}, \dotsc, s_{k})(v_{1},
    \dotsc, v_{n})$, entonces para cada estructura $\mathbf{A} \ \text{y} \ a_{1}, \dotsc a_{n} \in A$, se tiene:
    \[
      t(s_{1}, \dotsc, s_{k})^{\mathbf{A}}[a_{1}, \dotsc, a_{n}] = t^{\mathbf{A}}[s_{1}^{\mathbf{A}}[a_{1}, \dotsc,
      a_{n}], \dotsc, s_{k}^{\mathbf{A}}[a_{1}, \dotsc, a_{n}]]
    \]
  \end{lemma}
  \begin{proof}
    Probaremos que valen (a) y (b), por induccion en el $l$ tal que $t\in T_{l}^{\tau }.$ El caso $l=0$ es dejado al lector. Supongamos entonces que valen (a) y (b) siempre que $t\in T_{l}^{\tau }$ y veamos que entonces valen (a) y (b) cuando $t\in T_{l+1}^{\tau }-T_{l}^{\tau }$. Hay $f\in \mathcal{F} _{m} \ \text{y} \ t_{1}, \dotsc, t_{m}\in T_{l}^{\tau }$ tales que $ t_{1}=_{d}t_{1}(w_{1}, \dotsc, w_{k}), \dotsc, t_{m}=_{d}t_{m}(w_{1}, \dotsc, w_{k}) \ \text{y} \  t=f(t_{1}, \dotsc, t_{m})$. Notese que por (a) de la HI tenemos que

    $\displaystyle t_{i}(s_{1}, \dotsc, s_{k})=_{d}t_{i}(s_{1}, \dotsc, s_{k})(v_{1}, \dotsc, v_{n})\text{, } i=1, \dotsc, m $

    lo cual ya que
    $\displaystyle t(s_{1}, \dotsc, s_{k})=f(t_{1}(s_{1}, \dotsc, s_{k}), \dotsc, t_{m}(s_{1}, \dotsc, s_{k})) $

    nos dice que
    $\displaystyle t(s_{1}, \dotsc, s_{k})=_{d}t(s_{1}, \dotsc, s_{k})(v_{1}, \dotsc, v_{n}) $

    obteniendo asi (a). Para probar (b) notemos que por (b) de la hipotesis inductiva
    $\displaystyle t_{j}(s_{1}, \dotsc, s_{k})^{\mathbf{A}}[\vec{a}]=t_{j}^{\mathbf{A}}[s_{1}^{ \mathbf{A}}[\vec{a}], \dotsc, s_{k}^{\mathbf{A}}[\vec{a}]],j=1, \dotsc, m $

    lo cual nos dice que
    $\displaystyle \begin{array}{ccl} t(s_{1}, \dotsc, s_{k})^{\mathbf{A}}[\vec{a}] & = & f(t_{1}(s_{1}, \dotsc, s_{k}), \dotsc, t_{m}(s_{1}, \dotsc, s_{k}))^{\mathbf{A}}[\vec{a}] \\ & = & f^{\mathbf{A}}(t_{1}(s_{1}, \dotsc, s_{k})^{\mathbf{A}}[\vec{a} ], \dotsc, t_{m}(s_{1}, \dotsc, s_{k})^{\mathbf{A}}[\vec{a}]) \\ & = & f^{\mathbf{A}}(t_{1}^{\mathbf{A}}[s_{1}^{\mathbf{A}}[\vec{a} ], \dotsc, s_{k}^{\mathbf{A}}[\vec{a}]], \dotsc, t_{m}^{\mathbf{A}}[s_{1}^{\mathbf{A}}[ \vec{a}], \dotsc, s_{k}^{\mathbf{A}}[\vec{a}]]) \\ & = & t^{\mathbf{A}}[s_{1}^{\mathbf{A}}[\vec{a}], \dotsc, s_{k}^{\mathbf{A}}[\vec{ a}]] \end{array} $
  \end{proof}

  % Lemma 151. Con prueba. Lemma 61.
  \begin{lemma} \label{lemma_61}
    \PN Sea $\tau$ un tipo cualquiera y supongamos $\varphi \in F^{\tau}$. Si $\varphi =_{d} \varphi(v_{1}, \dotsc,
    v_{n})$, entonces se da una y solo una de las siguientes:
    \begin{enumerate}[(1)]
      \item $\varphi = (t \equiv s)$, con $t, s \in \TAU$, únicos y tales que las variables que ocurren en $t$ o en $s$
      están todas en $ \{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = r(t_{1}, \dotsc, t_{m})$, con $r \in \mathcal{R}_{m} \ \text{y} \ t_{1}, \dotsc, t_{m} \in \TAU$, únicos y
      tales que las variables que ocurren en cada $t_{i}$ están todas en $\{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = (\varphi_{1} \wedge \varphi_{2})$, con $\varphi_{1}, \varphi_{2} \in F^{\tau}$, únicas y tales
      que $Li(\varphi_{1}) \cup Li(\varphi_{2}) \subseteq \{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = (\varphi_{1} \vee \varphi_{2})$, con $\varphi_{1}, \varphi_{2} \in F^{\tau}$, únicas y tales que
      $Li(\varphi_{1}) \cup Li(\varphi_{2}) \subseteq \{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = (\varphi_{1} \rightarrow \varphi_{2})$, con $\varphi_{1}, \varphi_{2} \in F^{\tau}$, únicas y
      tales que $Li(\varphi_{1}) \cup Li(\varphi_{2}) \subseteq \{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = (\varphi_{1} \leftrightarrow \varphi_{2})$, con $ \varphi_{1}, \varphi_{2} \in F^{\tau}$, únicas
      y tales que $Li(\varphi_{1}) \cup Li(\varphi_{2}) \subseteq \{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = \lnot \varphi_{1}$, con $\varphi_{1} \in F^{\tau}$, única y tal que $Li(\varphi_{1}) \subseteq
      \{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = \forall v_{j} \varphi_{1}$, con $v_{j} \in \{v_{1}, \dotsc, v_{n}\} \ \text{y} \ \varphi_{1} \in
      F^{\tau}$, únicas y tales que $ Li(\varphi_{1}) \subseteq \{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = \forall v \varphi_{1}$, con $v \in Var-\{v_{1}, \dotsc, v_{n}\} \ \text{y} \ \varphi_{1}\ in F^{\tau}$,
      únicas y tales que $ Li(\varphi_{1}) \subseteq \{v_{1}, \dotsc, v_{n}, v\}$.
      \item $\varphi = \exists v_{j} \varphi_{1}$, con $v_{j} \in \{v_{1}, \dotsc, v_{n}\} \ \text{y} \ \varphi_{1} \in
      F^{\tau}$, únicas y tales que $ Li(\varphi_{1}) \subseteq \{v_{1}, \dotsc, v_{n}\}$.
      \item $\varphi = \exists v \varphi_{1}$, con $v \in Var-\{v_{1}, \dotsc, v_{n}\} \ \text{y} \ \varphi_{1} \in F^{\tau}$,
      únicas y tales que $ Li(\varphi_{1}) \subseteq \{v_{1}, \dotsc, v_{n}, v\}$.
    \end{enumerate}
  \end{lemma}
  \begin{proof}
    Induccion en el k tal que $\varphi \in F_{k}^{\tau}$
  \end{proof}

  % Lemma 152. Con prueba. Lemma 62.
  \begin{lemma} \label{lemma_62}
    \PN Supongamos $\varphi =_{d} \varphi(v_{1}, \dotsc, v_{n})$. Sea $\mathbf{A} = (A, i)$ un modelo de tipo $\tau$ y
    sean $a_{1}, \dotsc, a_{n} \in A$, entonces:
    \begin{enumerate}
      \item Si $\varphi = (t \equiv s)$, entonces:
      \begin{center}
        $\mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ t^{\mathbf{A}}[a_{1}, \dotsc,
        a_{n}]=s^{\mathbf{A}}[a_{1}, \dotsc, a_{n}]$
      \end{center}
      \item Si $\varphi = r(t_{1}, \dotsc, t_{m})$, entonces:
      \begin{equation*}
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ (t_{1}^{A}[a_{1}, \dotsc,
        a_{n}], \dotsc, t_{m}^{A}[a_{1}, \dotsc, a_{n}])\in r^{A}
      \end{equation*}
      \item Si $\varphi = (\varphi_{1} \wedge \varphi_{2})$ entonces:
      \[
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ \mathbf{A} \models \varphi_{1}
        [a_{1}, \dotsc, a_{n}] \ \text{y} \ \mathbf{A} \models \varphi_{2}[a_{1}, \dotsc, a_{n}]
      \]
      \item Si $\varphi = (\varphi_{1} \vee \varphi_{2})$ entonces:
      \[
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ \mathbf{A} \models \varphi_{1}
        [a_{1}, \dotsc, a_{n}] \ \text{o} \ \mathbf{A} \models \varphi_{2}[a_{1}, \dotsc, a_{n}]
      \]
      \item Si $\varphi = (\varphi_{1} \rightarrow \varphi_{2})$ entonces:
      \[
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ \mathbf{A} \models \varphi_{2}
        [a_{1}, \dotsc, a_{n}] \ \text{o} \ \mathbf{A} \not\models \varphi_{1}[a_{1}, \dotsc, a_{n}]
      \]
      \item Si $\varphi = (\varphi_{1} \leftrightarrow \varphi_{2})$ entonces:
      \begin{eqnarray*}
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si ya sea} \ && \mathbf{A} \models
        \varphi_{1}[a_{1}, \dotsc, a_{n}] \ \text{y} \ \mathbf{A} \models \varphi_{2}[a_{1}, \dotsc, a_{n}] \ \text{o}
        \\
        && \mathbf{A} \not\models \varphi_{1}[a_{1}, \dotsc, a_{n}] \ \text{y} \ \mathbf{A} \not\models \varphi_{2}
        [a_{1}, \dotsc, a_{n}]
      \end{eqnarray*}
      \item Si $\varphi = \lnot \varphi_{1}$ entonces:
      \[
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ \mathbf{A} \not\models
        \varphi_{1}[a_{1}, \dotsc, a_{n}]
      \]
      \item Si $\varphi = \forall v\varphi_{1}$ con $v\not\in \{v_{1}, \dotsc, v_{n}\} \ \text{y} \ \varphi_{1} =_{d}
      \varphi_{1}(v_{1}, \dotsc, v_{n}, v)$ entonces:
      \[
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ \mathbf{A} \models \varphi_{1}
        [a_{1}, \dotsc, a_{n},a] \ \text{para todo} \ a \in A
      \]
      \item Si $\varphi = \forall v_{j}\varphi_{1}$ entonces:
      \[
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ \mathbf{A} \models \varphi_{1}
        [a_{1}, \dotsc, a, \dotsc, a_{n}] \ \text{para todo} \ a \in A
      \]
      \item) Si $\varphi = \exists v\varphi_{1}$ con $v\not\in \{v_{1}, \dotsc, v_{n}\} \ \text{y} \ \varphi_{1} =_{d}
      \varphi_{1}(v_{1}, \dotsc, v_{n}, v)$ entonces:
      \[
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ \mathbf{A} \models \varphi_{1}
        [a_{1}, \dotsc, a_{n}, a] \ \text{para algún} \ a \in A
      \]
      \item) Si $\varphi = \exists v_{j}\varphi_{1}$ entonces:
      \[
        \mathbf{A} \models \varphi \lbrack a_{1}, \dotsc, a_{n}] \ \text{si y solo si} \ \mathbf{A} \models \varphi_{1}
        [a_{1}, \dotsc, a, \dotsc, a_{n}] \ \text{para algún} \ a \in A
      \]
    \end{enumerate}
  \end{lemma}
  \begin{proof}
  \end{proof}

  % Lemma 153. Sin prueba. Lemma 63.
  \begin{lemma} \label{lemma_63}
    \PN Si $Qv$ ocurre en $\varphi$ a partir de $i$, entonces hay una única fórmula $\psi$ tal que $Qv\psi$ ocurre en
    $\varphi$ a partir de $i$.
  \end{lemma}

  % Lemma 154. Sin prueba. Lemma 64.
  \begin{lemma} \label{lemma_64}
    \PN Supongamos $\varphi =_{d} \varphi(w_{1}, \dotsc, w_{k}), t_{1} =_{d} t_{1}(v_{1}, \dotsc, v_{n}), \dotsc, t_{k}
    =_{d} t_{k}(v_{1}, \dotsc, v_{n})$ y supongamos además que cada $w_{j}$ es sustituible por $t_{j}$ en $\varphi$,
    entonces:
    \begin{enumerate}[(a)]
      \item $Li(\varphi(t_{1}, \dotsc, t_{k})) \subseteq \{v_{1}, \dotsc, v_{n}\}$
      \item Si declaramos $\varphi(t_{1}, \dotsc, t_{k}) =_{d} \varphi(t_{1}, \dotsc, t_{k})(v_{1}, \dotsc, v_{n})$,
      entonces para cada estructura $\mathbf{A} \ \text{y} \ \vec{a} \in A^{n}$ se tiene:
        \[
          \mathbf{A} \models \varphi(t_{1}, \dotsc, t_{k})[\vec{a}] \ \text{si y solo si} \ \mathbf{A} \models \varphi
          \lbrack t_{1}^{\mathbf{A}}[\vec{a}], \dotsc, t_{k}^{ \mathbf{A}}[\vec{a}]]
        \]
    \end{enumerate}
  \end{lemma}