¿Cómo mostrar que $\vdash (\forall x \beta \to \alpha) \leftrightarrow \exists x (\beta \to \alpha)$?

Question

Suponga $x$ no se encuentra libre en la $\alpha$, muestran que: $$\vdash (\forall x \beta \to \alpha) \leftrightarrow \exists x (\beta \to \alpha)$$

Este es un ejercicio en la página 130, Matemáticas, Introducción a la Lógica, Herbert B. Enderton（2ed).

Aquí está mi intento: Para el '$\to$' la dirección, ya que $x$ no se encuentra libre en la $\alpha$, $α→∀x α$ $\forall x \alpha \to \alpha$ como axioma lógico(En la segunda fórmula, tenemos$\alpha_x^x = \alpha$). Por lo tanto es suficiente para mostrar $\vdash (\forall x \beta \to \forall x \alpha) \rightarrow \exists x (\beta \to \alpha)$. Por lógica axioma $∀ x(α→β)→( ∀ x α→∀x β)$, sería suficiente para mostrar $\vdash \forall x (\beta \to \alpha) \rightarrow (\exists x (\beta \to \alpha))$. Se ha demostrado en un ejercicio anterior que hay una deducción $∀ x ϕ→∃x ϕ$, por lo que estamos hecho para el "$\to$" parte.

Para mí el problema es cómo mostrar el "$\leftarrow$" de dirección.

Añadido: Aquí la lógica de los axiomas que podemos emplear:

1. Tautologías(en el sentido de la lógica proposicional);
2. $∀ x α →α^x_ t $, where $t$ is substitutable for $x$ in $α$ ($α^x_ t$ is the formula derived from $\alpha$ by replacing $x$ by a term $t$);
3. $∀ x(α→β)→( ∀ x α→∀x β)$;
4. $α→∀x α$ donde $x$ no se encuentra libre en la $α$.

Además, la generalización y teorema de deducción principio puede ser utilizado:

Si $\Gamma \vdash ϕ$ $x$ no se encuentra libre en cualquier fórmula en$\Gamma$,$\Gamma \vdash ∀ x ϕ$.

Si $\Gamma ; γ \vdash ϕ,$$\Gamma \vdash γ \to ϕ$.

Answer 1

Tener el OP pregunta ya ha recibido respuestas, presento este "largo" comentario destinado a proporcionar una prueba de uso de Enderton del axiomas y modus ponens, que es la única regla de inferencia (ver Herbert Enderton, Matemáticas, Introducción a la Lógica (2º - 2001)).

Tenemos que demostrar (P3A) [ver Ejercicio 8, página 130] :

$\vdash (\forall x \beta \rightarrow \alpha) \leftrightarrow \exists x (\beta \rightarrow \alpha)$ si $x$ no se encuentra libre en la $\alpha$.

Primera parte : $\leftarrow$

(1) $\forall x \beta$ --- asumido

(2) $\beta_c^x$ - - - (1) por Ax.2 y mp, donde la constante símbolo $c$ no ocurre en $\alpha, \beta$

(3) $\beta_c^x \rightarrow \alpha$ --- asumido

(4) $\alpha$ --- de (2) y (3) por mp

Por el COROLARIO 24H (REGLA de la IE) [página 124], habiendo demostrado la $\forall x \beta, \beta_c^x \rightarrow \alpha \vdash \alpha$ donde $c$ no ocurre en $\beta$ o en $\alpha$ (debido a $x \notin FV(\alpha)$), tenemos :

(5) $\forall x \beta, \exists (\beta \rightarrow \alpha) \vdash \alpha$

(6) $\exists (\beta \rightarrow \alpha) \vdash (\forall x \beta \rightarrow \alpha)$ --- de (5) por DT.

---

Segunda parte : $\rightarrow$

(1) $\lnot \beta \vdash \beta \rightarrow \alpha$ - - - $\vDash_{TAUT} \lnot \phi \rightarrow (\phi \rightarrow \psi)$ , asumiendo $\lnot \beta$

(2) $\forall x \beta \rightarrow \alpha$ --- asumido

(3) $\lnot \exists x (\beta \rightarrow \alpha)$ --- asumido

(4) $\exists x (\beta \rightarrow \alpha)$ - - - (1) por la "deriva de la regla" : $\varphi_t^x \rightarrow \exists x \varphi$ [comprobable de Ax.2] y mp

Así tenemos : $\lnot \beta, \lnot \exists x (\beta \rightarrow \alpha) \vdash \exists x (\beta \rightarrow \alpha)$, a partir de (1) y (4) y $\lnot \beta, \lnot \exists x (\beta \rightarrow \alpha) \vdash \lnot \exists x (\beta \rightarrow \alpha)$, a partir de (1) y (3); aplicamos : COROLARIO 24E (REDUCTIO AD ABSURDUM) [página 119] y $\vDash_{TAUT} \lnot \lnot \phi \rightarrow \phi$ y mp para concluir con :

