de Epsilonrekening

overzicht

tegen het begin van de eeuw werden David Hilbert en Henri Poincaré erkend als de twee belangrijkste wiskundigen van hun generatie. Hilberts reeks van wiskundige interesses was breed, en omvatte een interesse in de grondslagen van de wiskunde: hisFoundations of Geometry werd gepubliceerd in 1899, en van de lijst van vragen gesteld aan het International Congress of mathematicians in 1900, drie behandelde duidelijk fundamentele kwesties.,na de publicatie van Russell ‘ s paradox presenteerde Hilbert een toespraak op het Derde Internationale Congres van Math-mathematici in 1904, waar hij voor het eerst zijn plan schetste om een rigoureuze basis voor de wiskunde te bieden door middel van syntactischeconsistentie-bewijzen. Maar hij kwam niet serieus op het onderwerp terug tot 1917, toen hij met de hulp van Paul Bernays een reeks lezingen begon over de grondslagen van de Mathematica., Hoewel Hilbert onder de indruk was van het werk van Russell en Whitehead in hun PrincipiaMathematica, raakte hij ervan overtuigd dat de logicistische poging om de wiskunde tot logica te reduceren, niet kon slagen, in het bijzonder vanwege het niet-logische karakter van hun axioma van reduceerbaarheid. Tegelijkertijd beschouwde hij de intuïtionistische afwijzing van de wet van het uitgesloten midden als onaanvaardbaar voor de wiskunde. Om de bezorgdheid over de ontdekking van de logische en theoretische paradoxen te ondervangen, was daarom een nieuwe aanpak nodig om de moderne mathematische methoden te rechtvaardigen.,in de zomer van 1920 had Hilbert een dergelijke aanpak geformuleerd. Ten eerste moesten moderne wiskundige methoden worden vertegenwoordigd in formele deductivesystemen. Ten tweede moesten deze formele systemen syntactisch geconsistent worden bewezen, niet door een model te vertonen of hun consistentie met een ander systeem te verminderen, maar door een direct metamathetisch argument met een expliciet, “finitair” karakter. De aanpak werd bekend als Hilbert ‘ s programma. De epsilonrekening moest de eerste component van dit programma leveren, terwijl zijn Epsilon substitutiemethode de tweede component moest leveren.,

De epsiloncalculus is, in zijn meest basale vorm, een uitbreiding van de eerste-orde predicaatlogica met een “Epsilon operatie”die voor elke ware existentiële Formule Een getuige van de existentiële kwantificeerder kiest. De uitbreiding is conservatief in de zindat het geen nieuwe first-order gevolgen toevoegt. Maar omgekeerd kunnen kwantificeerders worden gedefinieerd in termen van de epsilonen, terwijl de logica van de eerste orde kan worden begrepen in termen van kwantificeer-vrijereasoning met betrekking tot de Epsilon-operatie. Het is deze laatste featuredie de calculus geschikt maakt voor het doel van het provingconsistentie., Geschikte uitbreidingen van de epsilonrekening maken het mogelijk om sterkere, kwantificationele theorieën van getallen en sets in kwantificer-vrije calculi in te bedden. Hilbert verwachtte dat het mogelijk zou zijn om de consistentie van dergelijke uitbreidingen aan te tonen.

de Epsilonrekening

in zijn Hamburg lecture in 1921 (1922) presenteerde Hilbert voor het eerst het idee om een dergelijke operatie te gebruiken om het principe van het uitgesloten midden in een formeel systeem voor rekenkunde aan te pakken., Deze ideeën werden ontwikkeld in de Epsilon calculus en de Epsilon substitutionmethod in een reeks lezingen tussen 1921 en 1923, en inHilbert ‘ s (1923). De eindpresentatie van de Epsilon-calculus is te vinden in Wilhelm Ackermann ‘ s proefschrift (1924).

Deze sectie zal een versie van de calculus beschrijven die overeenkomt met de eerste-orde logica, terwijl uitbreidingen naar de eerste – en tweede-orderarithmetic hieronder zullen worden beschreven.

zij \(L\) een eerste-orde taal, dat wil zeggen, een lijst vanconstant, functie en relatie symbolen met gespecificeerde arities., De verzameling termen van epsilon en de verzameling formules van \(L\) worden gelijktijdig als volgt gedefinieerd:

