¿Alguien puede ayudarme a probar ~(AvB) |- ~(BvA) mediante deducción natural?

Hecho 1. ¬(A ∨ B) |= ¬(B ∨ A)

Prueba. La forma negada de la conclusión sugiere una forma obvia de proceder: asumir (B ∨ A) con la esperanza de derivar una contradicción. La forma disyuntiva de esta suposición sugiere el segundo paso (prueba por análisis de caso): asumir B, derivar algún enunciado Γ, luego asumir A y derivar ese Γ nuevamente; luego usando (B ∨ A) y esas dos derivaciones concluyen Γ. He aquí una forma de aplicar esas técnicas:

1. ¬(A ∨ B) [ Dado ]
2. (B ∨ A) [ Suposición ]
3. B [ Suposición ]
4. (A ∨ B) [ ∨-introducción, 3 ]
5. ⊥ [ ⊥-introducción, 4, 1]
6. A [ Suposición ]
7. (A ∨ B) [ ∨-introducción, 6 ]
8. ⊥ [ ⊥-introducción, 7, 1]
9. ⊥ [ ∨-eliminación, 2, 3-5, 6-8]
10. ¬(B ∨ A) [ ¬-introducción, 2-9].

Hecho 2. ¬(A ∨ ¬(A ∧ B)) ≡ ⊥

Prueba. El espacio combinatorio es más grande aquí, dado que no ha especificado qué reglas puede usar y si debe probar esto de manera semántica, teórica, etc. Aquí esbozaré una variante algebraica. Queremos mostrar que ¬(A ∨ ¬(A ∧ B)) ≡ ⊥. Podemos proceder de la siguiente manera:

1. ¬(A ∨ ¬(A ∧ B)) ≡ ⊥ [ Objetivo ]
2. (UN ∨ ¬(UN ∧ B)) ≡ ⊤
3. (A ∨ (¬A ∨ ¬B)) ≡ ⊤ [ De Morgan ]
4. (A ∨ ¬A ∨ ¬B) ≡ ⊤ [ Asociatividad ]
5. (⊤ ∨ ¬B) ≡ ⊤
6. ⊤ ≡ ⊤.

Otro método sería utilizar valoraciones (tablas de verdad). Queremos mostrar que v(¬(A ∨ ¬(A ∧ B))) = 0. El hecho útil es: v(¬φ) = 1 - v(φ). Procedemos de la siguiente manera.

1. v(¬(A ∨ ¬(A ∧ B))) = 0 [ Objetivo ]
2. v(A ∨ ¬(A ∧ B)) = 1
3. v(A) = 1 o v(¬(A ∧ B)) = 1
4. v(A) = 1 o v(A ∧ B) = 0
5. v(A) = 1 o (v(A) = 0 o v(B) = 0)
6. (v(A) = 1 o v(A) = 0) o v(B) = 0
7. 1 o v(B) = 0
8. 1

Esto es más o menos lo mismo que el anterior. Puedes ir con el que está más cerca del sistema que usas. No justifiqué los pasos porque, como se ha señalado, no sabemos qué reglas puedes usar.

Demostrar que una fórmula φ es una contradicción equivale a derivar ⊥ de ella (es decir: φ ⊢ ⊥ ).

Prueba :

(i) ~(Av~(A&B)) --- premisa

(ii) ~A --- asumido [1]

(iii) A&B --- asumido [2]

(iv) A --- de (iii) por &-elim

(v) ⊥ --- de (ii) y (iv) por →-elim

(vi) ~(A&B) --- de (iii) y (v) por →-intro, descargando [2]

(vii) Av~(A&B) --- de (vi) por v-intro

(viii) ⊥ --- de (i) y (vii) por →-elim

(ix) A --- de (ii) y (viii) por RAA (o Doble Negación ), descargando [1]

(x) Av~(A&B) --- de (ix) por v-intro

