¿Puede la FPA demostrar realmente su coherencia?

Question

Primero formularé la pregunta y luego la explicaré.

PREGUNTA: FPA puede demostrar su propia consistencia en el sentido godeliano. Pero, ¿puede realmente demostrar su consistencia?

FPA es una teoría de primer orden multiordenada, con minúsculas o minúsculas (para los números) y mayúsculas o mayúsculas para las relaciones de n-aridad (n >= 1). (En la práctica, creo que se puede limitar la teoría a relaciones en las que n = 1, 2 ó 3).

Se presupone una comprensión total.

FPA tiene un símbolo constante 0, una relación 1-aria N (número natural) y un símbolo de relación 2-aria S (sucesión).

En este contexto se pueden escribir los axiomas de Peano:

(PA1) N0
(PA2) $\forall$ n (Nn $\Rightarrow$ $\exists$ m (Nm & Sn,m))
(PA3) $\forall$ n $\forall$ m $\forall$ m' (Nn & Nm & Nm' & Sn,m & Sn,m' $\Rightarrow$ m = m')
(PA4) $\forall$ n $\forall$ m $\forall$ n' (Nn & Nm & Nn' & Sn,m & Sn',m $\Rightarrow$ n = n')
(PA5) $\forall$ n (Nn $\Rightarrow$ $\neg$ Sn,0)
(PA6) $\forall$ P (P0 & $\forall$ n $\forall$ m(Pn & Sn,m $\Rightarrow$ Pm) $\Rightarrow$ $\forall$ n(Nn $\Rightarrow$ Pn))

FPA asume todos los axiomas de Peano excepto (PA2), es decir, todo excepto la totalidad de la relación de sucesión. Tiene como modelos estándar todos los segmentos iniciales así como el modelo estándar de los números naturales. {0} es un modelo. Por lo tanto, es agnóstico en cuanto a si los números naturales siguen y siguen.

En FPA es posible definir fórmulas para la suma, multiplicación, menor que, exponenciación, y, excepto obviamente para la totalidad y cualquier propiedad relacionada, demostrar las propiedades habituales. Intuitivamente, la existencia de un número natural n implica que todo número menor que n existe.

Se pueden definir predicados para números:
uno(n) si y sólo si S0,n & Nn,
dos(n) si y sólo si $\exists$ x (uno(x) & Sx,n) & Nn
Obviamente no se puede demostrar que exista cualquier n tal que uno(n). Pero si tal n existe, entonces se puede demostrar que tiene todas las propiedades habituales de 1. De manera similar para dos, tres, etc.

FPA demuestra el Teorema Fundamental de la Aritmética.

La recursividad está disponible y es posible definir fórmulas que expresen la sintaxis a la manera de Godel. Por ejemplo, Término1(n) ("n es un término en minúsculas") podría definirse como siete(n) $\vee$ $\exists$ y $\exists$ z (+(y,y,n) & eleven(z) & z >= n). (Siete(n) expresa que n es 0, y las variables en minúscula son los números pares >= once).

Se puede continuar y definir una fórmula GProof(n,x) que dice que n es el número de Godel de una prueba en FPA de un wff cuyo número de Godel es x. Sea $\mathcal{F}$ ser " $\neg$ 0 = 0", entonces GCons(FPA) es la fórmula:
$\neg$ $\exists$ p (GProof(p, $\mathcal{F}$ ))

Pero FPA demuestra GCons(FPA). Intuitivamente, el razonamiento es el siguiente. Supongamos que $\neg$ GCons(FPA). Entonces existe un número p tal que GProof(p, $\mathcal{F}$ ). Pero, debido a la naturaleza de la Godelización, y su uso de un único número para representar secuencias de números mediante exponenciación, este es un número muy grande, fácilmente mayor que el que se requiere para definir "verdadero en {0}" para todas las proposiciones de longitud menor que las proposiciones de la supuesta prueba. FPA puede demostrar que los axiomas son verdaderos en {0}, que las reglas de deducción preservan la verdad en {0} para todos los pasos de la prueba, pero por supuesto $\mathcal{F}$ no es verdadera en {0}. Contradicción, por lo que FPA demuestra GCons(FPA).

Bueno, esto sí que parece un poco trampa, porque utiliza el hecho de que la Godelización, al utilizar números para representar secuencias, necesita números muy grandes. En lugar de números en minúsculas para codificar una secuencia, se pueden utilizar letras en mayúsculas: R es una secuencia si y sólo si dom(R) es {x : x <= n} para algún número natural n. Uno puede entonces redefinir una fórmula RProof(R,S) que dice que R es una secuencia que representa una prueba de la proposición representada por la secuencia S. Y definir una nueva fórmula RCons(FPA).

La pregunta es: ¿prueba FPA RCons(FPA)?

La demostración de la fórmula de Godelización no pasa porque ahora sólo está implicado un número pequeño (la longitud de la demostración), y esto no es suficiente, al menos a primera vista, para construir un modelo de verdadero-en{0} para las proposiciones de la demostración. Para demostrar que FPA demuestra RCons(FPA), bastaría con demostrar que cualquier prueba de una inconsistencia tendría que ser muy, muy larga. Para demostrar que FPA no demuestra RCons(FPA), tal vez la prueba original de Godel pasaría, pero esto me pone nervioso, debido al problema con GCons(FPA).

Perdón por la pregunta tan larga, ¡pero se agradece cualquier ayuda!

Answer 1

En principio, la respuesta puede depender del sistema de pruebas, pero mientras se ciña a alguno de los sistemas de pruebas habituales de tipo Hilbert o secuencial, esto no debería importar.

En primer lugar, como se explica en https://mathoverflow.net/questions/120106 la pregunta es equivalente a la demostrabilidad de la consistencia de FPA en $I\Delta_0+\Omega_1$ . (El hecho de utilizar objetos de segundo orden para codificar pruebas y fórmulas corresponde a utilizar todos los números en lugar de sólo los logarítmicamente pequeños en $I\Delta_0+\Omega_1$ de ahí que se acabe obteniendo la declaración de coherencia habitual).