substitutie en de begrippen vrije en gebonden variabele worden op de gebruikelijke manier gedefinieerd; met name wordt de variabele \(x\) gebonden op de term \(\varepsilon X A\). De bedoelde interpretatie is dat\(\varepsilon x A\) duidt op een \(x\) bevredigend \(A\), als er één is., De epsilontermen worden dus beheerst door het volgende axioma (Hilberts “transfinietaxioma”): \ bovendien bevat de epsilonrekening een complete verzameling axioma ’s die de klassieke propositionele connectiva regelen, en axioma’ s die het gelijkheidssymbool regelen.De enige regels van de calculus zijn de volgende:

• Modus ponens
• substitutie: van \(A(x)\), concluderen \(A(t)\), voor elke term\(t.,\)

eerdere vormen van de epsilonrekening (zoals die in 1923 gepresenteerd werd) gebruiken een dubbele vorm van de epsilonoperator, waarin\(\varepsilon x A\) een waarde geeft die\(A(x)\) vervalst. Bovenstaande versie werd gebruikt in Ackermann ‘ s proefschrift (1924) en is standaard geworden.

merk op dat de zojuist beschreven calculus vrij is van kwantificeerders. Kwantificeerders kunnen als volgt worden gedefinieerd: \ de gebruikelijke kwantificeringsaxioma ‘ s en-regels kunnen daaruit worden afgeleid, zodat de definities hierboven dienen om de eerste-ordelogica in de epsilonrekening te verankeren., Het omgekeerde is echter niet waar: niet elke formule in de epsiloncalculus is het beeld van een gewone gekwantificeerde formule onder deze bedding. Daarom is de epsilonrekening expressiever dan de predicaatrekening, simpelweg omdat epsilontermen complexer kunnen worden gecombineerd dan kwantificeerders.

de stellingen van Epsilon

Het tweede deel van Hilbert en Bernays’ Grundlagen derMathematik (1939) geeft een overzicht van de resultaten op de Epsilon-calculus die tegen die tijd waren bewezen., Dit omvat een bespreking van de eerste en tweede stelling van epsilon met toepassing op de eerste-orde logica, de Epsilon substitutie methode voor arithmet open inductie, en een ontwikkeling van de analyse (dat wil zeggen,tweede-orde rekenkunde) met de Epsilon calculus.

de eerste en tweede stelling van epsilon zijn als volgt:

in de eerste stelling van epsilon is “kwantificer-free predicatelogic” bedoeld om de substitutieregel hierboven op te nemen, soquantifier-vrije axioma ‘ s gedragen zich als hun universele sluitingen., Aangezien de epsilonrekening de eerste-ordelogica omvat, impliceert de eerste Epsilon theoremimplies dat elke omweg door de eerste-ordelogica die wordt gebruikt om een kwantificer-vrije stelling uit kwantificer-vrije axioma ‘ s te verkrijgen, uiteindelijk kan worden vermeden. De tweede stelling van epsilon laat zien dat elke stap door de epsilonrekening die wordt gebruikt om een stelling in de taal van de predicaatrekening af te leiden uit axioma ‘ s in de taal van de predicaatrekening ook kan worden vermeden.,

meer in het algemeen stelt de eerste stelling van epsilon vast dat kwantificeerders en epsilonen altijd kunnen worden geëlimineerd uit een bewijs van aquantifier-vrije formule uit andere kwantificer-vrije formules. Dit is van bijzonder belang voor Hilberts programma, omdat de Epsilons de rol van ideale elementen in de wiskunde spelen. Als kwantifier-vrije formules overeenkomen met het” reële “deel van de wiskundige theorie, toont de eerste Epsilon-stelling aan dat idealementenuit bewijzen van reële verklaringen kunnen worden geëlimineerd, mits de axioma’ s ook reële verklaringen zijn.,

