7.8 Modelo matemático de las fórmulas elementales

En esta sección daremos un modelo matemático de los conceptos de término elemental de tipo \(\tau\) y fórmula elemental de tipo \(\tau\). Esto corresponde al punto (1) del Programa de Lógica Matemática.

7.8.1 Variables

Las variables usadas en las fórmulas elementales no estaban del todo especificadas. Para hacer bien preciso este concepto definiremos un conjunto concreto de variables. Sea \(Var\) el siguiente conjunto de palabras del alfabeto \(\{\mathsf{X},\mathit{0},\mathit{1},...,\mathit{9},\mathbf{0},\mathbf{1},...,\mathbf{9}\}\): \[Var=\{\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2},...,\mathsf{X}\mathbf{9},\mathsf{X}\mathit{1}\mathbf{0},\mathsf{X}\mathit{1}\mathbf{1},...,\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathit{2}\mathbf{0},\mathsf{X}\mathit{2}\mathbf{1},...\}\] Es decir el elemento \(n\)-ésimo de \(Var\) es la palabra de la forma \(\mathsf{X}\alpha\) donde \(\alpha\) es el resultado de reemplazar en la palabra que denota \(n\) en notación decimal, el último numeral por su correspondiente numeral bold y los otros por sus correspondientes itálicos. Para dar un último ejemplo, el elemento trecientos cuarenta y unésimo de \(Var\) es la siguiente palabra de longitud cuatro: \[\mathsf{X}\mathit{3}\mathit{4}\mathbf{1}\] A los elementos de \(Var\) los llamaremos variables. La razón por la cual usamos numerales itálicos y bold es que a los numerales normales los usamos habitualmente en los tipos y será conveniente que entonces no ocurran en las variables. Además tomamos el último símbolo de cada variable en bold para que de esta manera nunca una variable sea una subpalabra de otra variable distinta a ella, lo cual contribuye a simplificar la escritura de los resultados.

Denotaremos con \(x_{i}\) al \(i\)-ésimo elemento de \(Var\), para cada \(i\in\mathbf{N}\).

7.8.2 Términos

Dado un tipo \(\tau\), definamos recursivamente los conjuntos de palabras \(T_{k}^{\tau}\), con \(k\geq0\), de la siguiente manera: \[\begin{aligned} T_{0}^{\tau} & =Var\cup\mathcal{C}\\ T_{k+1}^{\tau} & =T_{k}^{\tau}\cup\{f(t_{1},...,t_{n}):f\in\mathcal{F}_{n}\text{, }n\geq1\text{ y }t_{1},...,t_{n}\in T_{k}^{\tau}\}. \end{aligned}\] Nótese que arriba \(f(t_{1},...,t_{n})\) denota el resultado de concatenar las \(n+(n-1)+3\) siguientes palabras \[f\;\;\;(\;\;\;t_{1}\;\;\;,\;\;\;t_{2}\;\;\;,\;\;\;...\;\;\;,\;\;\;t_{n}\;\;\;)\] es decir que \(f(t_{1},...,t_{n})\) es una palabra de longitud \[\left|f\right|+\left|t_{1}\right|+...+\left|t_{n}\right|+(n-1)+2\] (\(n-1\) cuenta la cantidad de comas). Sea \[T^{\tau}=\bigcup_{k\geq0}T_{k}^{\tau}\] Los elementos de \(T^{\tau}\) serán llamados términos de tipo \(\tau\). Un término \(t\) es llamado cerrado si \(x_{i}\) no es subpalabra de \(t\), para cada \(i\in\mathbf{N}\). Definamos \[T_{c}^{\tau}=\{t\in T^{\tau}:t\text{ es cerrado}\}\] Es muy importante entender que un término de tipo \(\tau\) como objeto matemático es una palabra. También debería quedar claro que el concepto de término de tipo \(\tau\), a diferencia del concepto de término elemental de tipo \(\tau\), es un concepto definido en forma matemática precisa.

Algunos ejemplos:

1. adhocprefix(E1)adhocsufix Sea \(\tau=(\{\mathrm{uno},\mathrm{doli}\},\{\mathrm{MAS},\mathrm{P}\},\{\mathrm{Her}\},a)\), con \(a\) dado por \(a(\mathrm{MAS})=4\), \(a(\mathrm{P})=1\) y \(a(\mathrm{Her})=3\). Entonces

   1. adhocprefix-adhocsufix Las palabras \(\mathrm{uno}\), \(\mathrm{doli}\) y \(\mathsf{X}\mathit{15666}\mathbf{9}\) son términos de tipo \(\tau\) ya que pertenecen a \(T_{0}^{\tau}\)

   2. adhocprefix-adhocsufix \(\mathrm{MAS}(\mathrm{uno},\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5})\) y \(\mathrm{P}(\mathrm{uno})\) son términos de tipo \(\tau\) ya que pertenecen a \(T_{1}^{\tau}\) (por que?)

   3. adhocprefix-adhocsufix Las palabras \[\mathrm{P}(\mathrm{P}(\mathrm{uno}))\ \ \ \ \ \mathrm{MAS}(\mathrm{P}(\mathsf{X}\mathbf{4}),\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5})\] son términos de tipo \(\tau\) ya que pertenecen a \(T_{2}^{\tau}\)

   4. adhocprefix-adhocsufix \(\mathrm{P}(\mathrm{MAS}(\mathrm{P}(\mathsf{X}\mathbf{4}),\mathrm{MAS}(\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{3},\mathsf{X}\mathbf{4}),\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5}))\) es un término ya que pertenece a \(T_{3}^{\tau}\)

   5. adhocprefix-adhocsufix \(\mathrm{uno}\), \(\mathrm{doli}\), \(\mathrm{P}(\mathrm{uno})\) y \(\mathrm{MAS}(\mathrm{uno},\mathrm{doli},\mathrm{doli},\mathrm{doli})\) son términos cerrados de tipo \(\tau\)

2. adhocprefix(E2)adhocsufix Sea \(\tau=(\{0,1\},\{+,\times,\uparrow\},\emptyset,a)\), con \(a\) dado por \(a(+)=2\), \(a(\times)=3\) y \(a(\uparrow)=1\). Entonces \[\mathsf{X}\mathit{111}\mathbf{9}\ \ \ \ \ \ \ \ 0\ \ \ \ \ \ \ \ 1\ \ \ \ \ \ \ \ +(+(\mathrm{\uparrow}(\mathsf{X}\mathbf{4}),\times(\mathsf{X}\mathbf{2},1,0)),\times(1,\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{3}))\] son términos de tipo \(\tau\). También \(\mathrm{\uparrow}(+(\mathrm{\uparrow}(0),\times(0,1,0)))\) es un término cerrado de tipo \(\tau\)

3. adhocprefix(E3)adhocsufix Sea \(\tau=(\emptyset,\{\mathsf{s},\mathsf{i}\},\emptyset,\{(\mathsf{s},2),(\mathsf{i},2)\})\) el tipo de los reticulados terna. Entonces \[\mathsf{s}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{3})\ \ \ \ \ \ \ \ \ \mathsf{s}(\mathsf{s}(\mathsf{X}\mathbf{4},\mathsf{X}\mathit{1}\mathbf{4}),\mathsf{i}(\mathsf{X}\mathbf{2},\mathsf{X}\mathit{111}\mathbf{9}))\] son términos de tipo \(\tau\). No hay términos cerrados de tipo \(\tau\). Cabe destacar que \((\mathsf{X}\mathbf{2\ }\mathsf{s\ X}\mathbf{3})\) no es un término de tipo \(\tau\) aunque probar esto no es trivial de la definición de término y requiere de una demostración.

Observación importante: Notar que los términos de tipo \(\tau\) son un modelo matemático de los términos elementales puros de tipo \(\tau\), es decir aquellos en los cuales no ocurren nombres de elementos fijos. Medite...

El siguiente resultado es intuitivamente obvio por lo cual en general lo utilizaremos sin hacer mención explicita.

Proof. Es claro de la definicion de los \(T_{k}^{\tau}\) que \(T_{i}^{\tau}\subseteq T_{j}^{\tau}\) siempre que \(i\leq j\). Por definición de \(T^{\tau}\) tenemos que hay números \(k_{1},...,k_{n}\) tales que \(t_{i}\in T_{k_{i}}^{\tau}\), para \(i=1,...,n\). Es claro que entonces \(t_{1},...,t_{n}\in T_{K}^{\tau}\), donde \(K=\mathrm{max}\{k_{1},...,k_{n}\}\), lo cual nos dice que \(f(t_{1},...,t_{n})\in T_{K+1}^{\tau}\subseteq T^{\tau}\).  

El siguiente resultado es también intuitivamente claro y es útil para demostrar propiedades de los términos.

Proof. Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Si \(t\in T_{k+1}^{\tau}\), entonces se da alguna de las siguientes:

   1. adhocprefix(a)adhocsufix \(t\in Var\cup\mathcal{C}\)

   2. adhocprefix(b)adhocsufix \(t=f(t_{1},...,t_{n})\), con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T_{k}^{\tau}\).

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Es directo ya que por definición \(T_{0}^{\tau}=Var\cup\mathcal{C}\) y \[T_{1}^{\tau}=T_{0}^{\tau}\cup\{f(t_{1},...,t_{n}):f\in\mathcal{F}_{n}\text{, }n\geq1\text{ y }t_{1},...,t_{n}\in T_{0}^{\tau}\}\]

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Sea \(t\in T_{(k+1)+1}^{\tau}\). Por definición de \(T_{(k+1)+1}^{\tau}\) tenemos dos casos:

Caso \(t\in T_{k+1}^{\tau}\). Ya que \(\mathrm{Enu}_{k}\) es verdadero, tenemos que se da alguna de las siguientes

1. adhocprefix(a)adhocsufix \(t\in Var\cup\mathcal{C}\)

2. adhocprefix(b)adhocsufix \(t=f(t_{1},...,t_{n})\), con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T_{k}^{\tau}\).

Ya que \(T_{k}^{\tau}\subseteq T_{k+1}^{\tau}\) tenemos que se da alguna de la siguientes

1. adhocprefix(a)adhocsufix \(t\in Var\cup\mathcal{C}\)

2. adhocprefix(b)adhocsufix \(t=f(t_{1},...,t_{n})\), con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T_{k+1}^{\tau}\).

lo cual es justamente la conclusión de \(\mathrm{Enu}_{k+1}\).

Caso \(t=f(t_{1},...,t_{n})\) con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T_{k+1}^{\tau}\). Claramente en este caso se da la conclusión de \(\mathrm{Enu}_{k+1}\).  

Algunos ejemplos de propiedades de los términos las cuales se pueden probar fácilmente usando el lema anterior son

1. adhocprefix-adhocsufix Si \(t\in T^{\tau}\) es tal que en \(t\) ocurre el símbolo \()\), entonces \(t=f(t_{1},...,t_{n})\) con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T^{\tau}\).

2. adhocprefix-adhocsufix Ningún término comienza con un símbolo del alfabeto \(\{\mathit{0},\mathit{1},...,\mathit{9}\}\)