Ahora, trabajando en $I\Delta_0+\Omega_1$ (o equivalentemente, Buss's $S_2$ ), la consistencia del FPA es equivalente a la consistencia de la teoría de segundo orden del modelo con universo de primer orden de un elemento (en cualquier lenguaje finito, todo es equivalente), ya que las dos teorías son interpretables entre sí. Esto, a su vez, puede reducirse al cálculo proposicional cuantificado: puesto que sólo hay un elemento de primer orden (y sólo un $n$ -de elementos para cada $n$ ), puede ignorar los cuantificadores y variables de primer orden, y sustituir las variables de segundo orden por variables proposicionales tanto en los cuantificadores de segundo orden como en las fórmulas atómicas. (Fórmulas atómicas puramente de primer orden como $t=s$ puede sustituirse por la constante $\top$ por la verdad). Así pues, la cuestión es si $I\Delta_0+\Omega_1$ demuestra la consistencia del cálculo proposicional cuantificado ( $G$ ).

La respuesta es que éste es uno de los principales problemas abiertos en la materia, pero se conjetura que es falso. Existe una especie de correspondencia de los subsistemas de aritmética acotada con los sistemas de pruebas proposicionales; en particular, los fragmentos $T^i_2$ de $S_2$ ( ${}=I\Delta_0+\Omega_1$ ) corresponden a los fragmentos $G_i$ del cálculo proposicional cuantificado, obtenido restringiendo todas las fórmulas de la prueba (o alternativamente, todas las fórmulas de corte en la formulación del cálculo secuencial) a $\Sigma^q_i$ o $\Pi^q_i$ fórmulas (= fórmulas en forma prenex con un máximo de $i$ bloques cuantificadores). Es decir:

• $T^i_2$ demuestra la consistencia (e incluso alguna forma de principio de reflexión) de $G_i$ .

• A la inversa, $\mathrm{Con}_{G_i}$ implica sobre una teoría de base débil todo $\forall\Delta^b_1$ -consecuencias de $T^i_2$ (y consecuencias más complejas de $T^i_2$ puede axiomatizarse mediante un principio de reflexión adecuado). Un hecho relacionado es que si $T^i_2$ demuestra una $\forall\Sigma^b_i$ se puede traducir en una secuencia de tautologías proposicionales cuantificadas que tendrán pruebas polinómicamente acotadas en $T^i_2$ .

• Si $P$ es cualquier sistema de prueba proposicional cuya consistencia es demostrable en $T^i_2$ entonces $G_i$ simula polinómicamente $P$ .

$S_2$ es la unión de sus fragmentos finitamente axiomatizables $T^i_2$ . Esto significa que $S_2$ demuestra la coherencia de cada fragmento $G_i$ pero, por otro lado, si demostró la consistencia del cálculo proposicional cuantificado completo $G$ implicaría que $G_i$ simula polinómicamente $G$ para algunos $i$ y se supone que es falso. Dicho de otro modo, el $\forall\Delta^b_1$ -consecuencias de $S_2$ (así como $S_2$ sí mismo) no se suponen finitamente axiomatizables.

La correspondencia de las teorías y los sistemas de pruebas proposicionales también se extiende a las clases de complejidad. Los conjuntos definibles por $\Sigma^b_i$ fórmulas del modelo estándar de aritmética son exactamente las que se pueden calcular en el $i$ -nivel $\Sigma^P_i$ de la jerarquía polinómica. Las teorías $T^i_2$ tienen inducción para $\Sigma^b_i$ fórmulas, y su total demostrable $\Sigma^b_{i+1}$ -Las funciones definibles son $\mathrm{FP}^{\Sigma^P_i}$ por lo que estas teorías corresponden a niveles de la jerarquía polinómica. Por el lado proposicional, la satisfabilidad de $\Sigma^q_i$ fórmulas es un $\Sigma^P_i$ -problema completo. Tomando la unión, $S_2$ corresponde a la jerarquía polinómica completa $\mathrm{PH}$ . Sin embargo, la clase de complejidad correspondiente a $G$ es $\mathrm{PSPACE}$ ya que la satisfacción de fórmulas proposicionales cuantificadas no restringidas es $\mathrm{PSPACE}$ -completa. Así, preguntando $S_2$ para demostrar la consistencia de $G$ está en el mismo espíritu que colapsar $\mathrm{PSPACE}$ a $\mathrm{PH}$ (y por tanto a algún su nivel fijo). (No me cite. Aunque el colapso del $T^i_2$ jerarquía sí implica el colapso de $\mathrm{PH}$ Sin embargo, en el caso de los sistemas de prueba proposicionales, esta analogía no es muy clara).

Para dar también un límite superior a la fuerza de consistencia, la consistencia de $G$ y, por tanto, de FPA, es demostrable en las teorías correspondientes a $\mathrm{PSPACE}$ . La teoría más conocida es la de Buss $U^1_2$ que es una extensión de "segundo orden" de $S_2$ con comprensión para conjuntos acotados definidos por fórmulas acotadas sin cuantificadores de segundo orden, y longitud inducción para $\Sigma^1_1$ -fórmulas. Obsérvese que aquí las cosas se complican mucho, ya que los objetos de primer orden de $U^1_2$ corresponden a objetos de segundo orden de FPA, y los objetos de segundo orden de $U^1_2$ no tienen análogos en FPA. Alan Skelley formuló una teoría equivalente (técnicamente, RSUV-isomorfa) $W^1_1$ . Esto es sintácticamente un tercer orden aritmética, y es más directamente comparable a la FPA (ya que los números de una teoría corresponden a los números de la otra, y los conjuntos corresponden a los conjuntos). $W^1_1$ demuestra la coherencia de $G$ y, por tanto, de FPA.

Answer 2

EDIT: Me retracto. Véanse los comentarios.

Afirmo que la respuesta es "Sí", es decir, que FPA (y $IΔ_0+Ω_1$ ) puede demostrar la consistencia de $G$ .

Consideremos el sistema de pruebas $G$ como se encuentra en Logical Foundations of Proof Complexity de Stephen Cook y Phuong Nguyen, con dos simplificaciones: axiomas $A→A$ debe tener $A$ atómica; y la fórmula objetivo para existencial-derecha o universal-izquierda debe ser $⊤$ o $⊥$ .

$<e>$ representa la secuencia unaria que enumera precisamente un elemento, $<e_1,e_2>$ o simplemente $e_1,e_2$ es una secuencia que enumera dos elementos, etc. y si $s_1,s_2$ son secuencias, entonces que su concatenación sea $s_1⌢s_2$ . En $IΔ_0+Ω_1$ las propiedades habituales de las secuencias y concatenaciones pueden demostrarse y se asumirán aquí.

Las fórmulas atómicas son constantes $⊤$ y $⊥$ y variables $A, B, C, .... , x, y, z, ...$ Si $ϕ$ y $ψ$ son fórmula, y $X$ es una variable, $¬ϕ, (ϕ∨ψ), (ϕ∧ψ), ∃Xϕ,$ y ∀Xϕ también son fórmulas. No se permite que una variable acotada aparezca libre fuera del ámbito del cuantificador - p. ej. $((X∧A)∨∀Xϕ)$ no está permitido - ni tampoco estar en el ámbito de un cuantificador que lo utilice de nuevo - p.ej. $∀X(ϕ∧∃Xψ)$ no está permitido. Las secuencias de fórmulas (tal vez vacías) se representarán con letras griegas mayúsculas como $Γ$ y $Δ$ . Las secuencias son de la forma $Γ→Δ$ es decir, en efecto, los secuentes son una secuencia de dos elementos, siendo ambos elementos secuencias de fórmulas. Las variables limitadas y libres de una fórmula se definen como de costumbre. Sea $free(ϕ)$ y $bnd(ϕ)$ sea el conjunto de todas las variables libres y acotadas, respectivamente, de una fórmula $ϕ$ . Por la condición anteriormente expuesta, $bnd(ϕ)∩free(ϕ)=∅$ .

Los axiomas son:

$A→A$ , $→⊤$ , $⊥→$

Como ya se ha señalado $A$ debe ser una fórmula atómica.

Donde A y B son fórmulas cualesquiera, las reglas de deducción son:

Debilitamiento

A la izquierda: ${\dfrac{\Gamma\rightarrow \Delta}{A,\Gamma\rightarrow\Delta}}$ Bien: ${\dfrac{\Gamma\rightarrow \Delta}{\Gamma\rightarrow\Delta,A}}$

Intercambio

A la izquierda: ${\dfrac{\Gamma_1 ,A,B,\Gamma_2\rightarrow\Delta}{\Gamma_1 ,B,A,\Gamma_2\rightarrow\Delta}}$ Bien: ${\dfrac{\Gamma\rightarrow\Delta_1 ,A,B, \Delta_2}{\Gamma \rightarrow\Delta_1 ,B,A, \Delta_2}}$

Contracción

A la izquierda: ${\dfrac{\Gamma ,A,A\rightarrow\Delta}{\Gamma ,A\rightarrow\Delta}}$ Bien: ${\dfrac{\Gamma\rightarrow\Delta ,A,A}{\Gamma\rightarrow\Delta,A}}$

¬

A la izquierda: ${\dfrac{\Gamma\rightarrow\Delta,A}{\neg A,\Gamma\rightarrow\Delta}}$ Bien: ${\dfrac{A,\Gamma\rightarrow\Delta}{\Gamma\rightarrow\Delta,\neg A}}$

∧

A la izquierda: ${\dfrac{A,B,\Gamma\rightarrow\Delta}{(A \land B),\Gamma\rightarrow\Delta}}$ Bien: ${\dfrac{\Gamma\rightarrow\Delta,A\qquad\Gamma\rightarrow \Delta,B}{\Gamma\rightarrow\Delta,(A\land B)}}$

∨

A la izquierda: ${\dfrac{A,\Gamma\rightarrow\Delta\qquad B,\Gamma\rightarrow \Delta}{(A \lor B),\Gamma\rightarrow\Delta}}$ Bien: ${\dfrac{\Gamma\rightarrow\Delta,A,B}{\Gamma\rightarrow\Delta,(A \lor B)}}$

Corte

${\dfrac{\Gamma\rightarrow \Delta,A\qquad A,\Gamma\rightarrow\Delta}{\Gamma\rightarrow\Delta}}$

∀

A la izquierda: ${\dfrac{A(c),\Gamma\rightarrow\Delta}{\forall x\, A(x) ,\Gamma\rightarrow\Delta}}$ Bien: ${\dfrac{\Gamma\rightarrow\Delta,A(p)}{\Gamma\rightarrow\Delta,\forall x\,A(x)}}$

∃

A la izquierda: ${\dfrac{A(p), \Gamma\rightarrow\Delta}{\exists xA(x) ,\Gamma\rightarrow\Delta}}$ Bien: ${\dfrac{\Gamma\rightarrow\Delta,A(c)}{\Gamma\rightarrow\Delta,\exists x\,A(x)}}$

En las últimas normas $p$ es una variable libre, llamada variable propia, que no debe aparecer en el secuente inferior, y $c$ se denomina fórmula objetivo, que como ya se ha indicado se limita a $⊤$ y $⊥$ .

A $G$ prueba $π$ de longitud $n$ de un secuente $q$ es una secuencia de secuencias tal que para todo $i≤n$ , $π(i)$ es un axioma o $∃j,k<i$ s.t. $π(i)$ puede deducirse de $π(j)$ y quizás $π(k)$ utilizando una de las Reglas de Deducción, y tal que $π(n)=q$ . Desde $n$ puede deducirse del contexto o carece de importancia, se omitirá su mención, y puesto que todas las pruebas serán $G$ pruebas, mención de $G$ se suprimirá, por lo que hablaremos simplemente de una prueba $π$ de un secuente $q$ . Si $π$ es una prueba, entonces para cada secuente $q$ que aparece en la secuencia, existe una subsecuencia de $π$ que es una prueba de $q$ .

Sea $free(π)$ sea el conjunto de variables que aparecen libres en alguna parte de una prueba $π$ , $eigen(π)$ el conjunto de variables propias eliminadas por $∀$ Derecha o $∃$ Izquierda en $π$ y $var(π)$ las variables, libres o ligadas, que aparecen en $π$ . Claramente, $eigen(π)⊆free(π)⊆var(π)$ .

En $IΔ_0+Ω_1$ es fácil contar el número total de caracteres de una fórmula $ϕ$ un secuente $q$ o una prueba $π$ y esta capacidad y ciertas propiedades sobre esta función $tlen$ se asumirá sin pruebas. Por ejemplo, se asumirá sin pruebas que si $π$ es la prueba $π'$ con el secuente $q$ deducido como paso adicional, es decir, si $π=π'⌢q$ entonces $tlen(π)≥tlen(π')+tlen(q)$ .

Def 1. Definir la forma normal de negación $ϕ^*$ de una fórmula $ϕ$ por recursividad:

$ϕ^*=ϕ$ si $ϕ$ es atómico

$(ϕ∧ψ)^*=ϕ^*∧ψ^*$

$(ϕ∨ψ)^*=ϕ^*∨ψ^*$

$(∃xϕ(x))^*=∃x(ϕ(x))^*$

$(∀xϕ(x))^*=∀x(ϕ(x))^*$

$(¬ϕ)^*=¬ϕ$ si $ϕ$ es atómico

$(¬¬ϕ)^*$ = $ϕ$

$(¬(ϕ∧ψ))^*=((¬ϕ)^*∨(¬ψ^*))$

$(¬(ϕ∨ψ))^*=((¬ϕ)^*∧(¬ψ^*))$

$(¬∃xϕ(x))^*=∀x(¬ϕ(x))^*$

$(¬∀xϕ(x))^*=∃x(¬ϕ(x))^*$

Si $ϕ^*=ϕ$ entonces decimos $ϕ$ está en forma normal de negación. Un signo de negación en $ϕ^*$ debe aparecer directamente delante de una fórmula atómica.

Porque el $^*$ como máximo añade un signo de negación antes de cada variable, como máximo duplica el número total de caracteres de una fórmula. Así, $tlen(ϕ^*)≤2(tlen(ϕ))$ .

Observaciones 2. Para cualquier fórmula $ϕ$

1/ $(ϕ^* )^*=ϕ^*$

2/ $(¬(¬ϕ)^* )^*=ϕ^*$

Obsérvese que las barreras libres y ligadas no cambian bajo $^*$ por lo que para cualquier fórmula $ϕ$ las variables libres (o ligadas) son todas iguales en: $ϕ, ¬ϕ, ϕ^*,$ y $(¬ϕ)^*$ .

Def 3. Para una secuencia de fórmulas $Γ=ϕ_1,ϕ_2,...,ϕ_k$ defina

$¬Γ=¬ϕ_1,¬ϕ_2,...,¬ϕ_k$

$Γ^*=ϕ_1^*,ϕ_2^*,...,ϕ_k^*$

Así $(¬Γ)^*=(¬ϕ_1 )^*,(¬ϕ_2 )^*,...,(¬ϕ_k )^*$ .

En $Γ$ es la secuencia vacía (es decir $k=0$ ), entonces $¬Γ$ y $Γ^*$ son también las secuencias vacías.

Para un secuente $Γ→Δ$ defina $(Γ→Δ)^*=(¬Γ)^*⌢Δ^*$ .

Se supondrán algunos hechos básicos sobre los árboles binarios etiquetados, que al igual que con las secuencias pueden representarse y demostrarse fácilmente en $IΔ_0+Ω_1$ . Por ejemplo, cuando $T_1$ y $T_2$ son árboles binarios finitos, se pueden formar nuevos árboles binarios finitos con raíz $η$ y los niños ambos $T_1$ y $T_2$ o simplemente $T_1$ . $T_1$ y (si está presente) $T_2$ se denominan árboles hijos del nuevo árbol. En el primer caso, representamos el nuevo árbol mediante $[η;T_1;T_2]$ y en el segundo $[η;T_1]$ . Si un árbol consta sólo de una raíz $η$ y sin hijos, represéntelo como $[η]$ . Si $η$ se etiqueta $ϕ$ podemos abusar de la notación y escribir $[ϕ;T_1;T_2]$ y $[ϕ;T_1]$ y $[ϕ]$ . Decimos que el tamaño de un árbol binario $T$ es el número de sus nodos y escribir $size(T)$ .

Def 4. Un árbol semántico o semárbol $T$ es un árbol binario finito etiquetado con fórmulas tales que:

1/ La raíz de $T$ se etiqueta con una fórmula $ϕ$ en forma normal negativa

2/ Las hojas de $T$ están etiquetados con una fórmula atómica o su negación

3/ Las posibles ramas con sus etiquetas son las siguientes:

Partir: Padre: $ψ$ Hijos: $ψ$ y $ψ$

$∧$ : Padre: $(ψ_1∧ψ_2)$ Hijos: $ψ_1$ y $ψ_2$

$∨$ : Padre: $(ψ_1∨ψ_2)$ Hijos: $ψ_1$ y $ψ_2$

$∃$ : Padre: $∃xψ(x)$ Niño: $ψ(c)$ donde $c$ es $⊤$ o $⊥$

$∀$ : Padre: $∀xψ(x)$ Niño: $ψ(E)$ donde $E$ es alguna variable

4/ Si una variable $E$ se introduce a través de un $∀$ se introduce así en todo el árbol exactamente una vez, y no aparece (libre o acotada) en $ϕ$

Establecer $root(T)$ a la fórmula que etiqueta la raíz de $T$ . $T$ se dice que es un semárbol para $ϕ$ si $root(T)=ϕ^*$ .

Obsérvese que no se da ninguna explicación para un padre de la forma $¬ψ$ ya que en las fórmulas en forma normal de negación, $¬$ sólo puede aparecer antes de una fórmula atómica. Esta omisión fuerza fórmulas de la forma $¬ψ$ para ser las etiquetas de las hojas.

Si una variable aparece en un semárbol $T$ debe aparecer o bien libre en la fórmula que etiqueta la raíz, o bien ser introducida (una y sólo una vez) a través de una fórmula $∀$ o ser una variable ficticia que aparece después de un signo de cuantificación. Establecer $free(T)$ para ser el conjunto de la primera, $intro(T)$ para el segundo, y $bnd(T)$ para el tercero. Por la condición 4/ y la condición sobre variables libres y acotadas en las fórmulas, $free(T)$ , $intro(T)$ y $bnd(T)$ deben ser disjuntos. También se establece $var(T)=free(T)∪intro(T)$ y $var^+ (T)=var(T)∪bnd(T)$ . Evidentemente, si una variable aparece en una hoja, debe pertenecer a $var(T)$ .

Prop 5. Sea $ϕ$ sea una fórmula en forma normal de negación, $v$ un conjunto de variables tales que $(free(ϕ)∪bnd(ϕ))∩v=∅$ . Supongamos que el número $n$ de elementos de $v$ es igual al número de cuantificadores universales en $ϕ$ . Entonces existe un semárbol $T$ para $ϕ$ con tamaño $≤tlen(ϕ)$ tal que $intro(T)=v$ . Además, si $ψ$ etiqueta un nodo del árbol, $tlen(ψ)≤tlen(ϕ)$ .

Prueba:

Supongamos que $ϕ$ es una fórmula atómica o su negación. Entonces $n=0$ y $v=∅$ . Establecer $T=[ϕ]$ .

Supongamos que $ϕ$ es de la forma $(ϕ_1∨ϕ_2)$ o $(ϕ_1∧ϕ_2)$ y partición $v$ en dos conjuntos $v_1$ y $v_2$ de cualquier manera, de forma que para ambos $i=1,2$ el número $n_i$ de elementos de $v_i$ es igual al número de cuantificadores en $ϕ_i$ . Por la hipótesis de inducción, tanto para $i=1,2$ existe un semárbol $T_i$ para $ϕ_i$ con tamaño $≤tlen(ϕ_i)$ tal que $intro(T_i)=v_i$ y, si $ψ$ etiqueta un nodo del árbol, $tlen(ψ)≤tlen(ϕ_i)$ . A continuación, establezca $T=[ϕ;T_1;T_2]$ .

Supongamos que $ϕ$ es de la forma $∃xϕ_1(x)$ . Entonces $ϕ_1(⊤)$ tendrá el mismo número de cuantificadores universales que $ϕ$ . Por la hipótesis de inducción, existe un semárbol $T_1$ para $ϕ_1(⊤)$ con tamaño $≤tlen(ϕ_1(⊤))$ tal que $intro(T_1)=v$ y, si $ψ$ etiqueta un nodo del árbol, $tlen(ψ)≤tlen(ϕ_1(⊤))$ . A continuación, establezca $T=[ϕ;T_1]$ .

Finalmente supongamos $ϕ$ es de la forma $∀xϕ_1 (x)$ . Elija cualquier elemento $E∈v$ y fijar $v^-=v∖{E}$ . Entonces, el número de elementos de $v^-$ es igual al número de cuantificadores universales en $ϕ_1 (E)$ por lo que, por la hipótesis de inducción, existe un semárbol $T_1$ para $ϕ_1(E)$ con tamaño $≤tlen(ϕ_1(E))$ tal que $intro(T_1)=v^-$ y, si $ψ$ etiqueta un nodo del árbol, $tlen(ψ)≤tlen(ϕ_1(E))$ . A continuación, establezca $T=[ϕ;T_1]$ y nota $intro(T)=intro(T')∪\{E\}=v$ . //

Llamar a algún árbol garantizado por la proposición anterior $\mathcal{B}(ϕ,v)$ .

Def 6. Una misión $σ$ sobre un conjunto de variables $v$ (quizás vacía) es una función de $v∪\{⊥,⊤\}$ a ${0,1}$ donde $σ(⊤)=1$ y $σ(⊥)=0$ . Sea $ι$ sea la asignación sobre el conjunto vacío, entonces $ι(⊤)=1$ y $ι(⊥)=0$ .

Una misión $σ$ se extiende a las negaciones de fórmulas atómicas de forma natural, utilizando

$σ(¬ϕ)=1-σ(ϕ)$

Por lo tanto, cualquier asignación en un conjunto $v$ con $var(T)⊆v$ puede extenderse a todas las hojas de un semárbol $T$ . A continuación, puede extenderse a todo el árbol de la siguiente manera, donde $ϕ$ es el padre y $ψ_1$ y $ψ_2$ son los hijos (en el caso de Split, $∨$ y $∧$ ) o $ψ$ es el hijo (en el caso de $∃$ y $∀$ ).

Dividir $: σ(ϕ)=σ(ψ_1)+σ(ψ_2)-σ(ψ_1)σ(ψ_2)$

$∧ : σ(ϕ)=σ(ψ_1)σ(ψ_2)$

$∨ : σ(ϕ)=σ(ψ_1)+σ(ψ_2)-σ(ψ_1)σ(ψ_2)$

$∃ : σ(ϕ)=σ(ψ)$

$∀ : σ(ϕ)=σ(ψ)$

En $η$ es un nodo de $T$ y $σ$ es una asignación, establece $σ_T(η)$ al valor asignado a ese nodo cuando $σ$ se amplía como se acaba de describir. Set $val_σ(T)=σ_T(η)$ donde $η$ es el nodo raíz de $T$ .

Observación 7. Sea $T$ sea un semárbol, y sea $σ,σ'$ ser asignaciones en $v_1,v_2$ respectivamente, donde $var(T)⊆v_1,v_2$ . Supongamos que $σ↾var(T)=σ'↾var(T)$ . Entonces $σ_T(η)=σ'_T(η)$ para cualquier nodo $η$ de $T$ y en particular $val_σ(T)=val_{σ' }(T)$ .

Def 8. Que $T$ y $T'$ sean semárboles. Decimos $T$ y $T'$ están separados si $free(T)∪free(T')$ , $intro(T)$ y $intro(T')$ son disjuntos.

Observaciones 9.

(1) Si $[η;T_1;T_2]$ es un semárbol, entonces $T_1,T_2$ están separados.

(2) Si $T$ y $[η;T_1]$ están separados, entonces también lo están $T,T_1$ . Y si $T$ y $[η;T_1;T_2]$ están separados, entonces también lo están $T,T_1$ y $T,T_2$ .

(3) Si $T$ y $T'$ están separados, entonces $var(T)∩var(T')=free(T)∩free(T')$ .

Def 10. Escriba $ϕ∼ψ$ si $ϕ^*=(¬ψ)^*$ .

Def 11. Let $T$ y $T'$ sean semárboles. Escriba $T∼T'$ si $root(T)∼root(T')$ .

Observaciones 12. Si $T∼T'$ entonces $free(T)=free(T')$ . Así que si además $T$ y $T'$ están separados, entonces $var(T)∩var(T')=free(T)$ .

Def 13. Sea $T$ sea un semárbol, $X∈free(T)$ y $c$ una constante. Escribe $T[X/c]$ para el árbol $T$ con cada aparición libre de $X$ sustituido por $c$ .

Observaciones 14. Si $T$ es un semárbol, $X∈free(T)$ y $c$ una constante, entonces $T[X/c]$ es un semárbol. Si además $root(T)=ϕ(X)$ entonces $root(T[X/c])=ϕ(c)$ Supongamos además $σ$ es una asignación en $var(T)$ y que $i=σ(X)$ . $i=0$ o $1$ por lo que existe una constante $c$ tal que $ι(c)=σ(X)$ . Para ello $c$ , $val_σ(T)=val_σ (T[X/c])$ .

Def 15. Sea $T$ y $T'$ sean semárboles con $free(T)=free(T')$ . $T$ y $T'$ son conjuntamente satisfacibles si existe una asignación $σ$ en $var(T)∪var(T')$ tal que para todas las asignaciones $τ$ en $var(T)∪var(T')$ si $τ↾free(T)=σ↾free(T)$ entonces $val_τ(T)=val_τ(T')=1$ .