(5) $\lnot \exists x (\beta \rightarrow \alpha) \vdash \beta$

(6) $\forall x \beta$ --- de (5) por GENERALIZACIÓN TEOREMA [página 117] ($x$ no es libre en los supuestos (2), debido a que $x \notin FV(\alpha$), y (3) y la asunción (1) ha sido "dado de alta" en (5))

(7) $\alpha$ --- de (2) y (6) por mp

(8) $\beta \rightarrow \alpha$ --- a partir De (7) y $\vDash_{TAUT} \phi \rightarrow (\psi \rightarrow \phi)$ y mp

(9) $\exists x(\beta \rightarrow \alpha)$ --- a partir de (8) por la "deriva de la regla" en (4) por encima de

Aplicamos de nuevo COROLARIO 24E (REDUCTIO AD ABSURDUM) con : $\lnot \exists x (\beta \rightarrow \alpha), \forall x \beta \rightarrow \alpha \vdash \lnot \exists x (\beta \rightarrow \alpha)$, e $\lnot \exists x (\beta \rightarrow \alpha), \forall x \beta \rightarrow \alpha \vdash \exists x (\beta \rightarrow \alpha)$, a partir de (2)-(9), y la Doble Negación para concluir con :

(10) $(\forall x \beta \rightarrow \alpha) \vdash \exists x (\beta \rightarrow \alpha)$.

---

---

Anexo

Añadimos como un ejercicio de la prueba en Enderton del sistema de (Q2B) [ver Ejercicio 8, página 130] :

$\vdash (\alpha \rightarrow \exists x \beta) \leftrightarrow \exists x (\alpha \rightarrow \beta)$ si $x$ no se encuentra libre en la $\alpha$.

Primera parte : $\rightarrow$

(Me ha "racionalizado" un poco el "tautológica" pasos)

(1) $\alpha \rightarrow \exists x \beta$ --- asumido

(2) $\forall x \lnot (\alpha \rightarrow \beta)$ --- asumido

(3) $\alpha \land \lnot \beta$ - - - (2) por Tirante

(4) $\lnot \beta$ - - - (3) Taut

(5) $\forall x \lnot \beta$ --- por la Generalización Teorema [página 117], debido a que $x$ no es libre en los supuestos (1) y (2)

(6) $\lnot \exists x \beta$ --- abreviatura

(7) $\alpha$ - - - (3) Taut

(8) $\exists x \beta$ - - - (1) por mp.

Deriva de la contradicción [con (6) y (8)], se aplica el Corolario 24E (Reductio ad Absurdum) [página 119] : si $\Gamma \cup \{ \varphi \}$ es inconsistente, entonces a$\Gamma \vdash \lnot \varphi$,$\Gamma = \{ \alpha \rightarrow \exists x \beta \}$, e $\varphi := \forall x \lnot (\alpha \rightarrow \beta)$.

Por lo tanto podemos concluir :

(9) $\lnot \forall x \lnot (\alpha \rightarrow \beta)$

que es : $\alpha \rightarrow \exists x \beta \vdash \exists x (\alpha \rightarrow \beta)$.

Finalmente :

(A) $\vdash (\alpha \rightarrow \exists x \beta) \rightarrow \exists x (\alpha \rightarrow \beta)$ --- por el Teorema de la Deducción.

---

Segunda parte : $\leftarrow$

(1) $\alpha \rightarrow \beta[x/c]$ --- asumido, donde $c$ es una persona constante

(2) $\lnot \beta[x/c] \rightarrow \lnot \alpha$ --- Taut

(3) $\forall x \lnot \beta$ --- asumido

(4) $\lnot \beta[x/c]$ --- de Ax.2 y 3) por mp

(5) $\lnot \alpha$ --- forma (2) y (4) por mp

(6) $\forall x \lnot \beta \rightarrow \lnot \alpha$ --- forma (3) y (5) por el Teorema de Deducción

(7) $\alpha \rightarrow \lnot \forall x \lnot \beta$ --- Taut

(8) $\alpha \rightarrow \exists x \beta$ --- abreviatura.

Ahora aplicamos el Corolario 24H (Regla de la IE) : suponga que la constante de símbolo $c$ no ocurre en $\varphi, \psi$ o $\Gamma$,$\Gamma \cup \{ \varphi[x/c] \} \vdash \psi$; a continuación,$\Gamma, \exists x \varphi \vdash \psi$, donde $\Gamma = \emptyset$, $\varphi[x/c] := \alpha \rightarrow \beta[x/c]$ y $\psi := \alpha \rightarrow \exists x \beta$.

Por lo tanto podemos concluir con :

$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.

Finalmente :

(B) $\vdash \exists x (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \exists x \beta)$.

El teorema se sigue de (A) y (B).

---

---

2º Addendum

Para la segunda parte : $\leftarrow$, se puede probar sin Corolario 24H (Regla de la IE).