3. adhocprefix-adhocsufix Si \(t\in T^{\tau}\) comienza con \(\mathsf{X}\) entonces \(t\in Var\)

4. adhocprefix-adhocsufix Si \(t\in T^{\tau}\) y \(\left[t\right]_{i}=)\), con \(i<\left\vert t\right\vert\), entonces \(\left[t\right]_{i+1}=\) \(,\) o \(\left[t\right]_{i+1}=\) \()\)

5. adhocprefix-adhocsufix Si \(t\in T^{\tau}\), entonces \(\left\vert t\right\vert _{(}=\left\vert t\right\vert _{)}\).

Dejamos al lector probar estas propiedades, varias de las cuales se usarán en la prueba del Lema de Mordisqueo mas abajo.

Una posible forma de probar que una palabra dada no es un término es encontrar una propiedad que posean todos los términos la cual no cumpla dicha palabra. Por ejemplo si \(\tau=(\emptyset,\{glp\},\emptyset,a)\), con \(a(glp)=1\), la palabra \(\alpha=glp((\mathsf{X}\mathit{13}\mathbf{3})\) no es un término ya que \(\left\vert \alpha\right\vert _{(}\neq\left\vert \alpha\right\vert _{)}\).

7.8.2.1 Unicidad de la lectura de términos

Recordemos que \(\beta\) es un tramo inicial (propio) de \(\alpha\) si hay una palabra \(\gamma\) tal que \(\alpha=\beta\gamma\) (y \(\beta\notin\{\varepsilon,\alpha\}\)). En forma similar se define tramo final (propio).

Dada una palabra \(\alpha\) denotemos con \(SPar(\alpha)\) al número entero \(\left\vert \alpha\right\vert _{(}-\left\vert \alpha\right\vert _{)}\). Pensaremos que los paréntesis izquierdos de \(\alpha\) valen \(1\) y los derechos valen \(-1\). Con esta idea \(SPar(\alpha)\) es la “suma de paréntesis de \(\alpha\)”.

Proof. Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Sea \(t\in T_{k}^{\tau}\). Se tiene:

   1. adhocprefix(1)adhocsufix \(SPar(t)=0\).

   2. adhocprefix(2)adhocsufix Si \(z\) es tramo inicial de \(t\), entonces \(SPar(z)\geq0\)

   3. adhocprefix(3)adhocsufix Si \(z\) es tramo final de \(t\), entonces \(SPar(z)\leq0\)

   4. adhocprefix(4)adhocsufix Si \(z\) es tramo inicial propio de \(t\) y en \(z\) ocurre algún paréntesis, entonces \(SPar(z)>0\)

   5. adhocprefix(5)adhocsufix Si \(z\) es tramo final de \(t\), \(z\neq\varepsilon\) y \(SPar(z)=0\), entonces a la izquierda de \(z\) en \(t\) no ocurren paréntesis.

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Es directo.

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos \(t\in T_{k+1}^{\tau}\). Probaremos que \(t\) cumple (1), (2), (3), (4) y (5). Por definición de \(T_{k+1}^{\tau}\) hay dos casos.

Caso \(t\in T_{k}^{\tau}\). Entonces ya que vale \(\mathrm{Enu}_{k}\) tenemos que \(t\) cumple (1), (2), (3), (4) y (5).

Caso \(t=f(t_{1},...,t_{n})\), con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T_{k}^{\tau}\). Ya que vale \(\mathrm{Enu}_{k}\) tenemos que \(t_{1},...,t_{n}\) cumplen (1), (2), (3), (4) y (5). Es fácil notar entonces que \(t\) cumple (1). Veamos que \(t\) cumple (4). Sea \(z\) un tramo inicial propio de \(t\) y supongamos que en \(z\) ocurre algún paréntesis. Nótese que \(z\) es de la forma \(z=f(t_{1},...,t_{i},z_{1}\) con \(0\leq i\leq n-1\) y \(z_{1}\) un tramo inicial de \(t_{i+1}\) (en el caso \(i=0\) interpretamos \(t_{1},...,t_{i}=\varepsilon)\). Ademas nótese que: \[SPar(z)=1+\left(\sum_{j=1}^{i}SPar(t_{j})\right)+SPar(z_{1})\] Ya que \(t_{1},...,t_{i}\) cumplen (1) tenemos que \[\left(\sum_{j=1}^{i}SPar(t_{j})\right)=0\] Además ya que \(t_{i+1}\) cumple (2) y \(z_{1}\) es un tramo inicial de \(t_{i+1}\) tenemos que \[SPar(z_{1})\geq0\] O sea que \(SPar(z)>0\).

Veamos que \(t\) cumple (5). Supongamos que \(z\) es tramo final de \(t\), \(z\neq\varepsilon\) y \(SPar(z)=0\). Supongamos primero que \(\left|z\right|<\left|(t_{1},...,t_{n})\right|\). Ya que \(z\neq\varepsilon\) tenemos que \(z\) es de la forma \(z=z_{1},t_{i},...,t_{n})\) con \(1<i\leq n+1\) y \(z_{1}\) un tramo final de \(t_{i-1}\) (en el caso \(i=n+1\) interpretamos \(t_{i},...,t_{n}=\varepsilon)\). Además nótese que: \[SPar(z)=SPar(z_{1})+\left(\sum_{j=i}^{n}SPar(t_{j})\right)+1\] Ya que \(t_{i},...,t_{n}\) cumplen (1) tenemos que \[\left(\sum_{j=i}^{n}SPar(t_{j})\right)=0\] Además ya que \(t_{i-1}\) cumple (3) y \(z_{1}\) es un tramo final de \(t_{i-1}\) tenemos que \[SPar(z_{1})\leq0\] O sea que \(SPar(z)<0\), lo cual es absurdo. O sea que \(\left|z\right|\geq\left|(t_{1},...,t_{n})\right|\). Pero entonces es claro que a la izquierda de \(z\) en \(t\) no ocurren paréntesis.  

Mordisqueo. Nótese que en la definición de tipo se exige que nunca un nombre de cte sea subpalabra propia de otro nombre de cte, lo cual garantiza que nunca puede ser un nombre de cte un tramo inicial o final propio de otro nombre de cte. Lo que si puede suceder es que un tramo final propio de un nombre de cte \(c\) sea un tramo inicial propio de otro nombre de cte \(d\). Mas formalmente puede suceder que haya palabras \(x,y,z\), las tres distintas de \(\varepsilon\) tales que \(c=xy\) y \(d=yz\). En tal caso solemos decir que las palabras \(c\) y \(d\) se mordisquean. Por ejemplo si \(\tau=(\{\mathrm{uno}\),\(\mathrm{noli}\},\emptyset,\emptyset,\emptyset)\), es fácil ver que \(\tau\) es un tipo y que \(\mathrm{uno}\) y \(\mathrm{noli}\) se mordisquean. El lema siguiente nos dice que este es el único caso de mordisqueo de términos.

Proof. Hay varios casos. Recomendamos repasar la definición de tipo ya que haremos un uso fino de la misma, sin hacer mención explícita.

Caso \(s\in\mathcal{C}\). Ya que \(y\neq\varepsilon\) tenemos que \(t\) debe comenzar con un símbolo que ocurre en un nombre de cte. Esto nos dice que \(t\) no puede ser ni una variable ni de la forma \(f(t_{1},...,t_{n})\), es decir \(t\in\mathcal{C}\).

Caso \(s\in Var\). Si \(x\neq\varepsilon\) tenemos que \(t\) debe comenzar con alguno de los siguientes símbolos \[\mathit{0}\;\mathit{1\;}...\;\mathit{9}\;\mathbf{0}\;\mathbf{1}\ ...\;\mathbf{9}\] lo cual es absurdo (justificar). O sea que \(x=\varepsilon\) y por lo tanto \(s=y\). Ya que \(t=yz=sz\), tenemos que \(t\) debe comenzar con \(\mathsf{X}\). Pero esto dice que \(t\in Var\) (justificar). Ahora sigue fácilmente de la igualdad \(t=sz\) que \(z\) debe ser \(\varepsilon\).

