le calcul D’Epsilon

aperçu

Au tournant du siècle, David Hilbert et Henri Poincaré étaient reconnus comme les deux mathématiciens les plus importants de leur génération. La gamme d’intérêts mathématiques de Hilbert était large, et comprenait un intérêt pour les fondements des mathématiques: hisFoundations of Geometry a été publié en 1899, et de la liste des questions posées au Congrès international des mathématiciens en 1900, trois abordées distinctement foundationalissues.,

à la suite de la publication du paradoxe de Russell, Hilbert a présenté un discours au troisième Congrès International des mathématiciens en 1904, où, pour la première fois, il a esquissé son plan pour fournir une base rigoureuse pour les mathématiques par des preuves de cohérence syntaxique. Mais il n’est pas revenu sérieusement sur le sujet jusqu’en 1917, lorsqu’il a commencé une série de conférences sur les fondements de la mathématique avec L’aide de Paul Bernays., Bien que Hilbert wasimpressed par le travail de Russell et Whitehead dans leur PrincipiaMathematica, il est devenu convaincu que la tentative de logicist toreduce mathématiques à la logique ne pouvait pas réussir, en raison en particulier tothe caractère non logique de leur axiome de réductibilité. En même temps, il a jugé le rejet intuitionniste de la loi du milieu exclu comme inacceptable pour les mathématiques. Par conséquent, afin de répondre aux préoccupations soulevées par la découverte des paradoxes logiques etensemble-théoriques, une nouvelle approche était nécessaire pour justifier les méthodes mathématiques modernes.,

dès l’été 1920, Hilbert avait formulé une telle approche. Premièrement, les méthodes mathématiques modernes devaient être représentées dans les déductionsystèmes. Deuxièmement, ces systèmes formels devaient être prouvés syntaxiquement cohérents, non pas en présentant un modèle ou en réduisant leur cohérence à un autre système, mais par un argument métamathématique direct d’un caractère « finitaire” explicite. L  » approche est devenue connuecomme le programme de Hilbert. Le calcul epsilon devait fournir le premier composant de ce programme, tandis que sa méthode de substitution epsilon devait fournir la seconde.,

le calcul epsilon est, dans sa forme la plus élémentaire, une extension de la logique des prédicats de premier ordre avec une « opération epsilon”qui choisit, pour toute vraie formule existentielle, un témoin du quantificateur existentiel. L’extension est conservatrice dans le sensqu’elle n’ajoute aucune nouvelle conséquence de premier ordre. Mais, inversement, les quantificateurs peuvent être définis en termes d’epsilons, la logique de premier ordre peut être comprise en termes de quantification sans quantificateur impliquant l’opération epsilon. C’est cette dernière caractéristiquece qui rend le calcul pratique dans le but de prouverconsistance., Des extensions appropriées du calcul epsilon rendent possible d’intégrer des théories quantificationnelles plus fortes des nombres et des ensembles dans des calculs sans quantificateur. Hilbert s’attendait à ce qu’il seraitpossible de démontrer la cohérence de telles extensions.

le calcul D’Epsilon

dans sa conférence de Hambourg en 1921 (1922), Hilbert a présenté pour la première fois l’idée d’utiliser une telle opération pour traiter du principe du milieu exclu dans un système formel d’arithmétique., Ces idées ont été développées dans le calcul d’epsilon et la méthode de substitution d’epsilon dans une série de cours magistraux entre 1921 et 1923, et dans celui d’Hilbert (1923). La présentation finale de l’epsilon-calculpeut être trouvée dans la thèse de Wilhelm Ackermann (1924).

Cette section décrira une version du calcul correspondant à la logique du premier ordre, tandis que les extensions à la logique du premier et du deuxième ordre seront décrites ci-dessous.

soit \(l\) un langage de premier ordre, c’est-à-dire une liste de symboles de constance, de fonction et de relation avec des arities spécifiées., L’ensemble des termes epsilon et l’ensemble des formules de \(L\) sont définis de manière réductrice, simultanément, comme suit:

