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.