Caso \(s\) es de la forma \(f(s_{1},...,s_{n})\). Ya que \(y\neq\varepsilon\), tenemos que \()\) ocurre en \(t\). O sea que \(t\) es de la forma \(g(t_{1},...,t_{m})\) (justificar). Supongamos que \(z\neq\varepsilon\). Nótese que \(y\) es un tramo inicial propio de \(g(t_{1},...,t_{m})\). Ya que en \(y\) ocurre el símbolo \()\) (4) del Lema \(SPar\) en Términos nos dice que \(SPar(y)>0\). Pero ya que \(y\) es tramo final de \(f(s_{1},...,s_{n})\), tenemos por (3) del mismo lema que \(SPar(y)\leq0.\) El absurdo así obtenido nos dice que \(z=\varepsilon\). Pero entonces \(s=xt\). Probaremos que \(x=\varepsilon\). Ya que \(s=xt\), se tiene que \[f(s_{1},...,s_{n})=xg(t_{1},...,t_{m})\] Por (1) del Lema \(SPar\) en Términos aplicado a cada \(t_{i}\) obtenemos que \(SPar((t_{1},...,t_{m}))=0\). Pero \((t_{1},...,t_{m})\) es un tramo final del termino \(f(s_{1},...,s_{n})\) lo cual por (5) del mismo lema nos dice que a la izquierda de \((t_{1},...,t_{m})\) en \(f(s_{1},...,s_{n})\) no ocurren paréntesis. Obviamente esto nos dice que \[\left|(s_{1},...,s_{n})\right|\leq\left|(t_{1},...,t_{m})\right|\] Y ya que en \(f\) no ocurre el símbolo \((\) deberá suceder que \[\left|(t_{1},...,t_{m})\right|=\left|(s_{1},...,s_{n})\right|\] O sea que \(f=xg\). Pero esto por la definición de tipo nos dice que \(x=\varepsilon\).  

Proof. Nótese que (1) y (2) son excluyentes, es decir no pueden darse ambas. O sea que en virtud del Lema Menú para Términos, para probar que se da (1) o (2), sólo falta probar la unicidad en el punto (2). Supongamos que \[t=f(t_{1},...,t_{n})=g(s_{1},...,s_{m})\] con \(n,m\geq1,\;f\in\mathcal{F}_{n}\), \(g\in\mathcal{F}_{m}\), \(t_{1},...,t_{n},s_{1},...,s_{m}\in T^{\tau}\). Nótese que \(f=g\). O sea que \(n=m=a(f)\). Nótese que \(t_{1}\) es tramo inicial de \(s_{1}\) o \(s_{1}\) es tramo inicial de \(t_{1}\), lo cual por el lema anterior nos dice que \(t_{1}=s_{1}\). Con el mismo razonamiento podemos probar que deberá suceder \(t_{2}=s_{2},...,t_{n}=s_{n}\). Esto garantiza la unicidad de (2).

Veamos la última observación. Supongamos \(t\in T_{k+1}^{\tau}\) y supongamos se da (2). El Lema Menú para Términos nos dice que \[t=g(s_{1},...,s_{m})\] con \(m\geq1\), \(g\in\mathcal{F}_{m}\) y \(s_{1},...,s_{m}\in T_{k}^{\tau}\). Pero la unicidad de (2) nos dice que \(n=m\), \(f=g\) y \(t_{1}=s_{1},...,t_{n}=s_{n}\) por lo cual \(t_{1},...,t_{n}\in T_{k}^{\tau}\).  

El teorema anterior es importante ya que nos permite definir recursivamente funciones con dominio contenido en \(T^{\tau}\). Por ejemplo podemos definir una función \(F:T^{\tau}\rightarrow T^{\tau}\), de la siguiente manera:

1. adhocprefix-adhocsufix \(F(c)=c\), para cada \(c\in\mathcal{C}\)

2. adhocprefix-adhocsufix \(F(v)=v\), para cada \(v\in Var\)

3. adhocprefix-adhocsufix \(F(f(t_{1},...,t_{n}))=f(F(t_{1}),...,F(t_{n}))\), si \(f\in\mathcal{F}_{n}\), con \(n\neq2\)

4. adhocprefix-adhocsufix \(F(f(t_{1},t_{2}))=f(t_{2},t_{1})\), si \(f\in\mathcal{F}_{2}.\)

Nótese que si la unicidad de la lectura no fuera cierta, entonces las ecuaciones anteriores no estarían definiendo en forma correcta una función ya que el valor de \(F\) en un término \(t\) estaría dependiendo de cual descomposición tomemos para \(t\).

7.8.2.2 Ocurrencia de términos en términos

Recomendamos al lector que antes de seguir repase los conceptos de ocurrencia y de reemplazo de ocurrencias en la Sección Ocurrencias, así entiende con madurez los enunciados que daremos.

Sean \(s,t\in T^{\tau}\). Diremos que \(s\) es subtérmino (propio) de \(t\) si (no es igual a \(t\) y) \(s\) es subpalabra de \(t\). A continuación veremos de que manera ocurren los subtérminos de un término.

Proof. (a) y (b) son fáciles y dejados al lector.

(c) Supongamos la ocurrencia de \(s\) comienza en algún \(t_{j}\). Entonces el Lema de Mordisqueo de Términos nos conduce a que dicha ocurrencia deberá estar contenida en \(t_{j}\). Veamos que la ocurrencia de \(s\) no puede ser a partir de un \(i\in\{1,...,\left\vert f\right\vert \}\). Supongamos lo contrario. Tenemos entonces que \(s\) debe ser de la forma \(g(s_{1},...,s_{m})\) ya que no puede estar en \(Var\cup\mathcal{C}\). Nótese que \(i\neq1\) ya que en caso contrario \(s\) sería un tramo inicial propio de \(f(t_{1},...,t_{n})\). Pero entonces \(g\) debe ser un tramo final propio de \(f\), lo cual es absurdo. Ya que \(s\) no puede comenzar con paréntesis o coma, hemos contemplado todos los posibles casos de comienzo de la ocurrencia de \(s\) en \(t\).

(d) Usaremos la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Supongamos \(t\in T_{k}^{\tau}\) y \(r,s\in T^{\tau}\). Si \(r,s\) ocurren en \(t\), entonces dichas ocurrencias son disjuntas o una ocurre dentro de otra.

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Supongamos \(t\in T_{0}^{\tau}\) y \(r,s\in T^{\tau}\) ocurren en \(t\). Hay dos casos.

Caso \(t\in Var\). Nótese que \(r\) y \(s\) deben pertenecer a \(Var\) ya que de lo contrario tendrían símbolos que no ocurren en \(t\) (use Lectura Única de Términos y la definición de tipo). Pero es fácil notar que nunca una variable es subpalabra propia de otra asique obtenemos \(r=s=t\) y claramente se cumple la conclusión de \(\mathrm{Enu}_{0}\).

Caso \(t\in\mathcal{C}\). Nótese que \(r\) y \(s\) deben pertenecer a \(\mathcal{C}\) ya que de lo contrario tendrían símbolos que no ocurren en \(t\) (use Lectura Única de Términos y la definición de tipo). Pero por (3) de la definición de tipo tenemos que nunca un nombre de cte es subpalabra propia de otro nombre de cte por lo cual se tiene que \(r=s=t\) y claramente se cumple la conclusión de \(\mathrm{Enu}_{0}\).

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos que \(t\in T_{k+1}^{\tau}\) y \(r,s\in T^{\tau}\) ocurren en \(t\). Por definición de \(T_{k+1}^{\tau}\), hay dos casos.

Caso \(t\in T_{k}^{\tau}\). Ya que es verdadero \(\mathrm{Enu}_{k}\), es claro que se cumple la conclusión de \(\mathrm{Enu}_{k+1}\).

Caso \(t=f(t_{1},...,t_{n})\), con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T_{k}^{\tau}\). Si \(r\) o \(s\) son iguales a \(t\), es claro que entonces se cumple la conclusión de \(\mathrm{Enu}_{k+1}\). Supongamos entonces ambos términos son distintos a \(t\). O sea que por (a), las ocurrencias de \(r\) y \(s\) en \(t\) suceden dentro de los \(t_{j}\), \(j=1,...,n\). Es claro que entonces ya que \(\mathrm{Enu}_{k}\) es verdadero se tiene que las ocurrencias de \(r\) y \(s\) en \(t\) son disjuntas o una contiene a la otra.

(e) Es consecuencia inmediata de (d).

(f) Su prueba es similar a la de (d) y es dejada al lector.  

Nota: Es importante notar que si bien no hemos definido en forma precisa el concepto de ocurrencia o de reemplazo de ocurrencias, la prueba del lema anterior es rigurosa en el sentido de que solo usa propiedades de los conceptos de ocurrencia y reemplazo de ocurrencias las cuales deberán ser comunes a cualquier definición o formulación matemática que se hiciera de aquellos conceptos. En este caso, es posible dar una definición precisa y satisfactoria de dichos conceptos aunque para otros conceptos tales como el de prueba absoluta de consistencia, aún no se ha encontrado una formulación matemática adecuada.

7.8.2.3 \(T^{\tau}\) es efectivamente computable

Dado un tipo \(\tau\), sea \(\Sigma_{\tau}\) el alfabeto finito formado por todos los símbolos que ocurren en alguna palabra de \(\mathcal{C}\cup\mathcal{F}\cup\mathcal{R}\) junto con los símbolos \[\forall\ \ \exists\ \ \lnot\ \ \vee\ \ \wedge\ \ \rightarrow\ \ \leftrightarrow\ \ (\ \ )\ \ ,\ \ \equiv\ \ \mathsf{X}\ \ \mathit{0}\ \ \mathit{1}\ \ ...\ \ \mathit{9}\ \ \mathbf{0}\ \ \mathbf{1}\ \ ...\ \ \mathbf{9}\] Nótese que entonces los conjuntos \(\mathcal{C},\text{ }\mathcal{F},\text{ }\mathcal{R}\text{ y }T^{\tau}\) son \(\Sigma_{\tau}\)-mixtos y también la función \(a:\mathcal{F}\cup\mathcal{R}\rightarrow\mathbf{N}\) es \(\Sigma_{\tau}\)-mixta.

Supongamos que los conjuntos \(\mathcal{C},\mathcal{F}\text{ y }\mathcal{R}\) son \(\Sigma_{\tau}\)-efectivamente computables y que la función \(a\) es \(\Sigma_{\tau}\)-efectivamente computable (esto sucede por ejemplo cuando los conjuntos \(\mathcal{C},\mathcal{F}\text{ y }\mathcal{R}\) son finitos). Entonces no es muy difícil convencerse que el conjunto \(T^{\tau}\) es también \(\Sigma_{\tau}\)-efectivamente computable, es decir hay un procedimiento efectivo que decide cuando una palabra de \(\Sigma_{\tau}^{*}\) es un término de tipo \(\tau\). Dejamos al lector que medite sobre esto (primero suponga que los conjuntos \(\mathcal{C}\text{ y }\mathcal{F}\) son finitos).

7.8.3 Fórmulas

Sea \(\tau\) un tipo. Las palabras de alguna de las siguientes dos formas \[\begin{array}{l} (t\equiv s),\;\text{con }t,s\in T^{\tau}\\ r(t_{1},...,t_{n})\text{, con }r\in\mathcal{R}_{n}\text{,}\ n\geq1\text{ y }t_{1},...,t_{n}\in T^{\tau} \end{array}\] serán llamadas fórmulas atómicas de tipo \(\tau\). Nótese que arriba \(r(t_{1},...,t_{n})\) denota el resultado de concatenar las \(n+(n-1)+3\) siguientes palabras \[r\;\;\;(\;\;\;t_{1}\;\;\;,\;\;\;t_{2}\;\;\;,\;\;\;...\;\;\;,\;\;\;t_{n}\;\;\;)\] Por ejemplo si \(\tau=(\{\mathrm{uno},\mathrm{doli}\},\{\mathrm{MAS},\mathrm{P}\},\{\mathrm{Her}\},a)\), con \(a\) dado por \(a(\mathrm{MAS})=4\), \(a(\mathrm{P})=1\) y \(a(\mathrm{Her})=3\), entonces

1. adhocprefix-adhocsufix \((\mathrm{uno}\equiv\mathrm{doli})\)

2. adhocprefix-adhocsufix \((\mathsf{X}\mathit{15666}\mathbf{9}\equiv\mathrm{doli})\)

3. adhocprefix-adhocsufix \(\mathrm{Her}(\mathrm{uno},\mathsf{X}\mathbf{4},\mathrm{doli})\)

4. adhocprefix-adhocsufix \((\mathrm{MAS}(\mathrm{uno},\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5})\equiv\mathrm{uno})\)

5. adhocprefix-adhocsufix \(\mathrm{Her}(\mathrm{P}(\mathrm{P}(\mathrm{uno})),\mathrm{MAS}(\mathrm{P}(\mathsf{X}\mathbf{4}),\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5}),\mathsf{X}\mathit{1}\mathbf{9})\)

son fórmulas atómicas de tipo \(\tau\).

