## Saturday, October 1, 2011

### EQ 3: Inference Rules

The logic EQ has four inference rules

(1) Substitution

$$\frac{E}{E[v := F]}$$

where E is an expression, v is a list of variables and F is a corresponding list of expressions.

Iow, if E is a theorem, so is E with all the variables in V replaced by the corresponding expressions in F.

E.g: Let E be 2.x/2 = x be a theorem.

Then by substitution, so is 2.(j + 5) / 2 = j + 5 where v=x and E = j+5

(2) Leibniz

$$\frac{X=Y}{E[z:=X]=E[z:=Y]}$$

NB: z is a variable, NOT an expression.

Two ways of looking at Leibniz

(A) Given an equality X = Y and an expression E,

(1) Choose a variable z within E
(2) Replace the equality with a new equality with z replaced by X on one side and Y on the other

(B) Given E,

(1) spot an *expression X* (NOT variable ) within E that needs replacement
(2) Find an equality X = Y
(3) consider the given expression E to be actually E [z := X]
(4) Use Leibniz with the equality (from (2) ) to get E [z := Y]

this is written as
$$\hspace{2 cm } E[z:=X]$$
= $$\hspace{0.5 cm }$$ Leibniz. z is z. X = Y
$$\hspace{2 cm } E[z:=Y$$

eg:

Given m = 2j (note: this is the equality X = Y) and E is m/2 = 2.(j - 1) prove that 2j/2 = 2(j-1)

Leibniz usage B: m on the LHS of E needs to be replaced with 2j, so we look for an equality with m on the left side, which we find in the given equality. If we consider the LHS of E to be E[z := m], then

$$\hspace{2 cm } m/2 = 2(j - 1)$$
= $$\hspace{0.5 cm }$$ Leibniz. z is m, m = 2j
$$\hspace{2 cm } 2j/2 = 2(j - 1)$$

(C) Combined use of Substitution and Leibniz

Strictly speaking, Substitution and Leibniz are distinct inference rules and the two should be used distinctly

Given we know that 2x/2 = x (note: this is the equality X=Y)

let E be 2j/2 = 2(j+1). prove j = 2(j-1 )

(separate use of Substitution and Leibniz)
$$\hspace{2 cm }E \equiv$$ 2j/2 = 2(j - 1)
= $$\hspace{0.5 cm }$$ Substitution j := x
$$\hspace{2 cm }$$ 2x/2 = 2(x - 1)
= $$\hspace{0.5 cm }$$ Leibniz z is 2x/2 with equality 2x/2 = x
$$\hspace{2 cm }$$ x = 2(x - 1)
= $$\hspace{0.5 cm }$$ Substitution x := j
$$\hspace{2 cm }$$j = 2(j - 1) QED

(simultaneous use of Substitution and Leibniz collapses some steps)
$$\hspace{2 cm }E \equiv$$ 2j/2 = 2(j - 1)
= $$\hspace{0.5 cm }$$ Substitution and Leibniz 2x/2:= x
$$\hspace{2 cm }$$j = 2(j - 1) QED

(3) Transitivity

$$\frac{X=Y,Y=Z}{X=Z}$$

iow if X = Y and Y = Z are theorems, so is X = Z

(4) Equanimity

$$\frac{E,E=F}{F}$$

iow a theorem is either an axiom or the result of an inference rule where the premises are axioms

Example for use of all 4 inference rules

Prove that $$\neg p \equiv p \equiv false$$

Proof:

(0) $$\hspace{2 cm } \neg p \equiv p \equiv false$$
(1) = $$\hspace{0.5 cm }$$ Leibniz and Substitution with Theorem $$\neg (x \equiv y) \equiv \neg x \equiv y$$ used in the reverse direction, substituting x,y := p,p and z = $$\neg p \equiv p$$
(2) $$\hspace{2 cm } \neg (p \equiv p) \equiv$$ false
(3) = $$\hspace{0.5 cm }$$ Leib + Sub using Theorem Identity of $$\equiv$$,$$x \equiv x \equiv$$ true , z is p $$\equiv$$ p, and x := p
(4) $$\hspace{2 cm } \neg true \equiv false$$
(3) = $$\hspace{0.5 cm }$$ is an Axiom and therefore
(5) $$\hspace{2 cm }$$ true QED

and since (0) = (2) and (2) = (4) and (4) = (5), by Transitivity (0) = (4)

and since (0) = (4) and (4) is a theorem, (0) is a theorem by Equanimity.