We present a variant of the Davis–Fechter’s technique for eliminating quantifiers in first-order logic, aimed at reducing the incidence of irrelevant dependencies in the construction of Skolem terms. The basic idea behind this contribution is to treat as a single syntactic unit every maximal ‘quantifier batch’, i.e., group of contiguous alike quantifiers, whose internal order (which has no significance) is thereby prevented from entangling the final result. Through concrete cross-translations, our version of the free-variable predicate calculus turns out to be equipollent—in means of expression and of proof—to the one originally proposed by Davis and Fechter and hence to a relatively conventional version of quantified first-order logic.
On the elimination of quantifiers through descriptors in predicate logic
Omodeo, E.
2012-01-01
Abstract
We present a variant of the Davis–Fechter’s technique for eliminating quantifiers in first-order logic, aimed at reducing the incidence of irrelevant dependencies in the construction of Skolem terms. The basic idea behind this contribution is to treat as a single syntactic unit every maximal ‘quantifier batch’, i.e., group of contiguous alike quantifiers, whose internal order (which has no significance) is thereby prevented from entangling the final result. Through concrete cross-translations, our version of the free-variable predicate calculus turns out to be equipollent—in means of expression and of proof—to the one originally proposed by Davis and Fechter and hence to a relatively conventional version of quantified first-order logic.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
