# Logical and alphabetological variant?

The notion of alphabetical variant is well known, so that a formula $x=x$ is an alphabetical variant of $y=y$ if $x$ and $y$ are distinct variables.

One may want to consider the set term $\{x:x \neq x \wedge A \}$ a logical variant of $\{x:x \neq x \}$ if $A$ is a tautology of predicate logic. Given such notions of alphabetical and logical variants, one may consider $\{x:x \neq x \wedge A \}$ an alphabetological variant of $\{y:y \neq y\}$.

Do my notions of logical variant and alphabetological variant have provenances?

-
For what it's worth, Takeuti's proof theory (2nd ed. 1987) refers to 'alphabetical variants' in p. 18 def 2.15 with reference to substitutions of bound variables only (so $x=x$ and $y=y$ are not alphabetical variants when $x\neq y$ according to this definition). –  Noel Vaillant Oct 2 '13 at 15:40
However, the formulas $\forall x((x\in z)\leftrightarrow(x = x))$ and $\forall y((y\in z)\leftrightarrow(y = y))$ are $\alpha$-equivalent for all $z\not\in\{x,y\}$, which is probably the notion you want to refer to (as Takeuti) under the label 'alphabetical variant'. As for 'logical variant', i have the feeling you are asking for the provenance of the so-called 'Lindenbaum-Tarski congruence' $\Gamma\vdash (\phi\leftrightarrow\psi)$ –  Noel Vaillant Oct 2 '13 at 15:52
Thanks, Noel. That leaves only the alphabetological variant, it seems. –  Frode Bjørdal Oct 2 '13 at 17:44
Can you confirm you are referring to the notion of $\alpha$-equivalence as per this? If so, I would be surprised if the idea did not originate from Russell or Frege. If not, I am not familiar with your notion. –  Noel Vaillant Oct 2 '13 at 18:26
Please use *italics* or **bold** instead of $math$ to emphasize text. –  François G. Dorais Oct 5 '13 at 14:56