Dado un tipo \(\tau\), definamos recursivamente los conjuntos de palabras \(F_{k}^{\tau}\), con \(k\geq0\), de la siguiente manera: \[\begin{array}{ccl} F_{0}^{\tau} & = & \{\text{fórmulas atómicas de tipo }\tau\}\\ F_{k+1}^{\tau} & = & F_{k}^{\tau}\cup\{\lnot\varphi:\varphi\in F_{k}^{\tau}\}\cup\{(\varphi\vee\psi):\varphi,\psi\in F_{k}^{\tau}\}\cup\\ & & \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \{(\varphi\wedge\psi):\varphi,\psi\in F_{k}^{\tau}\}\cup\{(\varphi\rightarrow\psi):\varphi,\psi\in F_{k}^{\tau}\}\cup\\ & & \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \{(\varphi\leftrightarrow\psi):\varphi,\psi\in F_{k}^{\tau}\}\cup\{\forall v\varphi:\varphi\in F_{k}^{\tau}\text{ y }v\in Var\}\cup\\ & & \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \{\exists v\varphi:\varphi\in F_{k}^{\tau}\text{ y }v\in Var\} \end{array}\] Nótese que arriba \((\varphi\wedge\psi)\) denota el resultado de concatenar las 5 siguientes palabras \[(\;\;\;\varphi\;\;\;\wedge\;\;\;\psi\;\;\;)\] Por dar otro ejemplo, \(\forall v\varphi\) denota el resultado de concatenar las 3 palabras siguientes \[\forall\;\;\;v\;\;\;\varphi\] Sea \[F^{\tau}=\bigcup_{k\geq0}F_{k}^{\tau}\] Los elementos de \(F^{\tau}\) serán llamados fórmulas de tipo \(\tau\). Es muy importante entender que una fórmula de tipo \(\tau\) como objeto matemático es una palabra. También debería quedar claro que el concepto de fórmula de tipo \(\tau\), a diferencia del concepto de fórmula elemental de tipo \(\tau\), es un concepto definido en forma matemática precisa.

Algunos ejemplos:

1. adhocprefix(E1)adhocsufix Sea \(\tau=(\{\mathrm{uno},\mathrm{doli}\},\{\mathrm{MAS},\mathrm{P}\},\{\mathrm{Her}\},a)\), con \(a\) dado por \(a(\mathrm{MAS})=4\), \(a(\mathrm{P})=1\) y \(a(\mathrm{Her})=3\). Entonces

   1. adhocprefix-adhocsufix \(\lnot((\mathsf{X}\mathbf{1}\equiv\mathsf{X}\mathbf{2})\wedge\mathrm{Her}(\mathrm{P}(\mathrm{doli}),\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9}))\)

   2. adhocprefix-adhocsufix \(\exists\mathsf{X}\mathbf{9}\mathrm{Her}(\mathrm{doli},\mathrm{doli},\mathsf{X}\mathbf{9})\)

   3. adhocprefix-adhocsufix \(\exists\mathsf{X}\mathbf{9}\lnot(\mathrm{uno}\equiv\mathrm{doli})\)

   4. adhocprefix-adhocsufix \(\lnot\exists\mathsf{X}\mathbf{9}\forall\mathsf{X}\mathbf{7(}\mathrm{Her}(\mathsf{X}\mathbf{9},\mathrm{doli},\mathsf{X}\mathbf{7})\rightarrow(\mathrm{P}(\mathrm{doli})\equiv\mathsf{X}\mathbf{7}))\)

   5. adhocprefix-adhocsufix \((\forall\mathsf{X}\mathit{555}\mathbf{9}\forall\mathsf{X}\mathbf{7}\exists\mathsf{X}\mathit{5}\mathbf{1}(\mathrm{MAS}(\mathrm{uno},\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5})\equiv\mathrm{uno})\rightarrow\mathrm{Her}(\mathrm{doli},\mathrm{doli},\mathrm{doli}))\)

   son fórmulas de tipo \(\tau\)

2. adhocprefix(E2)adhocsufix Sea \(\tau=(\{0,1\},\{\mathsf{s},\mathsf{i}\},\{\leq\},\{(\mathsf{s},2),(\mathsf{i},2),(\leq,2)\})\). Entonces

   1. adhocprefix-adhocsufix \(\mathrm{\leq}(1,0)\)

   2. adhocprefix-adhocsufix \(\mathrm{\leq}(\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2})\)

   3. adhocprefix-adhocsufix \(\lnot(\mathsf{s}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{1})\equiv\mathsf{X}\mathbf{2})\)

   4. adhocprefix-adhocsufix \(\forall\mathsf{X}\mathbf{2}\forall\mathsf{X}\mathbf{1}\mathrm{\leq}(\mathsf{X}\mathbf{2},\mathsf{s}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{1}))\)

   5. adhocprefix-adhocsufix \(((\mathsf{i}(\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2})\equiv0)\wedge(\mathsf{s}(\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2})\equiv1))\)

   6. adhocprefix-adhocsufix \(\forall\mathsf{X}\mathbf{9}\exists\mathsf{X}\mathbf{1}((0\equiv\mathsf{X}\mathbf{1})\rightarrow\exists\mathsf{X}\mathbf{1}\lnot\mathrm{\leq}(\mathsf{X}\mathbf{2},\mathsf{s}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{1})))\)

   son fórmulas de tipo \(\tau\). Cabe destacar que \((\mathsf{X}\mathbf{1}\leq\mathsf{X}\mathbf{2})\) no es una fórmula de tipo \(\tau\) aunque, como veremos en los ejercicios probar esto no es trivial de la definición de fórmula y requiere de una demostración.

Observación importante: Notar que las fórmulas de tipo \(\tau\) son un modelo matemático de las fórmulas elementales puras de tipo \(\tau\) , es decir aquellas en las cuales no ocurren nombres de elementos fijos. Medite...

El siguiente resultado es intuitivamente obvio por lo cual en general lo utilizaremos sin hacer mención explicita.

1. adhocprefix-adhocsufix Si \(\varphi_{1},\varphi_{2}\in F^{\tau}\) y \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}\), entonces \((\varphi_{1}\eta\varphi_{2})\in F^{\tau}\)

2. adhocprefix-adhocsufix Si \(\varphi\in F^{\tau}\), entonces \(\lnot\varphi\in F^{\tau}\)

3. adhocprefix-adhocsufix Si \(\varphi\in F^{\tau}\), \(Q\in\{\forall,\exists\}\) y \(v\in Var\), entonces \(Qv\varphi\in F^{\tau}\)

Proof. Veamos la primera propiedad. Es claro de la definición de los \(F_{k}^{\tau}\) que \(F_{i}^{\tau}\subseteq F_{j}^{\tau}\) siempre que \(i\leq j\). Supongamos \(\varphi_{1},\varphi_{2}\in F^{\tau}\) y \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}\). Por definición de \(F^{\tau}\) tenemos que hay números \(k_{1},k_{2}\) tales que \(\varphi_{i}\in F_{k_{i}}^{\tau}\), para \(i=1,2\). Es claro que entonces \(\varphi_{1},\varphi_{2}\in F_{K}^{\tau}\), donde \(K=\mathrm{max}\{k_{1},k_{2}\}\), lo cual nos dice que \((\varphi_{1}\eta\varphi_{2})\in F_{K+1}^{\tau}\subseteq F^{\tau}\).

Las pruebas de las otras propiedades son dejadas al lector.  

El siguiente lema es útil para probar propiedades acerca de los elementos de \(F^{\tau}\).

Proof. Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Si \(\varphi\in F_{k+1}^{\tau}\), entonces se da alguna de las siguientes:

   1. adhocprefix(a)adhocsufix \(\varphi=(t\equiv s),\) con \(t,s\in T^{\tau}\)

   2. adhocprefix(b)adhocsufix \(\varphi=r(t_{1},...,t_{n}),\) con \(r\in\mathcal{R}_{n}\), \(n\geq1\), \(t_{1},...,t_{n}\in T^{\tau}\)

   3. adhocprefix(c)adhocsufix \(\varphi=(\varphi_{1}\eta\varphi_{2}),\) con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\},\;\varphi_{1},\varphi_{2}\in F_{k}^{\tau}\)

   4. adhocprefix(d)adhocsufix \(\varphi=\lnot\varphi_{1},\) con \(\varphi_{1}\in F_{k}^{\tau}\)

   5. adhocprefix(e)adhocsufix \(\varphi=Qv\varphi_{1},\) con \(Q\in\{\forall,\exists\},\;v\in Var\) y \(\varphi_{1}\in F_{k}^{\tau}.\)

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Es directo de la definición de ya que por definición \(F_{1}^{\tau}\).

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Sea \(\varphi\in F_{(k+1)+1}^{\tau}\). Por definición de \(F_{(k+1)+1}^{\tau}\) tenemos varios casos:

Caso \(\varphi\in F_{k+1}^{\tau}\). Ya que \(\mathrm{Enu}_{k}\) es verdadero, tenemos que se da alguna de las siguientes

1. adhocprefix(a)adhocsufix \(\varphi=(t\equiv s),\) con \(t,s\in T^{\tau}\)

2. adhocprefix(b)adhocsufix \(\varphi=r(t_{1},...,t_{n}),\) con \(r\in\mathcal{R}_{n}\), \(n\geq1\), \(t_{1},...,t_{n}\in T^{\tau}\)

3. adhocprefix(c)adhocsufix \(\varphi=(\varphi_{1}\eta\varphi_{2}),\) con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\},\;\varphi_{1},\varphi_{2}\in F_{k}^{\tau}\)

4. adhocprefix(d)adhocsufix \(\varphi=\lnot\varphi_{1},\) con \(\varphi_{1}\in F_{k}^{\tau}\)

5. adhocprefix(e)adhocsufix \(\varphi=Qv\varphi_{1},\) con \(Q\in\{\forall,\exists\},\;v\in Var\) y \(\varphi_{1}\in F_{k}^{\tau}.\)

Ya que \(F_{k}^{\tau}\subseteq F_{k+1}^{\tau}\) tenemos que se da alguna de la siguientes

1. adhocprefix(a)adhocsufix \(\varphi=(t\equiv s),\) con \(t,s\in T^{\tau}\)

2. adhocprefix(b)adhocsufix \(\varphi=r(t_{1},...,t_{n}),\) con \(r\in\mathcal{R}_{n}\), \(n\geq1\), \(t_{1},...,t_{n}\in T^{\tau}\)

3. adhocprefix(c)adhocsufix \(\varphi=(\varphi_{1}\eta\varphi_{2}),\) con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\},\;\varphi_{1},\varphi_{2}\in F_{k+1}^{\tau}\)

4. adhocprefix(d)adhocsufix \(\varphi=\lnot\varphi_{1},\) con \(\varphi_{1}\in F_{k+1}^{\tau}\)

5. adhocprefix(e)adhocsufix \(\varphi=Qv\varphi_{1},\) con \(Q\in\{\forall,\exists\},\;v\in Var\) y \(\varphi_{1}\in F_{k+1}^{\tau}.\)

lo cual es justamente la conclusión de \(\mathrm{Enu}_{k+1}\).

Caso \(\varphi=(\varphi_{1}\eta\varphi_{2}),\) con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\},\;\varphi_{1},\varphi_{2}\in F_{k+1}^{\tau}\). Claramente en este caso se da la conclusión de \(\mathrm{Enu}_{k+1}\).

Caso \(\varphi=\lnot\varphi_{1},\) con \(\varphi_{1}\in F_{k+1}^{\tau}\). Claramente en este caso se da la conclusión de \(\mathrm{Enu}_{k+1}\).

Caso \(\varphi=Qv\varphi_{1},\) con \(Q\in\{\forall,\exists\},\;v\in Var\) y \(\varphi_{1}\in F_{k+1}^{\tau}.\) Claramente en este caso se da la conclusión de \(\mathrm{Enu}_{k+1}\).  

