Demuestre$\vdash (A_1 ↔ A_2) \vee (A_2 ↔ A_3) \vee (A_3 ↔ A_1) $ usando deducción natural.

Question

Creo que esto es cierto. Debido a que según el principio de la casilla de verificación, dos de $A_1, A_2, A_3$ deben tener el mismo valor verdadero. Pero no tengo idea de cómo probarlo ... ¿Puede alguien ayudarme?

Por supuesto, podemos usar leyes lógicas bien conocidas. Por ejemplo De Morgan, ley del medio excluido.

Answer 1

Comentario largo

Creo que la prueba es muy larga: podemos probar con un simple (pero similares) ejemplo :

$\vdash (A_1 \to A_2) \lor (A_2 \to A_3) \lor (A_3 \to A_1)$.

En este caso, la prueba es sencilla, el uso de EM :

1) $\vdash A_1 \lor \lnot A_1$

2) $A_1$ --- asumido [a] para $\lor$-elim

3) $A_3 \to A_1$ --- de 2) por $\to$-intro

4) $(A_2 \to A_3) \lor (A_3 \to A_1)$ --- a partir de 3) por $\lor$-intro

5) $(A_1 \to A_2) \lor (A_2 \to A_3) \lor (A_3 \to A_1)$ --- de 4) por $\lor$-intro

6) $\lnot A_1$ --- asumido [b] para $\lor$-elim

7) $A_1$ --- asumido [c]

8) $A_2$ --- de 6) y 7)

9) $A_1 \to A_2$ --- a partir de 7) y 8) por $\to$-intro, la descarga de [c]

10) $(A_1 \to A_2) \lor (A_2 \to A_3)$ --- de 9) por $\lor$-intro

11) $(A_1 \to A_2) \lor (A_2 \to A_3) \lor (A_3 \to A_1)$ --- 10) por $\lor$-intro

Ahora podemos concluir por $\lor$-elim de 1), la descarga de [a] y [b].

Answer 2

Aquí está una prueba en una Fitch estilo de deducción natural de la prueba:

Answer 3

Yo creo que se puede aprovechar el hecho de que los operadores <-> (biconditionnal) y " w " ( X-O, o exclusivo ) son, por así decir, la "negación" de cada uno de los otros , de la misma manera como & y NAND ( Que puede comprobarse mediante las tablas de verdad).

---

Voy a utilizar los siguientes hechos ( que puede ser comprobado con deducción natural, salvo, quizás, la primera parte de la realidad 1 , que está vinculado a la asociatividad de la disyunción; esta muy básico, hecho que podría requerir un método semántico, no sé).

(1) (AvBvC) es equivalente a (AvB)v C , que a su vez es equivalente a
(~ (AvB) --> C )

(2) [ regla de sustitución ] de ~(<--> B) inferir ( AwB) , y recíprocamente ( con " w" significado "o exclusivo" )

(3) [ w elim 1 ]de (AwB) y, inferir ~B / a partir de (AwB) y B, inferir ~

(4) [ w elim 2 ] de (AwB) y ~inferir B / a partir de (AwB) y ~B inferir Un

(5) [<-> Intro ] De (a --> B) y (B -->a) inferir (<--> B) [ <-> Intro ]

Estrategia :

Hecho (1) significa que, con el fin de demostrar (A1<->A2) v (A2<->A3) v (A3<->A1)

sólo tenemos que probar que : ~ ( (A1<->A2) v (A2<->A3) ) --> (A3<->A1) , que hace de la condicional a prueba una estrategia posible.

Prueba :

Ahora, supongamos que ( condicional prueba) que tiene :

~ ( (A1<->A2) v (A2<->A3) ).

Por la ley de DeMorgan, inferir, a partir de que :

~ (A1<->A2) & ~ (A2<->A3).

Eliminar y para llegar

~ (A1<->A2)

~ (A2<->A3).

El uso hecho (2) - que es : ~ (A <->B) fib (AwB) para obtener :

(A1 w A2)

(A2 w A3)

Ahora, supongamos que ( condicional a prueba dentro de nuestros principales condicional de la prueba) que han A1.

Usando el hecho de (3) inferir, a partir de A1 que : ~ A2. Y, usando el hecho de (4), inferir, a partir de ~ A2 A3 es cierto. Usted ha demostrado que :

                               IF A1 THEN A3

De la misma manera, supongamos que ( condicional prueba, aún dentro de la principal prueba condicional) que han A3.

Usando el hecho de (3), inferir que A2 es falso. Y usando el hecho de (4), inferir, a partir de ~A2 A1 es verdadero. Usted ha demostrado que :

                                  IF A3 THEN A1

Ahora , usando el hecho de que (5) (<-->Intro) inferir, a partir de (A1 --> A3) y (A3 --> A1) que

                                     **A1 <--> A3** 

Bajo nuestra principal hipótesis : ~ ( (A1<->A2) v (A2<->A3) ), hemos demostrado : A1 <--> A3.

El condicional a prueba la regla nos permite derivar de ahí que :

         ~  ( (A1<->A2) v (A2<->A3) ) --> A1 <--> A3

Pero , por el hecho de que (1) sabemos que esto es equivalente a :

            ( (A1<->A2) v (A2<->A3) ) v  (A1 <--> A3)  , 

y, finalmente, a nuestro objetivo :

               (A1<->A2) v (A2<->A3)  v  (A3 <--> A1) 

( a sabiendas de que el <-> operador es conmutativa)