dit idee wordt nauwkeurig gemaakt in een zekere algemene consistentie hetorem dat Hilbert en Bernays afleiden uit de eerste Epsilon-stelling, die het volgende zegt: Laat \(F\) elk formeel systeem zijn dat uit de predicaatcalculus voortvloeit door toevoeging van constante, functie, envoorbeelden plus ware axioma ‘ s die kwantificeer – en Epsilon-vrij zijn, en stel dat de waarheid van atomaire formules in de nieuwe taal decidable is. Dan is \(F\) consistent in de sterke zindat elke afgeleide kwantificeerder – en epsilon-vrije formule waar is.,Hilbert en Bernays gebruiken deze stelling om een finitair consistentieproof van de elementaire meetkunde te geven (1939, Sec.1.4).

de moeilijkheid voor het geven van consistentiebewijzen voor rekenkundige en analyse bestaat erin dit resultaat uit te breiden tot gevallen waarin het axioma ook ideale elementen bevat, d.w.z. epsilontermen.

verder lezen. De oorspronkelijke bronnen over de epsilonrekening en de stellingen van epsilon (Ackermann 1924, Hilbert & Bernays 1939) blijven alleen beschikbaar in het Duits. Leisenring 1969 is een relatief moderne boek-length introductie tot de Epsilon calculus in het Engels.,De eerste en tweede stelling van epsilon worden in detail beschreven in Zach2017. Moser & Zach 2006 geeft een gedetailleerde analyse voor de zaak zonder gelijkheid. De originele bewijzen worden gegeven voor axiomatische voorstellingen van de Epsilon-calculus. Maehara 1955 was de eerste sequente calculus met epsilontermen. Hij toonde hoe hij de tweede stelling van epsilon kon bewijzen met behulp van cut-eliminatie, en versterkte de stelling vervolgens tot het schema van extensionaliteit(Maehara 1957). Baaz et al. 2018 geven een verbeterde versie van de stelling van firstepsilon., Correcties op fouten in de literatuur (waaronder leisenring ‘ s boek) zijn te vinden in Flanagan 1975; Ferrari 1987;en Yasuhara 1982. Een variatie van de epsilonrekening op basis van Skolemfuncties, en dus compatibel met first-order logica, wordt besproken in Davis & Fechter 1991.

de zojuist beschreven versie van de stelling van Herbrand volgt direct uit de uitgebreide eerste stelling van Epsilon van Hilbert en Bernays., Met behulp van methoden geassocieerd met het bewijs van de tweede stelling van epsilon, echter, Hilbert en Bernays afgeleid een groter resultaat dat, net als Herbrand ‘ s oorspronkelijke formulering,biedt meer informatie. Om de twee delen van de stelling te begrijpen, helpt het om een bepaald voorbeeld te overwegen. Laat \(A\) de vorm \ zijn waarin \(B\) vrij is van kwantificeerders. De negatie van \(A\) is gelijk aan \ door Skolemiseren, d.w.z.,, gebruikmakend van functiesymbolen om de existentiële kwantificeerders te zien, verkrijgen we\ door de negatie hiervan te nemen, zien we dat de oorspronkelijke vorm “equivalent” is aan \

wanneer we verwijzen naar een instantie van de matrix van \(A^H\), we zijn een formule die wordt verkregen door termen in de expandedtaal te vervangen in de matrix van \(A^H\). We kunnen nu stellen dat Hilbert andBernays ‘formulering van de stelling van

Herbrand ook kan worden verkregen door gebruik te maken van cuteliminatie, via Gentzen’ s “midsequent stelling.,”Echter, het bewijs met behulp van de tweede stelling van epsilon heeft de distinctie van het zijn de eerste volledige en correcte bewijs van de stelling van Herbrand. Bovendien,en dit wordt zelden erkend, terwijl het bewijs op basis van cut-eliminatie slechts een binding geeft aan de lengte van de Herbrand disjunction als functie van de cut rank en complexiteit van de cutformules in het bewijs, biedt de lengte verkregen uit het bewijs op basis van de epsilonrekening een binding aan als een combinatie van het aantal toepassingen van het transfinietaxioma, en rang en graad van de epsilon-termen die daarin voorkomen., Met andere woorden, de lengte van de Herbrand disjunctie hangt alleen af van de kwantificerende complexiteit van de betrokken substituties, en,bijvoorbeeld, helemaal niet van de propositionele structuur of de lengte van de proof.

