Ayuda con la prueba ∀x:X(P⇒Q)⊣⊢∃x:X.(P∨Q)

Question

Estoy trabajando en un cálculo proposicional prueba y me gustaría confirmar que mi prueba es correcta ya que no estoy familiarizado con estos todavía.

EDIT: estamos usando las Matemáticas de Estructuras Discretas para informática por Gordon Ritmo.

Estos son la Equivalencia de las Leyes que nos dieron: http://www.filedropper.com/laws

De acuerdo a Peter Smith comentario en su respuesta a continuación:

A partir de lo que está disponible por medio de la línea de pasajes, el Ritmo parece ser el uso de un estándar de sistema de Deducción Natural, con subproofs

¬∀x:X.¬(P⇒Q)⊣⊢∃x:X.(¬P∨Q)

Mi razón principal para preocupante es que estas pruebas parecen ser los opuestos el uno del otro.

1   ¬∀x:X.¬(P⇒Q)    hypothesis  
2   ∃x:X.¬¬(P⇒Q)    ∃x:X.P ≡ ¬∀x:X.¬P   
3   ¬¬(P⇒Q)[x\x]    ∃ elimination   
4   ¬¬(P⇒Q)         P ≡ P[x\x]  
5   P⇒Q             double negation 
6   ¬P∨Q            P⇒Q ≡ ¬P∨Q  
7   (¬P∨Q)[x\x]     P ≡ P[x\x]  
8   ∃x:X.(¬P∨Q)     ∃ introduction

o//o proven for LHS

9   ∃x:X.(¬P∨Q)     hypothesis  
10  (¬P∨Q)[x\x]     ∃ elimination   
11  ¬P∨Q            P ≡ P[x\x]  
12  P⇒Q             P⇒Q ≡ ¬P∨Q  
13  (P⇒Q)[x\x]      P ≡ P[x\x]  
14  ∃x:X.(P⇒Q)      ∃ introduction  
15  ¬∀x:X.¬(P⇒Q)    ∃x:X.P ≡ ¬∀x:X.¬P

o//o proven for RHS

Gracias de antemano por sus sugerencias.

ACTUALIZACIÓN:

Tengo un "modelo de respuesta" por un problema similar.

∀x:X.¬(P^Q)⊣⊢∃x:X.¬(¬P∨¬Q)

1   ∀x:X.¬(P^Q)                 hypothesis
2   ¬(P^Q)[x\x]                 ∀ elimination
3   ¬(P^Q)                      P ≡ P[x\x]
    4   ∃x:X.¬(¬P∨¬Q)           assume
    5   ¬(P^Q)                  copy 3
    6   ∃x:X.¬(¬P∨¬Q)           assume
        7   ¬(¬P∨¬Q)            sub-hypothesis
        8   ¬(P^Q)              De Morgan's law
    9   ¬(¬P∨¬Q)⇒(P^Q)          ⇒ introduction on 7-8
    10  (¬(¬P∨¬Q)⇒(P^Q))[x\x]   P ≡ P[x\x]
    11  ∀x:X.((¬(P^Q))⇒(P^Q))   ∀ introduction
    12  P^Q                     ∃ elimination using 6
13  ∃x:X.¬(¬P∨¬Q)               ¬ introduction by contradiction using 4-5, 6-12

o//o proven for LHS

14  ∃x:X.¬(¬P∨¬Q)               hypothesis
15  ∀x:X.(¬P∨¬Q)                ∃x:X.P ≡ ¬∀x:X.¬P
16  (¬P∨¬Q)[x\x]                ∀ elimination
17  ¬P∨¬Q                       P ≡ P[x\x]
    18  ¬P                      assume
        19 P^Q                  sub-hypothesis
        20 P                    ^ elimination type 1 on 19
        21 P^Q                  sub-hypothesis
        22 ¬P                   copy 18
    23  ¬(P∨Q)                  ¬ introduction by contradiction using 19-20, 21-22
    24  ¬Q                      assume
        25  P^Q                 sub-hypothesis
        26  Q                   ^ elimination type 1 on 25
        27  P^Q                 sub-hypothesis
        28  ¬Q                  copy 24
    29  ¬(P∨Q)                  ¬ introduction by contradiction using 25-26,27-28
30  ¬(P^Q)                      V elimination using 18-23, 24-29
31  ¬(P^Q)[x\x]                 P ≡ P[x\x]
32  ∀x:X.¬(P^Q)                 ∀ introduction

o//o proven for LHS

En un método alternativo, a pasos de 18 - 29 podría evitarse mediante el uso de De Morgan de la ley donde

¬(P^Q) ≡ (¬P∨¬Q)

Gracias de antemano por mirar en esta.

