Quantificateur de branchement - Branching quantifier

Dans la logique d' un quantificateur de branchement , également appelé quantificateur Henkin , quantificateurs finis partiellement ordonné ou même quantificateur non linéaire , est un ordre partiel

${\displaystyle \langle Qx_{1}\dots Qx_{n}\rangle }$

de quantificateurs pour Q  {∀,∃}. C'est un cas particulier de quantificateur généralisé . En logique classique , les préfixes des quantificateurs sont ordonnés linéairement de telle sorte que la valeur d' une variable y _m liée par un quantificateur Q _m dépend de la valeur des variables

y ₁ , ..., y _{m -1}

lié par des quantificateurs

Qy ₁ , ..., Qy _{m -1}

précédant Q _m . Dans une logique à quantification partiellement ordonnée (finie) ce n'est en général pas le cas.

La quantification de branchement est apparue pour la première fois dans un document de conférence de 1959 de Leon Henkin . Les systèmes de quantification partiellement ordonnée ont une force intermédiaire entre la logique du premier ordre et la logique du second ordre . Ils servent de base à la logique indépendantiste de Hintikka et Gabriel Sandu .

Définition et propriétés

Le quantificateur Henkin le plus simple est ${\displaystyle Q_{H}}$

${\style d'affichage (Q_{H}x_{1},x_{2},y_{1},y_{2})\varphi (x_{1},x_{2},y_{1},y_{2} )\equiv {\begin{pmatrix}\forall x_{1}\,\exists y_{1}\\\forall x_{2}\,\exists y_{2}\end{pmatrix}}\varphi (x_{ 1},x_{2},y_{1},y_{2}).}$

Elle (en fait chaque formule avec un préfixe Henkin, pas seulement la plus simple) est équivalente à sa skolémisation de second ordre , c'est-à-dire

${\displaystyle \exists f\,\exists g\,\forall x_{1}\forall x_{2}\,\varphi (x_{1},x_{2},f(x_{1}),g( x_{2})).}$

Il est également assez puissant pour définir le quantificateur (c'est-à-dire "il y en a une infinité") défini comme ${\displaystyle Q_{\geq \mathbb {N} }}$

${\displaystyle (Q_{\geq \mathbb {N} }x)\varphi (x)\equiv \exists a(Q_{H}x_{1},x_{2},y_{1},y_{2} )[\varphi a\land (x_{1}=x_{2}\leftrightarrow y_{1}=y_{2})\land (\varphi (x_{1})\rightarrow (\varphi (y_{1} )\land y_{1}\neq a))].}$

Plusieurs choses en découlent, y compris la non-axiomatisabilité de la logique du premier ordre avec (observée pour la première fois par Ehrenfeucht ), et son équivalence avec le fragment de la logique du second ordre ( logique existentielle du second ordre ) - ce dernier résultat publié indépendamment en 1970 par Herbert Enderton et W. Walkoe. ${\displaystyle Q_{H}}$${\displaystyle \Sigma _{1}^{1}}$

Les quantificateurs suivants sont également définissables par . ${\displaystyle Q_{H}}$

• Rescher: « Le nombre de φ s est inférieur ou égal au nombre de ψ s »

${\displaystyle (Q_{L}x)(\varphi x,\psi x)\equiv \operatorname {Card} (\{x\colon \varphi x\})\leq \operatorname {Card} (\{x\ deux-points \psi x\})\équiv (Q_{H}x_{1}x_{2}y_{1}y_{2})[(x_{1}=x_{2}\leftrightarrow y_{1}=y_ {2})\land (\varphi x_{1}\rightarrow \psi y_{1})]}$

• Härtig: "Les & phiv s sont equinumerous avec le ψ s"

${\displaystyle (Q_{I}x)(\varphi x,\psi x)\equiv (Q_{L}x)(\varphi x,\psi x)\land (Q_{L}x)(\psi x ,\varphi x)}$

• Chang: « Le nombre de φ s est equinumerous avec le domaine du modèle »

${\style d'affichage (Q_{C}x)(\varphi x)\equiv (Q_{L}x)(x=x,\varphi x)}$

Le quantificateur de Henkin peut lui-même être exprimé comme un quantificateur de Lindström de type (4) . ${\displaystyle Q_{H}}$

Relation avec les langues naturelles

Hintikka dans un article de 1973 a avancé l'hypothèse que certaines phrases en langues naturelles sont mieux comprises en termes de quantificateurs de branchement, par exemple : « un parent de chaque villageois et un parent de chaque citadin se détestent » est censé être interprété, selon Hintikka, en tant que :

${\displaystyle {\begin{pmatrix}\forall x_{1}\,\exists y_{1}\\\forall x_{2}\,\exists y_{2}\end{pmatrix}}[(V(x_ {1})\coin T(x_{2}))\rightarrow (R(x_{1},y_{1})\coin R(x_{2},y_{2})\coin H(y_{1 },y_{2})\coin H(y_{2},y_{1}))].}$

qui est connu pour n'avoir aucun équivalent logique du premier ordre.

L'idée de branchement ne se limite pas nécessairement à l'utilisation des quantificateurs classiques comme feuilles. Dans un article de 1979, Jon Barwise a proposé des variantes des phrases Hintikka (comme on l'appelle parfois ci-dessus) dans lesquelles les quantificateurs internes sont eux-mêmes des quantificateurs généralisés , par exemple : « La plupart des villageois et la plupart des citadins se détestent. » Observant que n'est pas fermé par négation, Barwise a également proposé un test pratique pour déterminer si les phrases en langage naturel impliquent vraiment des quantificateurs de branchement, à savoir tester si leur négation en langage naturel implique une quantification universelle sur une variable définie (une phrase). ${\displaystyle \Sigma _{1}^{1}}$${\displaystyle \Pi _{1}^{1}}$

La proposition de Hintikka a été accueillie avec scepticisme par un certain nombre de logiciens car certaines phrases de premier ordre comme celle ci-dessous semblent capturer assez bien la phrase de Hintikka en langage naturel.

${\displaystyle [\forall x_{1}\,\exists y_{1}\,\forall x_{2}\,\exists y_{2}\,\varphi (x_{1},x_{2},y_ {1},y_{2})]\wedge [\forall x_{2}\,\exists y_{2}\,\forall x_{1}\,\exists y_{1}\,\varphi (x_{ 1},x_{2},y_{1},y_{2})]}$

où

${\displaystyle \varphi (x_{1},x_{2},y_{1},y_{2})}$

désigne

${\displaystyle (V(x_{1})\wedge T(x_{2}))\rightarrow (R(x_{1},y_{1})\wedge R(x_{2},y_{2}) \coin H(y_{1},y_{2})\coin H(y_{2},y_{1}))}$

Bien que de nombreux débats purement théoriques aient suivi, ce n'est qu'en 2009 que certains tests empiriques avec des étudiants formés à la logique ont révélé qu'ils étaient plus susceptibles d'attribuer des modèles correspondant à la phrase de premier ordre « bidirectionnelle » plutôt qu'à la phrase de quantification de branchement à plusieurs constructions linguistiques dérivées de la phrase Hintikka. Par exemple, on a montré aux élèves des graphiques bipartites non orientés — avec des carrés et des cercles comme sommets — et on leur a demandé si des phrases comme « plus de 3 cercles et plus de 3 carrés sont reliés par des lignes » décrivaient correctement les diagrammes.

Voir également

• Sémantique du jeu
• Logique de dépendance
• Logique favorable à l'indépendance (logique SI)
• quantificateur de Mostowski
• Quantificateur de Lindström
• Non-première commande

Les références

Liens externes

• Quantificateur de la théorie des jeux chez PlanetMath.