Rapport 20-2004
Arnaud Durand, Etienne Grandjean and Frédéric Olive
New results on arity vs. number of variables
In this paper, definability in existential second-order logic is considered. Our main goal it to study the relationships between the arity of second-order quantified (i.e. guessed) symbols and the number of first-order universal variables in formulas. The key idea behind this work is that bounding the arity of guessed symbols strongly limits the number of first-order universally quantified variables that are really needed to express properties.
We show that, as long as second-order quantifiers of formulas range over function and relation symbols of arity at most one, two first-order variables say no more than one.
We also generalize this result and show that for some varieties of formulas (including positive ones with unary signature) the number of universally quantified first-order variables does not really matter.
These results are first steps towards looking for an arity-based characterization of subclasses of NP and towards proving there exists a strict hierarchy purely based on arity for existential second-order logic, two long standing open questions in finite model theory.
Existential second-order logic, second-order arity vs. number of first-order variables, arity based hierarchy in second-order logic.
Dans cet article, on considère la définissabilité au second-ordre existentiel. Notre principal objectif est d'étudier les liens entre l'arité des symboles du second-ordre quantifiés (i.e. devinés) et le nombre de variables universelles du premier-ordre apparaissant dans les formules. L'idée clé de ce travail est qu'une borne sur l'arité des symboles devinés limite fortement le nombre de variables du premier-ordre universellement quantifiées réellement nécessaire à l'expression de propriétés.
Nous montrons que, tant que les symboles du second-ordre des formules considérées sont restreints à des symboles de relation et de fonction d'arité au plus 1, deux variables du premier ordre ne disent pas plus qu'une seule.
Nous généralisons ce résultat en montrant que pour certaines classes de formules (incluant les formules positives de signature unaire), le nombre de variables du premier-ordre universellement quantifiées n'a pas d'incidence sur le pouvoir d'expression.
Ces résultats sont un premier pas vers une caractérisation des sous-ensembles de NP basée sur l'arité, et vers la preuve d'une hiérarchie stricte de la logique du second-ordre existentiel purement basé sur l'arité, deux questions ouvertes depuis longtemps en théorie des modèles finis.
Logique du second-ordre existentiel, arité au second-ordre vs. nombre de variables du premier-ordre, hierarchie basée sur l'arité dans la logique du second-ordre.
@TECHREPORT{20-2004, AUTHOR = {Arnaud Durand, Etienne Grandjean and Frédéric Olive}, TITLE = {{New results on arity vs. number of variables}}, INSTITUTION = {{LIF}}, ADDRESS = {Marseille, France}, TYPE = {Research report}, NUMBER = {20-2004}, MONTH = {April}, YEAR = {2004}, NOTE = {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/20-2004.html}, }