La Substitution et les notions de variable libre et liée, sont définies de la manière habituelle; en particulier, la variable \(x\) devient liée dans le terme \(\varepsilon X A\). L’interprétation prévue est que\(\varepsilon x A\) désigne un \(x\) satisfaisant \(a\), s’il y en a un., Ainsi, les Termes d’epsilon sont régis par l’axiome suivant (« axiome transfinite” de Hilbert): \ de plus, le calcul d’epsilon comprend un ensemble complet d’axiomes régissant les connectives à proposition classique et d’axiomes régissant le symbole d’égalité.Les seules règles du calcul sont les suivantes:

• modus ponens
• Substitution: de \(A(x)\), conclure \(a(t)\), pour tout terme\(T.,\)

Les formes antérieures du calcul d’epsilon (comme celle présentée en 1923) utilisent une forme duale de l’opérateur epsilon, dans laquelle\(\varepsilon x a\) renvoie une valeur falsifiant \(a(x)\). La version ci-dessus a été utilisée dans la thèse D’Ackermann (1924), et est devenue la norme.

notez que le calcul qui vient d’être décrit est sans quantificateur. Quantifierscan être défini comme suit: \ L’habitude quantificateur axiomes et les règles peuvent être dérivées à partir de ceux-ci, de sorte que le definitionsabove servir à intégrer la logique du premier ordre dans l’epsilon de calcul., Theconverse est, cependant, pas vrai: toutes les formules dans l’epsiloncalculus est l’image d’une formule quantifiée ordinaire sous thisembedding. Par conséquent, le calcul d’epsilon est plus expressif que le calcul prédéterminé, simplement parce que les Termes d’epsilon peuvent être combinés de manière plus complexe que les quantificateurs.

the Epsilon Theorems

Le deuxième volume du Grundlagen derMathematik de Hilbert et Bernays (1939) fournit un compte rendu des résultats sur l’Epsilon-calcul qui avaient été prouvés à cette époque., Cela comprend une discussion des premier et deuxième théorèmes epsilon avec des applications à la logique du premier ordre, la méthode de substitution epsilon pour l’arithmétique avec induction ouverte, et un développement de l’analyse (c’est-à-dire l’arithmétique du second ordre) avec le calcul epsilon.

Les premier et deuxième théorèmes d’epsilon sont les suivants:

dans le premier théorème d’epsilon, « quantifier-free predicatelogic” est destiné à inclure la règle de substitution ci-dessus, donc les axiomes sans quantificateur se comportent comme leurs fermetures universelles., Puisque le calcul d’Epsilon inclut la logique du premier ordre, le premier théorème d’epsilon implique que tout détour par la logique des prédicats du premier ordre utilisé pour donner un théorème sans quantificateur à partir d’axiomes sans quantificateur peut finalement être évité. Le deuxième théorème d’epsilon montre que tout détour par le calcul d’epsilon utilisé pour dériver un théorème dans la langue du calcul des prédicats à partir d’axiomes dans le langage du calcul des prédicats peut également être évité.,

plus généralement, le premier théorème d’epsilon établit que les quantifierset les epsilons peuvent toujours être éliminés d’une preuve de formule sans aquantificateur à partir d’autres formules sans quantificateur. Ceci estd’une importance particulière pour le programme de Hilbert, puisque les épsilons jouent le rôle d’éléments idéaux en mathématiques. Si les formules sans quantificateur correspondent à la partie” réelle  » de la théorie mathématique, le premier théorème d’epsilon montre que les éléments idéaux peuvent être éliminés des preuves d’énoncés réels, à condition que les axiomes soient également des énoncés réels.,

cette idée est rendue précise dans un certain théorème de cohérence généralque Hilbert et Bernays dérivent du premier théorème d’epsilon, qui dit ce qui suit: soit \(F\) tout système formel qui résulte du calcul des prédicats par addition de constantes, de fonctions et de symboles prédéterminés plus de vrais axiomes qui sont quantificateurs-etpsilons – libres, et supposons que la vérité des formules atomiques dans le nouveau langage soit décidable. Alors \(F\) est cohérent dans le sens fortque chaque formule sans quantificateur et sans epsilon dérivable est vraie.,Hilbert et Bernays utilisent ce théorème pour donner une cohérence finitaireproof de la géométrie élémentaire (1939, Sec 1.4).

