On variable non-dependence of first-order formulas

TL;DR

This paper introduces the concept of variable non-dependence in first-order formulas, exploring its properties and applying it to simplify complex formulas by removing redundant quantifiers, especially in translations between theories.

Contribution

It defines and investigates variable non-dependence in first-order logic and demonstrates its utility in simplifying formulas with nested quantifiers.

Findings

Defined variable non-dependence and analyzed its properties

Applied the concept to simplify formulas with nested quantifiers

Improved understanding of formula translation processes

Abstract

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.