7.8.3.1 Unicidad de la lectura de fórmulas

Tal como para el caso de términos veremos que las fórmulas también tienen su unicidad de lectura. Definamos \[T=\{\lnot\}\cup\{Qv:Q\in\{\forall,\exists\}\text{ y }v\in Var\}\] \[T^{*}=\{\alpha_{1}...\alpha_{n}:\alpha_{1},...,\alpha_{n}\in T,\text{ }n\geq0\}\] (cuando \(n=0\), la concatenación \(\alpha_{1}...\alpha_{n}\) es igual a \(\varepsilon\)). Mas adelante nos hará falta el siguiente resultado básico.

Proof. Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Sea \(\tau\) un tipo. Sea \(\varphi\in F_{k}^{\tau}\). Entonces \(\varphi\) es de alguna de las siguientes formas:

   1. adhocprefix(1)adhocsufix \(\varphi=x(t\equiv s)\), con \(x\in T^{*}\) y \(t,s\in T^{\tau}\).

   2. adhocprefix(2)adhocsufix \(\varphi=xr(t_{1},...,t_{n})\), con \(x\in T^{*}\), \(n\in\mathbf{N}\), \(r\in\mathcal{R}_{n}\) y \(t_{1},...,t_{n}\in T^{\tau}\).

   3. adhocprefix(3)adhocsufix \(\varphi=x(\varphi_{1}\eta\varphi_{2})\), con \(x\in T^{*}\), \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}\) y \(\varphi_{1},\varphi_{2}\in F^{\tau}\).

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Sea \(\varphi\in F_{0}^{\tau}\). Ya que \(\varphi\) es atómica, es trivial que se da (1) o (2), tomando \(x=\varepsilon\).

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Sea \(\varphi\in F_{k+1}^{\tau}\). Probaremos que se da (1) o (2) o (3) para \(\varphi\). Por definición de \(F_{k+1}^{\tau}\) tenemos varios casos:

Caso \(\varphi\in F_{k}^{\tau}\). Ya que \(\mathrm{Enu}_{k}\) es verdadero, tenemos que se da (1) o (2) o (3) para \(\varphi\).

Caso \(\varphi=(\varphi_{1}\eta\varphi_{2}),\) con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}\text{ y }\varphi_{1},\varphi_{2}\in F_{k}^{\tau}\). Es claro que entonces se cumple (3) tomando \(x=\varepsilon\).

Caso \(\varphi=Qv\varphi_{1},\) con \(Q\in\{\forall,\exists\},\;v\in Var\) y \(\varphi_{1}\in F_{k}^{\tau}.\) Ya que \(\varphi_{1}\in F_{k}^{\tau}\) y vale \(\mathrm{Enu}_{k}\) tenemos que se da alguno de los siguientes casos:

1. adhocprefix(a)adhocsufix \(\varphi_{1}=x_{1}(t\equiv s)\), con \(x_{1}\in T^{*}\) y \(t,s\in T^{\tau}\).

2. adhocprefix(b)adhocsufix \(\varphi_{1}=x_{1}r(t_{1},...,t_{n})\), con \(x_{1}\in T^{*}\), \(n\in\mathbf{N}\), \(r\in\mathcal{R}_{n}\) y \(t_{1},...,t_{n}\in T^{\tau}\).

3. adhocprefix(c)adhocsufix \(\varphi_{1}=x_{1}(\psi_{1}\eta\psi_{2})\), con \(x_{1}\in T^{*}\), \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}\) y \(\psi_{1},\psi_{2}\in F^{\tau}\).

Supongamos que se da (b). Si tomamos \(x=Qvx_{1}\) entonces tenemos que \(x\in T^{*}\) y \(\varphi=xr(t_{1},...,t_{n})\) lo cual nos dice que se da (2) de \(\mathrm{Enu}_{k+1}\) para \(\varphi\). Análogamente si se da (a) o (b) es fácil ver que se da (1) o (3) de \(\mathrm{Enu}_{k+1}\) para \(\varphi\), respectivamente.

Caso \(\varphi=\lnot\varphi_{1}\), con \(\varphi_{1}\in F_{k}^{\tau}\). Similar al anterior.  

Nótese que el lema anterior nos dice que toda fórmula \(\varphi\in F^{\tau}\) es de la forma \(x\varphi_{1}\), con \(x\in T^{*}\) y \(\varphi_{1}\in F^{\tau}\) ya sea atómica o de la forma \((\alpha_{1}\eta\alpha_{2})\). Además \(x\) y \(\varphi_{1}\) están unívocamente determinados por \(\varphi\), a saber \(x\) es el mayor tramo inicial de \(\varphi\) que pertenece a \(T^{*}\) o dicho de otra forma \(x\) es el mayor tramo inicial de \(\varphi\) que no tiene símbolos de \(\{(\}\cup\{[r]_{1}:r\in\mathcal{R}\}\); y \(\varphi_{1}\) es lo que resta de este tramo inicial hasta completar \(\varphi\).

Proof. Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Sea \(\varphi\in F_{k}^{\tau}\). Se tiene:

   1. adhocprefix(1)adhocsufix \(SPar(\varphi)=0\).

   2. adhocprefix(2)adhocsufix Si \(z\) es tramo inicial de \(\varphi\), entonces \(SPar(z)\geq0\)

   3. adhocprefix(3)adhocsufix Si \(z\) es tramo final de \(\varphi\), entonces \(SPar(z)\leq0\)

   4. adhocprefix(4)adhocsufix Si \(z\) es tramo inicial propio de \(\varphi\) y en \(z\) ocurre algún paréntesis, entonces \(SPar(z)>0\)

   5. adhocprefix(5)adhocsufix Si \(z\) es tramo final de \(\varphi\), \(z\neq\varepsilon\) y \(SPar(z)=0\), entonces a la izquierda de \(z\) en \(\varphi\) no ocurren paréntesis.

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Sea \(\varphi\in F_{0}^{\tau}\). Hay dos casos.

Caso \(\varphi=r(t_{1},...,t_{n})\), con \(n\in\mathbf{N}\), \(r\in\mathcal{R}_{n}\) y \(t_{1},...,t_{n}\in T^{\tau}\). Por el Lema \(SPar\) en Términos tenemos que se cumplen

1. adhocprefix(a)adhocsufix \(SPar(t_{i})=0\), para \(i=1,...,n\)

2. adhocprefix(b)adhocsufix Para \(i=1,...,n\), si \(z\) es tramo inicial de \(t_{i}\), entonces \(SPar(z)\geq0\)

3. adhocprefix(c)adhocsufix Para \(i=1,...,n\), si \(z\) es tramo final de \(t_{i}\), entonces \(SPar(z)\leq0\)

4. adhocprefix(d)adhocsufix Para \(i=1,...,n\), si \(z\) es tramo inicial propio de \(t_{i}\) y en \(z\) ocurre algún paréntesis, entonces \(SPar(z)>0\)

5. adhocprefix(e)adhocsufix Para \(i=1,...,n\), si \(z\) es tramo final de \(t_{i}\), \(z\neq\varepsilon\) y \(SPar(z)=0\), entonces a la izquierda de \(z\) en \(t_{i}\) no ocurren paréntesis.

Es fácil notar entonces que \(\varphi\) cumple (1). Veamos que \(\varphi\) cumple (4). Sea \(z\) un tramo inicial propio de \(\varphi\) y supongamos que en \(z\) ocurre algún paréntesis. Nótese que \(z\) es de la forma \(z=r(t_{1},...,t_{i},z_{1}\) con \(0\leq i\leq n-1\) y \(z_{1}\) un tramo inicial de \(t_{i+1}\) (en el caso \(i=0\) interpretamos \(t_{1},...,t_{i}=\varepsilon)\). Además nótese que: \[SPar(z)=1+\left(\sum_{j=1}^{i}SPar(t_{j})\right)+SPar(z_{1})\] Por (a) tenemos que \[\left(\sum_{j=1}^{i}SPar(t_{j})\right)=0\] Ya que \(z_{1}\) es un tramo inicial de \(t_{i+1}\), (b) nos dice que \[SPar(z_{1})\geq0\] O sea que \(SPar(z)>0\).

Veamos que \(\varphi\) cumple (5). Supongamos que \(z\) es tramo final de \(\varphi\), \(z\neq\varepsilon\) y \(SPar(z)=0\). Supongamos primero que \(\left|z\right|<\left|(t_{1},...,t_{n})\right|\). Ya que \(z\neq\varepsilon\), tenemos que \(z\) es de la forma \(z=z_{1},t_{i},...,t_{n})\) con \(1<i\leq n+1\) y \(z_{1}\) un tramo final de \(t_{i-1}\) (en el caso \(i=n+1\) interpretamos \(t_{i},...,t_{n}=\varepsilon)\). Además nótese que: \[SPar(z)=SPar(z_{1})+\left(\sum_{j=i}^{n}SPar(t_{j})\right)+1\] Por (a) tenemos que \[\left(\sum_{j=i}^{n}SPar(t_{j})\right)=0\] Ya que \(z_{1}\) es un tramo final de \(t_{i-1}\), (c) nos dice que \[SPar(z_{1})\leq0\] O sea que \(SPar(z)<0\), lo cual es absurdo. O sea que \(\left|z\right|\geq\left|(t_{1},...,t_{n})\right|\). Pero entonces es claro que a la izquierda de \(z\) en \(\varphi\) no ocurren paréntesis.

Las pruebas de que \(\varphi\) cumple las propiedades (2) y (3) son dejadas al lector.

Caso \(\varphi=(t\equiv s)\), con \(t,s\in T^{\tau}\). Es dejado al lector.

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos \(\varphi\in T_{k+1}^{\tau}\). Probaremos que \(\varphi\) cumple (1), (2), (3), (4) y (5). Por definición de \(F_{k+1}^{\tau}\) hay varios casos.

Caso \(\varphi\in F_{k}^{\tau}\). Entonces ya que vale \(\mathrm{Enu}_{k}\) tenemos que \(\varphi\) cumple (1), (2), (3), (4) y (5).

Caso \(\varphi=(\varphi_{1}\eta\varphi_{2})\), con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}\text{ y }\varphi_{1},\varphi_{2}\in F_{k}^{\tau}\). Ya que vale \(\mathrm{Enu}_{k}\) tenemos que para \(i=1,2\) se dan:

1. adhocprefix(a)adhocsufix \(SPar(\varphi_{i})=0\), para \(i=1,2\)

2. adhocprefix(b)adhocsufix Para \(i=1,2\), si \(z\) es tramo inicial de \(\varphi_{i}\), entonces \(SPar(z)\geq0\)

3. adhocprefix(c)adhocsufix Para \(i=1,2\), si \(z\) es tramo final de \(\varphi_{i}\), entonces \(SPar(z)\leq0\)

4. adhocprefix(d)adhocsufix Para \(i=1,2\), si \(z\) es tramo inicial propio de \(\varphi_{i}\) y en \(z\) ocurre algún paréntesis, entonces \(SPar(z)>0\)

