论一阶公式的变量非依赖性
On variable non-dependence of first-order formulas
AI总结：
本文提出一阶逻辑中变量非依赖性的概念，允许在另一公式表达的约束下判定公式真值是否依赖某变量，并利用该概念通过提取和丢弃冗余嵌套量词来简化复杂公式。
摘要：
本文引入公式中变量非依赖性的概念。若一阶逻辑公式的真值不依赖于某变量的值，则该公式对该变量非依赖。此变量非依赖性可受公式中某些变量值的约束限制，这些约束由另一一阶公式表达。在研究其基本性质后，我们将此概念应用于简化复杂公式，方法是通过提取并丢弃冗余的嵌套量词。当使用翻译函数将一个理论解释为另一个理论时，通常会出现此类复杂公式。
英文摘要：
In this paper, we introduce a concept of non-dependence of variables in formulas. A formula in first-order logic is non-dependent of a variable if the truth value of this formula does not depend on the value of that variable. This variable non-dependence can be subject to constraints on the value of some variables which appear in the formula, these constraints are expressed by another first-order formula. After investigating its basic properties, we apply this concept to simplify convoluted formulas by bringing out and discarding redundant nested quantifiers. Such convoluted formulas typically appear when one uses a translation function interpreting a theory into another.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