Última actualización: he podido evitar hacer esta pregunta, pero gracias a toda la gente que trató de ayudarme. Voy a mirar en las respuestas ahora mismo y marca el mejor para referencia en el futuro.

Answer 1

1. Cualquier otra cosa es esto, esto no es proposicional de cálculo -- como el cálculo proposicional carece individuales de los cuantificadores.
2. Usted no dice lo/cuyo sistema de cálculo de predicado está utilizando (libro de texto de referencia? la notación es desconocida para mí), pero no conozco ningún sistema que permite a los el cuantificador existencial eliminación en la forma en que parecen estar utilizando es.

Una deducción normal de este tipo de cosas, el uso de la "introducción" y "eliminación" de las reglas, que se parecen más a esto:

1 $\quad\neg\forall x \neg (\varphi(x) \to \psi(x))$

2 $\quad\exists x (\varphi(x) \to \psi(x))$

3 $\quad|\quad (\varphi(a) \to \psi(a))\quad$ Asunción

4 $\quad|\quad (\neg\varphi(a) \lor \psi(a))\quad$ $\to/\lor$

5 $\quad|\quad \exists x(\neg\varphi(x) \lor \psi(x))\quad$ $\exists$-introducción

6 $\quad \exists x(\neg\varphi(x) \lor \psi(x))\quad$ $\exists$-eliminación, de 2 y subproof 3 -- 5

Answer 2

La prueba se ve como un buen inicio, para mí, y es muy completa! Generalmente, los cuantificadores se utilizan con los predicados, por ejemplo,$$\lnot \forall x.\lnot(P(x)\rightarrow Q(x)),$$ and then, $$\exists x. \lnot\lnot(P(x)\rightarrow Q(x)),$$ etc., so your notation is a bit unconventional.

But I understood well enough that your notation is to be taken as predicates about a quantified $ x\in X$, which you (existentially) instantiate some "a" to stand in for "some x", then proceed, until you eliminate the instantiated "a" back to an existentially quantified $x$.

También, al crear instancias de un cuantificador existencial, por lo general se lo hace con un "subproof": sangría, para ayudar a delinear el ámbito en el que se crea una instancia.

---

Dicho esto, la lógica de la prueba de la siguiente manera suficiente claridad.

Con respecto a sus preocupaciones: Cuando usted tiene una equivalencia (para probar), los pasos para la primera implicación son una especie de (a falta de un mejor término) "al revés" ("opuesto") cuando se acredite la segunda implicación. Eso se debe en parte a la naturaleza de la doble implicación / equivalencia, y el hecho de que la lógica de la manipulación en su prueba (aparte de la eliminación de cuantificador/introducción) que participan sólo equivalencias (identidades).

Buen trabajo de mostrar su trabajo. Y felicitaciones por hacer el esfuerzo para justificar todos sus pasos en tu prueba!

---

Con respecto a su Edición: usted realmente debería incluir subproofs en su prueba: como la introducción de una hipótesis al eliminar/crear una instancia de la existencialmente cuantificada declaración, y la necesidad de indicar el alcance de que la creación de instancias por la sangría, y luego terminar la subproof por la reintroducción del cuantificador existencial (citando la subproof en la justificación). Tal vez usted puede seguir la lógica aquí (Nota, sin embargo, como en Peter Smith respuesta, los predicados se suelen escribir con un argumento (variable o constante):

¬∀x:X.¬(P⇒Q)⊣⊢∃x:X.(¬P∨Q)

1   ¬∀x:X.¬(P⇒Q)    hypothesis  
2   ∃x:X.¬¬(P⇒Q)    ∃x:X.P ≡ ¬∀x:X.¬P (1)   
     |3 ¬¬(P⇒Q) assumption (P ≡ P[x\x]) 
     |4  P⇒Q    double negation (3)
     |5  ¬P∨Q   P⇒Q ≡ ¬P∨Q (4)  
     |6 ∃x(¬P∨Q)    ∃ introduction  (P ≡ P[x\x])    
7   ∃x:X.(¬P∨Q) ∃ elimination (2) & (3 - 6)

o//o proven for LHS

9   ∃x:X.(¬P∨Q) hypothesis  
     |10 (¬P∨Q) assumption ((P ≡ P[x\x]))       
     |11  P⇒Q   P⇒Q ≡ ¬P∨Q (2)  
     |12 ∃x(P⇒Q)    ∃ introduction  (P ≡ P[x\x])
13  ∃x:X.(P⇒Q)  ∃ elimination (9) & (10-12)     
14  ¬∀x:X.¬(P⇒Q)    ∃x:X.P ≡ ¬∀x:X.¬P

o//o proven for RHS