la difficulté de donner des preuves de cohérence pour l’arithmétique et l’analyse consiste à étendre ce résultat aux cas où les axiomes contiennent également des éléments idéaux, c’est-à-dire des termes epsilon.

Poursuite de la lecture. Les sources originales sur le calcul d’epsilon et les théorèmes d’epsilon (Ackermann 1924, Hilbert & Bernays 1939)restent disponibles uniquement en allemand. Leisenring 1969 est une introduction relativement moderne au calcul d’epsilon en anglais.,Le premier et le deuxième théorème d’epsilon sont décrits en détail dans Zach2017. Moser & Zach 2006 donne une analyse détaillée du cassans égalité. Les preuves originales sont données pour axiomatiqueprésentations de l’epsilon-calcul. Maehara 1955 a été le premier àconsidérer le calcul séquentiel avec les Termes epsilon. Il a montré comment prouver le deuxième théorème d’epsilon en utilisant l’élimination de la coupe, puis a renforcé le théorème pour inclure le schéma de l’extensionalité(Maehara 1957). Baaz et coll. 2018 donner une version améliorée du premierle théorème d’Epsilon., Des Corrections à des erreurs dans la littérature (y compris le livre de leisenring) peuvent être trouvées dans Flannagan 1975; Ferrari 1987;et Yasuhara 1982. Une variante du calcul epsilon basée sur les fonctions Skolem, et donc compatible avec la logique du premier ordre, est discutée dans Davis & Fechter 1991.

théorème D’Herbrand

la version du théorème D’Herbrand qui vient d’être décrite suit immédiatement le premier théorème D’Epsilon étendu d’Hilbert et Bernays., En utilisant des méthodes associées à la preuve du deuxième théorème d’epsilon, cependant, Hilbert et Bernays ont dérivé un résultat plus long qui,comme la formulation originale de Herbrand, fournit plus d’informations. Pour comprendre les deux parties du théorèmeci-dessous, il est utile de considérer un exemple particulier. Soit \(A\) la formula

\ où \(B\) est sans quantificateur. La négation de \(A\) est équivalente à \ en Skolémisant, c’est-à-dire,, en utilisant des symboles de fonction pour témoigner des quantificateurs existentiels, nous obtenons\ en prenant la négation de cela, nous voyons que la formula d’origine est « équivalente » à \

lorsque nous nous référons à une instance de la matrice de \(A^H\), nous obtenons une formule qui est obtenue en substituant des termes dans la langue expandedlangue dans la matrice de \(A^H\). Nous pouvons maintenant Énoncer la formulation de Hilbert andBernays du

Le théorème de Herbrand peut également être obtenu en utilisant cutelimination, via le « théorème du milieu du lendemain » de Gentzen., »Cependant, la preuve utilisant le deuxième théorème d’epsilon a la particularité d’être la première preuve complète et correcte du théorème d’Herbrand. De plus,et cela est rarement reconnu, alors que la preuve basée sur l’élimination de la coupure ne fournit une limite sur la longueur de la disjonction de Herbrand qu’en fonction du rang de coupe et de la complexité des formules de coupe dans la preuve, la longueur obtenue à partir de la preuve basée sur le calcul d’epsilon fournit une limite en fonction du nombre d’applications de l’axiome transfinite, ainsi que du rang et du degré des termes d’epsilon qui s’y trouvent., En d’autres termes, la longueur de la disjonction de Herbrand ne dépend que de la complexité quantitative des substitutions impliquées, et, par exemple,pas du tout de la structure propositionnelle ou de la longueur de la preuve.