(xi) ⊥ --- de (i) y (x) por →-elim

Conclusión :

~(Av~(A&B)) ⊢ ⊥

En primer lugar, ¿puedo cambiar primero usando las reglas de De Morgan ~(AvB)?~A&~B

Claro, podría usar reglas derivadas , sin embargo, el argumento de deducción natural más convincente para esta conmutatividad usaría las reglas fundamentales de inferencia; mostrando así que la conmutatividad se deriva directamente de las reglas de introducción que tienen versiones del lado izquierdo y derecho.

Después de todo, si usaste deMorgan's, entonces conmutarías una conjunción antes de usar deMorgan's nuevamente. Entonces, dado que tiene que justificar la conmutación de cualquier manera, también puede hacerlo sin usar ninguna regla derivada.

  1|_ ~(A v B)         : Premise
  2|   |_ B v A         : Assumption
  3|   |   |_ B          : Assumption
  4|   |   |  A v B      : Disjunction Introduction (3, Left)
   |   |   +
  5|   |   |_ A          : Assumption
  6|   |   |  A v B      : Disjunction Introduction (5, Right)
  7|   |  A v B         : Disjunction Elimination (2,3-4,5-6)
  8|   |  #             : Negation Elimination (1,7)
  9|  ~(B v A)         : Negation Introduction (2-8)

Y el segundo es:

~(Av~(A&B))

Tengo que deducir que esto es una contradicción.

Parece difícil porque se niega todo el argumento. No estoy seguro de qué asumir primero.

Use la Ley del Medio Excluido, suponga que A o ~A debe ser el caso. Para eliminar esa disyunción a algo usable, tienes que introducir una disyunción y una negación de una conjunción.

  0|  A v ~A              : Axiom (L.E.M.)
  1|_ ~(A v ~(A & B))     : Premise
  2|   |_ A                : Assumption
  3|   |  A v ~(A & B)     : Disjunction Introduction (2, R)
   |   +
  4|   |_ ~A               : Assumption
  5|   |   |_ A & B         : Assumption
  6|   |   |  A             : Conjunction Elimination (5, R)
  7|   |   |  #             : Negation Elimination (4,6)
  8|   |  ~(A & B)         : Negation Introduction (5-7)
  9|   |  A v ~(A & B)     : Disjunction Introduction (8, L)
 10|  A v ~(A & B)        : Disjunction Elimination (0,2-3,4-9)
 11|  #                   : Negation Elimination (1,10)

Revisión: Esto se puede reducir un poco.

  1|_ ~(A v ~(A & B))     : Premise
  2|  |_ A & B             : Assumption
  3|  |  A                 : Conjunction Elimination (2)
  4|  |  A v ~(A & B)      : Disjunction Introduction (3)
  5|  |  #                 : Negation Elimination (4,1)
  6|  ~(A & B)            : Negation Introduction (2-5)
  7|  A v ~(A & B)        : Disjunction Introduction (6)
  8|  #                   : Negation Elimination (7,1)

A continuación se muestran formas de probar estos argumentos.

El primero utiliza las Reglas de De Morgan (DeM), eliminación de conjunciones (E), introducción de conjunciones (∧I).

El objetivo del primer argumento es mostrar que dos oraciones conmutan sobre la disyunción conectiva con una negación conectiva sobre toda la disyunción. Esto requiere dividir la oración en cada disyunción y luego recombinar las oraciones en el orden diferente.

El segundo utiliza las Reglas de De Morgan (DeM), la eliminación de conjunciones (∧E), la eliminación de doble negativo (DNE) y la introducción de contradicciones (⊥I).

Referencias

Editor y comprobador de pruebas de deducción natural JavaScript/PHP estilo Fitch de Kevin Klement http://proofs.openlogicproject.org/

PD Magnus, Tim Button con adiciones de J. Robert Loftis remezcladas y revisadas por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, invierno de 2018. http://forallx.openlogicproject.org/