变量置换难以描述
Transposition of variables is hard to describe
AI总结：
本文研究了在公式中交换两个逻辑变量的函数p_{xy}的描述难度，证明了有限维代表性多项式等价代数无法通过有限等式公理系统 axiomatize，揭示了有限变量逻辑证明系统和多项式等价代数定义方程的后果。
摘要：
函数p_{xy}在公式中交换两个逻辑变量x,y的难度在于，每个等式公理系统必须包含对于每个有限n，包含p_{xy}和至少n个代数变量的等式，以及每个操作∃, =, ∨。这解决了Johnson在50多年前提出的问题：有限维α≥3的代表性多项式等价代数无法通过有限等式公理系统扩展代表性 cylindric 代数的等式理论。证明使用了一族非代表性多项式等价代数A_n，随着n增加，它们越来越接近可代表：其n生成子代数及其真约简都是可代表的。研究了RPEA_α的子变种格，并提出了关于置换操作相互作用和结果推广到无限维的新开放问题。
英文摘要：
The function $p_{xy}$ that interchanges two logical variables $x,y$ in formulas is hard to describe in the following sense. Let $F$ denote the Lindenbaum-Tarski formula-algebra of a finite-variable first order logic, endowed with $p_{xy}$ as a unary function. Each equational axiom system for the equational theory of $F$ has to contain, for each finite $n$, an equation that contains together with $p_{xy}$ at least $n$ algebraic variables, and each of the operations $\exists, =, \lor$. This solves a problem raised by Johnson [J. Symb. Logic] more than 50 years ago: the class of representable polyadic equality algebras of a finite dimension $α\ge 3$ cannot be axiomatized by adding finitely many equations to the equational theory of representable cylindric algebras of dimension $α$. Consequences for proof systems of finite-variable logic and for defining equations of polyadic equality algebras are given. The proof uses a family of nonrepresentable polyadic equality algebras ${\cal A}_n$ that are more and more nearly representable as $n$ increases: their $n$-generated subalgebras as well as their proper reducts are representable. The lattice of subvarieties of $RPEA_α$ is investigated and new open problems are asked about the interplay between the transposition operations and about generalizability of the results to infinite dimensions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