la version du théorème de Herbrand énoncée au début de cette section est essentiellement le cas particulier de (2) dans lequel la formula \(A\) est existentielle. À la lumière de ce cas particulier, (1) estéquivalent à l’affirmation selon laquelle une formule \(A\) est dérivable dans la logique des prédicats de premier ordre si et seulement si \(A^H\) l’est., La direction avant de cette équivalence est beaucoup plus facile à prouver; en fait, forany formula \(A, a \rightarrow A^H\) est dérivable dans la logique des prédicats.Prouver la direction inverse implique d’éliminer les symboles de fonction supplémentaires dans \(A^H\), et est beaucoup plus difficile, en particulier dansla présence d’égalité. C’est ici que les méthodes epsilon jouent un rôle central.

Une application frappante du théorème de Herbrand et des méthodes connexes est trouvée dans L’analyse de Luckhardt (1989) du théorème de Roth. Pour une discussion sur les extensions utiles des méthodes de Herbrand, voir Sieg 1991.,Une version modèle-théorique de ceci est discutée dans Avigad 2002a.

la méthode de Substitution D’Epsilon et L’arithmétique

comme indiqué ci-dessus, historiquement, l’intérêt principal dans l’epsiloncalculus était comme un moyen d’obtenir des preuves de cohérence.Les conférences de Hilbert de 1917-1918 notent déjà qu’onepeut facilement prouver la cohérence de la logique propositionnelle, en prenant des variables et des formules de proposition pour s’étendre sur les valeurs de vérité 0 et1, et en interprétant les connectives logiques comme les opérations arithmétiques correspondantes., De même, on peut prouver la cohérence de la logique prédéterminée (ou du pur calcul d’epsilon), en se spécialisant dans les interprétations où l’univers du discours a un seul élément.Ces considérations suggèrent le programme plus général suivant pour améliorer la cohérence:

• étendre le calcul epsilon de manière à représenter de plus grandes proportions des mathématiques.
• montrer, en utilisant des méthodes finitaires, que chaque preuve dans extendedsystem a une interprétation cohérente.,

supposons que nous souhaitions montrer que le système ci-dessus est cohérent; en d’autres termes, nous souhaitons montrer qu’il n’y a pas de preuve de la formule \(0 =1\). En poussant toutes les substitutions aux axiomes et en remplaçant les variables libres par la constante 0, Il suffit de montrer qu’il n’y a pas de preuve proposée de \(0 = 1\) à partir d’un ensemble fini d’instances fermées des axiomes. Pour cela, il suffit de montrer que, étant donné tout finiteset d’instances fermées d’axiomes, on peut assigner des valeurs numériques aux termes de telle sorte que tous les axiomes soient vrais sous l’interprétation., Étant donné que les opérations arithmétiques \(+\) et \(\times\)peuvent être interprétées de la manière habituelle, la seule difficulté consiste à déterminer les valeurs appropriées à attribuer aux termes epsilon.

la méthode de Substitution epsilon de Hilbert peut être décrite grossièrement comme suit:

Une preuve de cohérence finitaire est obtenue une fois qu’il est démontré de manière acceptable que ce processus de »réparations” successives se termine. Si c’est le cas, toutes les formules critiquessont de vraies formules sans Termes epsilon.,

Cette idée de base (la « Hilbertsche Ansatz”) a été énoncée en premier lieu par Hilbert dans son discours de 1922 (1923), et développée dans des conférences en 1922-23. Les exemples donnés ici, cependant, ne traitent que des preuves dans lesquelles toutes les instances de l’axiome transfinite correspondent à un seul terme epsilon \(\varepsilon x A(x)\). Le défi consistait à étendre l’approche à plus d’un terme epsilon, à des epsilonterms imbriqués, et finalement à des epsilons de second ordre (afin d’obtenir une preuve de cohérence non seulement de l’arithmétique, mais de l’analyse).,

Ce n’est qu’une esquisse des difficultés liées à l’extension de l’idée de Hilbert au cas général. Ackermann (1924) a fourni une telle généralisation en utilisant une procédure qui « revient en arrière”chaque fois qu’une nouvelle interprétation à un stade donné entraîne la nécessité de corriger une interprétation déjà trouvée à un stade précédent.

