alpha-equivalence
See also
Definition
Two formulas \(\phi\) and \(\psi\) are \(\alpha\text{-equivalent}\) if and only if they only differ by the names (i.e. symbolic representations) given to their variables.
Note
As of today, punctilious is focused on the development of propositional logic. This definition applies to propositional logic but is not accurate for first-order logic. Considering the definition provided by [TS00], in first-order logic alpha-equivalence should account for bound-variables but not free-variables. For this reason, once the development of punctiolious will cover first-order logic, we will need to refine these definitions and probably distinguish several types of alpha-equivalences.
Quotes
Expressions \(\mathcal{E}\), \(\mathcal{E}'\) which differ only in the names of bound variables will be regarded by us as identical. This is sometimes expressed by saying that \(\mathcal{E}\) and \(\mathcal{E}'\) are \(\alpha\text{-equivalent}\) . In other words, we are only interested in certain equivalence classes of (the concrete representations of) expressions, expressions “modulo renaming of bound variables”. [TS00, p. 3]
Sources
[TS00]