Using rules of inference (Leibniz) to prove theorems.

Question

Leibniz: If $A \equiv B$ is a theorem, then so is $C[p:= A] \equiv C[p:= B]$.
Note: p is "fresh" means p doesn't occur in $A, B, C$.

I am trying to understand how to use Leibniz rule of inference for my proof. I understand equanimity, and the other axioms and boolean logic. The example below (equational proof) is giving me a hard time.

Prove theorem $A \vee A \wedge B \equiv A$:
$A \vee (A \wedge B)$
$\Leftrightarrow$ < proven theorem $(A \wedge T \equiv A)$ + Leib, C-part: $p \vee (A \wedge B)$, p fresh >
$(A \wedge T) \vee (A \wedge B)$
$\Leftrightarrow$ < Distributivity of $\wedge$ over $\vee$ (2.4.23 (ii)) >
$A \wedge (T \vee B)$
$\Leftrightarrow$ < proven theorem $( B \vee T)$ (2.4.7) + redundant true metatheorem + symmetry of $\vee$, therefore theorem $T \vee B \equiv T$ + Leib, C-part: $A \wedge p$, p fresh >
$A \wedge T$
$\Leftrightarrow$ < proven theorem $( A \wedge T \equiv A)$ (2.4.20) >
$A$

I dont understand how to go from that first line to the second line. Why are we using Leib on $(A \wedge T \equiv A)$ and not the formula in the fist line? How do you choose what C should be? Also I tried working out Leib on $(A \wedge T \equiv A)$, I got $(A \wedge T) \vee (A \wedge B) \equiv A \vee A \wedge B$, so then why does the following line only take the left side of $\equiv$?

Answer 1

I will give you this answer.

Using the two identities : $A \equiv A \land T$ and $T \equiv B \lor T$, we have that :

$A \equiv A \land T \equiv A \land (B \lor T)$

by Leibniz.

Using Distributive law we have :

$ \equiv (A \land B) \lor (A \land T) \equiv (A \land B) \lor A$

by Leibniz, using again the above identity.

Finally :

$ \equiv A \lor (A \land B)$

by Commutativity.

About the correct understanding of Leibniz, I will refer to George Tourlakis, Mathematical Logic (2008), taht is based on equational logic.

See page 39, 1.4.1 Definition. (Schema Instance) :

Here are some examples of schemata:

(1) $A$: It is a formula-metavariable; if we replace the letter "$A$" by some formula, well, we get that formula as the result!

(2) $(A \equiv B)$: This schema has two formula-metavariables, $A$ and $B$. Whatever formulae we may replace $A$ and $B$ with, we get a formula [...]

(3) $A[p := B]$: This schema has two formula-metavariables, $A$ and $B$, and a Boolean metavariable, $p$. Whatever formulae we replace $A$ and $B$ with, and whichever Boolean variable replaces $p$, we get a formula [...].

See also page 40, 1.4.2 Definition. (Rules of Inference) :

The following two are our primitive or primary rules of inference, given with the help of the syntactic variables $A, B, p, C$ : [...]

from $\quad A \equiv B \quad $ , infer $\quad C[p := A] \equiv C[p := B] \quad$ (Leibniz).

For the "correct usage" of Leibniz you must take into account the difference between the (meta)-variables $A$ and $B$, which stay for formulas, and the (meta)-variable $p$, which stay for a Boolean letter.

In applying Leibniz to the formula

$A \land B \equiv A$

you must understand that the equivalence is between formulas; when you apply Leibniz, you must replace a Boolean letter "contained" into an existing formula (call it first) with another formula (call it second), obtaining a resulting formula (call it third). Leibniz says that third will be equivalent to first.

In our application, we have replaced into the formula $A$ (the $C$ of the rule) the Boolean letter $A$ (now, the $p$ of the rule) with the formula $A \land T$ (the $B$ of the rule, that is equivalent to $A$); this is the reason why : $A \equiv A \land T$.

So, the conclusion is, do not "mix" the different styles of variable in the formulas.

Answer 2

You can use Leibniz rule, but it is a rather ricky rule, if you use it with formulas that are not theorems you can go horribly astray, so i think it is more for protection than anything else.

You make it more complicated than it is by trying to do to many steps at once. better to do it really step by step (and don't worry about using to much paper)

I am not sure which book you use, and every book is a bit different

in this I use the rules from http://en.wikipedia.org/wiki/Equational_logic (and do play around with them as well)

1  (A v (A & B)) <-> (A v (A & B))          Theorem
2  (A & T ) <-> A                           Theorem
3  (A v (A & B)) <-> ((A & T)  v (A & B))   1,2 Leibniz
4  ((A & T) v (A & B)) <-> (A & (T v B))    Distribution Theorem
5  (A v (A & B)) <-> (A & (T v B))          3,4 Equanimity
6  (T v B) <-> T                            Theorem
7  (A v (A & B)) <-> (A & T)                5,6 Leibniz
8  (A v (A & B)) <-> A                      2,7 Equanimity
=======================

Hope this helps

Answer 3

If you can use Natural Deduction, working with assumption is much easier :

(a) we prove the "direction" : $A \rightarrow ...$

a.1) assume $A$

a.2) $A \lor (A \land B)$ --- from a.1) by $\lor$-intro

a.3) $A \rightarrow (A \lor (A \land B))$ --- from a.2) by $\rightarrow$-intro, discharging a.1).

(b) we prove the "direction" : $... \rightarrow A$

b.1) assume $A \lor (A \land B)$

b.2) assume $A$

b.3) assume $A \land B$

b.4) $A$ --- from b.3) by $\land$-elim

b.5) $A$ --- from b.1), b.3) and b.4), by $\lor$-intro, discharging b.2) and b.3)

b.6) $(A \lor (A \land B) ) \rightarrow A$ --- from b.5) by $\rightarrow$-intro, discharging b.1).

we have now :

$A \rightarrow (A \lor (A \land B))$

and

$(A \lor (A \land B) ) \rightarrow A$

and the equivalence is proved.