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$:

• $\mathrm{\neg }(E1\wedge E2)=\mathrm{\neg }E1\vee \mathrm{\neg }E2$
• $\mathrm{\neg }(E1\vee E2)=\mathrm{\neg }E1\wedge \mathrm{\neg }E2$

Law of Double Negation

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

Law of Excluded Middle

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

Law of Contradiction

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

Law of Implication

For any propositions $E1$ and $E2$, it follows that $E1\Rightarrow E2=\mathrm{\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 domain(b)$,

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

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 $\overline{x}=⟨x_1,\dots ,x_n⟩$ denote a vector of identifiers concatenated with selectors and $\overline{e}=⟨e_1,\dots ,e_n⟩$ denote a vector of expressions. Then textual substitition of $\overline{x}$ with $\overline{e}$ in expression $E$ is denoted as

Substitution is defined recursively as follows:

1. If each $x_i$ is a distinct identifier with a null selector, then $E_{\overline{e}}^{\overline{x}}$ is the simultaneous substitution of $\overline{x}$ with $\overline{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_{\overline{e},f,h,\overline{g}}^{\overline{x},b,c,\overline{y}}=E_{\overline{x},h,f,\overline{g}}^{\overline{x},c,b,\overline{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,\overline{g}}^{b\circ s_1,\dots ,b\circ s_m,\overline{x}}=E_{(b;s_1:e_1;\cdots ;s_m:e_m),\overline{g}}^{b,\overline{x}}$$

Note that simultaneous substitution is different from sequential substitution.

Identities

• $(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 $\overline{x}$ and fresh identifiers $\overline{u}$, $(E_{\overline{u}}^{\overline{x}}{)}_{\overline{x}}^{\overline{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.