de versie van de stelling van Herbrand aan het begin van deze sectie is in wezen het speciale geval van (2) waarin de formule \(A\) existentieel is. In het licht van dit bijzondere geval is (1) gelijkwaardig aan de bewering dat een formule \(A\) dan en slechts dan als \(A^H\) afgeleid kan worden van een infirst-orde predicaatlogica., De forwarddirection van deze equivalentie is veel gemakkelijker te bewijzen; in feite is voor elke formule \(A, A \rightarrow A^H\) afgeleid in predicaatlogica.Het bewijzen van de omgekeerde richting impliceert het elimineren van de additionalefunctiesymbolen in \(A^H\), en is veel moeilijker, vooral in aanwezigheid van gelijkheid. Hier spelen epsilonmethoden een centrale rol.

een opvallende toepassing van de stelling van Herbrand en aanverwante methoden wordt gevonden in Luckhardt”s (1989) analyse van de stelling van Roth. Voor een bespreking van nuttige uitbreidingen van de methoden van Herbrand, zie Sieg 1991.,Een modeltheoretische versie hiervan wordt besproken in Avigad 2002a.

De Epsilon-substitutiemethode en rekenkundige

zoals hierboven vermeld, was het primaire belang in de epsiloncalculus historisch gezien als een middel om consistentieproeven te verkrijgen.Hilberts lezingen van 1917-1918 merken al op dat één de consistentie van propositionele logica gemakkelijk kan bewijzen, door propositionele variabelen en formules te nemen om te variëren over waarheidswaarden 0 en 1, en de logische connectiva te interpreteren als de corresponderende arithmetische operaties., Evenzo kan men de consistentie vanpredicate logica (of de zuivere Epsilon calculus) bewijzen, door zich te specialiseren ininterpretaties waar het universum van discours één enkel element heeft.Deze overwegingen suggereren het volgende meer algemene programma voor het verbeteren van de consistentie:

• Breid de epsilonrekening zo uit dat deze grotere delen van de wiskunde vertegenwoordigt.
• aan de hand van eindige methoden tonen dat elk bewijs in het verlengde systeem een consistente interpretatie heeft.,

stel dat we willen laten zien dat het bovenstaande systeem consistent is; met andere woorden, we willen laten zien dat er geen bewijs is van de formule \(0 =1\). Door alle substituties naar de axioma ’s te duwen en freevariables te vervangen door de constante 0, volstaat het om aan te tonen dat er geen propositioneel bewijs is van \(0 = 1\) uit een eindige verzameling van gesloten instances van de axioma’ s. Daarvoor volstaat het om aan te tonen dat, gegeven een eindige verzameling van gesloten gevallen van axioma ‘s, Men numerieke waarden toterms kan toewijzen op een zodanige wijze dat alle axioma’ s waar zijn onder de interpretatie., Aangezien de rekenkundige bewerkingen \ ( + \ ) en \(\times\) op de gebruikelijke manier kunnen worden geïnterpreteerd, is het enige probleem het bepalen van de juiste waarden om toe te wijzen aan de Epsilon-termen.

De Epsilon-substitutiemethode van Hilbert kan ruwweg als volgt worden beschreven:

een definitief consistentiebewijs wordt verkregen zodra op een volstrekt aanvaardbare wijze wordt aangetoond dat dit proces van opeenvolgende”reparaties” wordt beëindigd. Als dat zo is, zijn alle kritische formula ‘ s ware formules zonder Epsilon-termen.,

dit basisidee (de “Hilbertsche Ansatz”) werd door Hilbert in zijn lezing uit 1922 (1923) uitgewerkt in lezingen in 1922-23. De hier gegeven voorbeelden hebben echter alleen betrekking op proofs waarbij alle gevallen van het transfinietaxioma overeenkomen met een enkele Epsilon term \(\varepsilon x A(x)\). De uitdaging bestond erin de aanpak uit te breiden tot meer dan één epsilonterm, tot geneste epsilonterms en uiteindelijk tot tweederangs epsilons (om niet alleen een bewijs van consistentie van rekenkunde, maar van analyse te verkrijgen).,

