What is Leibniz rule of inference? I don't understand how to use the Leibniz rule of inference to prove problems. For example, To prove this theorem: 
~(A ≡ B) ≡ ~A ≡ B

~(A ≡ B) 
<axiom>
A ≡ B ≡ ⊥
<leib + axiom: B ≡ ⊥ ≡ ⊥ ≡ B; "C-part" is A ≡ p; p fresh>
A ≡ ⊥ ≡ B
<leib + axiom: A  ≡ ⊥ ≡ ~A; "C-part" is p  ≡ B; p fresh>
~A ≡ B

It's not finished but can you guys help me understand why they used Leibniz. I can't visualize it. I know the rule of inference formula for Leibniz and looked online but i just don't understand when and how to use it. Also, please explain the c-part and p fresh. Thanks!
 A: The OP had three questions:  


*

*What is Leibniz rule of inference?

*How to use it?

*How to prove $\neg{(A \Leftrightarrow B)} \Leftrightarrow \neg{A} \Leftrightarrow B$ ?


The following is an attempt to improve on the already accepted answer. Hopefully it would help those who are reading Tourlakis' book and have similar questions.
The original idea behind Leibniz rule is actually very easy: On a domain where $x$ and $y$ are defined,  $\forall{P}, x=y \Leftrightarrow P(x)=P(y)$ , where $P$ is a predicate.
This is known as the Principle of Identity of Indiscernibles of Leibniz (see Kleene). Note that the keyword here is "for all". So, given that $x=y$ in R, $sin(x)=sin(y), cos(x)=cos(y), tan(x)=tan(y), ...$ and so on.
In propositional logic, this is done the abstract way. The $\forall P$ is replaced by a (to be constructed) well-formed formula $C$, and the place-holder "$( )$" is represented by a logic variable $p$ that occurs in $C$. The Leibniz principle now becomes the Leibniz rule:
$A \Leftrightarrow B  \Leftrightarrow C[p:=A] \Leftrightarrow C[p:=B]$
where $C[p:=A]$ means to substitute $A$ for $p$ in $C$, much like a predicate $P()$ would be a valid predicate only if you put an $x$ in the place holder "$()$". (This substitution is presented as Theorem 1 in Kleene's.)
Tourlakis lists only two inference rules: Equanimity and Leibniz. Some texts also includes Transitivity, which can be easily proved (as Tourlakis did as an example) using Leibniz and Equanimity:
$A \Leftrightarrow B, B \Leftrightarrow C \vdash A \Leftrightarrow C$
Proof:
(1) $A \Leftrightarrow B$ (hypothesis)
(2) $B \Leftrightarrow C$ (hypothesis)
(3) $A \Leftrightarrow B  \Leftrightarrow A \Leftrightarrow C$ ((2), Leibniz)
(4) $A \Leftrightarrow C$ ((1), (3), Equanimity)  
where in (3) we have set the "$C$" in the Leibniz rule to be the (sensibly constructed) well-formed formula $A \Leftrightarrow p$, where p does not occur in A. We then replace $p$ in $A \Leftrightarrow p$ by B and by C. Leibniz rule then stipulates that (3) is valid.
The above basic proof suggest a theorem to combine Leibniz and Equanimity:
Given that $A \Leftrightarrow B$, if $C[p:=A]$ is valid, then $C[p:=B]$ is valid, i.e. $C[p:=A]$ can be replaced by $C[p:=B]$. This is presented in Tourlakis as (Equanimity+Leibniz) and a corollary to Theorem 5 in Kleene. We can call it a relacement theorem here.
The Distributivity of Not (the third OP question) can now be proved easily:
$\neg{(A \Leftrightarrow B)} \Leftrightarrow \neg{A} \Leftrightarrow B$
Proof:
(1) $\neg{(A \Leftrightarrow B)}$ (hypothesis)
(2) $A \Leftrightarrow B \Leftrightarrow \perp$ (axiom)
(3) $A \Leftrightarrow \perp \Leftrightarrow B$ (replacement)
(4) $\neg{A} \Leftrightarrow B$ (replacement)
where:
in (2) we have invoked an axiom $\neg{A} \Leftrightarrow A \Leftrightarrow \perp$, and have substituted $A \Leftrightarrow B$ for $A$
in (3) we have replaced $B \Leftrightarrow \perp$ by $\perp \Leftrightarrow B$
in (4) we have invoked $\neg{A} \Leftrightarrow A \Leftrightarrow \perp$ again and have replaced $A \Leftrightarrow \perp$ by $\neg{A}$ 
Reference:
(1) Mathematical Logic, Kleene
(2) Mathematical Logic, Tourlakis
A: In equational logic, the Leibniz's rule of inference is:

from $A \equiv B$, infer $C [p:=A] \equiv C [p:=B]$,

where $A,B,C$ are formulas and $p$ is a sentential letter.
In a nutshell, if we replace in a formula $C$ (like e.g. $p \lor q$) the sentential letter $p$ in turn with a formula $A$ (e.g. $r \to s$) and an equivalent formula $B$ (e.g. $\lnot r \lor s$) the two results, call them $C_A$ and $C_B$, are also equivalent.
In the example: $(r \to s) \lor q \equiv (\lnot r \lor s) \lor q$.

For waht I understand, you are trying to prove:

$\lnot (A \equiv B) \equiv (\lnot A \equiv B)$.

Assume the premise:
1) $\lnot (A \equiv B)$
and use the axiom: $\lnot A \equiv A \equiv \bot$ to re-write it as:
2) $(A \equiv B) \equiv \bot$
Then apply Associativity of $\equiv$: $((A \equiv B) \equiv C) \equiv (A \equiv (B \equiv C))$, and the Equanimity rule of inference: from $A \equiv B$ and $A$, infer $B$ [it is the "equational" version of Modus Ponens] to get:
3) $A \equiv (B \equiv \bot)$.
Consider now the formula $A \equiv p$ (with $p$ new) and use the axiom: $(B \equiv \bot) \equiv (\bot \equiv B)$ [it is an instance of the more general axiom expressing the Symmetry of $\equiv$: $(A ≡ B) ≡ (B ≡ A)$ ].
We have two equivalent formulas that we will use in the $C$ formula of the Leibniz's rule, where $C$ is $A \equiv p$.
The two substitutions are: $(A \equiv p) [p := B \equiv \bot]$ and $(A \equiv p) [p := \bot \equiv B]$ respectively, and they are equivalent. Thus:
4) $(A \equiv (B \equiv \bot)) \equiv (A \equiv (\bot \equiv B))$.
Then apply Equanimity again with 3) to get:
5) $A \equiv (\bot \equiv B)$.
The final step is Associativity again followed by Equanimity to conclude with:

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


Note: my source for axioms and rules is:


*

*George Tourlakis, Mathematical Logic (2008).