la procédure D’Ackermann s’appliquait à un système de second ordre arithmétique, dans lequel, cependant, les termes du second ordre étaient limités soas pour exclure la liaison croisée des epsilons du second ordre., Cela équivaut,grosso modo, à une restriction à la compréhension arithmétique en tant que principe de formation des ensembles disponible (voir la discussion à la fin de cette section). D’autres difficultés avec les Termes epsilon de second ordre se sont manifestées, et il est rapidement devenu évident que la preuve telle qu’elle se tenait était fallacieuse. Cependant, personne dans L’école de Hilbert n’a réalisé l’extension de la difficulté jusqu’en 1930, lorsque Gödel a annoncé ses résultats incomplets., Jusque-là, on croyait que la preuve (au moins avec quelques modifications introduites par Ackermann, dont certaines impliquaient des idées de la version de von Neumann (1927) de la méthode epsilonsubstitution) passerait au moins pour la première partie. Hilbert et Bernays (1939) suggèrent que les méthodes utilisées ne fournissent qu’une preuve de cohérence pour l’arithmétique du premier ordre avec openinduction. En 1936, Gerhard Gentzen réussit à prouver la cohérence de l’arithmétique du premier ordre dans une formulation basée sur la logique prédéterminée sans le symbole epsilon., Cette preuve utilise l’induction transfinite jusqu’à \(\varepsilon_0\). Ackermann (1940) a été plus tard capable d’adapter les idées de Gentzen pour donner une preuve de cohérence correcte de l’arithmétique du premier ordre en utilisant la méthode de substitution Epsilon.

L’analyse, ou arithmétique du second ordre, est l’extension de l’arithmétique du premier ordre avec le schéma de compréhension pour les formulae arbitraires du second ordre. La théorie est imprédicative en ce sens qu’elle permet de définir des ensembles de nombres naturels à l’aide de quantificateurs qui s’étendent sur tout l’univers des ensembles, y compris, implicitement, l’ensemble étant défini., On peut obtenir des fragments prédicatifs de cette théorieen restreignant le type de formules autorisées dans la compréhensionaxiome. Par exemple, la restriction discutée en relation avecackermann ci-dessus correspond au système de compréhension arithmétique, dans lequel les formules n’impliquent pas de quantificateurs de second ordre. Il existe différentes façons d’obtenir des fragments d’analyse plus forts qui sont néanmoins justifiés de manière prédictive., Par exemple, on obtient une analyse ramifiée en associant un rang ordinal à des variables définies; grosso modo,dans la définition d’un ensemble d’un rang donné, les quantificateurs ne s’étendent que sur des ensembles de rang inférieur, c’est-à-dire ceux dont les définitions sont logiquement antérieures.

Poursuite de la Lecture. Les profils précoces de Hilbert et Ackermann sont discutés dans Zach 2003; 2004. La preuve de Von Neumann estle sujet de Bellotti 2016. La preuve d’Ackermann de 1940 est discutée dans Hilbert & Bernays 1970 et Wang 1963. Une présentation moderne estdonné par Moser 2006., Une application précoce de la substitution d’epsilon est l’interprétation sans contre-exemple (Kreisel 1951).

développements plus récents

dans cette section, nous discutons du développement de la méthode de substitution epsilon pour obtenir des résultats de cohérence pour les systèmes forts; ces résultats sont de nature mathématique. Nous ne pouvons malheureusement pas discuter des détails des preuves ici, mais nous voudrions indiquer que la méthode de substitution d’epsilon n’est pas morte avec le programme de Hilbert, et qu’une quantité importante de recherches actuelles est réalisée dans les formalismes d’epsilon.,