Dit is slechts een schets van de moeilijkheden in verband met de uitbreiding van het idee van Filbert tot het algemene geval. Ackermann (1924) voorzag in een dergelijke veralgemening door middel van een procedure die “terugkaatst”wanneer een nieuwe interpretatie in een bepaald stadium leidt tot de noodzaak om een interpretatie te corrigeren die reeds in een vorige fase werd gevonden.

Ackermann ‘ s procedure was van toepassing op een systeem van tweede-orderarithmetisch, waarin echter de tweede-ordervoorwaarden werden beperkt om kruisverbinding van tweede-orderepsilons uit te sluiten., Dit komt grofweg neer op een beperking van het rekenkundig begrip als het samenstellingsprincipe (zie de bespreking aan het eind van deze paragraaf). Verdere problemen met de tweede-orde Epsilon termsurved, en het werd al snel duidelijk dat het bewijs als het stood was misleidend. Maar niemand in Hilberts school realiseerde zich de omvang van de moeilijkheid tot 1930, toen Gödel zijn onvoltooide resultaten aankondigde., Tot dan werd aangenomen dat het bewijs (althans met enkele wijzigingen die Ackermann had aangebracht, waarvan sommige ideeën uit von Neumann ‘ s (1927) versie van de epsilonsubstitutiemethode betroffen) ten minste voor het eerste-ordedeel zou doorlopen. Hilbert and Bernays (1939) suggereren dat de alleen gebruikte methoden een consistentiebewijs bieden voor eerste-orde-rekenkunde met openinductie. In 1936 slaagde Gerhard Gentzen erin om een bewijs te leveren van de consistentie van de eerste-orde-rekenkunde in een formulering die gebaseerd was op de logica zonder het Epsilon-symbool., Dit bewijs gebruikt transfinite inductie tot \(\varepsilon_0\). Ackermann (1940) waslater in staat om Gentzen ‘ s ideeën aan te passen om een correctconsistentiebewijs van eerste-orde rekenkunde te geven met behulp van de Epsilon-substitutiemethode.

analyse, of tweede-orde rekenkunde, is de uitbreiding van de eerste-orderarithmetic met het begripsschema voor willekeurige tweede-orde Formulae. De theorie is impredicatief in die zin dat het on toestaat verzamelingen van natuurlijke getallen te definiëren met behulp van kwantificeerders die over het gehele universum van Verzamelingen reiken, inclusief, impliciet, De verzameling die wordt gedefinieerd., Men kan predicatieve fragmenten van deze theorie verkrijgen door het type formules te beperken dat in het begripsaxioma is toegestaan. Zo komt de in verband met Ackermann hierboven besproken beperking overeen met het rekenkundig begripsschema, waarin formules geen tweederangsquantifiers omvatten. Er zijn verschillende manieren om sterkere fragmenten van analyse te verkrijgen die niettemin predicatief gerechtvaardigd zijn., Bijvoorbeeld, men verkrijgt vertakte analyse door het associëren van een ordinale ranktom verzamelingen variabelen; ruwweg,in de definitie van een verzameling van een bepaalde rang, variëren de kwantificeerders slechts over verzamelingen van lagere rang, dat wil zeggen, die wiens definities logisch voorafgaan.

verder lezen. Hilbert ’s en Ackermann’ s earlyproofs worden besproken in Zach 2003; 2004. Von Neumann ‘ s bewijs is het onderwerp van Bellotti 2016. Ackermann ’s bewijs uit 1940 wordt besproken in Hilbert & Bernays 1970, en Wang 1963. Een moderne presentatie wordt gegeven door Moser 2006., Een vroege toepassing van Epsilon-substitutie is de No-counter-example-interpretatie (Kreisel 1951).

meer recente ontwikkelingen

