Una prueba de $(\forall x P(x)) \to A) \Rightarrow \exists x (P(x) \to A)$

Question

Recientemente he pedido a esta pregunta. En esa pregunta se me presentó una mano saludando a prueba como parte de la pregunta. Hubo cierta confusión en cuanto a la validez de mi mano saludando a prueba. Así que yo quería hacer que sea más precisa. La dificultad que he tenido es que han pasado 25 años desde que he escrito formal de la lógica de las pruebas. Me he olvidado de algunas de las reglas (Como la forma de manejar la introducción y eliminación de cuantificadores) y la regla de los nombres. Así que como verás a continuación he inventado los nombres de las reglas de la prueba a continuación.

Un par de preguntas.

1. Suponiendo que se utiliza el estándar de la regla de los nombres (en lugar de compuesto), es la prueba correcta. O hacer un par de pasos necesitan ser "apretados". ¿Qué es una buena referencia a la "norma" de la regla de los nombres que normalmente se usa en este sitio.
2. Nunca sé cómo componer este tipo de pruebas. Como en los pasos 3 a 5 de Caso 2, yo esperaría que aquellos a separarse para mostrar que $c$ sólo es válida en el contexto de la existencial. (Actualización: ahora están sangría utilizando \quad) (supongo que esto debe ser una cuestión separada en meta o un Látex sitio?)

Una prueba de $(\forall x P(x)) \to A) \Rightarrow \exists x (P(x) \to A)$

Voy a probar por el análisis de casos en $ \forall x P(x) $.

Caso 1: $ \forall x P(x) $

$$\begin{align} & (\forall x P(x)) \to A && \text{Hypothesis} & \tag{1} \\ & \forall x P(x) && \text{Case Hypothesis} & \tag{2} \\ & A && \text{Implication 1, 2} & \tag{3} \\ & \neg P(c) \vee A && \text{Or Introduction} & \tag{4} \\ & P(c) \to A && \text{Definition of Implies, 4} & \tag{5}\\ & \exists x (P(x) \to A) && \text{Existential Intro, 5} & \tag{6}\\ \end{align} $$

Caso 2: $ \neg \forall x P(x) $

$$\begin{align} & \neg \forall x P(x) && \text{Case Hypothesis} & \tag{1} \\ & \exists x \neg P(x) && \text{A Known Identity, 1} & \tag{2} \\ & \quad \neg P(c) && \text{Assumption, ref 2} & \tag{3} \\ & \quad \neg P(c) \vee A && \text{Or Introduction, 3} & \tag{4} \\ & \quad P(c) \to A && \text{Definition of Implies, 4} & \tag{5} \\ & \quad \exists x (P(x) \to A) && \text{Existential Intro, 5} & \tag{6} \\ & \exists x (P(x) \to A) && \text{Existential Elim, 2,6} & \tag{7} \\ \end{align} $$

ACTUALIZACIÓN: UN comentarista señaló que la afirmación es falsa en el caso de que el universo está vacío, así que vamos a suponer que un no-vacío del universo.

ACTUALIZACIÓN: Una respuesta a mi gracioso introducción de $\neg P(c)$ en el caso 2 paso 3. Traté de hacer las cosas más precisa mediante el uso de la sangría y se hace referencia a la EE como se muestra aquí: http://softoption.us/content/node/277

Answer 1

Abordar la pregunta 1, específicamente:

Yo no soy un experto en el tema, pero me tomó un par de lógica de los sujetos en la uni y en realidad nunca vio una convención de nomenclatura estándar para la deducción de reglas de primer orden de la lógica. Usted es probable encontrar diferentes autores, con diferentes convenios. Lo más importante es que usted siga las reglas correctamente y que tiene en este caso.

Answer 2

Esto depende de las reglas que usted está autorizado a utilizar. Si usted está autorizado a utilizar esas normas que estás usando parece bien - y todas las reglas que se ha utilizado parecen alowable demasiado.

El comentario de un no-vacío universo es inherente en una o varias de las reglas y ya es bastante razonable exigir que no está vacía universo esta hecho de no prohibición de estas reglas de alowable.

Dependiendo de cómo ver cuando se utiliza existencial de la introducción (o tal vez cuando introduce $c$ o a través de la introducción). Es a la conclusión de $\exists x \phi(x)$ $\forall x \phi(x)$ que se supone que no está vacía o es la suposición de que $\phi(c)$ implica que el $c$ se refiere a algo existente.

Tenga en cuenta que el segundo caso puede que no necesite depender de reglas que implican la no-vacío universo desde el caso premisa es falsa allí. Es por eso que, por ejemplo, a partir de la premisa puede concluir $\exists x\neg P(x)$

Answer 3

Estoy un poco desconcertado por su prueba en el caso 2, yo.e. bajo el supuesto de $\lnot \forall x \, P(x)$. Como la prueba de que debería ser válido clásico pero no intuitionistically (ya que se utiliza la ley de medio excluido), no se puede inferir, a partir de $\exists x \, \lnot P(x)$ que $P(c)$ (paso 3), el mejor que usted puede clásicamente hacer es aplicar la del teorema de Herbrand. De hecho, en deducción natural (ver Prawitz de la Deducción Natural) la eliminación de la regla de $\exists$ NO es de la forma

\begin{align*} \frac{\exists x A}{A[c/x]} \end{align*}

Entonces, yo creo que usted tiene que reformular el caso 2 de la siguiente manera. Suponga $\lnot \forall x \, P(x)$; esto significa que $\exists x \, \lnot P(x)$. Supongamos que $x$ es tal que $\lnot P(x)$: a continuación, $P(x) \to A$ desde cualquier declaración puede ser probado por medio de una contradicción (ex falso quodlibet), en particular,$A$. Por lo tanto, para cualquier $x$ tal que $\lnot P(x)$ nos han demostrado que, a $\exists x \, (P(x) \to A)$. Por lo tanto, bajo el supuesto de $\lnot \forall x \, P(x)$, nos han demostrado que, a $\exists x \, (P(x) \to A)$.

Yo formalizado su conjunto la prueba de $\forall x \, P(x) \to A \vdash \exists x \, (P(x) \to A)$ (después de mi argumento para el caso 2) en Prawitz de la deducción natural (supongo que te refieres a la deducción natural cuando dices "cómo controlar la introducción y eliminación de los cuantificadores"):

donde $\pi$ es una derivación clásica deducción natural (pero no es intuitionsitically válido) de la instancia de $\forall x \, P(x) \lor \lnot \forall x \, P(x)$ a de la ley del medio excluido, y $\pi_0$ es una derivación clásica deducción natural (pero no es intuitionsitically válido) de $\exists x \, \lnot P(x)$ bajo el supuesto de $\lnot \forall x \, P(x)$. Me puede detallar $\pi$ $\pi_0$ pero creo que está fuera del alcance de esta discusión.