5. adhocprefix(e)adhocsufix Para \(i=1,2\), si \(z\) es tramo final de \(\varphi_{i}\), \(z\neq\varepsilon\) y \(SPar(z)=0\), entonces a la izquierda de \(z\) en \(\varphi_{i}\) no ocurren paréntesis.

Por (a) tenemos que \(\varphi\) cumple (1). Es claro también que (b) nos dice que vale (2) y (c) que vale (3). Veamos que \(\varphi\) cumple (4). Sea \(z\) un tramo inicial propio de \(\varphi\). Hay dos casos posibles, uno que \(z\) sea de la forma \((z_{1}\) con \(z_{1}\) un tramo inicial de \(\varphi_{1}\) y el otro que \(z\) sea de la forma \((\varphi_{1}\eta z_{1}\) con \(z_{1}\) un tramo inicial de \(\varphi_{2}\). En ambos casos usando (b) obtenemos que \(SPar(z)>0\). En forma similar usando \((c)\) se puede probar que si \(z\) es tramo final propio de \(\varphi\), entonces \(SPar(z)<0\). Esto claramente implica que \(\varphi\) cumple (5).

Caso \(\varphi=Qv\varphi_{1}\) con \(Q\in\{\forall,\exists\},\;v\in Var\) y \(\varphi_{1}\in F_{k}^{\tau}\). Ya que vale \(\mathrm{Enu}_{k}\) tenemos que:

1. adhocprefix(a)adhocsufix \(SPar(\varphi_{1})=0\)

2. adhocprefix(b)adhocsufix Si \(z\) es tramo inicial de \(\varphi_{1}\), entonces \(SPar(z)\geq0\)

3. adhocprefix(c)adhocsufix Si \(z\) es tramo final de \(\varphi_{1}\), entonces \(SPar(z)\leq0\)

4. adhocprefix(d)adhocsufix Si \(z\) es tramo inicial propio de \(\varphi_{1}\) y en \(z\) ocurre algún paréntesis, entonces \(SPar(z)>0\)

5. adhocprefix(e)adhocsufix Si \(z\) es tramo final de \(\varphi_{1}\), \(z\neq\varepsilon\) y \(SPar(z)=0\), entonces a la izquierda de \(z\) en \(\varphi_{1}\) no ocurren paréntesis.

Es fácil usando las propiedades (a), (b), (c), (d) y (e) probar que \(\varphi\) cumple (1), (2), (3), (4) y (5).  

Proof. Caso \(\varphi=(t\equiv s)\), con \(t,s\in T^{\tau}\). Supongamos \(\psi\) es tramo final de \(\varphi\). Por (1) del Lema \(SPar\) en Fórmulas tenemos que \(SPar(\psi)=0\). Pero entonces (5) del mismo lema nos dice \(\psi=\varphi\) ya que \(\varphi\) comienza con paréntesis.

Caso \(\varphi=(\varphi_{1}\eta\varphi_{2})\), con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}\) y \(\varphi_{1},\varphi_{2}\in F^{\tau}\). Análogo al caso anterior.

Caso \(\varphi=r(t_{1},...,t_{n})\), con \(n\in\mathbf{N}\), \(r\in\mathcal{R}_{n}\) y \(t_{1},...,t_{n}\in T^{\tau}\). Supongamos \(\psi\) es tramo final de \(\varphi\). Por el Lema Tres Formatos tenemos que \(\psi=x\psi_{1}\), con \(x\in T^{*}\) y \(\psi_{1}\in F^{\tau}\) de la forma \((\beta_{1}\eta\beta_{2})\) o atómica. Ya que \(SPar(\psi)=0\) (5) del Lema \(SPar\) en Fórmulas nos dice que \(\psi=z(t_{1},...,t_{n})\) para algún tramo final \(z\) de \(r\). O sea que \(x\psi_{1}=z(t_{1},...,t_{n})\). Esto nos dice que \(x=\varepsilon\) ya que en \(z(t_{1},...,t_{n})\) no ocurren símbolos de \(\{\forall,\exists,\neg\}\). O sea que \(\psi_{1}=z(t_{1},...,t_{n})\). Ya que en \(z(t_{1},...,t_{n})\) no ocurren símbolos de \(\{\equiv,\wedge,\vee,\rightarrow,\leftrightarrow\}\) tenemos que \(\psi_{1}=\tilde{r}(s_{1},...,s_{m})\), con \(\tilde{r}\in\mathcal{R}_{m}\), \(m\geq1\) y \(s_{1},...,s_{m}\in T^{\tau}\). Tenemos entonces \(\tilde{r}(s_{1},...,s_{m})=z(t_{1},...,t_{n})\). Ya que ni \(z\) ni \(\tilde{r}\) tienen el símbolo \((\) deberá suceder que \(z=\tilde{r}\in\mathcal{R}\). O sea que \(z\in\mathcal{R}\) y además \(z\) es tramo final de \(r\) lo cual por la definición de tipo nos dice que \(z=r\). O sea que \(\psi=z(t_{1},...,t_{n})=r(t_{1},...,t_{n})=\varphi\).  

Proof. Supongamos \(z\neq\varepsilon\). Ya que el último símbolo de \(y\) es \()\) y \(y\) es un tramo inicial propio de la fórmula \(\psi\), (4) del Lema \(SPar\) en Fórmulas nos dice que \(SPar(y)>0\). Pero \(y\) es tramo final de la fórmula \(\varphi\) por lo cual \(SPar(y)\leq0\) ((1) del mismo lema). El absurdo obtenido nos dice que \(z=\varepsilon\). O sea que \(\varphi=x\psi\). Probaremos que \(x\in T^{*}\). Por el Lema Tres Formatos tenemos que \(\varphi=x_{1}\varphi_{1}\), con \(x_{1}\in T^{*}\) y \(\varphi_{1}\in F^{\tau}\) de la forma \((\alpha_{1}\eta\alpha_{2})\) o atómica. Por el mismo lema tenemos que \(\psi=y_{1}\psi_{1}\), con \(y_{1}\in T^{*}\) y \(\psi_{1}\in F^{\tau}\) de la forma \((\beta_{1}\eta\beta_{2})\) o atómica. O sea que \(x_{1}\varphi_{1}=xy_{1}\psi_{1}\). Esto nos dice que \(\varphi_{1}\) es tramo final de \(\psi_{1}\) o \(\psi_{1}\) es ramo final de \(\varphi_{1}\). Entonces el lema anterior nos dice que \(\varphi_{1}=\psi_{1}\) por lo cual \(x_{1}=xy_{1}\). Finalmente el Lema 7.9 nos dice que \(x\in T^{*}\).  

Proof. Nótese que el Lema Menú para Fórmulas nos dice que se da alguna de las 5 propiedades, salvo por la unicidad. Si una fórmula \(\varphi\) satisface (1), entonces \(\varphi\) no puede contener símbolos del alfabeto \(\{\wedge,\vee,\rightarrow,\leftrightarrow\}\) lo cual garantiza que \(\varphi\) no puede satisfacer (3). Además \(\varphi\) no puede satisfacer (2) o (4) o (5) ya que \(\varphi\) comienza con \((\). En forma análoga se puede terminar de ver que las propiedades (1),...,(5) son excluyentes.

Veamos entonces la unicidad en los distintos ítems. La unicidad en (4) y (5) es obvia. La de (3) se desprende fácilmente del lema anterior y la de los puntos (1) y (2) del lema análogo para términos.

Dejamos al lector probar la última observación usando el Lema Menú para Fórmulas.  

7.8.3.2 Ocurrencia de fórmulas en fórmulas

Una fórmula \(\varphi\) será llamada una subfórmula (propia) de una fórmula \(\psi\), cuando \(\varphi\) sea subpalabra de \(\psi\) (y no sea igual a \(\psi\)).

Proof. (a) Supongamos \(\psi\) es una subfórmula de una fórmula atómica de la forma \((t_{1}\equiv t_{2})\). Ya que en \((t_{1}\equiv t_{2})\) no ocurren símbolos de \(\{\wedge,\vee,\rightarrow,\leftrightarrow,\neg,\forall,\exists\}\) tenemos que \(\psi\) debe ser atómica. Ya que en \((t_{1}\equiv t_{2})\) no ocurren símbolos que ocurren en los nombres de relación, tenemos que \(\psi\) debe ser de la forma \((s_{1}\equiv s_{2})\). Ya que el símbolo \(\equiv\) ocurre solo una ves en \((t_{1}\equiv t_{2})\) tenemos que \(s_{1}\) debe ser tramo final de \(t_{1}\) y \(s_{2}\) debe ser tramo inicial de \(t_{2}\). Pero entonces el Lema de Mordisqueo de Términos nos dice que \(s_{1}\) debe ser igual a \(t_{1}\) y \(s_{2}\) debe igual a \(t_{2}\), lo cual nos dice que \(\psi=(t_{1}\equiv t_{2})\).

Supongamos \(\psi\) es una subfórmula de una fórmula atómica de la forma \(r(t_{1},...,t_{n})\). Ya que en \(r(t_{1},...,t_{n})\) no ocurren símbolos de \(\{\wedge,\vee,\rightarrow,\leftrightarrow,\neg,\forall,\exists\}\) tenemos que \(\psi\) debe ser atómica. Ya que en \(r(t_{1},...,t_{n})\) no ocurre el símbolo \(\equiv\) tenemos que \(\psi\) debe ser de la forma \(\tilde{r}(s_{1},...,s_{m})\). Pero los símbolos de \(\tilde{r}\) no ocurren en \((t_{1},...,t_{n})\) por lo cual debe suceder que \(\tilde{r}\) ocurra en \(r\). Esto claramente nos dice que \(\tilde{r}=r\) y que \((s_{1},...,s_{m})\) debe ser tramo inicial de \((t_{1},...,t_{n})\). Usando el Lema de Mordisqueo de Términos se puede ver fácilmente que entonces \((s_{1},...,s_{m})=(t_{1},...,t_{n})\), lo cual nos dice que \(\psi=r(t_{1},...,t_{n})\).

(b) Supongamos que \(\varphi\neq(\psi\eta\phi)\) y \(\varphi\) ocurre en \((\psi\eta\phi)\). Si la ocurrencia de \(\varphi\) comienza en \(\psi\) (resp. en \(\phi\)), entonces el Lema de Mordisqueo de Fórmulas nos dice que dicha ocurrencia debe estar contenida en \(\psi\) (resp. en \(\phi\)). Veamos que la ocurrencia de \(\varphi\) no puede comenzar en los otros tres lugares restantes (i. e. \(1,\text{ }\left|(\psi\eta\right|\text{ o }\left|(\psi\eta\phi)\right|\)). Si comienza a partir de \(1\), entonces \(\varphi\) es tramo inicial de \((\psi\eta\phi)\) lo cual por el Lema de Mordisqueo de Fórmulas nos dice que \(\varphi=(\psi\eta\phi)\), absurdo. Obviamente tampoco puede comenzar a partir de \(\left|(\psi\eta\right|\text{ o }\left|(\psi\eta\phi)\right|\) ya que entonces \(\varphi\) debería comenzar ya sea con \(\eta\text{ o })\).

(c) y (d) son similares a (b).

(e) Es consecuencia directa del Lema de Mordisqueo de Fórmulas.

(f) Es consecuencia directa de (e).

(g) Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Supongamos \(\lambda\in F_{k}^{\tau}\) y \(\varphi_{1},\varphi_{2}\in F^{\tau}\). Si \(\lambda^{\prime}\) es el resultado de reemplazar alguna ocurrencia de \(\varphi_{1}\) en \(\lambda\) por \(\varphi_{2}\), entonces \(\lambda^{\prime}\in F^{\tau}\).

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Sea \(\lambda\in F_{0}^{\tau}\). Por (a) deberá suceder que \(\varphi_{1}=\lambda\). O sea que \(\lambda^{\prime}=\varphi_{2}\) por lo cual \(\lambda^{\prime}\in F^{\tau}\).

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Sea \(\lambda\in F_{k+1}^{\tau}\) y \(\varphi_{1},\varphi_{2}\in F^{\tau}\). Sea \(\lambda^{\prime}=\) resultado de reemplazar alguna ocurrencia de \(\varphi_{1}\) en \(\lambda\) por \(\varphi_{2}\). Probaremos que \(\lambda^{\prime}\in F^{\tau}\). Por definición de \(F_{k+1}^{\tau}\) tenemos varios casos:

Caso \(\lambda\in F_{k}^{\tau}\). Ya que \(\mathrm{Enu}_{k}\) es verdadero, tenemos que \(\lambda^{\prime}\in F^{\tau}\).

Caso \(\lambda=(\lambda_{1}\eta\lambda_{2})\), con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\},\;\lambda_{1},\lambda_{2}\in F_{k}^{\tau}\). Si \(\varphi_{1}=\lambda\) entonces \(\lambda^{\prime}=\varphi_{2}\) y por lo tanto \(\lambda^{\prime}\in F^{\tau}\). Supongamos entonces \(\varphi_{1}\neq\lambda\). Por (b) la ocurrencia de \(\varphi_{1}\) en \(\lambda\) que fue reemplazada por \(\varphi_{2}\) para obtener \(\lambda^{\prime}\) sucede ya sea en \(\lambda_{1}\) o en \(\lambda_{2}\). Supongamos ocurra en \(\lambda_{2}\) y sea \(\lambda_{2}^{\prime}=\) resultado de reemplazar dicha ocurrencia de \(\varphi_{1}\) en \(\lambda_{2}\) por \(\varphi_{2}\). Ya que vale \(\mathrm{Enu}_{k}\) y \(\lambda_{2}\in F_{k}^{\tau}\) tenemos que \(\lambda_{2}^{\prime}\in F^{\tau}\). Ya que \(\lambda^{\prime}=(\lambda_{1}\eta\lambda_{2}^{\prime})\) obtenemos que \(\lambda^{\prime}\in F^{\tau}\).

