Proof of Transitivity (Inference Rule) using Leibniz rule and Equanimity

Question

In Tourlakis' Mathematical logic, we are given the following primitive rules of inference [p.40]:

• Leibniz rule: (A↔B) / (C[p≔A]↔C[p≔B])
• Equanimity: (A, A↔B) / B

Capture from the book

Then he goes to derive the following inference rule, using he previous two [p.47]:

• Transitivity: (A↔B, B↔C) / (A↔C)

Capture from the book

I have trouble proving how to use the primitive rules to proof Transitivity.

Leibniz rule: I understand that the Leibniz rule replaces in C (which is well formed formulae) any occurrence of the Boolean variable (atomic) p with A to get C[p≔A] and then replaces p with B to get C[p≔B], which yields to C[p≔A]↔C[p≔B].

Equanimity: If we assume A to be t and A↔B to be t, (because that's our premise), we get that B must be also t, because that's required for A↔B to be t.

Now, I don't see how to use either of the primitive formulae to prove Transitivity, I don't quite get how to use the Leibniz rule in Tourlakis' way. I would even go further and to state Transitivity as another primitive rule of inference, but I think just two is a nicer approach.

So, how to prove Transitivity using Leibniz and Equanimity?

Thank you!

Answer 1

Note: due to the fact that the example uses $A,B,C$ as schematic letters for formulas, I'll adopt a different letter for the formulation of Leibniz's rule:

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

Thus, to apply the rule with premise $B \equiv C$, we use as $X$ the formula $A \equiv p$.

The two substitutions are: $X[p := B] = (A \equiv p)[p := B] = A \equiv B$ and $X[p := C] = (A \equiv p)[p := C] = A \equiv C$, respectively.

In conclusion:

1. $A \equiv B$

2. $B \equiv C$

3. $X[p := B] \equiv X[p := C] \text { i.e. } A \equiv B \equiv A \equiv C$ --- from 1) and 2) by Leibniz.

Regarding

in step "we use as $X$ the formula $A≡p$" we assume the formula $A$ to be atomic, so that, when replacing $p$ in $X$ for $A$ we get $A$,

the answer is: no. We assume as $X$ the "composite" formula $A \equiv p$, where $p$ is atomic.