Observación 16. Supongamos que $T$ y $T'$ son conjuntamente satisfacibles. Entonces existe una asignación $σ$ en $var(T)∪var(T')$ tal que $val_σ(T)=val_σ(T')=1$ .

Def 17. Sea $T$ sea un semárbol, y sea U $= U_0,U_1,...,U_k$ sea una secuencia de semárboles donde $U_0=T, U_k$ es un árbol sin ramas (es decir, sólo tiene un nodo), y para todo $i$ con $0≤i<k$ tampoco:

$U_{i+1}$ es un árbol hijo de $U_i$ o

$∃V$ tal que $V$ es un árbol hijo de $U_i$ y para alguna variable libre $E$ y alguna constante $c$ , $U_{i+1} =V[E/c]$ .

Llame a U un análisis de raíz a hoja de $T$ . Digamos que una subsecuencia $S_0,S_1,...,S_j$ de U es Split-limpiado si para todo $i$ con $0≤i≤k, U_i$ no aparece en la subsecuencia si y sólo si la raíz de $U_i$ es una rama de Split.

Observación 18. En el contexto de la definición anterior, la raíz de $U_k$ no puede ser una rama Split, por lo que $S_j=U_k$ .

Teorema 19. Sea $T$ y $T'$ sean semárboles separados con $T∼T'$ . Y supongamos $T$ y $T'$ son conjuntamente satisfacibles. Entonces existe un análisis de raíz a hoja U \= $U_0,U_1,...,U_k$ de $T$ y un análisis de raíz a hoja U' $= U'_0,U'_1,...,U'_{k' }$ de $T'$ y Subsecuencias limpiadas por división $S_0,S_1,...,S_j$ de U y $S'_0,S'_1,...,S'_j$ de U' tal que para todo $i$ con $0≤i≤j$

