Database: Variable occurrence in equivalence chains

Proposition 27: Provided a variable x occurs in at least one of the statements \alpha, \beta, ..., \omega , it also occurs in the equivalence chain (\alpha \Leftrightarrow \beta \Leftrightarrow \cdots \Leftrightarrow \omega).

Proof: We shall argue by means of structural induction over the definition of equivalence chains.

Base cases: Suppose x occurs in at least one of \alpha , \beta and \gamma . Then, x occurs in at least one of \alpha or \beta , or else x occurs in \gamma . In the former case, x occurs in the equivalence (\alpha \Leftrightarrow \beta) by [14], so it occurs in the conjunction \big( (\alpha \Leftrightarrow \beta) \wedge (\beta \Leftrightarrow \gamma)) by definition of occurrence. In the latter case, x occurs in (\beta \Leftrightarrow \gamma) , and hence in the same conjunction, using the same two reasons. But this conjunction is the definition of (\alpha \Leftrightarrow \beta \Leftrightarrow \gamma) .

Inductive step: We take as the induction hypothesis that the desired result is known for statements \alpha, \beta, ..., \psi , and want to show from this that it is also justified for \alpha, \beta, ..., \psi, \omega . If x occurs in at least one of \alpha, \beta, ..., \psi, \omega , then it either occurs in at least one of \alpha, \beta, ..., \psi or it occurs in \omega . In the former case, x occurs in (\alpha \Leftrightarrow \beta \Leftrightarrow \cdots \Leftrightarrow \psi) by the induction hypothesis. In the latter case, it occurs in (\psi \Leftrightarrow \omega) by [14]. Thus, in either of the cases, it occurs in \big( (\alpha \Leftrightarrow \beta \Leftrightarrow \cdots \Leftrightarrow \psi) \wedge (\psi \Leftrightarrow \omega) \big) by definition of occurrence. This is precisely (\alpha \Leftrightarrow \beta \Leftrightarrow \cdots \Leftrightarrow \psi \Leftrightarrow \omega) . \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Conjunction
  3. Definition: Equivalence
  4. Definition: Occurrence of a variable
  5. Proposition: Variable occurrence in equivalences
  6. Terminology: Structural induction