(1) $\exists x(\alpha \rightarrow \beta)$ --- asumido

(2) $\alpha$ --- asumido

(3) $\lnot \exists x \beta$ --- asumido

(4) $\lnot \lnot \forall x \lnot \beta$ --- abreviación de $\exists$

(5) $\forall x \lnot \beta$ --- Taut

(6) $\lnot \beta$ --- Ax.2

(7) $\vDash_{TAUT} \alpha \rightarrow (\lnot \beta \rightarrow \lnot (\alpha \rightarrow \beta))$

(8) $\lnot (\alpha \rightarrow \beta)$ --- de (2), (6) y (7) por mp

(9) $\forall x \lnot (\alpha \rightarrow \beta)$ \begin{align*} \sum_{k=0}^{a-1}\binom{b}k\binom{n-b}{a-k}&=\sum_k\binom{n}k\binom{n-b}{a-k}-\binom{b}a\binom{n-b}0\\ &=\binom{n}a-\binom{b}a \endGen Th ($x \notin FV(\alpha)$)

(10) $\lnot \exists x (\alpha \rightarrow \beta)$ --- abreviatura

(11) $\lnot \lnot \exists x \beta$ --- aplicamos el Corolario 24E (Reductio ad Absurdum) [página 119] a (3), (1) y (10)

(12) $\exists x \beta$ --- Taut

(13) $\alpha \rightarrow \exists x \beta$ - - - (2) por el Teorema de la Deducción.

Así que de nuevo :

$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.

Answer 2

Si $\alpha$ mantiene, a ambos lados de la fib son verdaderas, ya que cualquier cosa que implica cierto. Así que supongamos $\alpha$ es falso.

Ahora suponga $\exists x (\beta \to \alpha)$. A continuación, tome $c$ un $x$, y llegar a $$\beta_c^x \to \alpha,$$ where we have used $\alpha_c^x=\alpha$, since $x$ is not free in $\alpha$. Since $\alpha$ is false, $\beta_c^x$ must be false, so that also $\forall x \beta$ is false, and from this $\forall x \beta \a \alpha$ de la siguiente manera.

Creo que los pasos son reversibles, de modo que uno podría hacer el forward implicación en una manera similar. Sin embargo, el OP solo se les preguntó acerca de la implicación inversa sólo se tratan. He utilizado "instanciación existencial" (que es lo que uno de los textos que he utilizado se llama), que no es una de las normas citadas en el OP, sin embargo creo que debe ser de alguna manera en cualquier formales axiomitization.

Answer 3

Como coffeemath ya se ha observado, en el caso interesante es α ser falso. En esa situación la implicación hacia α es el mismo como negación, lo que significa que la dirección de izquierda a derecha es en realidad una variante de la ley de de Morgan para cuantificadores (el duro clásica parte de ella).

Permite cambiar la notación a la de la prueba formal del sistema de Isabelle/Isar. La prueba de que parte de de Morgan, a continuación, se parece a esto:

theorem de_Morgan_classical:
  assumes *: "¬ (∀x. B x)"
  shows "∃x. ¬ B x"
proof (rule classical)
  assume **: "¬ (∃x. ¬ B x)"
  have "∀x. B x"
  proof
    fix x show "B x"
    proof (rule classical)
      assume "¬ B x"
      then have "∃x. ¬ B x" ..
      with ** show "B x" by contradiction
    qed
  qed
  with * show "∃x. ¬ B x" by contradiction
qed

Usted puede leer esto es pseudo-código, pero es la máquina marcada de deducción natural. Tenga en cuenta que en el lenguaje formal, la dependencia de algún argumento es explícita, como en B x, y sólo A significa que no dependen de variables ocultas.

En lugar de utilizar esa ley en la prueba, nos re-uso de su prueba a hacer un poco más general la versión de la siguiente manera:

lemma
  assumes *: "(∀x. B x) ⟶ A"
  shows "∃x. (B x ⟶ A)"
proof (rule classical)
  assume **: "¬ (∃x. (B x ⟶ A))"
  have "∀x. B x"
  proof
    fix x show "B x"
    proof (rule classical)
      assume "¬ B x"
      have "B x ⟶ A"
      proof
        assume "B x"
        with `¬ B x` show A ..
      qed
      then have "∃x. (B x ⟶ A)" ..
      with ** show "B x" by contradiction
    qed
  qed
  with * have A ..
  fix a from `A` have "B a ⟶ A" ..
  then show "∃x. (B x ⟶ A)" ..
qed

La otra dirección es la simple deducción natural, sin nada especial. No hay ninguna clásico de los casos a ser considerados.

lemma
  assumes *: "∃x. (B x ⟶ A)"
  shows "(∀x. B x) ⟶ A"
proof
  assume **: "∀x. B x"
  from * obtain a where ***: "B a ⟶ A" ..
  from ** have "B a" ..
  with *** show A ..
qed