On variable non-dependence of first-order formulas
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929689253117952 |
|---|---|
| author | Lefever, Koen Székely, Gergely |
| author_facet | Lefever, Koen Székely, Gergely |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_16633 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On variable non-dependence of first-order formulas Lefever, Koen Székely, Gergely Logic 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. |
| title | On variable non-dependence of first-order formulas |
| topic | Logic |
| url | https://arxiv.org/abs/2501.16633 |