1/ $S_i$ y $S'_i$ son independientes

2/ $S_i ∼ S'_i$

3/ $S_i$ y $S'_i$ son conjuntamente satisfacibles.

Pf:

Si $T$ y $T'$ son árboles sin ramas (es decir, con un solo nodo), la conclusión es obvia.

Rama dividida .

Supongamos que la raíz de $T$ o $T'$ es una rama Split, WLOG la raíz de $T$ . Entonces $T$ es de la forma $[ϕ;T_1;T_2]$ donde $T_1$ y $T_2$ también son semárboles con raíces etiquetadas $ϕ$ . Establecer $f=free(T)$ . Nota para ambos $i=1,2$ , $free(T_i)=f$ Así que $var(T_i)=f∪intro(T_i)$ y $T_i,T'$ están separados.

Sea $σ$ sea una asignación en $var(T)∪var(T')$ tal que para todas las asignaciones $τ$ en $var(T)∪var(T')$ con $τ↾f=σ↾f$ , $val_τ(T)=val_τ(T')=1$ .

Supongamos que $T_1$ y $T'$ no son conjuntamente satisfacibles. Entonces existe la asignación $μ$ en $var(T_1)∪var(T')$ con $μ↾f=σ↾f$ pero $val_μ(T_1)=0$ o $val_μ(T')=0$ . Desde $μ↾f=σ↾f$ , $val_μ(T')=1$ . Esto obliga a $val_μ(T_1)=0$ .