La prueba de los otros casos es similar y dejada al lector.  

7.8.3.3 Ocurrencias de términos en fórmulas

Ahora veremos como son las ocurrencias de términos en fórmulas. Si \(t\) es un término y \(\varphi\) una fórmula, una ocurrencia de \(t\) en \(\varphi\) se llamara contigua cuando dicha ocurrencia no es a partir del primer símbolo de \(\varphi\) y además el símbolo anterior en \(\varphi\) a dicha ocurrencia es ya sea \(\forall\) o \(\exists\). Dicho de otra forma una ocurrencia de \(t\) en \(\varphi\) se llamara contigua cuando dicha ocurrencia este contenida en una ocurrencia de una palabra de la forma \(Qt\), con \(Q\in\{\forall,\exists\}\). Es claro que solamente cuando \(t\) es una variable puede suceder que alguna ocurrencia de \(t\) en \(\varphi\) sea contigua. Esto se deduce de los dos siguientes hechos, fáciles de probar.

1. adhocprefix-adhocsufix Si \(Q\in\{\forall,\exists\}\) ocurre desde \(i\) en \(\varphi\in F^{\tau}\) entonces \(\mathsf{X}\) ocurre desde \(i+1\) en \(\varphi\).

2. adhocprefix-adhocsufix Si \(t\in T^{\tau}\) comienza con \(\mathsf{X}\) entonces \(t\in Var\).

Proof. (a) Ya que ningún término comienza con paréntesis o con el símbolo \(\equiv\) es claro que entonces la ocurrencia de \(t\) comienza en \(t_{1}\) o en \(t_{2}\). Pero entonces el Lema de Mordisqueo de Términos nos dice que la ocurrencia debe ser en \(t_{1}\) o en \(t_{2}\).

(b) Nótese que \(t\) no puede comenzar con un símbolo de \(r\) ya que \(r\in\mathcal{R}\). O sea que como tampoco puede comenzar con alguno de los tres símbolos \[(\:)\text{ ,}\] se tiene que la ocurrencia de \(t\) comienza en algún \(t_{j}\). Entonces el Lema de Mordisqueo de Términos nos conduce a que dicha ocurrencia deberá estar contenida en \(t_{j}\).

(c) Es claro que la ocurrencia de \(t\) comienza en \(\psi\) o en \(\phi\). Supongamos la ocurrencia de \(t\) comienza en \(\psi\). Ya que \(\eta\) no ocurre en \(t\) es claro entonces que dicha ocurrencia deberá estar contenida en \(\psi\). Supongamos la ocurrencia de \(t\) comienza en \(\phi\). Si \(t\) no termina con el símbolo \()\) entonces es claro que la ocurrencia de \(t\) está contenida en \(\phi\). Supongamos entonces \(t\) termina con el símbolo \()\) y la ocurrencia de \(t\) no está contenida en \(\phi\). Llegaremos a un absurdo. Nótese que \(t\) debe ser de la forma \(f(t_{1},...,t_{n})\) y además la palabra \(x=f(t_{1},...,t_{n}\) deberá ser tramo final de \(\phi\). Pero el Lema \(SPar\) en Términos nos dice que \(SPar(x)>0\) lo cual contradice al Lema \(SPar\) en Fórmulas que nos dice que \(SPar(x)\leq0\).

(d) Es trivial ya que ningún término comienza con el símbolo \(\lnot\)

(e) Es claro que la ocurrencia no puede ser a partir de \(1\) ya que ningún término comienza con \(\forall\) o \(\exists\). Si la ocurrencia de \(t\) comienza en \(x_{k}\) entonces por el Lema de Mordisqueo de Términos deberá pasar que \(t=x_{k}\) y la ocurrencia es justamente la de \(x_{k}\). Sólo queda entonces el caso en que la ocurrencia sucede dentro de \(\psi.\)

(f) Es consecuencia inmediata del Lema de Mordisqueo de Términos.

(g) Es consecuencia inmediata de (f).

(h) Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Supongamos \(\lambda\in F_{k}^{\tau}\) y \(t_{1},t_{2}\in T^{\tau}\). Si \(\lambda^{\prime}\) es el resultado de reemplazar alguna ocurrencia no contigua de \(t_{1}\) en \(\lambda\) por \(t_{2}\), entonces \(\lambda^{\prime}\in F^{\tau}\).

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Sea \(\lambda\in F_{0}^{\tau}\). Hay dos casos.

Caso \(\lambda=(s_{1}\equiv s_{2})\). Por (a) la ocurrencia no contigua de \(t_{1}\) en \(\lambda\) deberá suceder dentro de \(s_{1}\) o dentro de \(s_{2}\). Supongamos sucede dentro de \(s_{2}\). Sea \(s_{2}^{\prime}\) el resultado de reemplazar dicha ocurrencia de \(t_{1}\) en \(s_{2}\) por \(t_{2}\). Notar que \(\lambda^{\prime}=(s_{1}\equiv s_{2}^{\prime})\). Por el Lema de Ocurrencias de Términos en Términos se tiene que \(s_{2}^{\prime}\in T^{\tau}\), por lo cual obtenemos que \(\lambda^{\prime}\in F^{\tau}\). El caso en que la ocurrencia no contigua de \(t_{1}\) sucede en \(s_{1}\) es análogo.

Dejamos al lector hacer el caso \(\lambda=r(t_{1},...,t_{n})\) por ser muy similar.

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Sea \(\lambda\in F_{k+1}^{\tau}\) y \(t_{1},t_{2}\in T^{\tau}\). Sea \(\lambda^{\prime}=\) resultado de reemplazar alguna ocurrencia no contigua de \(t_{1}\) en \(\lambda\) por \(t_{2}\). Probaremos que \(\lambda^{\prime}\in F^{\tau}\). Por definición de \(F_{k+1}^{\tau}\) tenemos varios casos:

Caso \(\lambda\in F_{k}^{\tau}\). Ya que \(\mathrm{Enu}_{k}\) es verdadero, tenemos que \(\lambda^{\prime}\in F^{\tau}\).

Caso \(\lambda=(\lambda_{1}\eta\lambda_{2})\), con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\},\;\lambda_{1},\lambda_{2}\in F_{k}^{\tau}\). Por (c) la ocurrencia no contigua de \(t_{1}\) en \(\lambda\) sucede en \(\lambda_{1}\) o en \(\lambda_{2}\). Supongamos sucede en \(\lambda_{2}\). Nótese que dicha ocurrencia también es no contigua en \(\lambda_{2}\). Sea \(\lambda_{2}^{\prime}=\) resultado de reemplazar dicha ocurrencia no contigua de \(t_{1}\) en \(\lambda_{2}\) por \(t_{2}\). Ya que vale \(\mathrm{Enu}_{k}\) y \(\lambda_{2}\in F_{k}^{\tau}\) tenemos que \(\lambda_{2}^{\prime}\in F^{\tau}\). Pero \(\lambda^{\prime}=(\lambda_{1}\eta\lambda_{2}^{\prime})\) por lo cual \(\lambda^{\prime}\in F^{\tau}\). Si la ocurrencia no contigua de \(t_{1}\) en \(\lambda\) sucede en \(\lambda_{1}\) la prueba es similar.

Caso \(\lambda=Qx_{j}\lambda_{1}\) con \(Q\in\{\forall,\exists\},\;\lambda_{1}\in F_{k}^{\tau}\) y \(j\in\mathbf{N}\). Ya que la ocurrencia de \(t_{1}\) en \(\lambda\) es no contigua, (e) nos dice que debe suceder dentro de \(\lambda_{1}\). Además dicha ocurrencia de \(t_{1}\) en \(\lambda_{1}\) también es no contigua. Sea \(\lambda_{1}^{\prime}=\) resultado de reemplazar dicha ocurrencia no contigua de \(t_{1}\) en \(\lambda_{1}\) por \(t_{2}\). Ya que vale \(\mathrm{Enu}_{k}\) y \(\lambda_{1}\in F_{k}^{\tau}\) tenemos que \(\lambda_{1}^{\prime}\in F^{\tau}\). Pero \(\lambda^{\prime}=Qx_{j}\lambda_{1}^{\prime}\) por lo cual \(\lambda^{\prime}\in F^{\tau}\). Si la ocurrencia no contigua de \(t_{1}\) en \(\lambda\) sucede en \(\lambda_{1}\) la prueba es similar.

