¿Cómo puedo demostrar el principio del tercero excluido con la hipótesis dada (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?

Answer

1. 

   davy.ai

   July 28, 2023 at 7:54 pm

   Sí, con el teorema dado exluded_middle2 es posible demostrar la ley del tercero excluido. De hecho, el propio teorema es una reformulación de la ley del tercero excluido.

   Para demostrar excluded_middle2, debemos comenzar asumiendo la premisa:

   forall P Q : Prop, (P -> Q) -> (~P \/ Q)
   

   Luego queremos demostrar:

   forall P : Prop, P \/ ~P
   

   Para hacer esto, podemos hacer una prueba por contradicción: asumir que ~(P \/ ~P) y luego mostrar que esto conduce a una contradicción.

   Lemma excluded_middle : forall P : Prop, P \/ ~P.
   Proof.
   intros P.
   assert (P -> True) as p_t.
   + intros. apply I.
   + assert (~P -> True) as np_t.
     - intros. apply I.
     - assert ((P -> True) -> (~P \/ True)) as hyp.
       * intros Hp_t. apply H with (P := P) (Q := True). intros. apply Hp_t in H0. assumption.
       * destruct (hyp p_t).
         ++ left. assumption.
         ++ right. intros H'. apply H'. assumption.
   Qed.
   

   Aquí hemos usado la táctica assert para enunciar y demostrar subafirmaciones que utilizaremos en nuestra prueba general. Procedemos con estos pasos:

   1. Asumimos que P. Luego podemos demostrar True (es decir, que la afirmación siempre es verdadera) usando la táctica I.

   2. Asumimos ~P. Luego también podemos demostrar True (es decir, que la afirmación siempre es verdadera) usando la táctica I.

   3. Ahora queremos mostrar que tanto P como ~P son posibles. Aplicamos la premisa de excluded_middle2 con Q := True, lo cual se reduce a demostrar (P -> True) -> (~P \/ True). Podemos asumir P -> True y usarlo para aplicar la premisa de excluded_middle2 con Q := True.

   4. Ahora tenemos dos casos: o bien ~(P -> True) o bien ~True. Si ~(P -> True) entonces sabemos que P, como demostramos en el paso 1. Por lo tanto, podemos usar esa información para deducir Q := True y aplicar la premisa de excluded_middle2 para obtener ~P \/ True. Sabemos que P no puede sostenerse, por lo que debemos tener True.

   5. Si ~True, entonces esto es esencialmente equivalente a decir False. Por lo tanto, podemos usar la suposición de contradicción ~(P \/ ~P) para deducir False. Esto es una contradicción, por lo que nuestra suposición general (~(P \/ ~P)) debe ser falsa. Esto significa que P \/ ~P es verdadero, como se requiere.

Comments are closed.