Sea $τ'$ sea una asignación en $var(T_2)∪var(T')$ con $τ'↾f=σ↾f$ .

Establecer

$σ'=ι∪τ'↾(f∪intro(T_2)∪intro(T'))∪μ↾intro(T_1)$ .

A causa de la separación $σ'$ es una asignación bien definida en $var(T)∪var(T')$ . $σ'↾f=τ'↾f=σ↾f=μ↾f$ Así que $val_{σ'}(T)=val_{σ'}(T')=1$ . Desde $σ'↾intro(T_1)=μ↾intro(T_1)$ también $val_{σ' }(T_1)=0$ . Por la definición de asignación en una rama Split, $val_{σ'}(T_2)=1$ . Así $val_{τ'}(T_2)=1$ . Por lo tanto $T_2$ y $T'$ son conjuntamente satisfacibles.

Así que $T_1,T'$ o $T_2,T'$ son conjuntamente satisfacibles. Las otras condiciones son triviales, por lo que uno de estos pares satisface las condiciones del teorema, con un nodo menos, por lo que se aplica la hipótesis de inducción, y el prefijo $T$ al análisis raíz-hoja sin imprimación. Las subsecuencias limpiadas por Split siguen siendo las mismas, ya que la raíz de $T$ es una rama de Split.

En adelante, supongamos que las raíces de ambos $T$ y $T'$ no son ramas Split.

$∨$ rama .

Supongamos que la raíz de $T$ es un $∨$ rama. Entonces $T$ es de la forma $[(ϕ_1∨ϕ_2);T_1;T_2]$ donde $T_1$ y $T_2$ también son semárboles, con raíces etiquetadas como $ϕ_1,ϕ_2$ respectivamente, y $T'$ es de la forma $[(ψ_1∧ψ_2);T'_1;T'_2]$ donde $T'_1$ y $T'_2$ también son semárboles, con raíces etiquetadas como $ψ_1,ψ_2$ respectivamente, de forma que $ϕ_1∼ψ_1$ y $ϕ_2∼ψ_2$ . Nota $T_i,T'_j$ son independientes para cualquier $i,j=1,2$ .

Establecer $f=free(T)$ , $f_1=free(T_1)$ y $f_2=free(T_2)$ . Nota $f=free(T')$ , $f_1=free(T'_1)$ , $f_2=free(T'_2)$ y $f=f_1∪f_2$ .

Sea $σ$ sea una asignación en $var(T)∪var(T')$ tal que para todas las asignaciones $τ$ en $var(T)∪var(T')$ con $τ↾f=σ↾f$ , $val_τ(T)=val_τ(T')=1$ .

Si $T_1, T'_1$ son conjuntamente satisfacibles, aplicar la hipótesis de inducción y prefijar $T_1$ y $T'_1$ a las secuencias resultantes.

En caso contrario $T_1,T'_1$ no son conjuntamente satisfacibles. Entonces existe una asignación μ en $var(T_1)∪var(T'_1)$ con $μ↾f_1=σ↾f_1$ pero $val_μ(T_1)=0$ o $val_μ (T'_1)=0$ . Sea $τ'$ sea una asignación en $var(T_2)∪var(T'_2)$ con $τ'↾f_2=σ↾f_2$ . Nota $μ↾(f_1∩f_2)=τ'↾(f_1∩f_2)$ .

Establecer $σ'=ι∪μ∪τ'$ que está bien definido ya que por separatividad,

$(var(T_1)∪var(T'_1))∩(var(T_2)∪var(T'_2)))=f_1∩f_2$ .

$σ'↾(f_1∪f_2)=σ↾(f_1∪f_2)$ Así que $val_{σ'}(T)=val_{σ'}(T')=1$ . Por la definición de una asignación en un $∧$ rama, tanto $val_{σ'}(T'_1)=1$ y $val_{σ'}(T'_2)=1$ . Así $val_μ(T'_1)=1$ que obliga a $val_μ(T_1)=0$ y así $val_{σ'}(T_1)=0$ . Por la definición de una asignación en un $∨$ esto obliga a $val_{σ'}(T_2)=1$ . Así $val_{τ'}(T_2)=1$ . Por lo tanto $T_2$ y $T'_2$ son conjuntamente satisfacibles. Apliquemos ahora la hipótesis de inducción, y prefijemos $T_2$ y $T'_2$ a las secuencias resultantes.

$∧$ rama .

Por simetría.

$∃$ rama .

Supongamos que la raíz de $T$ es un $∃$ rama. Entonces $T$ es de la forma $[∃xϕ(x);T_1]$ donde $T_1$ es un semárbol, cuya raíz está etiquetada como $ϕ(c)$ para alguna constante $c$ y $T'$ es de la forma $[∀xψ(x);T'_1]$ donde $T'_1$ es un semárbol, cuya raíz está etiquetada como $ψ(E)$ para alguna variable $E∈intro(T')$ donde $E∉free(ψ(x))$ y $E∉var(T)$ . Claramente, $ϕ(c)∼ψ(c)$ .

Establecer $f=free(T)$ y $v=var(T)∪var(T')$ y $v-=v∖{E}$ . Nota $f=free(T')$ y $f=free(T_1)$ y $f∪{E}=free(T'_1)$ donde $E∉f$ .

Desde $T,T'$ son conjuntamente satisfacibles, existe una asignación $σ$ en $v$ s.t. para todas las asignaciones $τ$ en $v$ con $τ↾f=σ↾f$ , $val_τ(T)=val_τ(T')=1$ . Establecer $T''_1=T'_1[E/c]$ y $σ'=ι∪σ↾v-$ . Nota $f=free(T''_1)$ y $v-=var(T_1)∪var(T''_1)$ y $σ'$ es una asignación en $v-$ . Sea $τ'$ sea una asignación en $v-$ s.t. $τ'↾f=σ'↾f$ . Establecer $τ''$ a $τ'∪\{(E,ι(c))\}$ . Entonces $τ''$ es una asignación en $v$ s.t. $τ''↾f=σ↾f$ . Así que $val_{τ''}(T)=val_{τ''}(T')=1$ . Pero entonces $val_{τ''}(T_1)=1$ y $val_{τ''}(T'_1)=1$ . Esta última conjunción, junto con la observación de que $τ''(E)=ι(c)$ implica $val_{τ''}(T''_1)=1$ Así que $val_{τ'} (T_1)=1$ y $val_{τ'}(T''_1)=1$ . Así $T_1$ y $T''_1$ son conjuntamente satisfacibles, y claramente $T_1∼T''_1$ . Aplique ahora la hipótesis de inducción, y el prefijo $T_1$ y $T''_1$ a las secuencias resultantes.

$∀$ rama.

Por simetría. //

Corolario 20. Sea $T,T'$ sean semárboles separados con $T∼T'$ . Entonces $T,T'$ no son conjuntamente satisfacibles.

Pf:

Supongamos que fueran conjuntamente satisfacibles. Por el teorema anterior existen semárboles $U,U'$ s.t. ambos son sin ramas, $U∼U'$ y $U,U'$ son conjuntamente satisfacibles. Por las condiciones primera y segunda, las raíces de $U$ y $U'$ deben ser etiquetados por $E$ y $¬E$ para alguna fórmula atómica $E$ . Por la tercera condición existe $σ$ en $free(U)$ tal que $val_σ(U)=val_σ(U')=1$ . Pero esto es imposible. //

Def 21. Sea $t = T_1,...,T_k$ sea una secuencia de semárboles. Conjunto $val_σ(t)=1$ si $∃i(val_σ(T_i)=1)$ y $=0$ de lo contrario. Si $val_σ(t)=1$ para todas las asignaciones $σ$ en $∪_{i=1}^m var(T_i)$ escribe $val(t)=1$ .

Nota $k=0$ entonces $val(t)=0$ .

Teorema 22. Supongamos que $π$ es una prueba en forma de árbol donde cada instancia de una variable libre es como una variable propia. Sea $w$ sea el número de aplicaciones del debilitamiento en $π$ , dejemos que $β_i$ sea la fórmula introducida por el $i$ según un orden fijo, y que $w_i$ sea el número de cuantificadores universales en $β_i$ ( $1≤i≤w$ ). Sea $z_1,...,z_w$ sea un conjunto de conjuntos de variables disjuntos por pares tal que el número de elementos en cada uno de ellos $z_i$ es igual a $w_i$ y tal que $z_i∩var(π)=∅$ . Para cualquier subprueba $π'$ de $π$ set $weak(π') =⋃z_i$ donde la unión se realiza sobre cada $i$ de forma que $i$ l debilitamiento se produce en $π'$ .

Sea $q$ sea un secuente en la secuencia de prueba de $π$ donde $q=Γ→Δ=ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$ . Y que $q*=ψ_1,...,ψ_m$ . Deje también que $π_1$ sea la subprueba de $q$ en $π$ . Entonces existe una secuencia de semárboles $t=T_1,T_2,...,T_m$ tal que:

1/ cada uno $T_i$ es un semárbol para $ψ_i$

2/ $val(t)=1$

3/ $∑_{i=1}^m size(T_i)≤tlen(π_1)$

4/ Para todos $i,j(i≠j)$ , $T_i$ y $T_j$ son independientes

5/ $intro(T_i)⊆eigen(π_1)∪weak(π_1)$ para todos $i$

6/ Si $ϕ$ es una etiqueta de un nodo de $T_i$ entonces $tlen(ϕ)≤tlen(ψ_i)$ para todos $i$

Prueba:

Mostramos cómo construir un semárbol que satisfaga las seis condiciones para cada axioma y regla de deducción, por inducción sobre los pasos de $π_1$ limitado por la prueba $π$ .

Caso 1 . $q=A→A$ para la fórmula atómica $A$ . Nota $(A→A)*=<¬A,A>$ . Sea $T_1$ sea el semárbol con la raíz etiquetada $¬A$ y sin hijos, $T_2$ el semárbol con la raíz etiquetada $A$ y sin hijos. Entorno $t=T_1,T_2$ claramente $val_σ (t)=1$ para todas las asignaciones en $var(T_1)$ . Si $π_1$ es una prueba de $q$ , $π_1$ debe contener $q$ Así que $tlen(π_1)≥3≥(1+1)=size(T_1)+size(T_2)$ . Por fin, $T_1, T_2$ están vacuamente separadas.

Caso 2 . $q=⊥→$ o $q=→⊤$ . Entonces $q*=<¬⊥>$ o $q*=<⊤>$ . Ambos tienen semárboles triviales de tamaño 1 con sólo una raíz, la raíz etiquetada como $¬⊥$ o $⊤$ . Todas las condiciones 1/ a 6/ se cumplen fácilmente.

Para los casos de inducción, mediante sustituciones apropiadas que no aumenten la longitud del número de caracteres de la prueba, podemos suponer que cada variable propia que aparece en $π$ se elimina exactamente una vez mediante $∀$ -izquierda o $∃$ -derecha.

Caso 3 . Debilitamiento a la izquierda. Supongamos que $π_1=π_1'⌢<A,Γ→Δ>$ donde $π_1'$ contiene el secuente $Γ→Δ$ . Sea éste el $k$ ón del debilitamiento.

Obviamente, el $k$ l debilitamiento no está presente en $π_1'$ .

Sea $q'=Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$ . Nota $q^*=<(¬A)^*>⌢(q')^*$ . Supongamos que $t'=T_1,...,T_m$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q',t'$ . Establecer $T_0=\mathcal{B}((¬A)^*,z_k)$ de la proposición 5 y $t=T_0⌢t'$ .

Trivialmente $val(t)=1$ desde $val(t')=1$ .

$size(T_0)≤tlen((¬A)^*)$ Así que

$∑_{i=0}^m size(T_i)≤tlen(π_1')+tlen((¬A)^*)≤tlen(π_1)$ .

$intro(T_i)⊆eigen(π_1')∪weak(π_1')$ para todos $i(1≤i≤m). intro(T_0)=z_k$ y por suposición $z_k∩var(π)=∅$ . Así que $z_k∩eigen(π_1')=∅$ . Y desde el $k$ l debilitamiento no está presente en $π_1'$ , $z_k∩weak(π_1')=∅$ . Así $intro(T_0)∩intro(T_i)=∅$ para todos $i(1≤i≤m)$ . Además, $z_k∩free(ϕ_i)=∅$ para todos $i(1≤i≤m)$ ya que $free(ϕ_i)⊆var(π)$ Por último, supongamos $E∈free(T_0)∩intro(T_i)$ para algunos $i(1≤i≤m)$ . $E∈free(T_0)$ implica $E∈free(A)$ Así que $E$ aparece en el último paso de la subprueba $π_1$ . Por supuesto, esta instancia de $E$ como variable propia. Por lo tanto, si $E∈eigen(π_1')$ entonces $E$ se elimina dos veces como variable propia en $π$ una contradicción. Por lo tanto $E∈weak(π_1')$ pero esto contradice cada una de las $z_i$ siendo disjuntos de $var(π)$ . Así $T_0$ y $T_i$ son independientes para todos $i≠0$ .

Si $ϕ$ es la etiqueta de un nodo de $T_0$ entonces $tlen(ϕ)≤tlen((¬A)^*)$ .

Caso 4 . Debilitando a la derecha.

Como debilitamiento de la izquierda.

Caso 5 . Intercambio.

Trivial.

Caso 6 . Contracción a la izquierda. Supongamos que $π_1=π_1'⌢<Γ,A→Δ>$ donde $π_1'$ contiene el secuente $Γ,A,A→Δ$ .

Sea $q'=Γ,A,A→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$ con $ϕ_{k-1}=ϕ_k=A$ . Supongamos que $t'=T_1,...,T_m$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q',t'$ . Defina $T'=[(¬A)^*;T_{k-1};T_k]$ con $(¬A)^*$ siendo una rama Split, y establecer $t=T_1,...,T_{k-2},T',T_{k+1},...,T_m$ .

Caso 7 . Contracción Derecha.

Como Contracción Izquierda.

Caso 8 . $¬$ A la izquierda.

Trivial ya que $(¬¬A)^*=A^*$ Así que $(¬A,Γ→Δ)^*$ simplemente reorganiza el orden de la secuencia $(Γ→Δ,A)^*$ .

Caso 9 . $¬$ Bien.

También trivial.

Caso 10 . $∧$ A la izquierda. Supongamos que $π_1=π_1'⌢<(A∧B),Γ→Δ>$ donde $π_1'$ contiene el secuente $A,B,Γ→Δ$ .

Sea $q'=A,B,Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$ con $ϕ_1=A$ y $ϕ_2=B$ . Supongamos que $t'=T_1,...,T_m$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q',t'$ . Defina $T'=[(¬(A∧B))^*;T_1;T_2]$ donde la raíz es un $∨$ Rama, y establezca $t=T',T_3,...T_m$ .

Caso 11 . $∧$ De acuerdo. Supongamos que $π_1=π_A'⌢π_B'⌢Γ→Δ,(A∧B)$ donde $π_A'$ contiene el secuente $Γ→Δ,A$ y $π_B'$ el secuencial $Γ→Δ,B$ .

Porque $π$ es una prueba en forma de árbol, $π_A'$ y $π_B'$ son disjuntos.

Sea $q_A'=Γ→Δ,A = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},A$ y que $q_B'=Γ→Δ,B = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},B$ . Deje también que $q_A^*=ψ_1,...,ψ_{m-1},A^*$ y $q_B^*=ψ_1,...,ψ_{m-1},B^*$ . Supongamos que $u=U_1,U_2,...,U_m$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q_A',u$ . Supongamos además $v=V_1,V_2,...,V_m$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q_B',v$ . Para $1≤i≤m-1$ configure $T_i=[ψ_i;U_i;V_i]$ donde la raíz es una Split Branch, y establecer $T_m=[(A^*∧B^*);U_m;V_m]$ . El número de nuevos nodos es $m$ inferior a la longitud del se Por suposición $intro(U_i)⊆eigen(π_A')∪weak(π_A')$ y $intro(V_i)⊆eigen(π_B')∪weak(π_B')$ para $i(1≤i≤m)$ . Pero $π_A',π_B'$ son disjuntos, por lo que $eigen(U_i)∩eigen(V_j)=∅$ para evitar que las variables propias se eliminen dos veces en la prueba $π$ . También porque $π_A',π_B'$ son disjuntos, $weak(π_A')∩weak(π_B')=∅$ . $eigen(π_A')∩weak(π_B')=∅$ mediante la construcción del $z_i$ y del mismo modo $eigen(π_B')∩weak(π_A')=∅$ . Así $intro(U_i)∩intro(V_j)=∅$ para todos $i,j(1≤i,j≤m)$ . Si $E∈free(V_i)$ para algunos $i(1≤i≤m)$ entonces $E∈free(π_B')$ y debe ser entonces una instancia de una variable propia en $π$ . Pero entonces $E∉eigen(π_A')$ . También $E∉weak(π_B')$ mediante la construcción del $z_i$ . Así que $E∉intro(U_i)$ para cualquier $i$ . Así, todos los $U_i,V_j$ están separados por pares, por lo que $T_i$ están separados por pares.

Caso 12 . $∨$ Izquierda y derecha.

En $∧$ Derecha e izquierda.

Caso 13 . Corta. Supongamos que $π_1=π_1'⌢Γ→Δ$ donde $π_R'$ contiene el secuente $Γ→Δ,A$ y $π_L'$ contiene el secuente $A,Γ→Δ$ .

Sea $q_R'=Γ→Δ,A = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},A$ y que $q_L'=A,Γ→Δ = A,ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1}$ . Deje también que $q_R^*=ψ_1,...,ψ_{m-1},A^*$ y $q_L^*=(¬A)^*,ψ_1,...,ψ_{m-1}$ . Supongamos que $u=U_1,...,U_{m-1},U_R$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q_R',u$ . Y supongamos $v=V_L,V_1,...,V_{m-1}$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q_L',v$ . Tenga en cuenta que $U_R∼V_L$ y el par $U_R,V_L$ están separados por el mismo argumento utilizado en $∧$ R Para $1≤i≤m-1$ configure $T_i=[ψ_i;U_i;V_i]$ donde la raíz es una Split Branch, y establecer $t=T_1,T_2,...,T_{m-1}$ . Establecer $v=∪_{i=1}^{m-1} var(T_i)$ , $v'=var(U_R)∪var(V_L)$ , $v+=v∪v'$ y $f=free(U_R)$ . $f=free(V_L)$ Así que $v'=f∪intro(U_R)∪intro(V_L)$ . Por separación, $(intro(U_R)∪intro(V_L))∩v=∅$ Así que

$intro(U_R)∪intro(V_L)⊆v+∖v⊆v+$ .

Supongamos que $val(t)≠1$ . Entonces $val_μ (t)=0$ para alguna asignación $μ$ en $v$ . Ampliar $μ$ a $v+$ de cualquier manera y llamar a esta nueva asignación $σ$ . Todavía $val_σ(t)=0$ . Pero $val(u)=val(v)=1$ Así que $val_σ(u)=val_σ(v)=1$ Así que $val_σ(U_R)=val_σ(V_L)=1$ . Sea $τ$ sea una asignación en $v+$ tal que $τ↾f=σ↾f$ . Establece τ'=ι∪τ↾(v+∖v)∪σ↾v, una asignación en v+. Entonces val_(τ' ) (u)=val_(τ' ) (v)=1. Obviamente $τ'↾v=σ↾v$ Así que $val_(τ')(t)=0$ . Así $val_(τ')(U_R)=val_(τ')(V_L)=1$ . Por construcción $τ'↾v'=τ↾v'$ Así que $val_τ (U_R)=val_τ (V_L)=1$ . Por lo tanto $U_R,V_L$ son conjuntamente satisfacibles, contradiciendo el Corolario 20. Así pues, $val(t)=1$ .

Caso 14 . ∀ Izquierda. Supongamos que $π_1=π_1'⌢∀xA(x),Γ→Δ$ donde $π_1'$ contiene el secuente $A(c),Γ→Δ$ con $c$ una constante.

Sea $q'=A(c),Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$ con $ϕ_1=A(c)$ . Supongamos que $t'=T_1,...,T_m$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q',t'$ . Establecer $T'=[(¬∀xA(x))*;T_1]$ y $t=T',...,T_m$ . Nota $(¬∀xA(x))^*=∃x(¬A(x))^*$ por lo que la raíz de $T'$ es un $∃$ rama, y así $T'$ es efectivamente un semárbol.

Caso 15 . $∀$ A la derecha. Supongamos que $π_1=π_1'⌢Γ→Δ,∀xA(x)$ donde $π_1'$ contiene el secuente $Γ→Δ,A(p)$ con $p$ una variable que no aparece en $Γ$ o $Δ$ .

Sea $q'=Γ→Δ,A(p)=ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$ con $ϕ_m=A(p)$ . Supongamos que $t'=T_1,...,T_m$ es una secuencia de semárboles que satisfacen las condiciones 1/ a 6/ para $q',t'$ . Establecer $T'=[(∀xA(x))^*;T_m]$ y $t=T_1,...,T_{m-1},T'$ . Nota $(∀xA(x))^*=∀x(A(x))^*$ por lo que la raíz de $T'$ es un $∀$ rama, y así $T'$ es efectivamente un semárbol. $p$ sólo puede utilizarse como variable propia una vez, por lo que $p∉eigen(π_1')$ . Sea $1≤i≤m-1$ . $p∉weak(π_1')$ mediante la construcción del $z_i$ Así que $p∉intro(T_i)$ . También $p∉free(T_i)$ porque $free(T_i)=free(ϕ_i)$ .así $T'$ es independiente de cada uno de los $T_i$ (donde $1≤i≤m-1$ ).

Establecer $v=∪_{j=1}^m var(T_j)$ . Nota $v=∪_{j=1}^{m-1} var(T_j)∪var(T')$ desde $var(T_m)=var(T')$ . Sea $σ$ sea una asignación en $v$ . Entonces, por suposición, $val_σ(t')=1$ . Si $val_σ(T_j)=1$ para algunos $j(1≤j≤m-1)$ entonces $val_σ(t)=1$ . De lo contrario, $val_σ(T_m)=1$ así que por la definición de una asignación en un $∀$ rama, $val_σ(T')=1$ en cuyo caso $val_σ(t)=1$ .

Caso 16 . $∃$ Izquierda y derecha.

En $∀$ Derecha e izquierda. //

El secuente contradictorio es el secuente vacío, $ → $ .

Corolario 23. No hay prueba de contradicción.

Pf:

Supongamos que $π$ es una prueba. Se puede suponer que todas las variables libres son eigenvariables, porque si una variable libre no fuera una eigenvariable, habría que eliminarla por Cut. Pero entonces se podría sustituir a lo largo de la prueba por una constante.

Sea $e$ sea la secuencia vacía. Entonces $( → )^* = e$ . Por el teorema, $val(e)=1$ . Pero $val(e)=0$ . //

Answer 3

Esto es demasiado largo como comentario, pero puede considerarse una respuesta en el sentido de que da una mejor respuesta parcial a la pregunta (aunque no habrá ninguna justificación). Para entenderlo mejor puedes consultar mi respuesta anterior y leer los comentarios a la misma.

Relajar la restricción de que la fórmula objetivo de $\exists$ -Derecha y $\forall$ -La izquierda debe ser $\top$ o $\bot$ como sigue. Considere la regla

${\dfrac{\Gamma\rightarrow\Delta,A(t)}{\Gamma\rightarrow\Delta,\exists x\,A(x)}}$

siempre que cualquier variable en $t$ no se produce en $\Gamma$ o $\Delta$ . (Del mismo modo para $\forall$ -Izquierda). Observe que esta regla incluye los casos en que $t$ es $\top$ o $\bot$ ya que no hay ninguna variable en $\top$ o $\bot$ . Llama a este nuevo sistema $G-$ .

Afirmo (no lo justifico aquí) que aún se puede establecer una condición de separabilidad de los semárboles para las fórmulas demostrables en $G-$ y así $I\Delta_0 + \Omega_1$ demuestra la coherencia de $G-$ .

La relajación no parece completamente trivial, ya que las variables en $t$ mai se producen en $\exists x\,A(x)$ . Así, por ejemplo, se puede deducir:

${\dfrac{\rightarrow x \iff x}{\rightarrow\exists y (x \iff y)}}$

Así que $G-$ permite la demostración directa del ejemplo de Emil $A_n$ así que aparentemente $G$ [donde la fórmula objetivo se limita a $\top$ o $\bot$ ] no simula polinomialmente $G-$ .

Por desgracia, el ejercicio VII.3.6 parece fallar irremediablemente, o al menos no veo la manera de repararlo de forma significativa. Así que no puedo hacer ninguna afirmación sobre la fuerza de $G-$ en comparación con $G$ .