Les preuves de cohérence de Gentzen pour l’arithmétique ont lancé un domaine de recherche connu sous le nom d’analyse ordinale, et le programme de mesure de la force des théories mathématiques utilisant des notations ordinales est toujours poursuivi aujourd’hui. C’est particulièrement intéressant pour le programme étendu de Hilbert, où l’objectif est de justifier les mathématiques classiques par rapport aux systèmes constructifs, ouquasi-constructifs., Les méthodes d’élimination de la coupure de Gentzen (et les extensions de la logique infinitaire développées par PaulLorentzen, Petr Novikov et Kurt Schütte) ont, en grande partie,supplanté les méthodes de substitution epsilon dans ces activités. Mais les méthodes epsiloncalculus fournissent une approche alternative, et il existe toujoursrecherche active sur les moyens d’étendre les méthodes de Hilbert-Ackermann àdes théories plus solides. Le schéma général reste le même:

1. intégrer la théorie étudiée dans un epsiloncalcul approprié.
2. décrire un processus de mise à jour des affectations vers les epsilonterms.,
3. montrent que la procédure se normalise, c’est-à-dire que, compte tenu de tout ensemble de termes, il existe une séquence de mises à jour qui entraîne une assignation qui satisfait les axiomes.

puisque la dernière étape garantit la cohérence de la théorie originale,d’un point de vue fondamental, on s’intéresse aux méthodesutilisé pour prouver la normalisation. Par exemple, on obtient une analyse ordinale en attribuant des notations ordinales aux étapes de la procédure, de telle sorte que la valeur d’une notation diminue à chaque étape.,

dans les années 1960, Tait (1960, 1965, 2010) a étendu les méthodes d’Akermann pour obtenir une analyse ordinale des extensions de l’arithmétique avec des principes d’induction transfinite. Des versions plus détaillées et modernes de cette approche peuvent être trouvées dans Mints2001 et Avigad 2002b., Plus récemment, Mints, Tupailo et Buchholzhave considéré comme plus fort, mais toujours prédictivement justifiables, fragments d’analyse,y compris les théories de la compréhension arithmétique et a \(\Delta^{1}_1\)-règle de compréhension (Mints, Tupailo &Buchholz 1996; Mints & Tupailo 1999; Voir Aussi Mints 2016). Arai2002 a étendu la méthode de substitution epsilon aux théories qui permettent d’itérer la compréhension arithmétique le long des ordres de puits primitiverecursifs., En particulier, ses travaux produisent ordinalanalyses pour des fragments prédicatifs d’analyse impliquant transfinitehierarchies et induction transfinite.

quelques premières étapes ont été franchies dans l’utilisation de la méthode de substitution epsilon dans l’analyse des théories imprédicatives (voir Arai2003, 2006 et Mints 2015).

Une variante de l’étape 3 ci-dessus consiste à montrer que la procédure de normalisation n’est pas sensible au choix des mises à jour, c’est-à-dire que toute séquence de mises à jour se termine. C’est ce qu’on appelle strongnormalisation., Mints 1996 a montré que bon nombre des procéduresconsidéré ont cette propriété plus forte.

en plus de la branche traditionnelle et fondamentale de la théorie de la preuve, il existe aujourd’hui un grand intérêt pour la preuve structurelle,une branche du sujet qui se concentre sur les calculs déductifs logiques et leurs propriétés. Cette recherche est étroitement liée à des questions pertinentes pour l’informatique, ayant à voir avec la réduction automatisée, la programmation fonctionnelle et la vérification assistée par ordinateur.Ici aussi, les méthodes de style Gentzen ont tendance à dominer (voir à nouveau l’entrée sur la théorie de la preuve)., Mais le calcul d’epsilon peut également fournir des informations précieuses; cf. par exemple Aguilera & Baaz 2019, ou la discussion du théorème de Herbrand ci-dessus.

outre les études du calcul d’epsilon en théorie de la preuve,deux applications doivent être mentionnées. L’une est l’utilisation de l’epsilonnotation dans la théorie des ensembles de Bourbaki (1958).La seconde, d’intérêt peut-être plus actuel, est l’utilisation de l’opérateur Epsilon dans les systèmes de démonstration de théorème HOL et Isabelle, où la puissance expressive des termes epsilon donne des avantages pratiques significatifss.,

opérateurs Epsilon en linguistique, en philosophie et en logique Non classique

