En esta seccion daremos un modelo matematico de los conceptos de termino elemental de tipo \(\tau\) y formula elemental de tipo \(\tau\). Esto corresponde al punto (1) del Programa de Logica Matematica.
Las variables usadas en las formulas 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\)-esimo 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 notacion decimal, el ultimo numeral por su correspondiente numeral bold y los otros por sus correspondientes italicos. Para dar un ultimo ejemplo, el elemento trecientos cuarenta y unesimo 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 razon por la cual usamos numerales italicos y bold es que a los numerales normales los usamos habitualmente en los tipos y sera conveniente que entonces no ocurran en las variables. Ademas tomamos el ultimo simbolo 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\)-esimo elemento de \(Var\), para cada \(i\in\mathbf{N}\).
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}\] Sea \[T^{\tau}=\bigcup_{k\geq0}T_{k}^{\tau}\] Los elementos de \(T^{\tau}\) seran llamados terminos de tipo \(\tau\). Un termino \(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}\}\] Algunos ejemplos:
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
Las palabras \(\mathrm{uno}\), \(\mathrm{doli}\) y \(\mathsf{X}\mathit{15666}\mathbf{9}\) son terminos de tipo \(\tau\) ya que pertenecen a \(T_{0}^{\tau}\)
\(\mathrm{MAS}(\mathrm{uno},\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5})\) y \(\mathrm{P}(\mathrm{uno})\ \)son terminos de tipo \(\tau\) ya que pertenecen a \(T_{1}^{\tau}\) (por que?)
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 terminos de tipo \(\tau\) ya que pertenecen a \(T_{2}^{\tau}\)
\(\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 termino ya que pertenece a \(T_{3}^{\tau}\)
\(\mathrm{uno}\), \(\mathrm{doli}\), \(\mathrm{P}(\mathrm{uno})\) y \(\mathrm{MAS}(\mathrm{uno},\mathrm{doli},\mathrm{doli},\mathrm{doli})\) son terminos cerrados de tipo \(\tau\)
Lo que debe quedar claro es que como objetos matematicos los terminos son meras palabras, por ejemplo \(\mathrm{MAS}(\mathrm{uno},\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5})\) es una palabra (de longitud 20)
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 terminos de tipo \(\tau\). Tambien \(\mathrm{\uparrow}(+(\mathrm{\uparrow}(0),\times(0,1,0)))\) es un termino cerrado de tipo \(\tau\)
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 terminos de tipo \(\tau\). No hay terminos cerrados de tipo \(\tau\). Cabe destacar que \(\mathsf{X}\mathbf{2\ }\mathsf{s\ X}\mathbf{3}\) no es un termino de tipo \(\tau\) aunque esto no es trivial de la definicion de termino y requiere de una demostracion.
Observacion importante: Notar que los terminos de tipo \(\tau\) son un modelo matematico de los terminos elementales puros de tipo \(\tau\), es decir aquellos en los cuales no ocurren nombres de elementos fijos. Medite...
El siguiente lema es la herramienta basica para probar propiedades de los terminos.
7.2 ([Menu para terminos). Supongamos \(t\in T_{k}^{\tau}\), con \(k\geq1\). Entonces se da alguna de las siguientes:
adhocprefix(a)adhocsufix \(t\in Var\cup\mathcal{C}\)
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}\).
Proof. Por induccion en \(k\).
CASO \(k=1\): Es directo ya que por definicion \[T_{1}^{\tau}=Var\cup\mathcal{C}\cup\{f(t_{1},...,t_{n}):f\in\mathcal{F}_{n}\text{, }n\geq1\text{ y }t_{1},...,t_{n}\in T_{0}^{\tau}\}.\]
CASO \(k\Rightarrow k+1\): Sea \(t\in T_{k+1}^{\tau}\). Por definicion de \(T_{k+1}^{\tau}\) tenemos que \(t\in T_{k}^{\tau}\) o \(t=f(t_{1},...,t_{n})\) con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T_{k}^{\tau}\). Si se da que \(t\in T_{k}^{\tau}\), entonces podemos aplicar hipotesis inductiva y usar que \(T_{k-1}^{\tau}\subseteq T_{k}^{\tau}\). Esto completa el caso.
Algunos ejemplos de propiedades de los terminos las cuales se pueden probar facilmente usando el lema anterior son
adhocprefix-adhocsufix Si \(t\in T^{\tau}\) es tal que en \(t\) ocurre el simbolo \()\), entonces \(t=f(t_{1},...,t_{n})\) con \(f\in\mathcal{F}_{n}\), \(n\geq1\) y \(t_{1},...,t_{n}\in T^{\tau}\).
adhocprefix-adhocsufix Ningun termino comienza con un simbolo del alfabeto \(\{\mathit{0},\mathit{1},...,\mathit{9}\}\)
adhocprefix-adhocsufix Si \(t\in T^{\tau}\) comienza con \(\mathsf{X}\) entonces \(t\in Var\)
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}=\) \()\)
adhocprefix-adhocsufix Si \(t\in T^{\tau}\), entonces \(\left\vert t\right\vert _{(}=\left\vert t\right\vert _{)}\).
Una posible forma de probar que una palabra dada no es un termino es encontrar una propiedad que posean todos los terminos 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 termino ya que \(\left\vert \alpha\right\vert _{(}\neq\left\vert \alpha\right\vert _{)}\).
Definamos conjuntos \(Bal_{k}\), con \(k\geq1\) de la siguiente manera: \[\begin{aligned} Bal_{1} & =\{()\}\\ Bal_{k+1} & =Bal_{k}\cup\{(b_{1}...b_{n}):b_{1},...,b_{n}\in Bal_{k},n\geq1\}. \end{aligned}\] Sea \[Bal=\bigcup_{k\geq1}Bal_{k}\] 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).
7.3. Sea \(b\in Bal\). Se tiene:
adhocprefix(1)adhocsufix \(\left\vert b\right\vert _{(}-\left\vert b\right\vert _{)}=0\)
adhocprefix(2)adhocsufix Si \(x\) es tramo inicial propio de \(b\), entonces \(\left\vert x\right\vert _{(}-\left\vert x\right\vert _{)}>0\)
adhocprefix(3)adhocsufix Si \(x\) es tramo final propio de \(b\), entonces \(\left\vert x\right\vert _{(}-\left\vert x\right\vert _{)}<0\)
Proof. Probaremos por induccion en \(k\), que valen (1), (2) y (3) para cada \(b\in Bal_{k}\). El caso \(k=1\) es trivial. Supongamos \(b\in Bal_{k+1}\). Si \(b\in Bal_{k}\), se aplica directamente HI. Supongamos entonces que \(b=(b_{1}...b_{n})\), con \(b_{1},...,b_{n}\in Bal_{k}\), \(n\geq1\). Por HI, \(b_{1},...,b_{n}\) cumplen (1) por lo cual \(b\) cumple (1). Veamos que \(b\) cumple (2). Sea \(x\) un tramo inicial propio de \(b\). Notese que \(x\) es de la forma \(x=(b_{1}...b_{i}x_{1}\) con \(0\leq i\leq n-1\) y \(x_{1}\) un tramo inicial de \(b_{i+1}\) (en el caso \(i=0\) interpretamos \(b_{1}...b_{i}=\varepsilon)\). Pero entonces ya que \[\left\vert x\right\vert _{(}-\left\vert x\right\vert _{)}=1+\left(\sum_{j=1}^{i}\left\vert b_{j}\right\vert _{(}-\left\vert b_{j}\right\vert _{)}\right)+\left\vert x_{1}\right\vert _{(}-\left\vert x_{1}\right\vert _{)}\] tenemos que por HI, se da que \(\left\vert x\right\vert _{(}-\left\vert x\right\vert _{)}>0\). En forma analoga se puede ver que \(b\) cumple (3).
Dado un alfabeto \(\Sigma\) tal que \((\) y \()\) pertenecen a \(\Sigma\), definamos \(del:\Sigma^{\ast}\rightarrow\Sigma^{\ast}\), de la siguiente manera \[\begin{aligned} del(\varepsilon) & =\varepsilon\\ del(\alpha a) & =del(\alpha)a\text{, si }a\in\{(,)\}\\ del(\alpha a) & =del(\alpha)\text{, si }a\in\Sigma-\{(,)\} \end{aligned}\]
7.4. \(del(xy)=del(x)del(y)\), para todo \(x,y\in\Sigma^{\ast}\)
7.5. Supongamos que \(\Sigma\) es tal que \(T^{\tau}\subseteq\Sigma^{\ast}\). Entonces \(del(t)\in Bal\), para cada \(t\in T^{\tau}-(Var\cup\mathcal{C})\)
Notese que en la definicion 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 mordizquean. Por ejemplo si \(\tau=(\{\mathrm{uno}\),\(\mathrm{noli}\},\emptyset,\emptyset,\emptyset)\), es facil ver que \(\tau\) es un tipo y que \(\mathrm{uno}\) y \(\mathrm{noli}\) se mordizquean. El lema siguiente nos dice que este es el unico caso de mordizqueo de terminos.
7.6 ([Mordizqueo de Terminos). Sean \(s,t\in T^{\tau}\) y supongamos que hay palabras \(x,y,z\), con \(y\neq\varepsilon\) tales que \(s=xy\) y \(t=yz\) . Entonces \(x=z=\varepsilon\) o \(s,t\in\mathcal{C}\). En particular si un termino es tramo inicial o final de otro termino, entonces dichos terminos son iguales.
Proof. Supongamos \(s\in\mathcal{C}\). Ya que \(y\neq\varepsilon\) tenemos que \(t\) debe comenzar con un simbolo que ocurre en un nombre de cte, lo cual dice que \(t\) no puede ser ni una variable ni de la forma \(g(t_{1},...,t_{m})\), es decir \(t\in\mathcal{C}\). Supongamos \(s\in Var\). Si \(x\neq\varepsilon\) tenemos que \(t\) debe comenzar con alguno de los siguientes simbolos \[\mathit{0}\;\mathit{1\;}...\;\mathit{9}\;\mathbf{0}\;\mathbf{1}\ ...\;\mathbf{9}\] lo cual es absurdo. O sea que \(x=\varepsilon\) y por lo tanto \(t\) debe comenzar con \(\mathsf{X}\). Pero esto dice que \(t\in Var\) de lo que sigue facilmente que \(z=\varepsilon\). Supongamos entonces que \(s\) es de la forma \(f(s_{1},...,s_{n})\). Ya que \()\) debe ocurrir en \(t\), tenemos que \(t\) es de la forma \(g(t_{1},...,t_{m})\). O sea que \(del(s),del(t)\in Bal\). Ya que \()\) ocurre en \(y\), \(del(y)\neq\varepsilon\). Tenemos tambien que \[\begin{aligned} del(s) & =del(x)del(y)\\ del(t) & =del(y)del(z) \end{aligned}\] La primera igualdad, por (1) y (3) del Lema 7.3, nos dice que \[\left\vert del(y)\right\vert _{(}-\left\vert del(y)\right\vert _{)}\leq0,\] y la segunda que \[\left\vert del(y)\right\vert _{(}-\left\vert del(y)\right\vert _{)}\geq0,\] por lo cual \[\left\vert del(y)\right\vert _{(}-\left\vert del(y)\right\vert _{)}=0\] Pero entonces (3) del Lema 7.3 nos dice que \(del(y)\) no puede ser tramo final propio de \(del(s)\), por lo cual debe suceder que \(del(y)=del(s)\), ya que \(del(y)\neq\varepsilon\). Claramente entonces obtenemos que \(del(x)=\varepsilon\). Similarmente se puede ver que \(del(z)=\varepsilon\). Ya que que \(t\) termina con \()\) tenemos que \(z=\varepsilon\). O sea que \(f(s_{1},...,s_{n})=xg(t_{1},...,t_{m})\) con \(del(x)=\varepsilon\), de lo que se saca que \(f=xg\) ya que \((\) no ocurre en \(x\). De la definicion de tipo se desprende que \(x=\varepsilon\).
7.1. Dado \(t\in T^{\tau}\) se da una de las siguientes:
adhocprefix(1)adhocsufix \(t\in Var\cup\mathcal{C}\)
adhocprefix(2)adhocsufix Hay unicos \(n\geq1\),\(\;f\in\mathcal{F}_{n}\),\(\;t_{1},...,t_{n}\in T^{\tau}\) tales que \(t=f(t_{1},...,t_{n})\).
Proof. En virtud del Lema 7.2 solo nos 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}\). Notese que \(f=g\). O sea que \(n=m=a(f)\). Notese 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 debera suceder \(t_{2}=s_{2},...,t_{n}=s_{n}\).
El teorema anterior es importante ya que nos permite definir recursivamente funciones con dominio contenido en \(T^{\tau}\). Por ejemplo podemos definir una funcion \(F:T^{\tau}\rightarrow T^{\tau}\), de la siguiente manera:
adhocprefix-adhocsufix \(F(c)=c\), para cada \(c\in\mathcal{C}\)
adhocprefix-adhocsufix \(F(v)=v\), para cada \(v\in Var\)
adhocprefix-adhocsufix \(F(f(t_{1},...,t_{n}))=f(F(t_{1}),...,F(t_{n}))\), si \(f\in\mathcal{F}_{n}\), con \(n\neq2\)
adhocprefix-adhocsufix \(F(f(t_{1},t_{2}))=f(t_{2},t_{1})\), si \(f\in\mathcal{F}_{2}.\)
Notese que si la unicidad de la lectura no fuera cierta, entonces las ecuaciones anteriores no estarian definiendo en forma correcta una funcion ya que el valor de la imagen de un termino \(t\) estaria dependiendo de cual descomposicion tomemos para \(t\).
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 de 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 de que si comensamos a leer desde el lugar \(i\)-esimo de \(\beta\) en adelante, leeremos la palabra \(\alpha\) completa y luego posiblemente seguiran otros simbolos.
Notese que una palabra \(\alpha\) puede ocurrir en \(\beta\), a partir de \(i\), y tambien a partir de \(j\), con \(i\neq j\). En virtud de esto, hablaremos de las distintas ocurrencias de \(\alpha\) en \(\beta\). Por ejemplo hay dos ocurrencias de la palabra \(aba\) en la palabra \[cccccccabaccccabaccccc\] y tambien hay dos ocurrencias de la palabra \(aba\) en la palabra \[cccccccababacccccccccc\] En el primer caso diremos que dichas ocurrencias de \(aba\) son disjuntas ya que ocupan espacios disjuntos dentro de la palabra. En cambio en el segundo caso puede apreciarse que las dos ocurrencias se superponen en una posicion. A veces diremos que una ocurrencia esta contenida o sucede dentro de otra. Por ejemplo la segunda ocurrencia de \(ab\) en \(babbbfabcccfabccc\) esta contenida en la primer ocurrencia de \(fabc\) en \(babbbfabcccfabccc\).
No definiremos en forma matematica precisa el concepto de ocurrencia pero el lector no tendra problemas en comprenderlo y manejarlo en forma correcta.
Tambien haremos reemplazos de ocurrencias por palabras. Por ejemplo el resultado de reemplazar la primer ocurrencia de \(abb\) en \(ccabbgfgabbgg\) por \(oolala\) es la palabra \(ccoolalagfgabbgg\). Cuando todas las ocurrencias de una palabra \(\alpha\) en una palabra \(\beta\) sean disjuntas entre si, podemos hablar del resultado de reeplazar simultaneamente cada ocurrencia de \(\alpha\) en \(\beta\) por \(\gamma\). Por ejemplo si tenemos \[\begin{aligned} \alpha & =yet\\ \beta & =ghsyetcjjjyetbcpyeteabc\\ \gamma & =\%\% \end{aligned}\] entonces \(ghs\%\%cjjj\%\%bcp\%\%eabc\) es el resultado de reemplazar simultaneamente cada ocurrencia de \(\alpha\) en \(\beta\) por \(\gamma\). Es importante notar que los reemplazos se hacen simultaneamente y no secuencialmente (i.e. reemplazando la primer ocurrencia de \(\alpha\) por \(\gamma\) y luego al resultado reemplazarle la primer ocurrencia de \(\alpha\) por \(\gamma\) y asi sucesivamente). Obviamente el reemplazo secuencial puede dar un resultado distinto al simultaneo (que es el que usaremos en general) e incluso puede suceder que en el reemplazo secuencial el proceso se pueda iterar indefinidamente. Dejamos al lector armar ejemplos de estas cituaciones.
Tambien se pueden hacer reemplazos simultaneos de distintas palabras en una palabra dada. Supongamos tenemos palabras \(\alpha_{1},...,\alpha_{n},\beta\) tales que
adhocprefix-adhocsufix \(\alpha_{i}\neq\alpha_{j}\), para \(i\neq j\)
adhocprefix-adhocsufix Para cada \(i\), las distintas ocurrencias de \(\alpha_{i}\) en \(\beta\) son disjuntas
adhocprefix-adhocsufix Si \(\alpha_{i}\) ocurre en \(\beta\) y \(\alpha_{j}\) ocurre en \(\beta\), con \(i\neq j\), entonces dichas ocurrencias son disjuntas
entonces dadas palabras cualesquiera \(\gamma_{1},...,\gamma_{n}\) hablaremos del resultado de reemplazar simultaneamente:
adhocprefix-adhocsufix cada ocurrencia de \(\alpha_{1}\) en \(\beta\), por \(\gamma_{1}\)
adhocprefix-adhocsufix cada ocurrencia de \(\alpha_{2}\) en \(\beta\), por \(\gamma_{2}\)
adhocprefixadhocsufix \(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \vdots\)
adhocprefix-adhocsufix cada ocurrencia de \(\alpha_{n}\) en \(\beta\), por \(\gamma_{n}\)
Por ejemplo si tomamos \[\begin{aligned} \alpha_{1} & =gh\\ \alpha_{2} & =yet\\ \alpha_{3} & =ana\\ \beta & =ghbbbyetbbgh\%\%ana\#\#ana!!!ana\\ \gamma_{1} & =AA\\ \gamma_{2} & =BBBB\\ \gamma_{3} & =CCC \end{aligned}\] entonces \(AAbbbBBBBbbAA\%\%CCC\#\#CCC!!!CCC\) es el resultado de reemplazar simultaneamente:
adhocprefix-adhocsufix cada ocurrencia de \(\alpha_{1}\) en \(\beta\), por \(\gamma_{1}\)
adhocprefix-adhocsufix cada ocurrencia de \(\alpha_{2}\) en \(\beta\), por \(\gamma_{2}\)
adhocprefix-adhocsufix cada ocurrencia de \(\alpha_{3}\) en \(\beta\), por \(\gamma_{3}\)
Sean \(s,t\in T^{\tau}\). Diremos que \(s\) es subtermino (propio) de \(t\) si (no es igual a \(t\) y) \(s\) es subpalabra de \(t\). A continuacion veremos de que manera ocurren los subterminos de un termino.
7.7 ([Ocurrencias de terminos en terminos). Sean \(r,s,t\in T^{\tau}\).
adhocprefix(a)adhocsufix Si \(s\neq t=f(t_{1},...,t_{n})\) y \(s\) ocurre en \(t\), entonces dicha ocurrencia sucede dentro de algun \(t_{j}\), \(j=1,...,n\).
adhocprefix(b)adhocsufix Si \(r,s\) ocurren en \(t\), entonces dichas ocurrencias son disjuntas o una ocurre dentro de otra. En particular, las distintas ocurrencias de \(r\) en \(t\) son disjuntas.
adhocprefix(c)adhocsufix Si \(t^{\prime}\) es el resultado de reemplazar una ocurrencia de \(s\) en \(t\) por \(r\), entonces \(t^{\prime}\in T^{\tau}\).
Proof. (a) Supongamos la ocurrencia de \(s\) comienza en algun \(t_{j}\). Entonces el Lema 7.6 nos conduce a que dicha ocurrencia debera 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}\). Notese que \(i\neq1\) ya que en caso contrario \(s\) seria un tramo inicial propio de \(t\). Pero entonces \(g\) debe ser un tramo final propio de \(f\), lo cual es absurdo. Ya que \(s\) no puede comenzar con parentesis o coma, hemos contemplado todos los posibles casos de comienzo de la ocurrencia de \(s\) en \(t\).
(b) y (c) pueden probarse por induccion, usando (a).
Nota: Es importante notar que si bien no hemos definido en forma presisa el concepto de ocurrencia o de reemplazo de ocurrencias, la prueba del lema anterior es rigurosa en el sentido de que solo usa propiedades del concepto de ocurrencia y reemplazo de ocurrencias las cuales deberan ser comunes a cualquier definicion o formulacion matematica que se hiciera de aquellos conceptos. En este caso, es posible dar una defincion presisa y satisfactoria de dichos conceptos aunque para otros conceptos tales como el de prueba absoluta de consistencia, aun no se ha encontrado una formulacion matematica adecuada.
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}\] seran llamadas formulas atomicas de tipo \(\tau\). 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
adhocprefix-adhocsufix \((\mathrm{uno}\equiv\mathrm{doli})\)
adhocprefix-adhocsufix \((\mathsf{X}\mathit{15666}\mathbf{9}\equiv\mathrm{doli})\)
adhocprefix-adhocsufix \(\mathrm{Her}(\mathrm{uno},\mathsf{X}\mathbf{4},\mathrm{doli})\)
adhocprefix-adhocsufix \((\mathrm{MAS}(\mathrm{uno},\mathrm{doli},\mathsf{X}\mathit{1}\mathbf{9},\mathsf{X}\mathbf{5})\equiv\mathrm{uno})\)
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 formulas atomicas 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{formulas atomicas 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}\] Sea \[F^{\tau}=\bigcup_{k\geq0}F_{k}^{\tau}\] Los elementos de \(F^{\tau}\) seran llamados formulas de tipo \(\tau\).
Algunos ejemplos:
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
\(\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}))\)
\(\exists\mathsf{X}\mathbf{9}\mathrm{Her}(\mathrm{doli},\mathrm{doli},\mathsf{X}\mathbf{9})\)
\(\exists\mathsf{X}\mathbf{9}\lnot(\mathrm{uno}\equiv\mathrm{doli})\)
\(\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}))\)
\(\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 formulas de tipo \(\tau\)
adhocprefix(E2)adhocsufix Sea \(\tau=(\{0,1\},\{\mathsf{s},\mathsf{i}\},\{\leq\},\{(\mathsf{s},2),(\mathsf{i},2),(\leq,2)\})\) el tipo de los reticulados cuaterna. Entonces
\(\mathrm{\leq}(1,0)\)
\(\mathrm{\leq}(\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2})\)
\(\lnot(\mathsf{s}(\mathsf{X}\mathbf{2},\mathsf{X}\mathbf{1})\equiv\mathsf{X}\mathbf{2}))\)
\(\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}))\)
\(((\mathsf{i}(\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2})\equiv0)\wedge(\mathsf{s}(\mathsf{X}\mathbf{1},\mathsf{X}\mathbf{2})\equiv1))\)
\(\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 formulas de tipo \(\tau\). Cabe destacar que \((\mathsf{X}\mathbf{1}\leq\mathsf{X}\mathbf{2})\) no es una formula de tipo \(\tau\) aunque, como veremos en los ejercicios esto no es trivial de la definicion de formula y requiere de una demostracion.
Observacion importante: Notar que las formulas de tipo \(\tau\) son un modelo matematico de las formulas elementales puras de tipo \(\tau\) , es decir aquellas en las cuales no ocurren nombres de elementos fijos. Medite...
El siguiente lema es la herramienta basica que usaremos para probar propiedades acerca de los elementos de \(F^{\tau}\).
7.8 ([Menu para formulas). Supongamos \(\varphi\in F_{k}^{\tau}\), con \(k\geq1\). Entonces \(\varphi\) es de alguna de las siguientes formas
\(\varphi=(t\equiv s),\) con \(t,s\in T^{\tau}\).
\(\varphi=r(t_{1},...,t_{n}),\) con \(r\in\mathcal{R}_{n}\), \(t_{1},...,t_{n}\in T^{\tau}\)
\(\varphi=(\varphi_{1}\eta\varphi_{2}),\) con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\},\;\varphi_{1},\varphi_{2}\in F_{k-1}^{\tau}\)
\(\varphi=\lnot\varphi_{1},\) con \(\varphi_{1}\in F_{k-1}^{\tau}\)
\(\varphi=Qv\varphi_{1},\) con \(Q\in\{\forall,\exists\},\;v\in Var\) y \(\varphi_{1}\in F_{k-1}^{\tau}.\)
Proof. Induccion en \(k\).
Tal como para el caso de terminos veremos que las formulas tambien tienen su unicidad de lectura.
7.9. Sea \(\tau\) un tipo.
adhocprefix(a)adhocsufix Supongamos que \(\Sigma\) es tal que \(F^{\tau}\subseteq\Sigma^{\ast}\). Entonces \(del(\varphi)\in Bal\), para cada \(\varphi\in F^{\tau}\).
adhocprefix(b)adhocsufix Sea \(\varphi\in F_{k}^{\tau}\), con \(k\geq0\). Existen \(x\in(\{\lnot\}\cup\{Qv:Q\in\{\forall,\exists\}\) y \(v\in Var\})^{\ast}\) y \(\varphi_{1}\in F^{\tau}\) tales que \(\varphi=x\varphi_{1}\) y \(\varphi_{1}\) es de la forma \((\psi_{1}\eta\psi_{2})\) o atomica. En particular toda formula termina con el simbolo \()\).
Proof. (b) Induccion en \(k\). El caso \(k=0\) es trivial. Supongamos (b) vale para cada \(\varphi\in F_{k}^{\tau}\) y sea \(\varphi\in F_{k+1}^{\tau}\). Hay varios casos de los cuales haremos solo dos
CASO \(\varphi=(\psi_{1}\eta\psi_{2})\), con \(\psi_{1},\psi_{2}\in F_{k}^{\tau}\) y \(\eta\in\{\vee,\wedge,\rightarrow,\leftrightarrow\}\).
Podemos tomar \(x=\varepsilon\) y \(\varphi_{1}=\varphi\).
CASO \(\varphi=Qx_{i}\psi\), con \(\psi\in F_{k}^{\tau}\), \(i\geq1\) y \(Q\in\{\forall,\exists\}\).
Por HI hay \(\bar{x}\in(\{\lnot\}\cup\{Qv:Q\in\{\forall,\exists\}\) y \(v\in Var\})^{\ast}\) y \(\psi_{1}\in F^{\tau}\) tales que \(\psi=\bar{x}\psi_{1}\) y \(\psi_{1}\) es de la forma \((\gamma_{1}\eta\gamma_{2})\) o atomica. Entonces es claro que \(x=Qx_{i}\bar{x}\) y \(\varphi_{1}=\psi_{1}\) cumplen (b).
7.10. Ninguna formula es tramo final propio de una formula atomica, es decir, si \(\varphi=x\psi\), con \(\varphi\in F_{0}^{\tau}\) y \(\psi\in F^{\tau}\), entonces \(x=\varepsilon\).
Proof. Si \(\varphi\) es de la forma \((t\equiv s)\), entonces \(\left\vert del(y)\right\vert _{(}-\left\vert del(y)\right\vert _{)}<0\) para cada tramo final propio \(y\) de \(\varphi\), lo cual termina el caso ya que \(del(\psi)\) es balanceada. Supongamos entonces \(\varphi=r(t_{1},...,t_{n})\). Notese que \(\psi\) no puede ser tramo final de \(t_{1},...,t_{n})\) ya que \(del(\psi)\) es balanceada y \(\left\vert del(y)\right\vert _{(}-\left\vert del(y)\right\vert _{)}<0\) para cada tramo final \(y\) de \(t_{1},...,t_{n})\). Es decir que \(\psi=y(t_{1},...,t_{n})\), para algun tramo final \(y\) de \(r\). Ya que en \(\psi\) no ocurren cuantificadores ni nexos ni el simbolo \(\equiv\) el Lema 7.8 nos dice \(\psi=\tilde{r}(s_{1},...,s_{m})\), con \(\tilde{r}\in\mathcal{R}_{m}\), \(m\geq1\) y \(s_{1},...,s_{m}\in T^{\tau}\). Ahora es facil usando un argumento paresido al usado en la prueba del Teorema 7.1 concluir que \(m=n\), \(s_{i}=t_{i}\), \(i=1,...,n\) y \(\tilde{r}\) es tramo final de \(r\). Por (3) de la definicion de tipo tenemos que \(\tilde{r}=r\) lo cual nos dice que \(\varphi=\psi\) y \(x=\varepsilon\)
7.11. Si \(\varphi=x\psi\), con \(\varphi,\psi\in F^{\tau}\) y \(x\) sin parentesis, entonces \(x\in(\{\lnot\}\cup\{Qv:Q\in\{\forall,\exists\}\) y \(v\in Var\})^{\ast}\)
Proof. Por induccion en el \(k\) tal que \(\varphi\in F_{k}^{\tau}\). El caso \(k=0\) es probado en el lema anterior. Asumamos que el resultado vale cuando \(\varphi\in F_{k}^{\tau}\) y veamos que vale cuando \(\varphi\in F_{k+1}^{\tau}\). Mas aun supongamos \(\varphi\in F_{k+1}^{\tau}-F_{k}^{\tau}\). Primero haremos el caso en que \(\varphi=Qv\varphi_{1},\) con \(Q\in\{\forall,\exists\},\;v\in Var\) y \(\varphi_{1}\in F_{k}^{\tau}\). Supongamos \(x\neq\varepsilon\). Ya que \(\psi\) no comienza con simbolos de \(v\), tenemos que \(\psi\) debe ser tramo final de \(\varphi_{1}\) lo cual nos dice que hay una palabra \(x_{1}\) tal que \(x=Qvx_{1}\) y \(\varphi_{1}=x_{1}\psi\). Por HI tenemos que \(x_{1}\in(\{\lnot\}\cup\{Qv:Q\in\{\forall,\exists\}\) y \(v\in Var\})^{\ast}\) con lo cual \(x\in(\{\lnot\}\cup\{Qv:Q\in\{\forall,\exists\}\) y \(v\in Var\})^{\ast}\). El caso en el que \(\varphi=\lnot\varphi_{1}\) con \(\varphi_{1}\in F_{k}^{\tau}\), es similar. Note que no hay mas casos posibles ya que \(\varphi\) no puede comenzar con \((\) porque en \(x\) no ocurren parentesis por hipotesis
7.1 ([Mordisqueo de formulas). Si \(\varphi,\psi\in F^{\tau}\) y \(x,y,z\) son tales que \(\varphi=xy,\) \(\psi=yz\) y \(y\neq\varepsilon,\) entonces \(z=\varepsilon\) y \(x\in(\{\lnot\}\cup\{Qv:Q\in\{\forall,\exists\}\) y \(v\in Var\})^{\ast}\). En particular ningun tramo inicial propio de una formula es una formula.
Proof. Ya que \(\varphi\) termina con \()\) tenemos que \(del(y)\neq\varepsilon.\) Por un lema anterior tenemos que \(del(\varphi),del(\psi)\in Bal\). Ademas \[\begin{aligned} del(\varphi) & =del(x)del(y)\\ del(\psi) & =del(y)del(z) \end{aligned}\] La primera igualdad, por (1) y (3) del Lema 7.3, nos dice que \[\left\vert del(y)\right\vert _{(}-\left\vert del(y)\right\vert _{)}\leq0,\] y la segunda que \[\left\vert del(y)\right\vert _{(}-\left\vert del(y)\right\vert _{)}\geq0,\] por lo cual \[\left\vert del(y)\right\vert _{(}-\left\vert del(y)\right\vert _{)}=0\] Pero entonces (3) del Lema 7.3 nos dice que \(del(y)\) no puede ser tramo final propio de \(del(\varphi)\), por lo cual debe suceder que \(del(y)=del(\varphi)\), ya que \(del(y)\neq\varepsilon\). Claramente entonces obtenemos que \(del(x)=\varepsilon\). Similarmente se puede ver que \(del(z)=\varepsilon\). Pero \(\psi\) termina con \()\) lo cual nos dice que \(z=\varepsilon\). Es decir que \(\varphi=x\psi\). Por el lema anterior tenemos que \(x\in(\{\lnot\}\cup\{Qv:Q\in\{\forall,\exists\}\) y \(v\in Var\})^{\ast}\)
7.2. Dada \(\varphi\in F^{\tau}\) se da una y solo una de las siguientes:
adhocprefix(1)adhocsufix \(\varphi=(t\equiv s),\) con \(t,s\in T^{\tau}\)
adhocprefix(2)adhocsufix \(\varphi=r(t_{1},...,t_{n}),\) con \(r\in\mathcal{R}_{n}\), \(t_{1},...,t_{n}\in T^{\tau}\)
adhocprefix(3)adhocsufix \(\varphi=(\varphi_{1}\eta\varphi_{2}),\) con \(\eta\in\{\wedge,\vee,\rightarrow,\leftrightarrow\},\;\varphi_{1},\varphi_{2}\in F^{\tau}\)
adhocprefix(4)adhocsufix \(\varphi=\lnot\varphi_{1},\) con \(\varphi_{1}\in F^{\tau}\)
adhocprefix(5)adhocsufix \(\varphi=Qv\varphi_{1},\) con \(Q\in\{\forall,\exists\},\;\varphi_{1}\in F^{\tau}\) y \(v\in Var.\)
Mas aun, en los puntos (1), (2), (3), (4) y (5) tales descomposiciones son unicas.
Proof. Si una formula \(\varphi\) satisface (1), entonces \(\varphi\) no puede contener simbolos del alfabeto \(\{\wedge,\vee,\rightarrow,\leftrightarrow\}\) lo cual garantiza que \(\varphi\) no puede satisfacer (3). Ademas \(\varphi\) no puede satisfacer (2) o (4) o (5) ya que \(\varphi\) comienza con \((\). En forma analoga se puede terminar de ver que las propiedades (1),...,(5) son excluyentes.
La unicidad en las descomposiciones de (4) y (5) es obvia. La de (3) se desprende facilmente del lema anterior y la de los puntos (1) y (2) del lema analogo para terminos.
Una formula \(\varphi\) sera llamada una subformula (propia) de una formula \(\psi\), cuando \(\varphi\) (sea no igual a \(\psi\) y) sea subpalabra de \(\psi\).
7.12 ([Ocurrencias de formulas en formulas). Sea \(\tau\) un tipo.
adhocprefix(a)adhocsufix Las formulas atomicas no tienen subformulas propias.
adhocprefix(b)adhocsufix Si \(\varphi\) ocurre propiamente en \((\psi\eta\gamma),\) entonces tal ocurrencia es en \(\psi\) o en \(\gamma.\)
adhocprefix(c)adhocsufix Si \(\varphi\) ocurre propiamente en \(\lnot\psi\), entonces tal ocurrencia es en \(\psi.\)
adhocprefix(d)adhocsufix Si \(\varphi\) ocurre propiamente en \(Qx_{k}\psi,\) entonces tal ocurrencia es en \(\psi.\)
adhocprefix(e)adhocsufix Si \(\varphi_{1},\varphi_{2}\) ocurren en \(\varphi,\) entonces dichas ocurrencias son disjuntas o una contiene a la otra.
adhocprefix(f)adhocsufix Si \(\lambda^{\prime}\) es el resultado de reemplazar alguna ocurrencia de \(\varphi\) en \(\lambda\) por \(\psi\), entonces \(\lambda^{\prime}\in F^{\tau}\).
Proof. Ejercicio.
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 de 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 de que si comensamos a leer desde el lugar \(i\)-esimo de \(\beta\), en adelante, entonces leeremos la palabra \(\alpha\) completa y luego posiblemente seguiran otros simbolos.
Definamos recursivamente la relacion \("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:
adhocprefix(1)adhocsufix Si \(\varphi\) es atomica, entonces \(v\) ocurre libremente en \(\varphi\) a partir de \(i\) sii \(v\) ocurre en \(\varphi\) a partir de \(i\)
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
adhocprefix(a)adhocsufix \(v\) ocurre libremente en \(\varphi_{1}\) a partir de \(i-1\)
adhocprefix(b)adhocsufix \(v\) ocurre libremente en \(\varphi_{2}\) a partir de \(i-\left\vert (\varphi_{1}\eta\right\vert\)
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\)
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\).
Algunos ejemplos:
adhocprefix-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\).
\(\mathsf{X}\mathbf{9}\) ocurre libremente en \(\mathrm{Her}(\mathrm{doli},\mathrm{doli},\mathsf{X}\mathbf{9})\) a partir de \(15\)
\(\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\)
\(\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\).
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 formula \(\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)\) seran llamados variables libres de \(\varphi\). Por ejemplo, si \(\varphi\) es la formula \[(\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). Tambien 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 sera una formula \(\varphi\) tal que \(Li(\varphi)=\emptyset\). Usaremos \(S^{\tau}\) para denotar el conjunto de las sentencias de tipo \(\tau\).
adhocprefix(a)adhocsufix \(Li((t\equiv s))=\{v\in Var:v\) ocurre en \(t\) o \(v\) ocurre en \(s\}.\)
adhocprefix(b)adhocsufix \(Li(r(t_{1},...,t_{n}))=\{v\in Var:v\) ocurre en algun \(t_{i}\}.\)
adhocprefix(c)adhocsufix \(Li(\lnot\varphi)=Li(\varphi)\)
adhocprefix(d)adhocsufix \(Li((\varphi\eta\psi))=Li(\varphi)\cup Li(\psi).\)
adhocprefix(e)adhocsufix \(Li(Qx_{j}\varphi)=Li(\varphi)-\{x_{j}\}.\)
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 definicion 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 definicion 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))\).
(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 definicion 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 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)\).
Si \(\tau=(\mathcal{C},\mathcal{F},\mathcal{R},a)\) es un tipo, diremos que \(\tau^{\prime}\) es una extension 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 formulas de tipo \(\tau\) con la intencion de dar un modelo matematico del concepto de formula elemental de tipo \(\tau\) pero deberiamos notar que en las formulas de tipo \(\tau\) no hay nombres de elementos fijos por lo cual dichas formulas son un modelo matematico solo de ciertas formulas 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 cumplian alguna propiedad).
Cuando un matematico realiza una prueba elemental en una teoria elemental \((\Sigma,\tau)\) comienza la misma imaginando una estructura de tipo \(\tau\) de la cual lo unico que sabe es que cumple las sentencias de \(\Sigma\). Luego cuando fija un elemento y le pone nombre, digamos \(b\), podemos pensar que expandio 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 mecanica de prueba del matematico nos deja ver que es natural modelizar las formulas elementales de tipo \(\tau\) con formulas de tipo \(\tau_{1}\), donde \(\tau_{1}\) es alguna extension de \(\tau\) por constantes.