Cálculo de Deducción Natural Que Funciona por Vacío Estructuras

Question

Actualmente, estoy tratando con el cálculo de deducción natural por Gentzen. Este cálculo nos da reglas para manipular los llamados sequents.

Definición. Si $\Gamma$ es un conjunto de fórmulas y $\phi$ una fórmula, a continuación, $\Gamma\vdash\phi$ se llama un secuente.

Las reglas de este cálculo de deducción natural son:

• Hipótesis. $$ \begin{array}{c} \hline \Gamma\vdash\phi \end{array}\text{, donde $\phi\in\Gamma$} $$
• Reglas para $\land$. $$ \text{Introducción: } \begin{array}{c} \Gamma\vdash A\quad\Gamma\vdash B\\ \hline \Gamma\vdash A\land B \end{array}\qquad\qquad\text{Eliminación: } \begin{array}{c} \Gamma\vdash A\land B\\ \hline \Gamma\vdash A\quad\Gamma\vdash B \end{array} $$
• Reglas para $\lor$. $$ \text{Introducción: } \begin{array}{c} \Gamma\vdash A\\ \hline \Gamma\vdash A\lor B \end{array} \quad \begin{array}{c} \Gamma\vdash B\\ \hline \Gamma\vdash A\lor B \end{array} \qquad\text{Eliminación: } \begin{array}{c} \Gamma\vdash A\lor B\quad\Gamma\cup \{A\}\vdash C\quad\Gamma\cup \{B\}\vdash C\\ \hline \Gamma\vdash C \end{array} $$
• Reglas para $\rightarrow$.

$$ \text{Introducción: } \begin{array}{c} \Gamma\cup \{A\}\vdash B\\ \hline \Gamma\vdash A\rightarrow B \end{array}\qquad\qquad\text{Eliminación: } \begin{array}{c} \Gamma\vdash A\rightarrow B\quad\Gamma\vdash A\\ \hline \Gamma\vdash B \end{array} $$

• Reglas para $\neg$.

$$ \text{Introducción: } \begin{array}{c} \Gamma \cup\{A\}\vdash\bot\\ \hline \Gamma\vdash \neg A \end{array}\qquad\qquad\text{$\neg\neg$ Eliminación: } \begin{array}{c} \Gamma\vdash \neg\neg A\\ \hline \Gamma\vdash A \end{array} $$

• La regla para $\bot$. $$ \text{Introducción: } \begin{array}{c} \Gamma\vdash A\quad\Gamma\vdash \neg A\\ \hline \Gamma\vdash\bot \end{array} $$

• Reglas para $\forall$. $$ \text{Introducción: } \begin{array}{c} \Gamma\vdash\phi[u/x]\\ \hline \Gamma\vdash\forall x(\phi) \end{array}\text{, $u$ no libre en $\Gamma$}\qquad\text{Eliminación: } \begin{array}{c} \Gamma\vdash\forall x(\phi)\\ \hline \Gamma\vdash\phi[t/x] \end{array} $$

• Reglas para $\exists$. $$ \text{Introducción: } \begin{array}{c} \Gamma\vdash\phi[t/x]\\ \hline \Gamma\vdash\exists x(\phi) \end{array}\qquad\text{Eliminación: } \begin{array}{c} \Gamma\vdash\exists x(A)\quad \Gamma\cup \{A[u/x]\}\vdash B\\ \hline \Gamma\vdash B \end{array} \text{, $u$ no libre en $\Gamma$ o $B$.} $$

