EQ 7: Leibniz Axiom and Theorems

(1) Axiom, Leibniz: (e = f) \( \Rightarrow \) \( E_e^z = E_f^z \)

Note 1: difference between Leibniz Inference Rule and the Leibniz Axiom.

The inference rule states that if X = Y in all states then \( E_X^z = E_Y^z\) in all states.

The axiom states that if (x = y) in one state then \(E_x^z = E_y^z \) in that state.

Note 2: the implication is one way. iow \( E_e^z = E_f^z \) \( \nRightarrow \) (e = f)

e.g: Let E \( \equiv \) false \( \wedge \) zee . Here \( E_e^z = E_f^z \) but e \( \neq \) f

Substitution Theorems:

If an equality conjuncts or implies, or a conjunction with an equality as a conjunct implies , an Expression E containing one side of the equality, you can replace that part of E with the other side of the equality.

(2) Theorem: Substitution 1: (e = f) \( \wedge\) \( E_e^z \equiv \) (e = f) \( \wedge\) \( E_f^z \)

(3) Theorem: Substitution 2: (e = f) \( \Rightarrow\) \( E_e^z \equiv \) (e = f) \( \Rightarrow\) \( E_f^z \)

(4) Theorem: Substitution 3: q \( \wedge \) (e = f) \( \Rightarrow\) \( E_e^z \equiv \) q \( \wedge \) (e = f) \( \Rightarrow\) \( E_f^z \)

Replace By True Theorems:

If a variable conjuncts or implies, or a conjunction with a variable as a conjunct implies an expression E containing that variable, the occurences of the variable in the expression can be replaced by true

(5) Theorem Replace by true 1: p \( \wedge\) \( E_p^z \equiv \) p \( \wedge\) \( E_{true}^z \)

(6) Theorem: Replace by true 2: p \( \Rightarrow \) \( E_p^z \equiv \) p \( \Rightarrow \) \( E_{true}^z \)

(7) Theorem: Replace by true 3: q \( \wedge \) p \( \Rightarrow \) \( E_p^z \equiv \) q \( \wedge \) p \( \Rightarrow \) \( E_{true}^z \)

Example:

Prove p \( \wedge \) q \( \Rightarrow \) ( p \( \equiv \) q)

\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( p \( \equiv \) q)

=\( \hspace{0.5 cm } \) recognize pattern. conjunction with a variable (p) on one side implying an expression containing the same variable
\( \hspace{0.5 cm } \) invoke Theorem (6) above, replace p in expression by true

\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( true \( \equiv \) q)

=\( \hspace{0.5 cm } \) recognize pattern. conjunction with a variable (q) on one side implying an expression containing the same variable
\( \hspace{0.5 cm } \) invoke Theorem (6) above, replace q in expression by true

\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( true \( \equiv \) true)

=\( \hspace{0.5 cm } \) Theorem: true is the identity of \( \equiv \), m \( \equiv \) m \( \equiv \) true

\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) true

=\( \hspace{0.5 cm } \) Theorem: true is the Right Zero of \( \Rightarrow \), m \( \Rightarrow \) true \( \equiv \) true

\( \hspace{2 cm }\) true

Replace By False Theorems:

If an Expression E containing a variable p disjuncts p, implies p or implies a disjunction with p on one side,p can be replaced by false in the expression

(8) Theorem: Replace by False 1: \( E_p^z\) \( \vee \) p \( \equiv \) \( E_{false}^z\) \( \vee \) p

(9) Theorem: Replace by False 2: \( E_p^z\) \( \Rightarrow \) p \( \equiv \) \( E_{false}^z\) \( \Rightarrow \) p

(10) Theorem: Replace by False 2: \( E_p^z\) \( \Rightarrow \) p \(\vee\) q \( \equiv \) \( E_{false}^z\) \( \Rightarrow \) p \(\vee\) q

(11) Theorem: Shannon: \( E_p^z\) \( \equiv \) ( p \(\wedge\) \( E_{true}^z\) ) \(\vee\) ( \( \neg \) p \(\wedge\) \( E_{false}^z\) )