Prove $\vdash \neg(A\equiv B) \equiv \neg A\equiv B$

Question

I'm having a hard time understanding how to prove this: here is the proof I've read - however I understand that this is actually proving $(B\equiv \bot) \vdash \neg(A\equiv B) \equiv \neg A\equiv B$:

$$\neg(A\equiv B)$$ <=> (axiom) $$(A\equiv B)\equiv \bot$$ <=> (Leib + axiom: $B\equiv \bot \equiv \bot \equiv B$; 'C-part' is $A\equiv p$)

Question: How come I can use $B\equiv \bot$ in an axiom? $$A\equiv \bot \equiv B$$ <=> (Leib + axiom: $A\equiv \bot \equiv \neg A$; 'C-part' is $p\equiv B$) $$\neg A \equiv B$$

Answer 1

The proof uses Equational logic (see also this post for details).

We start form the premise :

1) $¬(A≡B)$

and we want to transform it (through equivalences) into the conclusion.

The first step uses the axiom defining $\lnot$ : $\lnot A \equiv (A \equiv \bot)$ to get :

2) $(A≡B) \equiv \bot$.

The next step uses associativity of $\equiv$ to get :

3) $A≡ (B \equiv \bot)$.

Now we use Leibniz's rule :

from $D_1 \equiv D_2$ and $C[p:=D_1]$ derive $C[p:=D_2]$, where $C$ is a formula and $C[p:=D_i]$ is obtained from $C$ replacing part $p$ with formula $D_i$,

with axiom for symmetry of $\equiv$ : $(B \equiv \bot) \equiv (\bot \equiv B)$.

This means to use the axiom as $C$ and $(B \equiv \bot)$ as $D_1$ and $A$ as $D_2$, to get :

4) $A \equiv (\bot \equiv B)$.

Apply associativity again to get :

5) $(A \equiv \bot) \equiv B$

and finally use Leibniz again with the axiom for $\lnot$ to replace $(A \equiv \bot)$ in 5) with $\lnot A$ to conclude with :

6) $\lnot A \equiv B$.

Answer 2

$\vdash X\equiv X$ by rule of identity. (Equivalence is reflexive).

$\lnot X$ is equivalent to $X\equiv \bot$, by the definition of negation and falsity.   $\lnot X$ says "$X$ is false", which is to say $X\equiv\bot$.

$(X\equiv Y)\equiv Z$ is equivalent to $X\equiv (Y\equiv Z)$ because the biconditional operator is associative.   Since there is thus no ambiguity about order of association, we often express these as also being equivalent to $X\equiv Y\equiv Z$ .

The biconditional operator is also commutative, so $X\equiv Y$ is equivalent to $Y\equiv X$.

Now, applying these rules as substitutions.

$$\begin{align}&\vdash \lnot (A\equiv B)\equiv\lnot(A\equiv B) &&\text{by Identity}\\&\vdash \lnot (A\equiv B)\equiv ((A\equiv B)\equiv\bot)&&\text{by definition of negation}\\&\vdash \lnot (A\equiv B)\equiv (A\equiv (B\equiv\bot))&&\text{by association}\\&\vdash \lnot (A\equiv B)\equiv (A\equiv (\bot\equiv B))&&\text{by commutation}\\&\vdash \lnot (A\equiv B)\equiv ((A\equiv \bot)\equiv B)&&\text{by association}\\&\vdash \lnot (A\equiv B)\equiv (\lnot A\equiv B)&&\text{by definition of negation}\\&\vdash \lnot (A\equiv B)\equiv \lnot A\equiv B&&\text{by unambiguous association} \end{align}$$