Equivalence Transformation

Overview

Equivalence-transformation is a proof system used alongside classical truth-functional predicate logic. It is the foundation upon which predicate transformers are based.

A proposition is said to be a tautology if it evaluates to $T$ in every state it is well-defined in. We say propositions $E1$ and $E2$ are equivalent if $E1=E2$ is a tautology. In this case, we say $E1=E2$ is an equivalence.

Axioms

Commutativity

For propositions $E1$ and $E2$:

• $(E1\wedge E2)=(E2\wedge E1)$
• $(E1\vee E2)=(E2\vee E1)$
• $(E1=E2)=(E2=E1)$

Associativity

For propositions $E1$, $E2$, and $E3$:

• $E1\wedge (E2\wedge E3)=(E1\wedge E2)\wedge E3$
• $E1\vee (E2\vee E3)=(E1\vee E2)\vee E3$

Distributivity

For propositions $E1$, $E2$, and $E3$:

• $E1\vee (E2\wedge E3)=(E1\vee E2)\wedge (E1\vee E3)$
• $E1\wedge (E2\vee E3)=(E1\wedge E2)\vee (E1\wedge E3)$

De Morgan’s

For propositions $E1$ and $E2$:

• $\neg (E1\wedge E2)=\neg E1\vee \neg E2$
• $\neg (E1\vee E2)=\neg E1\wedge \neg E2$

Law of Negation

For any proposition $E1$, it follows that $\neg (\neg E1)=E1$.

Law of Excluded Middle

For any proposition $E1$, it follows that $E1\vee \neg E1=T$.

Law of Contradiction

For any proposition $E1$, it follows that $E1\wedge \neg E1=F$.

Law of Implication

For any propositions $E1$ and $E2$, it follows that $E1\Rightarrow E2=\neg E1\vee E2$.

Law of Equality

For any propositions $E1$ and $E2$, it follows that $(E1=E2)=(E1\Rightarrow E2)\wedge (E2\Rightarrow E1)$.

Law of Or-Simplification

For any propositions $E1$ and $E2$, it follows that:

• $E1\vee E1=E1$
• $E1\vee T=T$
• $E1\vee F=E1$
• $E1\vee (E1\wedge E2)=E1$

Law of And-Simplification

For any propositions $E1$ and $E2$, it follows that:

• $E1\wedge E1=E1$
• $E1\wedge T=E1$
• $E1\wedge F=F$
• $E1\wedge (E1\vee E2)=E1$

Law of Identity

For any proposition $E1$, $E1=E1$.

Inference Rules

• Rule of Substitution
  • Let $P(r)$ be a predicate and $E1=E2$ be an equivalence. Then $P(E1)=P(E2)$ is an equivalence.
• Rule of Transitivity
  • Let $E1=E2$ and $E2=E3$ be equivalences. Then $E1=E3$ is an equivalence.

Selectors

A selector denotes a finite sequence of subscript expressions, each enclosed in brackets. $ϵ$ denotes the empty selector. For example, variable $x$ is equivalently denoted as $x\circ ϵ$ whereas for array $b$, $b[i]$ is equivalently denoted as $b\circ [i]$.

Selector update syntax allows specifying a new value with previous subscripted values overridden. For instance, $(b;i:e)$ denotes $b$ with $b[i]$ now referring to $e$. More formally, for any $j\in \mathrm{domain}(b)$, $(b;i:e)[j]=\{\begin{array}{l}i=j\to e\\ i\ne j\to b[j]\end{array}$

Generalizing further to all variable types $x$, \begin{align*} (x; \epsilon{:}e) & = e \\ (x; [i] {\circ} s{:}e)[j] & = \begin{cases} i \neq j \rightarrow x[j] \\ i = j \rightarrow (x[j]; s{:}e) \end{cases} \end{align*}

Substitution

Textual substitution refers to the replacement of a free identifier with an expression, introducing parentheses as necessary. This concept amounts to the Substitution Rule with different notation.

Simple

If $x$ denotes a variable and $e$ an expression, substitution of $x$ by $e$ is denoted as $E_e^x$

General

We can generalize textual substitution to operate on a vector of reference-expression pairs, where each reference corresponds to some identifier concatenated with a selector. Let $\bar{x}=⟨x_1,\dots ,x_n⟩$ denote a vector of identifiers concatenated with selectors and $\bar{e}=⟨e_1,\dots ,e_n⟩$ denote a vector of expressions. Then textual substitition of $\bar{x}$ with $\bar{e}$ in expression $E$ is denoted as $E_{\bar{e}}^{\bar{x}}$

Substitution is defined recursively as follows:

1. If each $x_i$ is a distinct identifier with a null selector, then $E_{\bar{e}}^{\bar{x}}$ is the simultaneous substitution of $\bar{x}$ with $\bar{e}$.
2. Adjacent reference-expression pairs may be permuted as long as they begin with different identifiers. That is, for all distinct $b$ and $c$, $E_{\bar{e},f,h,\bar{g}}^{\bar{x},b,c,\bar{y}}=E_{\bar{x},h,f,\bar{g}}^{\bar{x},c,b,\bar{y}}$
3. Multiple assignments to subparts of an object $b$ can be viewed as a single assignment to $b$. That is, provided $b$ does not begin any of the $x_i$, $E_{e_1,\dots ,e_m,\bar{g}}^{b\circ s_1,\dots ,b\circ s_m,\bar{x}}=E_{(b;s_1:e_1;\cdots ;s_m:e_m),\bar{g}}^{b,\bar{x}}$

Note that simultaneous substitution is different from sequential substitution.

Theorems

• $(E_u^x{)}_v^x=E_{u_v^x}^x$

  • The only possible free occurrences of $x$ that may appear after the first of the substitutions occur in $u$.

• If $y\notin FV(E)$, then $(E_u^x{)}_v^y=E_{u_v^y}^x$.

  • $y$ may not be free in $E$ but substituting $x$ with $u$ can introduce a free occurrence. It doesn’t matter if we perform the substitution first or second though.

• $s(E_e^x)=s(E_{s(e)}^x)$

  • Substituting $x$ with $e$ and then evaluating is the same as substituting $x$ with the evaluation of $e$.

• Let $s$ be a state and $s^{\prime }=(s;x:s(e))$. Then $s^{\prime }(E)=s(E_e^x)$.

• Given identifiers $\bar{x}$ and fresh identifiers $\bar{u}$, $(E_{\bar{u}}^{\bar{x}}{)}_{\bar{x}}^{\bar{u}}=E$.

States

A state is a function that maps identifiers to $T$ or $F$. A proposition can be equivalently seen as a representation of the set of states in which it is true.

Bibliography

• Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
• Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.