Derivación lógica sentencial: ~(A ≡ B) ├ (~A ≡ B)

El bicondicional es aburrido porque tienes que dividirlo en dos partes:

1) ¬[(A→B) ∧ (B→A)] --- premisa

2) A --- asumido [a]

3) B→A --- de 2)

4) B --- asumido [b]

5) A→B --- de 4)

6) (A→B) ∧ (B→A) --- de 3) y 5)

7) ¡contradicción! con 1)

8) ¬A --- de 2) y 7), descargando [a]

9) B → ¬A --- de 4) y 8), descargando [b].

De la misma manera, tenemos que derivar: ¬A → B .

10) ¬A --- asumido [c]

11) ¬B --- asumido [d]

12) A --- asumido [e]

13) ¡contradicción! con 10)

14) B --- de 13)

15) A→B --- de 12) y 14), descargando [e]

16) B --- asumido [f]

17) ¡contradicción! con 11)

18) A --- de 17)

19) B→A --- de 16) y 18) descargando [f]

20) (A→B) ∧ (B→A) --- de 15) y 19)

21) ¡contradicción! con 1)

22) B --- de 11) por Doble Negación , descargando [d]

23) ¬A→B --- de 10) y 22), descargando [c].

Ahora concluimos de 9) y 23) con:

24) ¬A ≡ B .

Aquí hay una prueba usando el software Fitch: