Demostrar por Hilbert deducción: $\vdash _{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$

Question

Realmente me gustaría su ayuda para probar:

$\vdash_{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$

Donde $HFOL$ es la prueba del sistema que contiene los Hilbert relevantes axiomas:

1. $A\rightarrow(B \rightarrow A)$
2. $(A\rightarrow(B\rightarrow C))\to((A\rightarrow B)\rightarrow(A\rightarrow C))$
3. $(A\rightarrow B)\rightarrow ((A\rightarrow\bar{B})\rightarrow \bar{A})$
4. $\bar{\bar{A}} \rightarrow A$

Además de los dos siguientes axiomas:

$\forall x(B\to A)\to (\exists xB \to A)$

$\forall x(A \to B) \to (A \to \forall x B)$

Restringido a su uso, mientras que sólo $x$ no es una variable libre en $A$.

Y otros dos axiomas: $\forall xA \to A \{ t/x \}$, $A\{t/x\} \to \exists xA$ donde $t$ es gratuito para asignación de lugar de$x$$A$.

Finalmente hay el $MP$ regla: De $A, A\to B$ llegamos a la conclusión de $B$ y el Gen de la regla que de $A$ llegamos a la conclusión de $\forall xA$.

He intentado par de maneras diferentes, pero no vienen con cualquier smart resultado.

Alguna sugerencia?

Answer 1

Bien, usted puede utilizar el teorema de la deducción debido a que ∀x((a→B)) no tiene variables libres. Después de usar se obtiene: ∀x((a→B))⊢HFOL(∀xA→(∀xB))

Ahora haremos una prueba en HFOL:

1. ∀x((a→B)) - por supuesto.
2. ∀x((A→B)→(a→B) - primer axioma.
3. (A→B) - MP en 1,2.
4. (A→B)→A - debido a que usted puede probar en hpc.
5. Un - MP en 3,4.
6. ∀xA - Gen en 5.
7. (A→B)→B - debido a que usted puede probar en hpc.
8. B - MP en 3,7.
9. ∀xB - Gen en 8.
10. (∀xA→(∀xB)) - debido a que usted puede probar en hpc.

Answer 2

Jozef, perdonar la torpeza de mi notación, ya que no estoy acostumbrado a HFOL,me gustó el desafío. También me ofreció una segunda prueba en Dijsktra del Estilo, ya que me pareció una ayuda útil a mi intuición, ya que usted menciona que se ha intentado muchas cosas, sin suerte. Puede resultar muy útil.

---

Prueba en HFOL:

$\forall x(\neg (A\rightarrow \neg B))\vdash\neg (\forall xA\rightarrow \neg \forall xB)$

Sabiendo $(A\rightarrow B)\rightarrow ((A\rightarrow \neg B)\rightarrow \neg A)$, se puede intentar:

$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash \neg (A\rightarrow \neg B), (A\rightarrow \neg B)$

Tomé $\neg (A\rightarrow \neg B), (A\rightarrow \neg B)$ porque podemos obtener $\neg (A\rightarrow \neg B)$ fácilmente.

Llegamos $\neg (A\rightarrow \neg B)$ $\forall x(\neg (A\rightarrow \neg B))$ y $\forall xA\rightarrow A{t/x}$.

Ahora para la parte difícil. $A\rightarrow \neg B$

$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash A\rightarrow \neg B$

Conocer el MP regla se puede intentar:

$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB,A\vdash \neg B$

Llegamos $\forall xA$ $A$ y el Gen de la regla.

Llegamos $\neg \forall xB$ a partir de $\forall xA$, $\forall xA\rightarrow \neg \forall xB$ y el MP de la regla.

Llegamos $\neg B$$\neg \forall xB$$\forall xA\rightarrow A\lbrace{ t/x\rbrace}$.

Hecho.

---

Ahora en el de Dijkstra Estilo.

$\forall x(\neg (A \rightarrow \neg B))\rightarrow \neg (\forall xA \rightarrow \neg \forall xB)$

$=\lbrace p\rightarrow q = \neg p\vee q \rbrace$

$\forall x(\neg (\neg A \vee \neg B)) \rightarrow \neg (\neg \forall xA \vee \neg \forall xB)$

$=\lbrace de Morgan\rbrace$

$\forall x(A \wedge B)\rightarrow (\forall xA \wedge \forall xB)$

$=\lbrace Distributivity\,\, of \,\, \forall\,\, over\,\, \wedge \rbrace$

$(\forall xA \wedge \forall xB)\rightarrow (\forall xA \wedge \forall xB)$

Hecho.

Edit: Para aclarar el motivo por el que he encontrado la segunda prueba útil para ayudar a mi intuición. Como puede ver, esta prueba es considerablemente más corto. Esto es debido a que el estilo permite más general de las leyes (en lugar de un conjunto mínimo de axiomas) y porque prefiere normas que eviten el análisis de casos. Esto significa que es mucho más fácil de probar algo de este estilo.

Ahora, para mí, el paso más difícil en mi primera prueba fue:

$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash \neg (A\rightarrow \neg B), (A\rightarrow \neg B)$

Yo sabía que tenía que aplicar $(A\rightarrow B)\rightarrow ((A\rightarrow \neg B)\rightarrow \neg A)$ Pero tuve que decidir, ¿qué fórmula utilizar como $B$.

Volviendo a mi segunda prueba, $\forall x(\neg (A \rightarrow \neg B))$ $\neg (\forall xA \rightarrow \neg \forall xB)$ son iguales. Eso significaba que cualquier cosa que yo podría probar con una, yo podría probar con el otro.

Así que, cuando me doy cuenta de que yo podía demostrar $\neg (A \rightarrow \neg B)$$\forall x(\neg (A \rightarrow \neg B))$, yo sabía que podía demostrar lo contrario de $(\forall xA \rightarrow \neg \forall xB)$. Esto redujo la cantidad de cosas para tratar inmensamente.

Answer 3

Los convenios 1.
1. Podemos abreviar el símbolo $\vdash_\mbox{HFOL}$$\vdash$.
2. Podemos abreviar el plazo wff de HFOL por wff.
3. Se denota una prueba formal como una deducción, y un metaproof como un prueba.
4. Al dar abreviado deducciones, nos referimos a subdeductions por citando lemmata.

Desde el Lemmata 1 y 2 se utilizan en la prueba de la Deducción Teorema, no vamos a presuponer que el Teorema de la Deducción en su pruebas.

Lema 1. Deje $A$ ser un wff.
A continuación,$\vdash A \rightarrow A$.

Prueba. Vamos a dar una deducción.
$$\begin{array}{lll} 1. & (A \rightarrow ((A \rightarrow A) \rightarrow A)) \rightarrow & \\ & ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \mbox{Axiom schema 2} \\ 2. & A \rightarrow ((A \rightarrow A) \rightarrow A) & \mbox{Axiom schema 1} \\ 3. & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \mbox{MP: 2, 1} \\ 4. & A \rightarrow (A \rightarrow A) & \mbox{Axiom schema 1} \\ 5. & A \rightarrow A & \mbox{MP: 4, 3} \end{array}$$ Por lo tanto, podemos concluir que $\vdash A \rightarrow A$.

Q. E. D.

Lema 2. Vamos $A$, $B$, y $C$ ser wffs.
A continuación,$A \rightarrow B, B \rightarrow C \vdash A \rightarrow C$.

Prueba. Vamos a dar una deducción.
$$\begin{array}{lll} 1. & A \rightarrow B & \mbox{Hyp} \\ 2. & B \rightarrow C & \mbox{Hyp} \\ 3. & (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) & \mbox{Axiom schema 2} \\ 4. & (B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C)) & \mbox{Axiom schema 1} \\ 5. & A \rightarrow (B \rightarrow C) & \mbox{MP: 2, 4} \\ 6. & (A \rightarrow B) \rightarrow (A \rightarrow C) & \mbox{MP: 5, 3} \\ 7. & A \rightarrow C & \mbox{MP: 1, 6} \end{array}$$ Por lo tanto, podemos concluir que $A \rightarrow B, B \rightarrow C \vdash A \rightarrow C$.

Q. E. D.

Definición 1 (Depende). Deje $B_1, \ldots, B_k$ ser una deducción, y deje $A$ $C$ ser wffs.

1. Un subconjunto $M$ $\{ B_1, \ldots, B_k \}$ es llamado inductivo y si sólo si las tres propiedades siguientes están satisfechos:
   • Si $A$ es algunas hipótesis de la deducción $B_1, \ldots, B_k$, luego $A \in M$.
   • Si por $1 \leq i \leq k$, $B_i$ es una consecuencia directa por MPde algunos wffs $B_p$ $B_q$ con $1 \leq p < i$, $1 \leq q < i$, y $\{ B_p, B_q \} \cap M \neq \emptyset$ ,$B_i \in M$.
   • Si por $1 \leq i \leq k$, $B_i$ es una consecuencia directa por la Generaciónde algunos wff $B_p \in M$$1 \leq p < i$,$B_i \in M$.
2. Deje $D = \bigcap \{ M | \mbox{$M$ is an inductive set} \}$.
3. La wff $C$ se dice que dependen de $A$ para $B_1, \ldots, B_k$ si y sólo si $C \in D$.

Observación. El conjunto $D$ está bien definido desde $\{ B_1, \ldots, B_k \}$ es un conjunto inductivo.

La Proposición 1 (Teorema De La Deducción). Deje $\Gamma$ ser un conjunto de wffs, y deje $A$ $B$ ser wffs. Suponga que en algunos deducción $B_1, \ldots, B_k$ mostrando que $\Gamma, A \vdash B$, la no aplicación de Gen a un wff que depende de a $A$ $B_1, \ldots, B_k$ tiene como variable cuantificada un variable libre de $A$. A continuación,$\Gamma \vdash A \rightarrow B$.

Prueba. Ver constructivo que se prueba en el libro [1]. Se utiliza sólo propiedades de la libreta de autor de la teoría formal de K que también se les da por la teoría formal HFOL.

Lema 3. Deje $A$ $B$ ser wffs.
A continuación,$A \vdash (A \rightarrow B) \rightarrow B$.

Prueba. Desde $A, A \rightarrow B \vdash B$ por MP, podemos aplicar el Teorema de la Deducción y a la conclusión de que $A \vdash (A \rightarrow B) \rightarrow B$.

Q. E. D.

Lema 4. Deje $A$ $B$ ser wffs. Entonces
1. $A, B \rightarrow \neg A \vdash \neg B$.
2. $\vdash (B \rightarrow \neg A) \rightarrow (A \rightarrow \neg B)$.
3. $A \vdash \neg \neg A$.
4. $\vdash A \rightarrow \neg \neg A$.
5. $\neg A, \neg B \rightarrow A \vdash B$.
6. $\vdash (\neg B \rightarrow A) \rightarrow (\neg A \rightarrow B)$.
7. $A, \neg A \vdash B$.
8. $\vdash \neg A \rightarrow (A \rightarrow B)$.

Prueba. Anuncio de 1. Vamos a dar una deducción.
$$\begin{array}{lll} 1. & A & \mbox{Hyp} \\ 2. & B \rightarrow \neg A & \mbox{Hyp} \\ 3. & A \rightarrow (B \rightarrow A) & \mbox{Axiom schema 1} \\ 4. & B \rightarrow A & \mbox{MP: 1, 3} \\ 5. & (B \rightarrow A) \rightarrow ((B \rightarrow \neg A) \rightarrow \neg B) & \mbox{Axiom schema 3} \\ 6. & (B \rightarrow \neg A) \rightarrow \neg B & \mbox{MP: 4, 5} \\ 7. & \neg B & \mbox{MP: 2, 6} \end{array}$$ Por lo tanto, podemos concluir que $A, B \rightarrow \neg A \vdash \neg B$, como fue necesario.

Ad 2. Aplicando dos veces el Teorema de la Deducción a Lema 4.1, se se puede concluir que el Lema 4.2 sostiene, como era necesario.

Ad 3. Vamos a dar una abreviado de la deducción.
$$\begin{array}{lll} 1. & A & \mbox{Hyp} \\ 2. & A \rightarrow (\neg A \rightarrow A) & \mbox{Axiom schema 1} \\ 3. & \neg A \rightarrow A & \mbox{MP: 1, 2} \\ 4. & \neg A \rightarrow \neg A & \mbox{Lemma 1} \\ 5. & (\neg A \rightarrow A) \rightarrow ((\neg A \rightarrow \neg A) \rightarrow \neg \neg A) & \mbox{Axiom schema 3} \\ 6. & (\neg A \rightarrow \neg A) \rightarrow \neg \neg A & \mbox{MP: 3, 5} \\ 7. & \neg \neg A & \mbox{MP: 4, 6} \end{array}$$ Por lo tanto, podemos concluir que $A \vdash \neg \neg A$, como era necesario.

Anuncio de 4. La aplicación de la Deducción del Teorema de Lema 4.3, podemos concluir que $\vdash A \rightarrow \neg \neg A$, como era necesario.

Anuncio de 5. Vamos a dar una abreviado de la deducción.
$$\begin{array}{lll} 1. & \neg A & \mbox{Hyp} \\ 2. & \neg B \rightarrow A & \mbox{Hyp} \\ 3. & A \rightarrow \neg \neg A & \mbox{Lemma 4.4} \\ 4. & \neg B \rightarrow \neg \neg A & \mbox{Lemma 2: 2, 3} \\ 5. & \neg \neg B & \mbox{Lemma 4.1: 1, 4} \\ 6. & \neg \neg B \rightarrow B & \mbox{Axiom schema 4} \\ 7. & B & \mbox{MP: 5, 6} \end{array}$$ Por lo tanto, podemos concluir que $\neg A, \neg B \rightarrow A \vdash B$, como era necesario.

Anuncio de 6. Aplicando dos veces el Teorema de la Deducción a Lema 4.5, podemos a la conclusión de que $\vdash (\neg B \rightarrow a) \rightarrow (\neg a \rightarrow B)$, como era necesario.

Anuncio de 7. Vamos a dar una abreviado de la deducción.
$$\begin{array}{lll} 1. & A & \mbox{Hyp} \\ 2. & \neg A & \mbox{Hyp} \\ 3. & \neg A \rightarrow (\neg B \rightarrow \neg A) & \mbox{Axiom schema 1} \\ 4. & \neg B \rightarrow \neg A & \mbox{MP: 2, 3} \\ 5. & \neg \neg B & \mbox{Lemma 4.1: 1, 4} \\ 6. & \neg \neg B \rightarrow B & \mbox{Axiom schema 4} \\ 7. & B & \mbox{MP: 5, 6} \end{array}$$ Por lo tanto, podemos concluir que $A, \neg A \vdash B$, como era necesario.

Anuncio de 8. Aplicando dos veces el Teorema de la Deducción a Lema 4.7, se se puede concluir que el Lema 4.8 sostiene.

Q. E. D.

Lema 5. Deje $A$ $B$ ser wffs. Entonces
1. $A, B \vdash \neg (A \rightarrow \neg B)$.
2. $\neg (A \rightarrow \neg B) \vdash A$.
3. $\neg (A \rightarrow \neg B) \vdash B$.

Prueba. Anuncio de 1. Vamos a dar una abreviado de la deducción.
$$\begin{array}{lll} 1. & A & \mbox{Hyp} \\ 2. & B & \mbox{Hyp} \\ 3. & (A \rightarrow \neg B) \rightarrow \neg B & \mbox{Lemma 3: 1} \\ 4. & ((A \rightarrow \neg B) \rightarrow \neg B) \rightarrow (B \rightarrow \neg (A \rightarrow \neg B)) & \mbox{Lemma 4.2} \\ 5. & B \rightarrow \neg (A \rightarrow \neg B) & \mbox{MP: 3, 4} \\ 6. & \neg (A \rightarrow \neg B) & \mbox{MP: 2, 5} \end{array}$$ Por lo tanto, podemos concluir que $A, B \vdash \neg (A \rightarrow \neg B)$, como fue necesario.

Ad 2. Vamos a dar una abreviado de la deducción.
$$\begin{array}{lll} 1. & \neg (A \rightarrow \neg B) & \mbox{Hyp} \\ 2. & \neg A \rightarrow (A \rightarrow \neg B) & \mbox{Lemma 4.8} \\ 3. & (\neg A \rightarrow (A \rightarrow \neg B)) \rightarrow (\neg (A \rightarrow \neg B) \rightarrow A) & \mbox{Lemma 4.6} \\ 4. & \neg (A \rightarrow \neg B) \rightarrow A & \mbox{MP: 2, 3} \\ 5. & A & \mbox{MP: 1, 4} \end{array}$$ Por lo tanto, podemos concluir que $\neg (A \rightarrow \neg B) \vdash A$, como fue necesario.

Ad 3. Vamos a dar una abreviado de la deducción.
$$\begin{array}{lll} 1. & \neg (A \rightarrow \neg B) & \mbox{Hyp} \\ 2. & \neg B \rightarrow (A \rightarrow \neg B) & \mbox{Axiom schema 1} \\ 3. & (\neg B \rightarrow (A \rightarrow \neg B)) \rightarrow (\neg (A \rightarrow \neg B) \rightarrow B) & \mbox{Lemma 4.6} \\ 4. & \neg (A \rightarrow \neg B) \rightarrow B & \mbox{MP: 2, 3} \\ 5. & B & \mbox{MP: 1, 4} \end{array}$$ Por lo tanto, podemos concluir que $\neg (A \rightarrow \neg B) \vdash B$.

Q. E. D.

Proposición 2 (Principal De La Proposición). Deje $A$ $B$ ser wffs, y deje $x$ ser una de las variables. Entonces
1. $\forall x \neg (A \rightarrow \neg B) \vdash \neg (\forall x A \rightarrow \neg \forall x B)$.
2. $\vdash \forall x \neg (A \rightarrow \neg B) \rightarrow \neg (\forall x A \rightarrow \neg \forall x B)$.

Prueba. Anuncio de 1. Vamos a dar una abreviado de la deducción.
$$\begin{array}{lll} 1. & \forall x \neg (A \rightarrow \neg B) & \mbox{Hyp} \\ 2. & \forall x \neg (A \rightarrow \neg B) \rightarrow \neg (A \rightarrow \neg B) & \mbox{Axiom schema 7} \\ 3. & \neg (A \rightarrow \neg B) & \mbox{MP: 1, 2} \\ 4. & A & \mbox{Lemma 5.2: 3} \\ 5. & \forall x A & \mbox{Gen: 4} \\ 6. & B & \mbox{Lemma 5.3: 3} \\ 7. & \forall x B & \mbox{Gen: 6} \\ 8. & \neg (\forall x A \rightarrow \neg \forall x B) & \mbox{Lemma 5.1: 5, 7} \end{array}$$ Por lo tanto, podemos concluir que la Proposición 2.1 sostiene, como era necesario.

Ad 2. Desde que aplicar Gen en el abreviado de la deducción de los de la prueba de la Proposición 2.1 sólo con la persona a la variable $x$ como cuantificado variable y $x$ no es una variable libre en $\forall x \neg (a \rightarrow \neg B)$, podemos aplicar el Teorema de Deducción a la Proposición 2.1, y a la conclusión de que $$\vdash \forall x \neg (a \rightarrow \neg B) \rightarrow \neg (\forall x \rightarrow \neg \forall x B).$$

Q. E. D.

Referencias

[1]: Mendelson, Elliott. Introducción a la lógica matemática. 3ª ed. (c) 1987 por Wadsworth. ISBN 0-534-06624-0.