• Reglas para $=$. $$ \text{Introducción: } \begin{array}{c} \hline \Gamma\vdash t = t \end{array} \qquad\text{Eliminación: } \begin{array}{c} \Gamma\vdash t_1=t_2\quad\Gamma\vdash A\\ \hline \Gamma\vdash A[t_1//t_2] \end{array} $$

(donde $A[t_1//t_2]$ es una fórmula que fue el resultado de la $A$ mediante la sustitución de todas o algunas apariciones libres de $t_1$$A$$t_2$)

Mi problema con este cálculo. El problema con el cálculo de la dada anteriormente es que sólo funciona para los no-vacío estructuras. Por lo tanto, hay frases como $\exists x(x=x)$, que es derivable en este cálculo, pero no se sostienen en el vacío de las estructuras. Pero estoy buscando un cálculo que funciona por vacío estructuras demasiado. Cuando digo "funciona por vacío estructuras demasiado", me explico: Si la demandada cálculo demuestra una frase, entonces esta frase debe mantener en todas las estructuras, también en el vacío de las estructuras.

Estoy buscando un cálculo que funciona para todas las estructuras, y no sólo por la falta de vacío estructuras.

Es por eso que mi pregunta es:

¿Cómo se puede modificar la ecuación dada anteriormente dicho que este nuevo cálculo funciona para todas las estructuras, y no sólo por la falta de vacío estructuras?

Temas relacionados con:

• deducción natural: la introducción del cuantificador universal y la eliminación del cuantificador existencial, explicó

• Completa el cálculo de la lógica de primer orden de trabajo para vaciar estructuras demasiado

Answer 1

La forma más fácil (y en mi opinión limpio) manera de hacer esto es para aumentar el contexto. En el secuente cálculo se presenta, tiene la mano izquierda de la sequent ser un conjunto $Γ$ de las fórmulas. En lugar de eso, usted necesita tener un conjunto de sentencias $S$ de los axiomas y de un contexto de la cadena de $Q$. $Q$ es una lista ordenada, cada elemento, ya sea condicional o contexto universal o existencialmente cuantificada variable. La idea es que todas las variables libres en el lado derecho de la sequent debe ser cuantificado en $Q$. Por lo que debe ser capaz de obtener el "$S;\forall x \vdash x=x$" pero no sólo "$S \vdash x=x$". Doy las normas precisamente a continuación.

Conectivo reglas

Las reglas para los operadores booleanos son esencialmente las mismas que antes, pero en lugar de modificar la mano izquierda $Γ$ de fórmulas, podemos modificar el contexto de la cadena. Así que aquí está el cambiar las reglas: $\def\imp{\rightarrow}$

[$S$ es cualquier frase conjunto, y $Q$ es cualquier cadena de contexto, y $A,B,C$ son cualquiera de las fórmulas.]

∨elim $\dfrac{S;Q \vdash A \lor B \quad S;Q \vdash A \imp C \quad S;Q \vdash B \imp C}{S;Q \vdash C}$

→sub $\dfrac{}{S;Q,A \vdash A}$ [Todas las variables libres en $A$ debe ser cuantificado en $Q$.]

→reformular $\dfrac{S;Q \vdash B}{S;Q,A \vdash B}$ [Todas las variables libres en $A$ debe ser cuantificado en $Q$.]

→intro $\dfrac{S;Q,A \vdash B}{S;Q \vdash A \imp B}$

→elim $\dfrac{S;Q \vdash A \quad S;Q \vdash A \imp B}{S;Q \vdash B}$

⊥elim $\dfrac{S;Q,A \vdash \bot}{S;Q \vdash \neg A}$

Cuantificador reglas

El cuantificador reglas se construyen de la misma manera, para capturar la estructura lógica de la misma manera como Fitch estilo de cálculo. Tenga en cuenta que este sistema va a prohibir la derivación de la sentencia con la variable de sombra (cuantificadores anidados que cuantificar a través de la misma variable). Elegí este enfoque, ya que es "más natural" y para evitar el problema de sustituibilidad (o de colisión de la libertad) que muchos libros de texto que describe Hilbert estilo de los sistemas tienen que lidiar con.

[$x,y$ son ninguna de las variables, y $t$ es cualquier término cuyas variables libres son todos los cuantificados en $Q$.]

∀repetir $\dfrac{S;Q \vdash A}{S;Q,\forall x \vdash A}$ [$x$ no debe ser cuantificado en $Q$ o usados (libre o unido) en $A$.]

∀intro $\dfrac{S;Q,\forall x \vdash A}{S;Q \vdash \forall x\ ( A )}$

∀elim $\dfrac{S;Q \vdash \forall x\ ( A )}{S;Q \vdash A[t/x]}$ [tenga en cuenta que $t$ debe existir (véase más arriba de lo $t$ debe ser).]

∃intro $\dfrac{S;Q \vdash A[t/x]}{S;Q \vdash \exists x\ ( A )}$ [$x$ no debe ser cuantificado en $Q$, y tenga en cuenta que $t$ debe existir.]

∃elim $\dfrac{S;Q \vdash \exists x\ ( A ) \quad S;Q,\forall y,A[y/x] \vdash B}{S;Q \vdash B}$ [$y$ no debe ser utilizado en $B$]

Axioma de igualdad y de reglas

Finalmente, hemos de modificar ligeramente las reglas de los axiomas y de la igualdad, de modo que no se metan con el contexto de la cadena.

axioma $\dfrac{}{S \cup \{A\};{} \vdash A}$

=intro $\dfrac{}{S;Q \vdash t=t}$ [Todas las variables libres en $t$ debe ser cuantificado en $Q$.]

Nota de pie de página

En esta sección le doy el original existencial reglas que había en el lugar de los ∃elim regla anterior. No son preferibles porque involucran una restricción global y por lo que las reglas no se define una relación en sequents sino más bien una relación en todo el secuente-estilo de las pruebas, lo cual es indeseable desde el punto de un secuente cálculo era capturar toda la información necesaria sobre provability de una frase en una sola secuente.

∃elim $\dfrac{S;Q \vdash \exists x\ ( A )}{S;Q,\exists y \vdash A[y/x]}$ [$y$ no debe ocurrir en $Q$ en todos los pasos anteriores! (*)]

∃unbind $\dfrac{S;Q,\exists x \vdash A}{S;Q \vdash A}$ [$x$ no debe ser utilizado en $A$.]

∃repetir $\dfrac{S;Q \vdash A \quad S;Q,\exists x \vdash B}{S;Q,\exists x \vdash A}$ [$x$ no debe ser utilizado en $A$.]

(*) Se considera una prueba como una secuencia de la regla de las aplicaciones, y sólo cuando no hay ninguna regla anterior, la aplicación ha $x$ se producen como una variable cuantificada, podemos utilizar la ∃de elim regla para obtener $\exists x$ como parte de la cadena de contexto. Pensé que el 'global' de la naturaleza de esta regla era inevitable, sin algo equivalente a marcado a lo largo de toda la secuencia de los pasos anteriores en la prueba de la izquierda de la "$\vdash$", pero como se muestra arriba se puede evitar.

Answer 2

Hace la siguiente propuesta de trabajo? Por favor, dígame lo que piensa de la siguiente modificación de la ecuación dada en la pregunta. Si usted encuentra algún error, por favor dígame.

---

La solución es un sonido de tratar con variables libres.

Definición. Un secuente es una expresión de la forma $[V]\ \Gamma\vdash\phi$ donde

• $V$ es un conjunto finito de variables,
• $\Gamma$ es un conjunto de fórmulas, cada una de cuyas variables libres son elementos de $V$,
• $\phi$ es una fórmula cuyas variables libres son elementos de $V$.

Ahora podemos formular las reglas para $\forall, \exists$ $=$ como sigue:

• Reglas para $\forall$. $$ \text{Introducción: } \begin{array}{c} [V\cup\{u\}]\ \Gamma\vdash\phi[u/x]\\ \hline [V]\ \Gamma\vdash\forall x(\phi) \end{array}\text{ ($u\not\in V$)}\qquad\text{Eliminación: } \begin{array}{c} [V]\ \Gamma\vdash\forall x(\phi)\\ \hline [V]\ \Gamma\vdash\phi[t/x] \end{array} $$

• Reglas para $\exists$. $$ \text{Introducción: } \begin{array}{c} [V]\ \Gamma\vdash\phi[t/x]\\ \hline [V]\ \Gamma\vdash\exists x(\phi) \end{array}\text{ (donde cada variable libre que ocurren en $t$ es un elemento de $V$)}\qquad\text{Eliminación: } \begin{array}{c} [V]\ \Gamma\vdash\exists x(A)\quad [V\cup\{u\}]\ \Gamma\cup \{A[u/x]\}\vdash B\\ \hline [V]\ \Gamma\vdash B \end{array} \text{ ($u\not\in V$, $u$ no es libre en $B$)} $$

• Reglas para $=$. $$ \text{Introducción: } \begin{array}{c} \hline [V]\ \Gamma\vdash t = t \end{array} \qquad\text{Eliminación: } \begin{array}{c} [V]\ \Gamma\vdash t_1=t_2\quad[V]\ \Gamma\vdash A\\ \hline [V]\ \Gamma\vdash A[t_1//t_2] \end{array} $$

(donde $A[t_1//t_2]$ es una fórmula que fue el resultado de la $A$ mediante la sustitución de todas o algunas apariciones libres de $t_1$$A$$t_2$)

El proposicional fragmento puede ser formalizado como en el anterior, uno sólo tiene que escribir $[V]$ frente a cada secuente.

Answer 3

[Edit: Este post fue debido a una mala interpretación de ooooooo's del sistema, que requiere que todas las variables libres en el derecho de la sequent están en el conjunto de variables de la izquierda (como el mío, por lo que es vergonzoso, que yo me lo perdí). Que impide que mi segundo paso de ir a través de. Sin embargo, mi intuición no me dicen si su sistema está sano o no, pero se va a intentar demostrarlo. Esta es la izquierda justo para grabar.]

La siguiente prueba de la contradicción en ooooooo's sistema propuesto muestra que tiene un problema fundamental, que es que es incapaz de capturar correctamente el orden de la cadena de contexto, que es una secuencia en mi sistema propuesto. (Esto es aparte de la facilidad corregido el problema de que si no son constantes, entonces es incapaz de obtener el verdadero el enunciado "$\exists x\ ( \neg \bot )$".)

$[]\ Γ \vdash \forall y\ \exists x\ ( P(x,y) )$

$[]\ Γ \vdash \exists x\ ( P(x,y) )$ [∀elim]

$[u,v]\ Γ,P(u,y) \vdash P(u,y)$ [hyp]

$[u]\ Γ,P(u,y) \vdash \forall v\ ( P(u,v) )$ [∀intro] (*)

$[u]\ Γ,P(u,y) \vdash \exists x\ \forall v\ ( P(x,v) )$ [∃intro]

$[]\ Γ \vdash \exists x\ \forall v\ ( P(x,v) )$ [∃elim]

Básicamente, parece que la intención de la interpretación de un conjunto adicional de variables es que son universalmente cuantificado, por lo que (*) es el punto en el que un imprudente cuantificador interruptor se lleva a cabo, con "$\forall v$" saltando "$P(u,y) \rightarrow$".

Sin embargo, ahora que lo pienso más, la idea de capturar existencial eliminación a través de universal subcontextos (que implícitamente presente en el sistema original en la pregunta) debe proporcionar una forma para eliminar la naturaleza global de la ∃de elim regla en mi sistema, que voy a añadir a mi respuesta en un minuto.

Answer 4

En un universo, cada $\forall$ se convierte en verdadera y cada una de las $\exists$ se convierten en falso. Así que usted puede simplemente dividir cualquier teorema en dos casos, uno de los casos se supone que el universo está vacío y en un caso no. En el caso de que el universo está vacío, todo es reducible a la lógica proposicional. En el caso de que el universo no está vacío, puede volver a la original de la lógica. Introducir un universo en constante $U$ a representar si el universo está habitado.

Así que los axiomas se convierte en:

$$\frac{ U , \forall x ~ \phi }{\phi[u / x]} \quad \forall\text{Elim}$$

$$\frac{ U , \phi[u / x] }{ \exists x ~ \phi} \quad \exists\text{Intro}$$

$$\frac{\lnot \forall x ~ \phi}{U} \quad \forall\text{Inhabited}$$ $$\frac{\exists x ~ \phi}{U} \quad \exists\text{Inhabited}$$ $$\frac{\forall x ~ \bot}{\lnot U} \quad \forall\text{Uninhabited}_1$$ $$\frac{\lnot \exists x ~ \top}{\lnot U} \quad \exists\text{Uninhabited}_1$$

$$\frac{\lnot U}{\forall x ~ \phi} \quad \forall\text{Uninhabited}_2$$ $$\frac{\lnot U}{\lnot \exists x ~ \phi} \quad \exists\text{Uninhabited}_2$$

Puede haber algunos reduncancy en esas inferencias debido a que si se puede inferir $\forall x ~ \lnot P = \lnot \exists x ~ P$. La estructura de la prueba del teorema de T es:

$$\begin{array} {ll} U \lor \lnot U & \text{Provable with Propositional logic} \\ U \vdash T & \text{Regular proof of T} \\ \lnot U \vdash T & \text{By applying the Uninhabited}_2\text{ inferences and propositional logic} \\ T & \lor\text{ Elim} \end{array}$$

Tenga en cuenta que el $\lnot U \vdash T$ puede ser resuelto a través de algoritmos, como propostional lógica es trivialmente solucionable.

Es de suponer que usted desea una lógica que no introduce un universal habitar en constante $U$, y no procede a lo largo de 2 casos. La variable de "cadenas" en las otras respuestas son efectivamente sólo esta $U$ constante, donde $U$ iff la variable de la cadena no está vacía, como lo que puedo decir de todos modos. Uno de los enfoques para la reestructuración de la lógica es para ver donde el universo habitado suposición viene desde el subyacente $\lambda$-cálculo. Se puede definir una cuantificación universal como

$$\forall M = (M = \lambda x . \top)$$ o, equivalentemente, $$\forall (\lambda x . \phi) = ((\lambda x . \phi) = (\lambda x . \top))$$

(Sin tener en cuenta el tipo de consideraciones en aras de la brevedad, y no factorizando la M como lo haría para un axioma, y el uso de infix para mejorar la legibilidad). Esta definición no supone un universo habitado. También se $\forall\text{Elim}$ $\forall\text{Intro}$ puede ser traducido

$$(\forall (\lambda x . \phi) = \top) \iff ((\lambda x . \phi)~u = \top)$$

El $\implies$ lado de la anterior infringe el universo reclamación por asumir ese $u$ que existe en absoluto. El problema parece venir de la siguiente inferencia

$$(\lambda x . A) = (\lambda x. B) \vdash A = B$$

que no tiene por qué ser cierto en un universo vacío. Ex, $f(x) = x$$g(x) = x + 1$, asumiendo $x \ne x + 1$, todavía puede darse el caso de que $f = g$ si su dominio está vacía. Entonces, el desafío parece ser la traducción de $\forall (\lambda x . \phi) \implies ((\lambda x . \phi) = (\lambda x . \top))$ en el primer orden de la lógica sin asumiendo $(\lambda x . A) = (\lambda x. B) \vdash A = B$.

Esto me lleva a sospechar (no tengo la integridad prueba de ello) que $\forall\text{Elim}$ puede ser reemplazado por 2 axiomas:

$$\forall x ~ \forall y P \vdash \forall x P[t / y] \quad \forall\text{Elim}_\forall$$ $$\exists x ~ \forall y P \vdash \exists x P[t / y] \quad \forall\text{Elim}_\exists$$

Ambas afirmaciones son correctas (la segunda se le ha pedido un par de veces en las matemáticas.stackexchange, curiosamente) en el original de la lógica así como en el vacío del universo, y que efectivamente dicen que el cuantificador universal no pueden ser eliminados, a menos que realmente hay un contexto en el que la variable puede ser instanciado.

Tengo sólo se centró en $\forall$ en lugar de $\exists$ porque $\exists$ puede ser definido como: $\lnot \forall \lnot$ en algunas lógicas.