In dit hoofdstuk bespreken we de ontwikkeling van de Epsilon-substitutiemethode voor het verkrijgen van consistentieresultaten voor sterke systemen; deze resultaten zijn van wiskundige aard. We kunnen hier helaas niet de details van de bewijzen bespreken, maar willen graag aangeven dat de Epsilon-substitutiemethode niet is gestorven met Hilbert ‘ s programma, en dat er een aanzienlijke hoeveelheid lopend onderzoek wordt verricht in Epsilon-formalismen.,Gentzen ‘ s consistentieproeven voor rekenkunde lanceerde een onderzoeksgebied dat ordinale analyse wordt genoemd, en het programma voor het meten van de sterkte van wiskundige theorieën met behulp van ordinale notaties wordt vandaag de dag nog steeds voortgezet. Dit is met name relevant voor het uitgebreide programma van Hilbert, waar het doel is om de klassieke wiskunde te rechtvaardigen ten opzichte van constructieve, ofquasi-constructieve systemen., Gentzen ‘ s methoden van cut-eliminatie (en uitbreidingen van infinitaire logica ontwikkeld door PaulLorentzen, Petr Novikov, en Kurt Schütte) hebben, voor een groot deel,verdrongen Epsilon substitutie methoden in deze bezigheden. Maar epsiloncalculus methoden bieden een alternatieve benadering, en er is nog steeds actief onderzoek naar manieren om Hilbert-Ackermann methoden uit te breiden tot meer theorieën. Het algemene patroon blijft hetzelfde:

