Demostración $\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle \implies \langle \exists y: P.y : Q.y \rangle $ es un teorema.

Question

Una posible prueba utilizando un sistema de Deducción Natural como Fitch no es difícil. Pero, me gustaría probarlo usando Equational Logic. Este sistema usa reglas comunes de lógica proposicional como DeMorgan, etc., y reglas de lógica de predicados que se usan en libros como:

• Un enfoque lógico para las matemáticas discretas (David Gries).
  • El libro completo se puede encontrar aquí: https://link.springer.com/book/10.1007/978-1-4757-3837-7
  • Lista de reglas en la página 503.
• Programación en la década de 1990 (Edward Cohen).

Mi prueba comienza de la siguiente manera:

Supongo que el antecedente se mantiene $$\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle$$ y trata de alcanzar $$\langle \exists x:: P.x \land Q.x \rangle$$

Prueba intentada:

$$ \begin{align*} & \langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle\\ \implies & \{\text{Instantiation } (\forall)\}\\ & P.a \land \langle \exists x:: Q.x \rangle \\ \equiv & \{\text{Distributivity of} \land \text{over} \exists \} \\ & \langle \exists x:: P.a \land Q.x \rangle \end{align*} $$

Por supuesto, la prueba no está completa. ¿Alguien sabe si esta prueba es posible en este contexto?

Answer 1

Al crear una prueba formal para una implicación lógica, es útil razonar primero intuitivamente sobre ella. Esto también puede ayudar a revelar si una prueba parcial en la que está trabajando conduce a un callejón sin salida. Por ejemplo, su prueba parcial se lee intuitivamente como:

Me caigo $x$ tener propiedad $P.x$ y hay algo $x$ con propiedad $Q.x$, entonces debe haber algo $x$ con propiedad $P.x\land Q.x$: de hecho, deja $a$ ser un objeto arbitrario, entonces sabemos que tiene propiedad $P.a$. Dado que hay algunos$x$ con propiedad $Q.x$, podemos concluir que hay algunos $x$ con $P.a\land Q.x$... pero ahora que?

Esto revela que probablemente no fue la mejor idea instanciar primero el cuantificador universal, sino el cuantificador existencial:

Me caigo $x$ tener propiedad $P.x$ y hay algo $x$ con propiedad $Q.x$, entonces debe haber algo $x$ con la propiedad $P.x\land Q.x$: de hecho, dice el objeto con propiedad $Q$ se llama $a$ (así que eso $Q.a$), entonces ya que todos $x$ tener propiedad $P.x$, entonces especialmente $a$ debe tener propiedad $P.a$. Combinando esto con el hecho de que$a$ tiene propiedad $Q.a$, podemos concluir que $a$ tiene propiedad $P.a\land Q.a$. En particular, hay algunos $x$ con $P.x\land Q.x$.

Escribir esto formalmente usando la deducción natural se vería así:

1. $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle$ (suposición para la introducción de implicaciones)
2. $\langle \exists x :: Q.x\rangle$(conjunción elim, 1)
   2.1$Q.a$(supuesto de eliminación existencial)
   2.2$\langle \forall x :: P.x\rangle$(conjunción elim, 1)
   2.3$P.a$(eliminación universal, 2,2)
   2,4$P.a\land Q.a$(introducción de conjunción, 2.1, 2.3)
   2.5$\langle \exists x :: P.x\land Q.x\rangle$ (introducción existencial, 2.4)
3. $\langle \exists x :: P.x\land Q.x\rangle$ (eliminación existencial, 2, 2.1-2.5)

de lo que concluimos $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle \implies \langle \exists x :: P.x\land Q.x\rangle$ por implicación intro en 1-3.

Este argumento guía cómo producir un argumento axiomático. El truco principal en este caso es que una intro existencial se elude al razonar para envolver todo el argumento en el cuantificador existencial. Entonces puede razonar dentro del alcance de un cuantificador existencial como si no estuviera allí.

(antecedente) $\langle \forall x :: P.x\rangle\land\langle\exists x :: Q.x\rangle$

$\equiv$ $\langle \forall y :: P.y\rangle\land\langle\exists x :: Q.x\rangle$ (cambio de variables)

$\equiv$ $\langle \exists x :: \langle \forall y :: P.y\rangle \land Q.x\rangle$ (distributividad de $\land$ encima $\exists$; esto envuelve toda la declaración en$\exists$)

$\implies$ $\langle \exists x :: P.x \land Q.x \rangle$ (instanciación de $\forall$ a $x$)

Answer 2

El truco sería instanciar específicamente al testigo de lo existencial.

$${\langle\forall x::P.x\rangle\land\langle\exists x::Q.x\rangle\\\Downarrow~\\\langle\exists x:Q.x:P.x\rangle\land\langle\exists x::Q.x\rangle}$$