Caso \(\lambda=\lnot\lambda_{1}\), con \(\lambda_{1}\in F_{k}^{\tau}\). Es dejado al lector.

7.8.3.4 \(F^{\tau}\) es efectivamente computable

Dado un tipo \(\tau\), sea \(\Sigma_{\tau}\) el alfabeto finito formado por todos los símbolos que ocurren en alguna palabra de \(\mathcal{C}\cup\mathcal{F}\cup\mathcal{R}\) junto con los símbolos \[\forall\ \ \exists\ \ \lnot\ \ \vee\ \ \wedge\ \ \rightarrow\ \ \leftrightarrow\ \ (\ \ )\ \ ,\ \ \equiv\ \ \mathsf{X}\ \ \mathit{0}\ \ \mathit{1}\ \ ...\ \ \mathit{9}\ \ \mathbf{0}\ \ \mathbf{1}\ \ ...\ \ \mathbf{9}\] Nótese que entonces los conjuntos \(\mathcal{C},\text{ }\mathcal{F},\text{ }\mathcal{R},\text{ }T^{\tau}\text{ y }F^{\tau}\) son \(\Sigma_{\tau}\)-mixtos y también la función \(a:\mathcal{F}\cup\mathcal{R}\rightarrow\mathbf{N}\) es \(\Sigma_{\tau}\)-mixta.

Supongamos que los conjuntos \(\mathcal{C},\mathcal{F}\text{ y }\mathcal{R}\) son \(\Sigma_{\tau}\)-efectivamente computables y que la función \(a\) es \(\Sigma_{\tau}\)-efectivamente computable (esto sucede por ejemplo cuando los conjuntos \(\mathcal{C},\mathcal{F}\text{ y }\mathcal{R}\) son finitos). Ya observamos antes que \(T^{\tau}\) es entonces \(\Sigma_{\tau}\)-efectivamente computable. Basándose en esto no es muy difícil convencerse que el conjunto \(F^{\tau}\) es también \(\Sigma_{\tau}\)-efectivamente computable. Dejamos al lector que medite sobre esto (primero suponga que los conjuntos \(\mathcal{C}\text{ y }\mathcal{F}\) son finitos).

7.8.3.5 Variables libres

Recordemos que dadas palabras \(\alpha,\beta\in\Sigma^{\ast}\), con \(\left\vert \alpha\right\vert ,\left\vert \beta\right\vert \geq1\), y un natural \(i\in\{1,...,\left\vert \beta\right\vert \}\), se dice que \(\alpha\) ocurre a partir de \(i\) en \(\beta\) cuando se dé que existan palabras \(\delta,\gamma\) tales que \(\beta=\delta\alpha\gamma\) y \(\left\vert \delta\right\vert =i-1\). Intuitivamente hablando \(\alpha\) ocurre a partir de \(i\) en \(\beta\) cuando se dé que si comenzamos a leer desde el lugar \(i\)-ésimo de \(\beta\), en adelante, entonces leeremos la palabra \(\alpha\) completa y luego posiblemente seguirán otros símbolos.

Definamos recursivamente la relación \("v\mathit{\ ocurre\ libremente\ en\ }\varphi\mathit{\ a\ partir\ de\ }i"\), donde \(v\in Var\), \(\varphi\in F^{\tau}\) y \(i\in\{1,...,\left\vert \varphi\right\vert \}\), de la siguiente manera:

1. adhocprefix(1)adhocsufix Si \(\varphi\) es atómica, entonces \(v\) ocurre libremente en \(\varphi\) a partir de \(i\) sii \(v\) ocurre en \(\varphi\) a partir de \(i\)

2. adhocprefix(2)adhocsufix Si \(\varphi=(\varphi_{1}\eta\varphi_{2})\), entonces \(v\) ocurre libremente en \(\varphi\) a partir de \(i\) sii se da alguna de las siguientes

   1. adhocprefix(a)adhocsufix \(v\) ocurre libremente en \(\varphi_{1}\) a partir de \(i-1\)

   2. adhocprefix(b)adhocsufix \(v\) ocurre libremente en \(\varphi_{2}\) a partir de \(i-\left\vert (\varphi_{1}\eta\right\vert\)

3. adhocprefix(3)adhocsufix Si \(\varphi=\lnot\varphi_{1}\), entonces \(v\) ocurre libremente en \(\varphi\) a partir de \(i\) sii \(v\) ocurre libremente en \(\varphi_{1}\) a partir de \(i-1\)

4. adhocprefix(4)adhocsufix Si \(\varphi=Qw\varphi_{1}\), entonces \(v\) ocurre libremente en \(\varphi\) a partir de \(i\) sii \(v\neq w\) y \(v\) ocurre libremente en \(\varphi_{1}\) a partir de \(i-\left\vert Qw\right\vert\)

Dados \(v\in Var\), \(\varphi\in F^{\tau}\) y \(i\in\{1,...,\left\vert \varphi\right\vert \}\), diremos que \("v\) ocurre acotadamente en \(\varphi\) a partir de \(i"\) cuando \(v\) ocurre en \(\varphi\) a partir de \(i\) y \(v\) no ocurre libremente en \(\varphi\) a partir de \(i\).

Veamos algunos ejemplos. Sea \(\tau=(\{\mathrm{uno},\mathrm{doli}\},\{\mathrm{MAS},\mathrm{P}\},\{\mathrm{Her}\},a)\), con \(a\) dado por \(a(\mathrm{MAS})=4\), \(a(\mathrm{P})=1\) y \(a(\mathrm{Her})=3\). Entonces:

1. adhocprefix-adhocsufix \(\mathsf{X}\mathbf{9}\) ocurre libremente en \(\mathrm{Her}(\mathrm{doli},\mathrm{doli},\mathsf{X}\mathbf{9})\) a partir de \(15\)

2. adhocprefix-adhocsufix \(\mathsf{X}\mathbf{9}\) ocurre acotadamente en \(\exists\mathsf{X}\mathbf{9}\mathrm{Her}(\mathrm{doli},\mathrm{doli},\mathsf{X}\mathbf{9})\) a partir de \(2\) y de \(18\)

3. adhocprefix-adhocsufix \(\mathsf{X}\mathbf{2}\) ocurre libremente en \((\exists\mathsf{X}\mathbf{2}\mathrm{Her}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{7},\mathrm{uno})\rightarrow\mathrm{Her}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{7},\mathrm{uno}))\) a partir de \(16\) y acotadamente a partir de \(3\) y \(7\).

4. adhocprefix-adhocsufix Sea \(\varphi=((\mathsf{X}\mathbf{1}\equiv\mathsf{X}\mathbf{2})\wedge\exists\mathsf{X}\mathbf{2}\mathrm{Her}(\mathrm{P}(\mathrm{doli}),\mathrm{doli},\mathsf{X}\mathbf{2}))\). La variable \(\mathsf{X}\mathbf{2}\) ocurre libremente en \(\varphi\) a partir de \(6\) y ocurre acotadamente en \(\varphi\) a partir de \(11\) y de \(30\).

Dada una fórmula \(\varphi\), sea \[Li(\varphi)=\{v\in Var:\text{hay un }i\text{ tal que }v\text{ ocurre libremente en }\varphi\text{ a partir de }i\}\text{.}\] Los elementos de \(Li(\varphi)\) serán llamados variables libres de \(\varphi\). Por ejemplo, si \(\varphi\) es la fórmula \[(\exists\mathsf{X}\mathbf{7}(\mathsf{X}\mathbf{7}\equiv\mathsf{X}\mathbf{6})\rightarrow((\mathsf{X}\mathbf{1}\equiv\mathsf{X}\mathbf{2})\wedge\exists\mathsf{X}\mathbf{2}\mathrm{Her}(\mathrm{doli},\mathrm{doli},\mathsf{X}\mathbf{2})))\] tenemos que \(Li(\varphi)=\{\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{6}\}\) (justifique). También si \[\varphi=(\exists\mathsf{X}\mathbf{2}\mathrm{Her}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{7},\mathrm{uno})\rightarrow\mathrm{Her}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{7},\mathrm{uno}))\] entonces \(Li(\varphi)=\{\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{7}\}\).

Una sentencia será una fórmula \(\varphi\) tal que \(Li(\varphi)=\emptyset\). Usaremos \(S^{\tau}\) para denotar el conjunto de las sentencias de tipo \(\tau\).

Proof. (a) y (b) son triviales de las definiciones y dejadas al lector

(d) 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\) o \(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)\)

Supongamos ahora que \(v\in Li(\varphi)\cup Li(\psi)\). S.p.d.g. 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 nótese que esto nos dice por definición 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))\).

(c) es similar a (d)

(e) 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 definición tenemos que \(v\neq x_{j}\) 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 definición 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 definición 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)\).  

7.8.4 Modelo matemático de las fórmulas elementales de tipo \(\tau\)

Si \(\tau=(\mathcal{C},\mathcal{F},\mathcal{R},a)\) es un tipo, diremos que un tipo \(\tau^{\prime}\) es una extensión de \(\tau\) por nombres de constante si \(\tau^{\prime}\) es de la forma \((\mathcal{C}^{\prime},\mathcal{F},\mathcal{R},a)\) con \(\mathcal{C}^{\prime}\) tal que \(\mathcal{C}\subseteq\mathcal{C}^{\prime}\).

Hemos definido las fórmulas de tipo \(\tau\) con la intención de dar un modelo matemático del concepto de fórmula elemental de tipo \(\tau\) pero deberíamos notar que en las fórmulas de tipo \(\tau\) no hay nombres de elementos fijos por lo cual dichas fórmulas son un modelo matemático solo de ciertas fórmulas elementales de tipo \(\tau\), a saber aquellas en las cuales no hay nombres de elementos fijos (llamadas puras). Recordemos que estos nombres se usaban en las pruebas elementales para denotar elementos fijos (a veces arbitrarios y otras veces que cumplían alguna propiedad).

Cuando un matemático realiza una prueba elemental en una teoría elemental \((\Sigma,\tau)\) comienza la misma imaginando una estructura de tipo \(\tau\) de la cual lo único que sabe es que cumple las sentencias de \(\Sigma\). Luego cuando fija un elemento y le pone nombre, digamos \(b\), podemos pensar que expandió su estructura imaginaria a una de tipo \((\mathcal{C}\cup\{b\},\mathcal{F},\mathcal{R},a)\) y continua su razonamiento. Esto lo puede hacer muchas veces a lo largo de una prueba por lo cual su estructura imaginaria va cambiando de tipo. Esta mecánica de prueba del matemático nos deja ver que es natural modelizar las fórmulas elementales de tipo \(\tau\) con fórmulas de tipo \(\tau_{1}\), donde \(\tau_{1}\) es alguna extensión de \(\tau\) por nombres de constante.