1. Integreer de onderzochte theorie in een geschikte epsiloncalculus.
2. Beschrijf een proces voor het bijwerken van toewijzingen aan de epsilonterms.,
3. laat zien dat de procedure aan het normaliseren is, dat wil zeggen dat, gegeven een reeks voorwaarden, er een reeks updates is die resulteert in een toewijzing die voldoet aan de axioma ‘ s.aangezien de laatste stap de consistentie van de oorspronkelijke theorie garandeert,is men vanuit fundamenteel oogpunt geïnteresseerd in de methoden die worden gebruikt om normalisatie te bewijzen. Zo verkrijgt men bijvoorbeeld een ordinalanalyse door ordinale notaties toe te wijzen aan stappen in de procedure, zodanig dat de waarde van een notatie met elke stap afneemt.,

   in de jaren 1960, Tait (1960, 1965, 2010) breiddedackermann ‘ s methods to obtain an ordinal analysis of extensionsof arithmetic with principles of transfinite induction. Meer gestroomlijnde en moderne versies van deze aanpak zijn te vinden in Mints2001 en Avigad 2002b., Meer recentelijk hebben Mints, Tupailo en Buchholz sterkere, maar nog steeds voorspellende, fragmenten van de analyse beschouwd, waaronder theorieën over rekenkundige bevattelijkheid en een\(\Delta^{1}_1\)-bevattingsregel (Mints, Tupailo &Buchholz 1996; Mints & Tupailo 1999; zie ook Mints 2016). Arai2002 heeft de Epsilon-substitutiemethode uitgebreid tot theorieën die het mogelijk maken om het rekenkundig begrip te herhalen langs primitiverecursieve putvolgorde., In het bijzonder levert zijn werk ordinalalanalyses op voor predicatieve fragmenten van analyse met transfinitehierarchieën en transfiniet inductie.

   enkele eerste stappen zijn gezet bij het gebruik van de Epsilon substitutiemethode in de analyse van impredicatieve theorieën (zie Arai2003, 2006 and Mints 2015).

   een variatie op bovenstaande stap 3 houdt in dat wordt aangetoond dat de normaliseringsprocedure niet gevoelig is voor de keuze van updates, dat wil zeggen dat elke reeks updates wordt beëindigd. Dit heet strongnormalisatie., Mints 1996 heeft aangetoond dat veel van de onderzochte procedures deze sterkere eigenschap hebben.

   naast de traditionele, fundamentele tak van de bewijstheorie is er tegenwoordig veel belangstelling voor structurele bewijstheorie,een tak van het onderwerp die zich richt op logische deductivecalculi en hun eigenschappen. Dit onderzoek houdt nauw verband met kwesties die relevant zijn voor de informatica, die te maken hebben met geautomatiseerde reductie, functionele programmering en computerondersteunde verificatie.Ook hier hebben Gentzen-stijl methoden de neiging om te domineren (zie nogmaals het artikel over de bewijstheorie)., Maar de epsilonrekening kan ook waardevolle inzichten opleveren; cf. bijvoorbeeld Aguilera & Baaz 2019, of de bespreking van de stelling van Herbrand hierboven.

   naast de onderzoeken van de epsilonrekening in de bewijstheorie moeten twee toepassingen worden vermeld. Een daarvan is het gebruik van epsilonnotatie in Bourbaki ‘ s Theorie des ensembles (1958).De tweede, misschien nog interessanter, is het gebruik van de Epsilon-operator in de theorem-proving systemen HOL en Isabelle, waar de expressieve kracht van Epsilon-termen aanzienlijke praktische voordelen oplevert.,

   Epsilonoperatoren in taalkunde, filosofie en niet-klassieke logica

   Het lezen van de epsilonoperator als een operator voor onbepaalde keuze(“an \(x\) zodanig dat \(A(x)\)”) suggereert dat het een nuttig hulpmiddel kan zijn bij de analyse van Onbepaalde en bepaalde zelfstandige naamwoorden in de formele semantiek. De Epsilon-notatie is in feite zo gebruikt,en deze toepassing is met name nuttig gebleken bij de behandeling van eenaforische verwijzing.

   beschouw het bekende voorbeeld

   1. elke boer die een ezel bezit verslaat het.,ns}(x, y)) \rightarrow\mathrm{Beats}(x, y))\)

   Het nadeel is dat “een ezel” suggereren een existentialquantifier, en dus de analyse moet op een of andere manier, parallel in formthe analyse van de zin 3 gegeven door 4:

   maar de dichtst mogelijke formalisering,

   1. \(\forall x ((\mathrm{Boer}(x) \wedge \exists y(\mathrm{Ezel}(y) \wedge \mathrm{Eigenaar}(x, y)) \rightarrow\mathrm{Beats}(x, y))\)

   Zoals opgemerkt door von Heusinger (1994), dit suggereert dat Neale iscommitted te voornaamwoorden wordt dubbelzinnig tussen duidelijke beschrijvingen\((\jota\)-expressies) en whe-uitingen., Heusinger stelt in plaats daarvan voor om Epsilon-operatoren te gebruiken die zijn geïndexeerd op basis van keuzefuncties (die afhankelijk zijn van de context). Volgens deze benadering is de analyse van(1)

   deze benadering van het omgaan met voornaamwoorden met behulp van epsilonoperatoren die zijn geïndexeerd door keuzefuncties stelt von Heusinger in staat om met een breed scala aan omstandigheden om te gaan (zie Egli en von Heusinger, 1995; von Heusinger, 2000).

   toepassingen van de Epsilon-operator op het gebied van formele semantiek en keuzefuncties in het algemeen hebben de laatste jaren veel belangstelling gekregen., Von Heusinger en Egli (2000a) noemen onder meer het volgende: representations of questions (Reinhart, 1992), specificindefinites(Reinhart 1992; 1997; Winter 1997), E-Type voornaamwoorden (Hintikka and Kulas 1985; Slater 1986; Chierchia 1992, Egli and vonHeusinger 1995) en definitieve zelfstandige zinnen (von Heusinger 1997,2004).

   voor de bespreking van de vraagstukken en toepassingen van de epsilonoperatorin taalkunde en taalfilosofie, zie B. H., Slater ‘ s artikel over Epsilon calculi (Geciteerd in de andere Internet Resourcess sectie hieronder), en de collecties von Heusinger en Egli 2000 envon Heusinger en Kempson 2004.

   Meyer Viol (1995a, 1995b) bevat verdere bewijs – en modeltheoretische studies van de epsilonrekening; specifiek intuïtionistische epsiloncalculi. Hier gelden de stellingen van epsilon niet meer, dat wil zeggen dat de introductie van epsilontermen niet-conservatieve uitbreidingen van de intuïtionistische logica voortbrengt. Andere onderzoeken van epsilonoperatoren in de intuïtionistische logica zijn te vinden in Shirai (1971), Bell (1993a,1993b) en DeVidi (1995)., Voor Epsilon-operators in veelgewaardeerde logica ‘ s,zie Mostowski (1963), voor modale epsilonrekening, Fitting (1975).

   verder lezen. Hieronder volgt een lijst van enkele publicaties op het gebied van taal en taalkunde die van belang zijn voor de epsiloncalculus en zijn toepassingen. De lezer richt zich met name op de collecties van Heusinger & Egli (eds.) 2000 and 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.

---