Tablas semánticas y metalógica: (El caso de la lógica de segundo orden)

= CR´ ITICA,Revista Hispanoamericana de Filosof´ ıa Vol. XXXI, No. 93 (diciembre 1999): 21–47 TABLAS SEMÁNTICAS Y METALÓGICA (EL CASO DE LA LÓGICA DE SEGUNDO ORDEN)∗ ÁNGEL NEPOMUCENO FERNÁNDEZ Departamento de Filosofía y Lógica y Filosofía de la Ciencia Universidad de Sevilla 1. Introducción El método de Beth, conocido como el método de las tablas semánticas,1permite la demostración del teorema de satisfacción cuya formulación puede ser la siguiente: Si Γes un conjunto consistente de sentencias de primer orden, entonces Γes satisfacible en un universo finito o infinito numerable. A partir de este resultado, Henkin2demuestra la completitud de la lógica de predicados de primer orden y señala que el método tiene aplicación en el estudio de lógica de orden superior. Es decir, este resultado puede ser extendido a lógicas superiores, en particular a la de segundo orden, de modo que de éstas, aunque con ciertas restricciones, se puede probar alguna forma de completitud. ∗Subvencionado parcialmente por el Proyecto de Investigación PB96-1301-C05-03 del Ministerio Español de Educación y Cultura. 1También llamado de los árboles semánticos, por la presentación arb´ orea invertida que se puede hacer al construirlas. Usaremos ambos apelativos indistintamente. 2V´ ease Henkin (1949) y Henkin (1950). 21 Esquemáticamente, el método de la prueba de este teorema, para primer orden, consiste en la extensión de Γaun conjunto Γωtal que sea máximamente consistente —incluir una nueva fórmula lo haría inconsistente— y ejemplificado —si una fórmula del tipo ∃xϕ∈Γ, entonces ϕ(b/x)3∈Γ; contiene alguna instancia de la matriz para un parámetro (constante individual) del lenguaje. Se define además una estructura interpretativa para dicho conjunto extendido, cuyo universo de discurso es el de ciertas clases de equivalencia de parámetros, por lo que es finito o, a lo sumo, numerable; se prueba que dicha estructura satisface todas las sentencias de Γωy, en consecuencia, también satisface las del conjunto inicial Γ. La completitud resulta entonces ser un corolario del teorema de satisfacción: si Γ|=ϕ, entonces Γ∪{¬ϕ}es no satisfacible, y por contraposición, Γ∪{¬ϕ}es no consistente y, en consecuencia, Γϕ. Aunque el método de árboles semánticos tiene algunos antecedentes, como, por ejemplo en Herbrand, fue elaborado por Beth, quien en 19554ideó una prueba del mismo teorema de satisfacción y, por lo tanto, de la completitud de la lógica de predicados de primer orden, que tiene sobre el método de Henkin la ventaja de ser más económica. Para la nueva demostración se definen los árboles de Beth y se prueba que si Γes satisfacible, entonces el árbol de Beth de Γes abierto; en segundo lugar, se prueba que si el árbol de Beth de Γes cerrado, entonces Γes no consistente. De esto último se sigue, por contraposición, que si Γes consistente, entonces el árbol semántico de Beth de Γno es cerrado (es abierto). En tercer lugar, se 3Sustitución de xpor ben ϕ, según se define más adelante. 4Beth (1955); hay una versión en español en Cuadernos Teorema, no. 18. 22 prueba que si el árbol de Beth de Γno es cerrado, entonces Γes satisfacible en un universo finito o infinito numerable. El último resultado junto con el anterior constituyen una versión del teorema de satisfacción, y su prueba es muy similar a la de Henkin: a partir de las sentencias de cualquiera de las ramas del árbol que haya quedado abierta se define una estructura interpretativa y se prueba que la misma satisface todas las sentencias de las ramas en cuestión. Se advierte, pues, una indudable utilidad del método en lógica de predicados de primer orden. ¿Es asimismo aplicable en lógica de predicados de orden superior, en particular, en la de segundo orden? Si para comprender mejor la naturaleza de la cuantificación hemos de afrontar los problemas que ésta suscita cuando se extiende a variables de predicado, tratándose de un asunto nada trivial, la respuesta a dicha cuestión no puede ser una espontánea afirmación de que tal método sería aplicable, mutatis mutandi, a orden superior; como tampoco una apresurada negativa dada la incompletitud esencial de la lógica de segundo orden. En este trabajo presentamos el procedimiento de tablas semánticas de Beth (y alguna modificación del mismo) en primer orden. A continuación se describe brevemente un lenguaje formal de segundo orden, destacando ciertas clases de fórmulas. En el apartado subsiguiente se trabaja con tablas aplicadas a (matrices de) sentencias de estas clases, definiendo reglas adicionales para tratar una de las clases en cuestión. Por último, se presenta una serie de observaciones sobre estas aplicaciones. A lo largo del texto aparecen los teoremas (y un lema) que hemos considerado relevantes; sus demostraciones se incluyen esquemáticamente, o se indica dónde pueden hallarse, salvo en el caso del teorema 9 y el lema necesario para probarlo, las cuales (y las definiciones necesarias), por su extensión, se han desarrollado en un apéndice. 23 2. Reglas de formación de árboles de primer orden Se han de especificar las nociones necesarias para las tablas semánticas de primer orden. A estos efectos, hacemos uso de L1, un lenguaje formal de primer orden sin identidad ni functores y con constantes individuales y predicativas (denominados parámetros yrelatores, respectivamente). Un árbol de Beth de sentencias es un conjunto de sucesiones de sentencias de L1; estas sucesiones se denominan ramas, generadas a partir de un conjunto no vacío de sentencias de L1por aplicación a éstas de las reglas detalladas más adelante así como a las sentencias no elementales resultantes. Dispuestas sucesivamente las sentencias generadoras (que son las asunciones iniciales), diremos que no están convenientemente marcadas si no son elementales, constituyendo el comienzo de una rama; a cada sentencia no elemental no convenientemente marcada se aplicará la regla correspondiente, escribiendo a continuación las sentencias resultantes y se marcará con determinado signo lógico como subíndice (excepto cuando se trate de un cuantificador, en cuyo caso se anotarán los parámetros utilizados); el proceso se continúa hasta que todas las sentencias no elementales queden marcadas o aparezca un par de contradicción, entendiendo por tal las sentencias elementales δyδde manera que una es negación de la otra. Sea ϕuna sentencia no elemental no convenientemente marcada; las reglas se definen en función del grado de complejidad de ϕ: 1. si ϕes ¬ψ, entonces (a) si ψes ¬β, entonces se añade β; (b) si ψes β∧γ, entonces se añade ¬β∨¬γ; (c) si ψes β∨γ, entonces se añade ¬β∧¬γ; (d) si ψes β→γ, entonces se añade β∧¬γ; 24 (e) si ψes ∃xβ, entonces se añade ∀x¬β; (f) si ψes ∀xβ, entonces se añade ∃x¬β; además se marca ϕcon ¬como subíndice. 2. Si ϕes ψ∧β, entonces se añaden consecutivamente ψyβ, y se marca ϕcon ∧. 3. Si ϕes ψ∨β, entonces se abren dos subramas, una con ψy otra con β, se marca ϕcon ∨, y decimos que ϕes un punto de bifurcación. 4. Si ϕes ψ→β, entonces se abren dos subramas, una con ¬ϕy otra con β, se marca ϕcon →, y, asimismo, decimos que ϕes un punto de bifurcación. 5. Si ϕes ∃xψ, entonces se añade ψ(bk+1/x), siendo bk+1 el parámetro de menor subíndice que no ocurría antes en la rama (es decir, únicamente ocurrían bi, para i≤k), y se marca ϕcon dicho parámetro. 6. Si ϕes ∀xψ, entonces se añaden ψ(b1/x), ψ(b2/x),..., ψ(bn/x), siendo b1,...,bntodos los parámetros que ocurren en fórmulas de la rama. Cuando en una rama aparece un par de contradicción —en cuyo caso se detiene el proceso, como se ha indicado— se dice que tal rama es cerrada. Una rama está acabada si es cerrada o, en otro caso, si todas sus fórmulas no elementales están convenientemente marcadas. Un árbol es cerrado cuando todas sus ramas son cerradas. Un árbol está acabado cuando todas sus ramas están acabadas. La propiedad fundamental de los árboles semánticos se expresa en el siguiente teorema cuya demostración omitimos para abreviar.5 5En Beth (1955) aparece la prueba del “teorema de árboles”; una demostración del teorema tal como se formula a continuación, aparece 25 Teorema 1: Dados un conjunto Γde sentencias y una sentencia ϕ∈L1,Γ|=ϕsi y sólo si el árbol de Γ∪{¬ϕ} es cerrado. También se puede enunciar diciendo que ϕes satisfacible si y sólo si el árbol de {ϕ}es abierto. A partir de una rama abierta se define una L1-estructura que satisface todas las sentencias de la rama en cuestión. Esta L1-estructura representa una clase de L1-estructuras que satisfacen ϕ. Además de los árboles de BETH, tomamos los árboles ∃- modificados6obtenidos mediante una ligera modificación de la definición del árbol respecto de las sentencias a que dan lugar las fórmulas de la forma ∃xϕ. Veamos la definición de la cláusula correspondiente en un caso y otro: 1. BETH. Se trata de la regla 5 citada: Si en una rama aparece una fórmula de la forma ∃xψy está convenientemente marcada, entonces aparece también ψ(bk+1/x), siendo bk,k≥1, el último parámetro que ocurría en la rama (antes de aplicar la regla 5). 2. ∃-MODIFICADOS. La anterior regla 5 se reformula de la siguiente manera: Si ϕes ∃xψ, entonces se abren subramas cada una de ellas con ψ(bi/x), para cada i≤k+ 1, siendo bk,k≥0, el último parámetro en Nepomuceno (1995), pp. 45–49 y 58–60 —para lógica proposicional y para lógica de predicados de primer orden, respectivamente. 6Díaz (1993) y Boolos (1984) idearon un tratamiento especial para fórmulas que generan árboles infinitos pero que son satisfacibles en dominios finitos. En Díaz (1993, p. 43) aparece una breve nota acerca del momento en que aparece tal tratamiento. En este punto, como en otros a lo largo del trabajo, hemos de reconocer la deuda contra´ ıda con las ideas expuestas en Díaz (1987) y Díaz (1993) (así como las incluidas en documentos inéditos del mismo autor), especialmente las nociones de ∆-fórmulas y las reglas especiales para determinados lenguajes. 26 que ocurría en la rama (antes de la aplicación de esta regla) y se marca ϕcon |b1|,...,|bk|,bk+1.7 Los árboles obtenidos aplicando esta nueva regla poseen ciertas ventajas sobre los de Beth. Veámoslo en un sencillo ejemplo: Sea la sentencia ∀x∃yRxy; el árbol de Beth tendría una única rama infinita, pero esta fórmula es satisfacible en un universo de un único individuo. En el árbol ∃-modificado, habría una rama con exactamente las siguientes sentencias: <∀x∃yRxy,∃yRa1y,Ra1a1>, la cual permite definir una L1-estructura que satisface todas las fórmulas de dicha rama, con tal de que se interpreten el primer parámetro y el relator de la manera adecuada, aunque también contenga ramas infinitas, como <∀x∃yRxy,∃yRa1y,Ra1a2,∃yRa2y,Ra2a3,...>. 3. Un lenguaje formal de segundo orden L2es un lenguaje formal de segundo orden obtenido a partir de L1, incluyendo variables predicativas y no restringiendo la cuantificación a las variables individuales. Así pues, si ϕes una fórmula de L2yses una variable de cualquier tipo (individual o predicativa de cierta aridad), entonces ∃sϕ, ∀sϕson fórmulas, y se dice que ses el sufijo del cuantificador correspondiente. Las fórmulas de L2que 7De este modo, las marcas |bi|,i≤kexpresan que se trata de ramas obtenidas por la nueva regla, mientras que la marca bk+1 indica que se trata de una rama correspondiente a un árbol de Beth. 27 carezcan de variables libres serán denominadas sentencias, como es usual. Sea ϕ∈L2, definimos ϕ(r/s), donde ses una variable y runa variable individual o parámetro, si ses individual, o bien una variable predicativa o relator de la misma aridad que s, si ésta es predicativa, según las cláusulas: 1. Si sno ocurre, o no ocurre libre, en ϕ, entonces ϕ(r/s) es ϕ. 2. Si res sufijo de un cuantificador bajo cuyo alcance cae s, entonces ϕ(r/s)esϕ. 3. En otro caso, ϕ(r/s) es la fórmula resultante de sustituir cada ocurrencia libre de sen ϕpor r. Para representar la sustitución en ϕde s1ys2por r1y r2—siempre que sean del tipo correspondiente— se anotará ϕ(r1,r2/s1,s2); en general, para sustitución de n≥1 términos, o sustitución simultánea, la notación es ϕ(r1,...,rn/s1,...,sn). La semántica de L2queda establecida de la siguiente manera: Una L2-estructura viene dada por un dominio o universo de discurso y una función interpretación: M=<D,>, en donde representa la denominada función interpretación, definida con dominio en los parámetros y relatores y rango en D(y en los predicados y relaciones definidos en D) de manera que 1. Para cada parámetro b,(b)∈D. 28 2. Para cada relator n-ádico R,(R)∈P(Dn), para todo n≥1. La noción de satisfacción y las restantes nociones semánticas (validez en un dominio, validez universal, etc.) son las usuales. Si ϕ∈L2es una sentencia M|=ϕindica que M satisface dicha sentencia; si Γes un conjunto de sentencias, Γ|=ϕindica que ϕes consecuencia lógica de Γ. Podemos considerar que los relatores de L1son también relatores de L2. Asimismo, cada fórmula de L1como una fórmula de L2. En general, si ϕ∈L2,X1,...,Xk, son sus variables predicativas, R1,...,Rkson relatores tales que la aridad de Ries la misma que la de Xi, para todo i≤k, y se verifica que ϕ(R1,...,Rk/X1,...,Xk)∈L1, entonces diremos que ϕes esencialmente de primer orden. Respecto de fórmulas de L2en forma prenexa, el teorema de Zykov establece: Para toda sentencia ϕ∈L2se puede obtener una sentencia ψen forma prenexa en la que los cuantificadores predicativos preceden a los cuantificadores individuales, tales que |=ϕ↔ψ.8 La demostración requiere la adopción de la semántica con axioma de elección. Por ahora, probadas una serie de equivalencias previas, lo que omitimos en aras de la brevedad, se obtiene: 8ϕ↔ψse puede considerar abreviatura de (ϕ→ψ)∧(ψ→ϕ) (de otro modo, fácilmente se redefiniría Lconteniendo este signo). La demostración original de Zykov (1956), es relativa a orden superior; en Hilbert-Ackermann (1962) aparece un resumen de su adaptación a segundo orden. 29 Lema:12 Dadas una sentencia Qγsiendo QyQprefijos cuantificacionales predicativos, y una L2-estructura M 1. Si Qes ∃X,M|=Qγsi y sólo si para todo i≤k, δi∈∆(γ,X),|∆(γ,X)|=k, M|=Qγ(δ1/X)∨Qγ(δ2/X)∨...∨Qγ(δk/X); 2. Si Qes ∀X,M|=QQγsi y sólo si para todo i≤k, δi∈∆(γ,X), |∆(γ,X)|=k, M|=Qγ(δ1/X)∧Qγ(δ2/X)∧...∧Qγ(δk/X). La demostración del Teorema 9 es análoga a la del Teorema 4, teniendo en cuenta este lema. . 5. Observaciones sobre estas aplicaciones De acuerdo con la metodología expuesta, hemos extendido el procedimiento de árboles de primer orden, teniendo en cuenta la modificación incluida para el tratamiento de la clase de las IZ, de manera que podemos reseñar algunas consecuencias, para lo cual tendremos en cuenta los resultados anteriores y los siguientes. Teorema 10: Para toda sentencia β∈Π1 1(1 1)existe otra sentencia β∗∈1 1(Π1 1), tales que |=βsi y sólo si β∗ es no satisfacible. En efecto, sea βde la forma ∀X1,...,Xmϕ,m≥1. Obviamente, |=βsi y sólo si ¬βes no satisfacible, pero ¬∀X1,...,Xmϕ←→ ∃ X1,...,Xm¬ϕ, 12 Como en el caso de las nociones necesarias para la demostración, hemos incluido ésta en el apéndice. 36 y∃X1,...,Xm¬ϕ∈1 1. De manera análoga, si βes de la forma ∃X1,...,Xmϕ, entonces β∗sería ∀X1,...,Xm¬ϕ. . Teorema 11: Para cada β∈Π1 1tal que ∀Z1,...,Zkβ∈ Π1 1y carezca variables libres,13 son equivalentes: 1. |=β(R1,...,Rk/Z1,...,Zk), siendo Rirelator de la misma aridad que Zi, para todo i≤k; 2. |=∀Z1,...,Zkβ; 3. si βes ∀X1,...,Xtϕ,t≥1, el árbol semántico de ¬ϕes cerrado. La demostración es trivial a partir de la evaluación de ∀ y del Teorema 8. . Teorema 12: Para cada β∈1 1tal que ∃Z1,...,Zkβ∈ 1 1y carezca variables libres, son equivalentes: 1. β(R1,...,Rk/Z1,...,Zk) es satisfacible, siendo Rirelator de la misma aridad que Zi, para todo i≤k; 2. ∃Z1,...,Zkβes satisfacible; 3. si βes ∃X1,...,Xtϕ,t≥1, el árbol semántico de ϕ es abierto. En efecto: (1) si y sólo si (2) por evaluación de ∃; (2) si y sólo si (3) si tenemos en cuenta el Teorema 4; (3) si y sólo si ϕes satisfacible (esencialmente de primer orden) si y sólo si lo es la sentencia ϕ(R1,...,Rk,S1,...,St/Z1,...,Zk,X1,...,Xt), donde Sjes relator de la misma aridad que Xj, para todo j≤t, si bien ésta es satisfacible si y sólo si 13 Z1,...,Zkson las variables libres de β, pudiendo ocurrir relatores. 37 ∃X1,...,Xtϕ(R1,...,Rk/Z1,...,Zk),es satisfacible, pero ∃X1,...,Xtϕ(R1,...,Rk/Z1,...,Zk) es precisamente β(R1,...,Rk/Z1,...,Zk), luego (3) si y sólo si (1). Respecto de las clases 1 1yΠ1 1hemos obtenido resultados en parte esperados. Pero el estudio de la clase IZ se puede considerar más novedoso. Van Benthen y Doets (1984) se habían ocupado de las primeras, aunque no de esta última; el lenguaje formal de primer orden que utilizan es un lenguaje con identidad. En cualquier caso, cabría considerar el método de los árboles alternativo a aquel que recurre a depuradas nociones de teoría abstracta de modelos (teoría de filtros: ultraproducto, ultrapotencia, colapso, etc.). Si bien nos hemos referido principalmente a sentencias en las cuales no ocurrían relatores, sino sólo variables predicativas ligadas, a partir de los últimos resultados es posible una ampliación de la aplicación del método. Asimismo, al operar sobre sentencias en forma prenexa con cuantificadores individuales precediendo a todos los cuantificadores predicativos, en el desarrollo de un árbol semántico, se obtienen sentencias de IZ, con las cuales se puede continuar si tenemos en cuenta lo estudiado más arriba. Si la aplicabilidad del método de tablas semánticas en lógica de segundo orden no nos lleva a logros espectaculares, nos permite, al menos, alcanzar ciertos resultados desde otra perspectiva, lo que invita a continuar la reflexión sobre la naturaleza misma de la cuantificación, cómo se pueden plantear extensiones de lógica elemental, etc. En particular, si a partir del método de Beth es demostrable la completitud de los sistemas de cálculo de primer orden. ¿Qué se puede decir acerca de los sistemas de cálculo de segundo orden tras las modificaciones propuestas? La corrección 38 de estos sistemas es un resultado conocido, también que la completitud es imposible como consecuencia del teorema de incompletitud de sistemas formales aritméticos de G¨ odel.14 No obstante, adoptando la nueva semántica propuesta por Henkin,15 es demostrable que los sistemas de cálculo de segundo orden son completos en sentido general. Consideremos un sistema de cálculo tipo Hilbert (ampliado a segundo orden), que representamos por (“α” indica que la fórmula αes demostrable en dicho cálculo). Adoptando la semántica estándar, la incompletitud de podemos enunciarla de la siguiente manera: existe una sentencia γ∈L2tal que |=γpero no es el caso que γ; a partir de la fórmula aritmética construida por G¨ odel es definible una tal sentencia γ. No obstante, cabe esperar una cierta completitud, sin necesidad de cambiar la semántica estándar, siempre que sea relativa a una clase restringida de sentencias, que desde luego no contendrá fórmulas como la mencionada. Sea la clase F∆⊆L2, tal que verifica 1. Si ϕ∈L2yϕ∈1 1∪Π1 1∪IZ, entonces ϕ∈F∆. 2. Si ψes la forma prenexa de ϕyψ∈F∆, entonces ϕ∈F∆. Respecto de esta clase, y teniendo en cuenta los resultados anteriores, se podrá establecer que para cada ϕ∈F∆, si |=ϕ, entonces ϕ, y, dada corrección de , 14 Manzano (1996) ha presentado una prueba directa de incompletitud, al margen del teorema de G¨ odel; dicha prueba está basada en ciertas técnicas de teoría de conjuntos y en la capacidad expresiva que caracteriza la lógica de segundo orden. 15 En Henkin (1950). Esquemáticamente, en sentido general, en las estructuras interpretativas se tienen en cuenta el universo de discurso (no vacío) y también universos relacionales (para cada aridad), los cuales poseen ciertas características algebraicas, como se describe en Manzano (1996), lo cual equivale a que todas las relaciones son definibles (con el lenguaje formal de que se trate). 39 para cada ϕ∈F∆,|=ϕsi y sólo si ϕ. 6. Ap´ endice Consideramos ahora el lenguaje formal L2=, obtenido a partir de L2con el relator diádico =y considerando que si aybson variables individuales o parámetros, a=b∈ L2=. Para mayor facilidad, se escribirá a=ben lugar de ¬(a=b). Por lo que respecta a la semántica de L2=, si M=<D,>, para cualesquiera parámetros ayb, M|=a=bsi y sólo si (a)=(b).16 Definimos, para βy cada variable predicativa n-ádica X, el conjunto de fórmulas ∆(β,X) por inducción sobre el grado de complejidad de β(para simplificar, consideraremos que ¬y∨son las únicas conectivas que ocurren en β). ∆(β,X) es el más pequeño conjunto que verifica: 1. Si en βno ocurre X, entonces ∆(β,X)=∅. 2. Si βes Xb1...bn, entonces ∆(β,X)={δ, ¬δ},en donde δes x1=b1∧...∧xn=bn. Por otra parte, se dice que δes positiva,y¬δnegativa. 3. Si βes ¬γ, entonces ∆(β,X)=∆(γ,X). 4. Si βes γ∨η, entonces, ∆(β,X) es el mínimo conjunto tal que: i. Si θ∈∆(γ,X)oθ∈∆(η,X)yθes positiva, entonces θ∈∆(β,X). ii. Para toda i,j≥1, si θi∈∆(γ,X)oθj∈∆(η,X) y ambas son positivas, entonces θi∨θj∈∆(β,X). iii.Para n>1, toda i≤n,siϑi∈∆(γ,X)oϑi∈ ∆(η,X)yϑies negativa, entonces ϑ1∧...∧ϑn∈ ∆(β,X). 16 Fácilmente se comprueba que |=a=b↔∀X(Xa ↔Xb). 40 5. Si βes Qγ, donde Qes un prefijo cuantificacional cuyos sufijos son Z1,...,Zm, las m≥1 variables predicativas distintas de Xque ocurren en γ, entonces ∆(Qγ,X)=∆(β(R1,...,Rm/Z1,...,Zm),X), siendo Riun relator de la misma aridad que Zi, para toda i≤m. Los árboles más arriba definidos se pueden modificar añadiendo: 1. Si en una rama ocurre una sentencia de la forma b= b, en donde bes un parámetro cualquiera, entonces se produce el mismo efecto que si se tratara de un par de contradicción; es decir, la rama es cerrada. 2. Si en una rama ocurren fórmulas de la forma β(aj/x) yai=aj, siendo éstos unos parámetros tales que i≤j, entonces se tachan todas las fórmulas β(aj/x) y se sustituyen por β(ai/x) (también se pueden tachar las mencionadas fórmulas de identidad). Dada una fórmula de la clase IZ, que tendrá, por tanto, la forma Q1Q2β, en donde βes esencialmente de primer orden, y teniendo en cuenta la modificación de las reglas de los árboles respecto de fórmulas de identidad, se definen las siguientes nuevas reglas específicas para el prefijo Q2 (para la construcción de árboles tanto de Beth, como ∃- modificados, aunque ya específicos de segundo orden). Sea un punto del árbol en que la fórmula a marcar tiene la forma Q2βyβno contiene variables individuales; para mayor facilidad consideremos que |Q2|=1 y, por tanto, únicamente ocurre un cuantificador predicativo, entonces 1. Si Q2βes ∃Xβ,Xvariable predicativa de aridad n≥1, entonces se abren subramas cada una con 41 β(ρi(b1,...,bn/x1,...,xn)/Xb1,...,bn), para toda ρi∈∆(β,X), marcándose la fórmula inicial con dichas ρicomo subíndices. 2. Si Q2βes ∀Xβ,Xvariable predicativa de aridad n≥1, entonces se añaden a la rama las fórmulas β(ρi(b1,...,bn/x1,...,xn)/Xb1,...,bn), para toda ρi∈∆(β,X), marcándose la fórmula inicial con dichas ρicomo subíndices. Demostración del Lema: [Inducción sobre el grado de complejidad de Qγ.] Comencemos considerando el caso en que Q=∅: 1. γes Xb1...bn, para n≥1. En tal caso, para cada L2-estructura M •M|=(b1=b1∧...∧bn=bn)∨(b1=b1∨...∨bn= bn), asimismo M|=∃Xγ(ambas son válidas en el correspondiente dominio); •Mno satisface (b1=b1∧...∧bn=bn)∧(b1= b1∨... ∨bn=bn), pero Mno satisface ∀Xγ tampoco. 2. γes ¬η; por hipótesis, M|=∃Xη⇐⇒ 17 M|= η(δ1/X)∨...∨η(δk/X), para δi∈∆(ηX), i≤k yk≥1; asimismo, M|=∀Xη⇐⇒ M|=η(δ1X)∧ ...∧η(δkX), para δi∈∆(ηX), i≤kyk≥1; además ∆(γ,X)=∆(η,X). Entonces, M|=∃X¬η⇐⇒ M|=¬∀Xη⇐⇒ no-(M|=∀Xη)⇐⇒ no-(M|= η(δ1/X)∧...∧η(δk/X)) ⇐⇒ M|=¬η(δ1/X)∨...∨ 17 Abreviatura que indica la equivalencia entre las proposiciones anotadas a sus extremos. Es decir, A⇐⇒ B, representa “si A, entonces B, y si B, entonces A”. 42 ¬η(δk/X). Recíprocamente, M|=∀X¬η⇐⇒ M|= ¬∃Xη⇐⇒ no-(M|=∃Xη)⇐⇒ no-(M|=η(δ1/X)∨ ...∨η(δk/X)) ⇐⇒ M|=¬η(δ1/X)∧...∧¬η(δk/X). 3. γes η∨θ. Establecemos, según la definición dada más arriba, ∆(γ,X)=∆ ∗, es el más pequeño conjunto tal que: i) si δ∈∆(η,X)óδ∈∆(θ, X)yδes positiva, entonces δ∈∆∗; ii) para todo i,j,siδi∈∆(η,X), δj∈∆(θ,X)y ambas son positivas, δi∨δj∈∆∗; iii) para todo i,j,siδi∈∆(η,X), δj∈∆(θ,X)y ambas son negativas, δi∧δj∈∆∗. Se nos presentan dos casos: (a) M|=∀X(η∨θ), entonces para toda asignación sde valores a las variables se verifica que M,s|=η∨θ;18 entonces, para cada δk∈∆(η/X), δm∈∆(θ/X), M|=η(δk/X)óM|=θ(δm/X). Si δ∈∆∗por i), M|=η(δ/X)óM|=θ(δ/X); si δ∈∆∗es δk∨δm, definida por ii), M|=η(δk∨δm/X)óM|= θ(δk∨δm/X); si δ∈∆∗es δk∧δmdefinida según iii), M|=η(δk∧δm/X)óM|=θ(δk∧δm/X). Es decir, para cada δ∈∆∗,M|=η(δ/X)∨θ(δ/X), luego M|=(η∨θ)(δ/X); si |∆∗|=r,M|=(η∨θ)(δ1/X)∧ ...∧(η∨θ)(δr/X). Recíprocamente, si |∆∗|=r, para δi∈∆∗,i≤r,M|=(η∨θ)(δ1/X)∧...∧(η∨ θ)(δr/X), entonces M|=(η(δ1/X)∨θ(δ1/X))∧...∧ (η(δr/X)∨θ(δr/X)), de donde, para toda asignación s, M,s|=η∨θ, y, por evaluación de ∀,M|=∀X(η∨θ). 18 En el caso básico, M,s|=Xb1,...,bnpara toda asignación ssi y sólo si M|=(b1=b1∧...)∧(b1=b1∧...) (ninguna es satisfecha por esta estructura). Por inducción, se establece que M,s|=γ, para toda asignación s, si y sólo si M|=γ(δ1/X)∧...∧γ(δrX) para toda δi∈∆(γ,X),|∆(γ,X)|=r. 43 (b)M|=∃X(η∨θ), entonces para alguna asignación s, M,s|=η∨θ; de manera análoga al caso precedente, hay alguna δ∈∆∗tal que M|=(η∨θ)(δ/X), es decir, M|=η(δ/X)∨θ(δ/X). Teniendo en cuenta la construcción de ∆∗, se alcanza que M|=(η∨ θ)(δ1/X)∨...∨(η∨θ)(δr/X). Recíprocamente, para δi∈∆∗,i≤r,siM|=(η∨θ)(δ1/X)∨...∨(η∨ θ)(δr/X), entonces M|=(η(δ1/X)∨θ(δ1/X))∨...∨ (η(δr/X)∨θ(δr/X)), de donde, para alguna asignación s, se verifica M,s|=η∨θ, y, por evaluación de ∃,M|=∃X(η∨θ). Consideremos ahora que |Q|=m≥1, siendo Z1,...,Zmlas variables (predicativas) sufijo de los mcuantificadores que integran Q. Habremos de tener en cuenta la cláusula 5 que define ∆(Qγ,X)=∆(γ(R1,...,Rm/ Z1,...,Zm),X); llamamos γa la fórmula γ(R1,...,Rm/ Z1,...,Zm). Entonces: 1. M|=∃XQγ; entonces para alguna asignación s, M,s|=Qγ; para cada δi∈∆(γ,X), i≤r, asignación s(que difiere de sa lo sumo con respecto de los valores de R1,...,Rm), M,s|=γ(δ1/X)∨ ...∨γ(δr/X).19 Fácilmente (iterando el caso de disyunción visto anteriormente) se alcanza que M,s|= Qγ(δ1/X)∨...∨Qγ(δr/X) (asimismo, recíprocamente). 2. M|=∀XQγ; entonces para toda asignación s, M,s|=Qγ; para cada δi∈∆(γ,X), i≤r, asignación s(que difiere de sa lo sumo con respecto de los valores de R1,...,Rm), M,s|=γ(δ1/X)∧ 19 En este apartado, como en el siguiente, cabría distinguir varios casos: Q=∀Z1∀Z2,oQ=∀Z1∃Z2,oQ=∃Z1∀Z2,oQ=∃Z1∃Z2 (con lo que m=2); supuesto para Q∗, estudiar el de Q=Q∗∀Zmo Q=Q∗∃Zm, teniendo siempre en cuenta el modo de evaluación de los cuantificadores (cuyo detalle omitimos para abreviar). 44 ...∧γ(δr/X). Fácilmente (teniendo en cuenta el caso de disyunción también visto antes) se alcanza que M,s|=Qγ(δ1/X)∧...∧Qγ(δr/X) (asimismo, recíprocamente). . BIBLIOGRAFÍA van Benthem, J. y K. Doets, 1984, “Higher-Order Logic”, Handbook of Philosophical Logic, Gabbay y Genthner (comps.), Kluwer Adademic Publishers, Dordrecht, vol. I, pp. 275–330. Beth, E.W., 1955, “Semantic Entailment and Formal Derivability”, en J. Hintikka (1969), The Philosophy of Mathematics, Oxford University Press Londres. [Traducido en Cuadernos Teorema, no. 18, “Entrañamiento semántico y derivabilidad formal”, Valencia, 1978.] Boolos, G., 1984, “Trees and Finite Satisfactibility”, Notre Dame Journal of Formal Logic, vol. 25, pp. 110–115. Díaz, E., 1993, “ ´ Arboles semánticos y modelos mínimos”, Madrid, Actas del I Congreso de la Sociedad de Lógica, Metodología y Filosofía de la Ciencia en España, pp. 40–43. ——, 1987, “Conjuntos enumerables representativos de conjuntos no enumerables”, Colloquium 1985–1986, Badajoz, vol. 15, pp. 51–66. Henkin, L., 1950, “Completeness in The Theory of Types”, en Hintikka (1969), pp. 53–63. ——, 1949, “The Completeness of The First-Order Functional Calculus”, en Hintikka (1969), pp. 42–52. Hilbert, D. y W. Ackerman, 1962, Elementos de lógica teórica. [Trad. V. Sánchez de Zabala, 6aedición), Tecnos, Madrid. Manzano, M., 1996, Extensions of First Order Logic, Cambridge University Press, Cambridge. 45