La théorie du premier ordre d'une structure finie a-t-elle un rang de quantificateur borné?

Soit toute structure finie. Est-ce que sa théorie du premier ordre a un rang de quantificateur borné, dans le sens où il y a un tel que pour tout avec il y a un avec et ? $\mathfrak{A}$ $\mathfrak{T} := \mathfrak{TH}(\mathfrak{A})$ $q\in\mathbb{N}$ $\varphi\in\mathfrak{T}$ $qr(\varphi) > q$ $\varphi'\in\mathfrak{T}$ $qr(\varphi')\leq q$ $\varphi'\equiv\varphi$

co.combinatorics lo.logic relational-structures D. Rusin
la source

N'est-ce pas une question pour Mathoverflow plutôt que pour la théorie CS?

Andrej Bauer

@Andrej, la théorie des modèles finis et la complexité descriptive sont également considérées comme faisant partie du TCS.

Kaveh

Excellent, c'est comme Bob Harper l'a dit une fois: les mathématiques sont un cas particulier de l'informatique.

Andrej Bauer

L'informatique est également un cas particulier des mathématiques, et ce sont aussi des cas particuliers de la logique, et vice versa.

fhyve

Réponses:

La théorie de toute structure finie est un modèle complet. En fait, il est facile de voir que toute formule est équivalente à une formule existentielle avec un quantificateur pour chaque élément de la structure, après quoi tous les quantificateurs de la formule d'origine peuvent être simulés par des conjonctions et des disjonctions. En particulier, le nombre de quantificateurs (d'où le rang des quantificateurs) est limité par la taille de la structure.

Emil Jeřábek
la source

En fait, un quantificateur universel supplémentaire est nécessaire, ce qui permet d'exprimer qu'il n'y a pas d'autres éléments. Dans toutes les réponses, il y a une hypothèse qui devrait être explicite: la présence de l'égalité, c'est-à-dire que x = y est une formule atomique autorisée.

Thomas S

Aucun quantificateur supplémentaire n'est nécessaire. N'oubliez pas que nous n'essayons pas d'axiomatiser la théorie de la structure, mais de trouver une formule équivalente à une donnée modulo la théorie. Et la présence de l'égalité est la norme universelle pour la logique classique du premier ordre. Son absence devrait être déclarée.

Emil Jeřábek

Ah. Tu as raison. "Théorie Modulo". Concernant l'égalité: comme nous essayons d'expliquer des choses faciles à des personnes extérieures à Logic, cela ne fait pas de mal de rendre le cadre explicite. Encore une remarque: remplacer les quantificateurs par des conjonctions et des disjonctions est parfaitement bon. Cependant, il existe des alternatives: comme une formule avec, disons, m variables libres définit une relation m-aire de A, la nouvelle formule peut, après avoir deviné tous les éléments et vérifier qui est lequel (automorphismes modulo), également "énumérer" explicitement tous tuples, pour lesquels l'ancienne formule donne "vrai".

Thomas S

Pour rendre ce que Emil a dit un peu plus concret: considérons la formule exprimant l'existence de k objets distincts. Cela montre que nous avons besoin d'un nombre illimité de quantificateurs.

Maintenant, vous avez une formule avec q quantificateurs et votre modèle contient k objets, vous pouvez exprimer la formule en indiquant que k objets distincts existent et que la relation entre eux peut être exprimée en CNF.

Kaveh
la source