La Lecture de l’opérateur epsilon comme un opérateur de choix indéfini(« an \(x\) tel que \(A(x)\)”) suggère qu’il pourrait être un outil utile dans l’analyse des phrases nominales indéfinies et définies en sémantique formelle. La notation epsilon a en effet été ainsi utilisée, et cette application s’est avérée utile en particulier pour traiter la référence anaphorique.

Considérons l’exemple familier

1. Tout fermier qui possède un âne le bat-il.,ns}(x, y)) \rightarrow\mathrm{Beats}(x, y))\)

l’inconvénient est que « un âne” suggère un quantificateur existentiel, et donc l’analyse devrait, en quelque sorte, parallèlel’analyse de la phrase 3 donnée par 4:

mais la formalisation la plus proche possible,

1. \(\forall x ((\mathrm{Farmer}(x) \wedge \exists y(\mathrm{donkey}(y) \Wedge \mathrm{owns}(x, y)) \rightarrow\mathrm{Beats}(X, Y))\)

comme l’a souligné von Heusinger (1994), cela suggère que Neale est engagé à ce que les pronoms soient ambigus entre les descriptions définies\((\IOTA\)-expressions) et whe-expressions., Heusinger suggère plutôt d’utiliser des opérateurs epsilon indexés par des fonctions de choix (qui dépendent du contexte). Selon cette approche, l’analyse de(1) est

Cette approche du traitement des pronoms à l’aide d’opérateurs epsilon indexés par des fonctions de choix permet à von Heusinger de faire face à une grande variété de circonstances (voir Egli et von Heusinger, 1995; von Heusinger,2000).

Les Applications de l’opérateur epsilon dans la sémantique formelle, et les fonctions de choix en général, ont reçu un intérêt significatif au cours des dernières années., Von Heusinger et Egli (2000A) énumèrent, entre autres, les suivants: représentations des questions (Reinhart, 1992), définitions spécifiques (Reinhart 1992; 1997; hiver 1997), pronoms de type E(Hintikka et Kulas 1985; Slater 1986; Chierchia 1992, Egli et vonHeusinger 1995) et phrases nominales définies (von Heusinger 1997,2004).

pour une discussion sur les questions et les applications de l’opérateur epsilon en linguistique et philosophie du langage, Voir B. H., Slater’sarticle on epsilon calculi (cité dans L’autre section de ressources Internet ci-dessous), et les collections von Heusinger et Egli 2000 etvon Heusinger et Kempson 2004.

Meyer Viol (1995a, 1995b) contient d’autres études théoriques sur la preuve et le modèle du calcul d’epsilon; en particulier les epsiloncalculi intuitionnistes. Ici, les théorèmes d’epsilon ne tiennent plus, c’est-à-dire que l’introduction de termes d’epsilon produit des extensions non conservatrices de la logique intuitionniste. Shirai (1971), Bell (1993a,1993b) et DeVidi (1995) ont d’autres recherches sur les opérateurs epsilon dans la logique intuitionniste., Pour les opérateurs epsilon dans les logiques à valeurs multiples,voir Mostowski (1963), pour modal epsilon calculus, Fitting (1975).

Poursuite de la Lecture. Ce qui suit est une liste de certaines publicationsdans le domaine de la langue et de la linguistique intéressant l’epsiloncalculus et ses applications. Le lecteur s’adresse en particulier aux collections von Heusinger & Egli (eds.) 2000 et von Heusinger& Kempson (eds.,) 2004 for further discussion and references: Bell1993a, 1993b; Chierchia 1992; DeVidi 1995;Egli & von Heusinger1995; Fine 1985; Fitting 1975; von Heusinger 1994, 1997, 2000, 2004;von Heusinger & Egli (eds.) 2000; von Heusinger & Kempson(eds.) 2004; Hintikka & Kulas 1985; Kempson, Meyer Viol, &Gabbay 2001; Meyer Viol 1995a, 1995b, Neale 1990; Mostowski 1963;Reinhart 1992, 1997; Slater 1986, 1988, 1994, 2000; and Winter1997.

---