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.