De Epsilon-calculus

Inhoudsopgave:

De Epsilon-calculus
De Epsilon-calculus

Video: De Epsilon-calculus

Video: De Epsilon-calculus
Video: Epsilon-delta limit definition 1 | Limits | Differential Calculus | Khan Academy 2024, Maart
Anonim

Toegang navigatie

  • Inhoud van het item
  • Bibliografie
  • Academische hulpmiddelen
  • Vrienden PDF-voorbeeld
  • Info over auteur en citaat
  • Terug naar boven

De Epsilon-calculus

Voor het eerst gepubliceerd op 3 mei 2002; inhoudelijke herziening ma 6 mei 2019

De epsilon-calculus is een logisch formalisme ontwikkeld door David Hilbert in dienst van zijn programma in de grondslagen van de wiskunde. De epsilon-operator is een termvormende operator die kwantoren in de gewone predikaatlogica vervangt. Specifiek, in de calculus, duidt een term (varepsilon x A) een aantal (x) bevredigende (A (x)) aan, als die er is. In Hilbert's Program spelen de epsilon-termen de rol van ideale elementen; het doel van Hilbert's finitistische consistentieproeven is om een procedure te geven die dergelijke termen uit een formeel bewijs verwijdert. De procedures waarmee dit moet worden uitgevoerd, zijn gebaseerd op Hilbert's epsilon-substitutiemethode. De epsilon-calculus heeft echter ook toepassingen in andere contexten. De eerste algemene toepassing van de epsilon-calculus was in Hilbert's epsilon-stellingen,die op hun beurt de basis vormen voor het eerste juiste bewijs van de stelling van Herbrand. Meer recentelijk zijn varianten van de epsilon-operator toegepast in de taal- en taalfilosofie om met anaforische voornaamwoorden om te gaan.

  • 1. Overzicht
  • 2. De Epsilon-calculus
  • 3. De stellingen van Epsilon
  • 4. De stelling van Herbrand
  • 5. De Epsilon-vervangingsmethode en rekenkunde
  • 6. Meer recente ontwikkelingen
  • 7. Epsilon-operators in taalkunde, filosofie en niet-klassieke logica
  • Bibliografie
  • Academische hulpmiddelen
  • Andere internetbronnen
  • Gerelateerde vermeldingen

1. Overzicht

Rond de eeuwwisseling werden David Hilbert en Henri Poincaré erkend als de twee belangrijkste wiskundigen van hun generatie. Hilbert's scala aan wiskundige interesses was breed en omvatte een interesse in de grondslagen van de wiskunde: zijn Foundations of Geometry werd gepubliceerd in 1899, en van de lijst met vragen die aan het International Congress of Mathematicians in 1900 werd gesteld, behandelden drie duidelijk fundamentele kwesties.

Na de publicatie van Russell's paradox hield Hilbert een toespraak voor het Derde Internationale Congres van Wiskundigen in 1904, waar hij voor het eerst zijn plan schetste om wiskunde te voorzien van een rigoureuze basis via syntactische consistentieproeven. Maar hij kwam pas in 1917 serieus terug op het onderwerp, toen hij met hulp van Paul Bernays een reeks lezingen begon over de grondslagen van de wiskunde. Hoewel Hilbert onder de indruk was van het werk van Russell en Whitehead in hun Principia Mathematica, raakte hij ervan overtuigd dat de logistische poging om wiskunde tot logica terug te brengen niet kon slagen, met name vanwege het niet-logische karakter van hun axioma van reduceerbaarheid. Tegelijkertijd achtte hij de intuïtionistische afwijzing van de wet van het uitgesloten midden onaanvaardbaar voor wiskunde. Daaromom de bezorgdheid weg te nemen die was ontstaan door de ontdekking van de logische en set-theoretische paradoxen, was een nieuwe benadering nodig om moderne wiskundige methoden te rechtvaardigen.

In de zomer van 1920 had Hilbert zo'n aanpak geformuleerd. Ten eerste moesten moderne wiskundige methoden worden weergegeven in formele deductieve systemen. Ten tweede moesten deze formele systemen syntactisch consistent blijken te zijn, niet door een model te tonen of door hun consistentie tot een ander systeem terug te brengen, maar door een direct metamathematisch argument van een expliciet, "finitair" karakter. De aanpak werd bekend als het programma van Hilbert. De epsilon-calculus was de eerste component van dit programma, terwijl zijn epsilon-substitutiemethode de tweede component was.

De epsilon-calculus is, in zijn meest basale vorm, een uitbreiding van de eerste-orde predikaatlogica met een 'epsilon-operatie' die, voor elke echte existentiële formule, een getuige is van de existentiële kwantificator. De extensie is conservatief in die zin dat het geen nieuwe eerste-orde consequenties toevoegt. Maar aan de andere kant kunnen kwantoren worden gedefinieerd in termen van de epsilons, dus logica van de eerste orde kan worden begrepen in termen van redeneren zonder redeneren waarbij de epsilon-bewerking betrokken is. Het is dit laatste kenmerk dat de calculus handig maakt om consistentie te bewijzen. Geschikte uitbreidingen van de epsilon-calculus maken het mogelijk om sterkere, kwantificatietheorieën van getallen en verzamelingen in kwantificatievrije calculi in te bedden. Hilbert verwachtte dat de consistentie van dergelijke uitbreidingen zou kunnen worden aangetoond.

2. De Epsilon-calculus

In zijn Hamburgse lezing in 1921 (1922) presenteerde Hilbert voor het eerst het idee om keuzefuncties te gebruiken om met het principe van het uitgesloten midden om te gaan in een formeel rekenstelsel. Deze ideeën zijn uitgewerkt in de epsilon-calculus en de epsilon-substitutiemethode in een reeks colleges tussen 1921 en 1923 en in Hilbert's (1923). De uiteindelijke presentatie van de epsilon-calculus is te vinden in het proefschrift van Wilhelm Ackermann (1924).

Deze sectie beschrijft een versie van de calculus die overeenkomt met de logica van de eerste orde, terwijl uitbreidingen van de rekenkunde van de eerste en tweede orde hieronder zullen worden beschreven.

Laat (L) een eerste-orde taal zijn, dat wil zeggen een lijst van constante, functie en relatie symbolen met gespecificeerde arities. De reeks epsilon-termen en de reeks formules van (L) worden inductief en tegelijkertijd als volgt gedefinieerd:

  • Elke constante van (L) is een term.
  • Elke variabele is een term.
  • Als (s) en (t) termen zijn, dan is (s = t) een formule.
  • Als (s_1, / ldots, s_k) termen zijn en (F) een (k) - ary functiesymbool is van (L, F (s_1, / ldots, s_k)) is een term.
  • Als (s_1, / ldots, s_k) termen zijn en (R) een (k) - relatie-symbool is van (L, R (s_1, / ldots, s_k)) een formule is.
  • Als (A) en (B) formules zijn, zijn (A / wedge B, A / vee B, A / rightarrow B) en (neg A).
  • Als (A) een formule is en (x) een variabele is, is (varepsilon x A) een term.

Substitutie en de begrippen vrije en gebonden variabele worden op de gebruikelijke manier gedefinieerd; in het bijzonder wordt de variabele (x) gebonden in de term (varepsilon x A). De beoogde interpretatie is dat (varepsilon x A) sommige (x) voldoet (A) aangeeft, als die er zijn. De epsilon-termen worden dus bepaald door het volgende axioma (Hilbert's "transfinite axiom"): [A (x) rightarrow A (varepsilon x A)) Bovendien bevat de epsilon-calculus een complete set axioma's die de klassieke propositionele connectieven en axioma's die het gelijkheidssymbool beheersen. De enige regels van de calculus zijn de volgende:

  • Modus Ponens
  • Vervanging: van (A (x)), conclusie (A (t)), voor elke term (t.)

Eerdere vormen van de epsilon-calculus (zoals gepresenteerd in Hilbert 1923) gebruiken een dubbele vorm van de epsilon-operator, waarin (varepsilon x A) een vervalsende waarde (A (x)) retourneert. Bovenstaande versie werd gebruikt in het proefschrift van Ackermann (1924) en is standaard geworden.

Merk op dat de zojuist beschreven calculus vrij is van kwantoren. Kwantificatoren kunnen als volgt worden gedefinieerd: (begin {align} exist x A (x) & / equiv A (varepsilon x A) / \ forall x A (x) & / equiv A (varepsilon x (neg A)) end {align}) De gebruikelijke kwantificatie axioma's en regels kunnen hieruit worden afgeleid, dus de bovenstaande definities dienen om logica van de eerste orde in te bedden in de epsilon calculus. Het omgekeerde is echter niet waar: niet elke formule in de epsilon-calculus is het beeld van een gewone gekwantificeerde formule onder deze inbedding. Daarom is de epsilon-calculus expressiever dan de predikaat-calculus, simpelweg omdat epsilon-termen op complexere manieren kunnen worden gecombineerd dan kwantoren.

Het is vermeldenswaard dat epsilon-termen niet-deterministisch zijn en daarom een vorm van het keuzeaxioma vertegenwoordigen. In een taal met constante symbolen (a) en (b) is (varepsilon x (x = a / vee x = b)) ofwel (a) of (b), maar de calculus laat volledig open wat het geval is. Men kan aan de calculus een schema van extensie toevoegen, (forall x (A (x) leftrightarrow B (x)) rightarrow / varepsilon x A = / varepsilon x B) die beweert dat de epsilon-operator hetzelfde toewijst getuige van gelijkwaardige formules (A) en (B). Voor veel toepassingen is dit aanvullende schema echter niet nodig.

3. De stellingen van Epsilon

Het tweede deel van Hilbert en Bernays 'Grundlagen der Mathematik (1939) geeft een overzicht van de resultaten van de tegen die tijd bewezen epsilon-calculus. Dit omvat een bespreking van de eerste en tweede epsilon-stellingen met toepassingen op eerste-orde logica, de epsilon-substitutiemethode voor rekenkunde met open inductie, en een ontwikkeling van analyse (dat wil zeggen, tweede-orde rekenkunde) met de epsilon-calculus.

De eerste en tweede epsilon-stellingen zijn als volgt:

Eerste stelling van epsilon: Stel dat (Gamma / cup {A }) een reeks formule-vrije formules is zonder het epsilon-symbool. Als (A) afleidbaar is van (Gamma) in de epsilon calculus, dan is (A) afleidbaar van (Gamma) in kwantificatorvrije predikaatlogica.

Tweede epsilon-stelling: Stel dat (Gamma / cup {A }) een reeks formules is die geen betrekking hebben op het epsilon-symbool. Als (A) afleidbaar is van (Gamma) in de epsilon calculus, dan is (A) afleidbaar van (Gamma) in de predikaatlogica.

In de eerste epsilon-stelling is het de bedoeling dat "kwantificeringsvrije predikaatlogica" de bovenstaande substitutieregel omvat, dus kwantificeringsvrije axioma's gedragen zich als hun universele sluitingen. Aangezien de epsilon-calculus logica van de eerste orde omvat, impliceert de eerste epsilon-stelling dat elke omweg door predikaatlogica van de eerste orde die wordt gebruikt om een kwantificeringsvrije stelling af te leiden uit kwantificeringsvrije axioma's uiteindelijk kan worden vermeden. De tweede epsilon-stelling laat zien dat elke omweg door de epsilon-calculus die wordt gebruikt om een stelling in de taal van de predikaatcalculus af te leiden uit axioma's in de taal van de predikaatcalculus ook kan worden vermeden.

Meer in het algemeen stelt de eerste epsilon-stelling vast dat kwantoren en epsilons altijd kunnen worden geëlimineerd uit een bewijs van een kwantificatorvrije formule uit andere kwantificatorvrije formules. Dit is van bijzonder belang voor Hilbert's programma, aangezien de epsilons de rol spelen van ideale elementen in de wiskunde. Als kwantificatorvrije formules overeenkomen met het "echte" deel van de wiskundige theorie, laat de eerste epsilon-stelling zien dat ideale elementen kunnen worden verwijderd uit bewijzen van echte verklaringen, op voorwaarde dat de axioma's ook echte verklaringen zijn.

Dit idee wordt nauwkeurig gemaakt in een bepaalde algemene consistentiestelling die Hilbert en Bernays afleiden uit de eerste epsilon-stelling, die het volgende zegt: Laat (F) elk formeel systeem zijn dat het resultaat is van de predikaatrekening door toevoeging van constante, functie, en predikaatsymbolen plus ware axioma's die kwantificerings- en epsilonvrij zijn, en veronderstel dat de waarheid van atomaire formules in de nieuwe taal beslissend is. Dan is (F) consistent in de sterke zin dat elke afleidbare kwantificator- en epsilonvrije formule waar is. Hilbert en Bernays gebruiken deze stelling om een eindig consistent bewijs van elementaire geometrie te geven (1939, Sec 1.4).

De moeilijkheid om consistente bewijzen te geven voor rekenen en analyse bestaat erin dit resultaat uit te breiden tot gevallen waarin de axioma's ook ideale elementen bevatten, dwz epsilon-termen.

Verder lezen. De oorspronkelijke bronnen over de epsilon-calculus en de epsilon-stellingen (Ackermann 1924, Hilbert & Bernays 1939) blijven alleen in het Duits beschikbaar. Leisenring 1969 is een relatief moderne boekintroductie van de epsilon-calculus in het Engels. De eerste en tweede epsilonstelling worden in Zach 2017 in detail beschreven. Moser & Zach 2006 geven een gedetailleerde analyse voor de zaak zonder gelijkheid. De originele bewijzen worden geleverd voor axiomatische presentaties van de epsilon-calculus. Maehara 1955 was de eerste die sequentiële calculus met epsilon-termen beschouwde. Hij liet zien hoe hij de tweede epsilon-stelling kon bewijzen met behulp van cut-eliminatie, en versterkte vervolgens de stelling met het schema van extensie (Maehara 1957). Baaz et al. 2018 geeft een verbeterde versie van de eerste epsilon-stelling. Correcties op fouten in de literatuur (inclusief Leisenring's boek) zijn te vinden in Flannagan 1975; Ferrari 1987; en Yasuhara 1982. Een variatie van de epsilon-calculus op basis van Skolem-functies, en daarom compatibel met eerste-orde logica, wordt besproken in Davis & Fechter 1991.

4. De stelling van Herbrand

Hilbert en Bernays gebruikten de methoden van de epsilon-calculus om stellingen over de eerste-orde-logica vast te stellen die niet verwijzen naar de epsilon-calculus zelf. Een voorbeeld hiervan is de stelling van Herbrand (Herbrand 1930; zie Buss 1995, Girard 1982 en sectie 2.5 van Buss 1998). Dit wordt vaak geformuleerd als de verklaring dat als een existentiële formule (bestaat x_1 / ldots / bestaat x_k A (x_1, / ldots, x_k)) af te leiden is in de eerste-orde predikatenlogica (zonder gelijkheid), waar (A) is zonder getallen, dan zijn er termenreeksen (t_ {1} ^ 1, / ldots, t_ {k} ^ 1, / ldots, t_ {1} ^ n, / ldots, t_k ^ n), zodat [A (t_ {1} ^ 1, / ldots, t_k ^ 1) vee / ldots / vee A (t_ {1} ^ n, / ldots, t_k ^ n)) een tautologie is. Als je te maken hebt met eerste-orde logica met gelijkheid,men moet "tautologie" vervangen door "tautologisch gevolg van substitutie-instanties van de gelijkheids axioma's"; we zullen de term "quasi-tautologie" gebruiken om een dergelijke formule te beschrijven.

De zojuist beschreven versie van de stelling van Herbrand volgt onmiddellijk uit de uitgebreide eerste stelling van Epsilon van Hilbert en Bernays. Door methoden te gebruiken die verband houden met het bewijs van de tweede epsilon-stelling, hebben Hilbert en Bernays echter een sterker resultaat verkregen dat, net als de oorspronkelijke formulering van Herbrand, meer informatie biedt. Om de twee delen van de stelling hieronder te begrijpen, helpt het om een bepaald voorbeeld te beschouwen. Laat (A) de formule zijn

(bestaat x_1 / voorall x_2 / bestaat voor x_3 / voorall x_4 B (x_1, x_2, x_3, x_4)) waar (B) vrij is van kwantificering. De negatie van (A) komt overeen met (voorall x_1 / bestaat x_2 / voorall x_3 / bestaat x_4 / neg B (x_1, x_2, x _3, x_4).) Door skolemiseren, dat wil zeggen met behulp van functiesymbolen om de existentiële kwantoren te zien, verkrijgen we (exist f_2, f_4 / forall x_1, x_3 / neg B (x_1, f_2 (x_1), x_3, f_4 (x_1, x_3)).) Als we dit negeren, zien we dat de oorspronkelijke formule "equivalent" is aan (forall f_2, f_4 / bestaat x_1, x_3 B (x_1, f_2 (x_1), x_3, f_4 (x_1, x_3)).)

De eerste clausule van de stelling hieronder, in dit specifieke geval, zegt dat de formule (A) hierboven afleidbaar is in eerste-orde logica, en alleen als er een opeenvolging van termen is (t_ {1} ^ 1, t_ {3} ^ 1, / ldots, t_ {1} ^ n, t_ {3} ^ n) in de uitgebreide taal met (f_2) en (f_4) zodat [B (t_ {1} ^ 1, f_2 (t_ {1} ^ 1), t_ {3} ^ 1, f_4 (t_ {1} ^ 1, t_ {3} ^ 1)) vee / ldots / vee B (t_ {1} ^ n, f_2 (t_ {1} ^ n), t_ {3} ^ n, f_4 (t_ {1} ^ n, t_ {3} ^ n))) is een quasi-tautologie.

De tweede clausule van de stelling hieronder, in dit specifieke geval, zegt dat de formule (A) hierboven afleidbaar is in eerste-orde logica, en alleen als er sequenties van variabelen zijn (x_ {2} ^ 1, x_ { 4} ^ 1, / ldots, x_2 ^ n, x_4 ^ n) en termen (s_ {1} ^ 1, s_ {3} ^ 1, / ldots, s_1 ^ n, s_3 ^ n) in het origineel taal zodanig dat [B (s_ {1} ^ 1, x_ {2} ^ 1, s_ {3} ^ 1, x_4 ^ 1) vee / ldots / vee B (s_1 ^ n, x_2 ^ n, s_3 ^ n, x_4 ^ n)) is een quasi-tautologie, en zodanig dat (A) van deze formule kan worden afgeleid met alleen de kwantificerings- en idempotentie-regels die hieronder worden beschreven.

Stel in het algemeen dat (A) een willekeurige prenex-formule is, in de vorm (mathbf {Q} _1 x_1 / ldots / mathbf {Q} _n x_n B (x_1, / ldots, x_n),) waar (B) is kwantificeringsvrij. Dan wordt (B) de matrix van (A) genoemd en wordt een instantie van (B) verkregen door termen in de taal van (B) te vervangen door enkele van zijn variabelen. De normale vorm van Herbrand (A ^ H) van (A) wordt verkregen door

  • het verwijderen van elke universele kwantor, en
  • elke universeel gekwantificeerde variabele (x_i) vervangen door (f_i (x_ {i} ^ 1, / ldots, x_ {i} ^ {k (i)})), waar (x_ {i} ^ 1, / ldots, x_ {i} ^ {k (i)}) zijn de variabelen die overeenkomen met de existentiële kwantoren die voorafgaan aan (mathbf {Q} _i) in (A) (in volgorde), en (f_i) is een nieuw functiesymbool dat voor deze rol is aangewezen.

Wanneer we verwijzen naar een instantie van de matrix van (A ^ H), bedoelen we een formule die wordt verkregen door termen in de uitgebreide taal te vervangen in de matrix van (A ^ H). We kunnen nu de formulering van Hilbert en Bernays noemen

Herbrand's stelling. (1) Een prenex-formule (A) is af te leiden in de predikaatrekening als en alleen als er een disjunctie is van instanties van de matrix van (A ^ H) die een quasi-tautologie is.

(2) Een prenex-formule (A) is af te leiden in de predicaatrekening als en alleen als er een disjunctie (bigvee_j B_j) is van instanties van de matrix van (A), zodat (bigvee_j B_j) is een quasi-tautologie en (A) kan worden afgeleid van (bigvee_j B_j) met behulp van de volgende regels:

  • van (C_1 / vee / ldots / vee C_i (t) vee / ldots / vee C_m)

    concluderen (C_1 / vee / ldots / vee / bestaat x C_i (x) vee / ldots / vee C_m) en

  • van (C_1 / vee / ldots / vee C_i (x) vee / ldots / vee C_m)

    conclusie (C_1 / vee / ldots / vee / forall xC_i (x) vee / ldots / vee C_m) (als (x) niet in (C_j) voor (j / ne i)),

evenals de onmacht van (vee) (van (C / vee C / vee D) conclusie (C / vee D)).

De stelling van Herbrand kan ook worden verkregen door middel van cut-elimination, via Gentzen's 'midsequent theorem'. Het bewijs dat de tweede epsilon-stelling gebruikt, onderscheidt zich echter als het eerste volledige en correcte bewijs van de stelling van Herbrand. Bovendien, en dit wordt zelden erkend, terwijl het bewijs op basis van snij-eliminatie alleen een beperking geeft aan de lengte van de Herbrand-disjunctie als een functie van de snijrang en complexiteit van de gesneden formules in het bewijs, de lengte verkregen uit het bewijs gebaseerd op de epsilon-calculus geeft een grens als functie van het aantal toepassingen van het transfinite axioma, en de rang en graad van de daarin voorkomende epsilon-termen. Met andere woorden, de lengte van de Herbrand-disjunctie hangt alleen af van de kwantificeringscomplexiteit van de betrokken substituties, en bijvoorbeeldhelemaal niet op de propositionele structuur of de lengte van het bewijs.

De versie van de stelling van Herbrand die aan het begin van deze sectie wordt vermeld, is in wezen het speciale geval van (2) waarin de formule (A) existentieel is. In het licht van dit speciale geval is (1) gelijk aan de bewering dat een formule (A) afleidbaar is in de eerste-orde predikaatlogica, al dan niet als (A ^ H) dat is. De voorwaartse richting van deze gelijkwaardigheid is veel gemakkelijker te bewijzen; in feite is voor elke formule (A, A / rightarrow A ^ H) af te leiden in de predikaatlogica. Het bewijzen van de omgekeerde richting houdt in dat de extra functiesymbolen in (A ^ H) worden geëlimineerd en is veel moeilijker, vooral in aanwezigheid van gelijkheid. Hier spelen de epsilon-methoden een centrale rol.

Gegeven een prenex-formule, wordt de normale Skolem-vorm (A ^ S) dubbel gedefinieerd in (A ^ H), dat wil zeggen door het vervangen van existentieel gekwantificeerde variabelen door het waarnemen van functies. Als (Gamma) een set van voorafgaande zinnen is, laat (Gamma ^ S) dan de set van hun normale Skolem-vormen aangeven. Met behulp van de deductiestelling en de stelling van Herbrand is het niet moeilijk aan te tonen dat het volgende paarsgewijs equivalent is: (begin {align} Gamma & / text {bewijst} A \\ / Gamma & / text {bewijst} A ^ H \\ / Gamma ^ S & / text {bewijst} A \\ / Gamma ^ S & / text {bewijst} A ^ H / end {align})

Een opvallende toepassing van de stelling van Herbrand en verwante methoden is te vinden in de analyse van Luckhardt (1989) van de stelling van Roth. Voor een bespreking van nuttige uitbreidingen van Herbrand's methoden, zie Sieg 1991. Een model-theoretische versie hiervan wordt besproken in Avigad 2002a.

5. De Epsilon-vervangingsmethode en rekenkunde

Zoals hierboven vermeld, was historisch gezien het primaire belang van de epsilon-calculus een middel om consistentiebewijzen te verkrijgen. Hilbert's lezingen uit 1917–1918 merken al op dat men gemakkelijk de consistentie van propositionele logica kan bewijzen door propositionele variabelen en formules te nemen die de waarheidswaarden 0 en 1 overschrijden, en de logische connectieven te interpreteren als de bijbehorende rekenkundige bewerkingen. Evenzo kan men de consistentie van predikaatlogica (of de zuivere epsilon-calculus) bewijzen door zich te specialiseren in interpretaties waarin het discoursuniversum één enkel element heeft. Deze overwegingen suggereren het volgende, meer algemene programma om consistentie te bewijzen:

  • Verleng de epsilon-calculus zodanig dat deze grotere delen van de wiskunde vertegenwoordigt.
  • Laat met finitaire methoden zien dat elk bewijs in het uitgebreide systeem een consistente interpretatie heeft.

Overweeg bijvoorbeeld de taal van rekenen, met symbolen voor (0), (1), (+), (times), (lt). Samen met kwantificatievrije axioma's die de basissymbolen definiëren, kan men specificeren dat de epsilon-termen (varepsilon x A (x)) de minste waarde kiezen die voldoet aan (A), als die er is, met het volgende axioma: (tag {*} A (x) rightarrow A (varepsilon x A (x)) wedge / varepsilon x A (x) le x) Het resultaat is een systeem dat sterk genoeg is om eerst te interpreteren -order (Peano) rekenen. Als alternatief kan men het epsilon-symbool gebruiken om aan het volgende axioma te voldoen: [A (y) rightarrow A (varepsilon x A (x)) wedge / varepsilon x A (x) ne y + 1.)

Met andere woorden, als er een getuige (y) voldoet (A (y)), retourneert de epsilon-term een waarde waarvan de voorganger niet dezelfde eigenschap heeft. Het is duidelijk dat de epsilon-term beschreven door (*) voldoet aan het alternatieve axioma; omgekeerd kan men controleren of gegeven (A) een waarde van (varepsilon x (bestaat z / le x A (x))) die voldoet aan het alternatieve axioma kan worden gebruikt om (varepsilon x A te interpreteren (x)) in (*). De betekenis van de epsilon-term kan verder worden vastgesteld met de axioma (varepsilon x A (x) ne 0 / rechterpijl A (varepsilon x A (x))) die vereist dat als er geen getuige is van (A), de term epsilon geeft 0. 0. Voor de onderstaande bespreking is het echter het handigst om alleen op (*) te focussen.

Stel dat we willen aantonen dat het bovenstaande systeem consistent is; we willen met andere woorden aantonen dat er geen bewijs is voor de formule (0 = 1). Door alle substituties naar de axioma's te pushen en vrije variabelen te vervangen door de constante 0, volstaat het om aan te tonen dat er geen propositioneel bewijs is van (0 = 1) van een eindige set gesloten instanties van de axioma's. Daarvoor is het voldoende om aan te tonen dat, gezien elke eindige reeks gesloten gevallen van axioma's, men numerieke waarden aan termen kan toewijzen op een zodanige manier dat alle axioma's waar zijn onder de interpretatie. Omdat de rekenkundige bewerkingen (+) en (times) op de gebruikelijke manier kunnen worden geïnterpreteerd, ligt het enige probleem in het vinden van geschikte waarden om toe te wijzen aan de epsilon-termen.

Hilbert's epsilon-substitutiemethode kan grofweg als volgt worden beschreven:

  • Gegeven een eindige reeks axioma's, begin met het interpreteren van alle epsilon-termen als 0.
  • Zoek een exemplaar van het axioma (*) hierboven dat onjuist is onder de interpretatie. Dit kan alleen gebeuren als men een term t heeft zodat (A (t)) waar is in de interpretatie, maar (A (varepsilon x A (x))) niet waar is of de waarde van (t) is kleiner dan de waarde van (varepsilon x A (x)).
  • "Herstel" de toewijzing door aan (varepsilon x A (x)) de waarde van (t) toe te wijzen en herhaal het proces.

Een eindig consistentiebewijs wordt verkregen zodra op een eindig aanvaardbare manier is aangetoond dat dit proces van opeenvolgende "reparaties" eindigt. Als dat zo is, zijn alle kritische formules echte formules zonder epsilon-termen.

Dit basisidee (de “Hilbertsche Ansatz”) werd voor het eerst door Hilbert uiteengezet in zijn lezing uit 1922 (1923) en uitgewerkt in lezingen in 1922–23. De daar gegeven voorbeelden hebben echter alleen betrekking op bewijzen waarin alle gevallen van het transfinite axioma overeenkomen met een enkele epsilon term (varepsilon x A (x)). De uitdaging was om de aanpak uit te breiden tot meer dan één epsilon-term, tot geneste epsilon-termen en uiteindelijk tot tweede-orde-epsilons (om niet alleen een rekenkundig maar ook een analysebewijs te verkrijgen).

De moeilijkheid bij het omgaan met geneste epsilon-termen kan als volgt worden beschreven. Stel dat een van de axioma's in het bewijs het transfinite axioma is [B (y) rightarrow B (varepsilon y B (y))) (varepsilon y B (y)) kan natuurlijk voorkomen in andere formules in het bewijs, in het bijzonder in andere transfinite axioma's, bijvoorbeeld [A (x, / varepsilon y B (y)) rightarrow A (varepsilon x A (x, / varepsilon y B (y)), / varepsilon y B (y))) Dus eerst lijkt het nodig om een juiste interpretatie te vinden voor (varepsilon y B (y)) voordat we proberen er een te vinden voor (varepsilon x A (x, / varepsilon y B (y))). Er zijn echter meer gecompliceerde patronen waarin epsilon-termen in een proef kunnen voorkomen. Een instantie van het axioma, die een rol speelt bij het bepalen van de juiste interpretatie voor (varepsilon y B (y)), kan [B (varepsilon x A (x,\ varepsilon y B (y))) rightarrow B (varepsilon y B (y))) Als (B) (0) niet waar is, dan in de eerste ronde van de procedure (varepsilon y B (y)) wordt geïnterpreteerd door 0. Een volgende wijziging van de interpretatie van (varepsilon x A (x, 0)) van 0 in, zeg maar, (n), zal resulteren in een interpretatie van deze instantie as (B (n) rightarrow B) (0) wat onwaar zal zijn als (B (n)) waar is. Dus de interpretatie van (varepsilon y B (y)) moet worden gecorrigeerd naar (n), wat op zijn beurt kan leiden tot de interpretatie van (varepsilon x A (x, / varepsilon y B (y))) om niet langer een echte formule te zijn.zal resulteren in een interpretatie van deze instantie als (B (n) rightarrow B) (0), wat onwaar zal zijn als (B (n)) waar is. Dus de interpretatie van (varepsilon y B (y)) moet worden gecorrigeerd naar (n), wat op zijn beurt kan leiden tot de interpretatie van (varepsilon x A (x, / varepsilon y B (y))) om niet langer een echte formule te zijn.zal resulteren in een interpretatie van deze instantie als (B (n) rightarrow B) (0), wat onwaar zal zijn als (B (n)) waar is. Dus de interpretatie van (varepsilon y B (y)) moet worden gecorrigeerd naar (n), wat op zijn beurt kan leiden tot de interpretatie van (varepsilon x A (x, / varepsilon y B (y))) om niet langer een echte formule te zijn.

Dit is slechts een schets van de moeilijkheden die betrokken zijn bij het uitbreiden van Hilbert's idee tot de algemene zaak. Ackermann (1924) zorgde voor een dergelijke veralgemening met behulp van een procedure die 'teruggaat' wanneer een nieuwe interpretatie in een bepaald stadium ertoe leidt dat een reeds in een eerdere fase gevonden interpretatie moet worden gecorrigeerd.

De procedure van Ackermann was van toepassing op een systeem van rekenkunde van de tweede orde, waarbij de termijnen van de tweede orde echter werden beperkt om kruisbinding van epsilons van de tweede orde uit te sluiten. Dit komt ruwweg neer op een beperking van het rekenkundig begrip als set-vormingsprincipe dat beschikbaar is (zie de discussie aan het einde van deze paragraaf). Verdere moeilijkheden met epsilon-termen van de tweede orde kwamen aan de oppervlakte, en het werd al snel duidelijk dat het bewijs in zijn huidige vorm misleidend was. Niemand op Hilbert's school besefte echter de omvang van de moeilijkheid tot 1930, toen Gödel zijn onvolledige resultaten aankondigde. Tot dan toe werd aangenomen dat het bewijs (althans met enkele door Ackermann aangebrachte wijzigingen),sommige van de ideeën uit von Neumanns (1927) versie van de epsilon-substitutiemethode) zouden in ieder geval voor het eerste-ordeonderdeel doorgaan. Hilbert en Bernays (1939) suggereren dat de gebruikte methoden alleen een consistentiebewijs opleveren voor eerste-orde rekenkunde met open inductie. In 1936 slaagde Gerhard Gentzen erin een bewijs te leveren van de consistentie van eerste-orde rekenkunde in een formulering gebaseerd op predikaatlogica zonder het epsilon-symbool. Deze proef gebruikt transfinite inductie tot (varepsilon_0). Ackermann (1940) was later in staat om Gentzen's ideeën aan te passen om een correct consistentiebewijs te geven van eerste-orde rekenkunde met behulp van de epsilon-substitutiemethode. Gerhard Gentzen slaagde erin een bewijs te leveren van de consistentie van eerste-orde rekenkunde in een formulering gebaseerd op predikaatlogica zonder het epsilon-symbool. Deze proef gebruikt transfinite inductie tot (varepsilon_0). Ackermann (1940) was later in staat om Gentzen's ideeën aan te passen om een correct consistentiebewijs van eerste-orde rekenkunde te geven met behulp van de epsilon-substitutiemethode. Gerhard Gentzen slaagde erin een bewijs te leveren van de consistentie van eerste-orde rekenkunde in een formulering gebaseerd op predikaatlogica zonder het epsilon-symbool. Deze proef gebruikt transfinite inductie tot (varepsilon_0). Ackermann (1940) was later in staat om Gentzen's ideeën aan te passen om een correct consistentiebewijs van eerste-orde rekenkunde te geven met behulp van de epsilon-substitutiemethode.

Hoewel de pogingen van Ackermann om een consistentiebewijs voor rekenkunde van de tweede orde te bereiken niet succesvol waren, gaven ze een duidelijker begrip van het gebruik van tweedelijns epsilon-termen bij de formalisering van de wiskunde. Ackermann gebruikte tweede-orde epsilon-termen (varepsilon f / A (f)), waarbij (f) een functievariabele is. Analoog aan het eerste-orde geval is (varepsilon f / A (f)) een functie waarvoor (A (f)) waar is, bijvoorbeeld (varepsilon f (x + f (x) = 2x)) is de identiteitsfunctie (f (x) = x). Nogmaals, analoog aan het geval van de eerste orde, kan men tweede-orde-epsilons gebruiken om tweede-orde-kwantoren te interpreteren. In het bijzonder kan voor elke tweede-orde formule (A (x)) een term (t (x)) worden gevonden zodat [A (x) leftrightarrow t (x) = 1) afleidbaar is in de calculus (de formule (A) kan andere vrije variabelen hebben,in dat geval komen deze ook voor in de term (t)). Dit feit kan men vervolgens gebruiken om begripsbeginselen te interpreteren. In een taal met functiesymbolen hebben deze de vorm (bestaat f / forall x (A (x) leftrightarrow f (x) = 1)) voor een willekeurige formule (A (x)). Begrip wordt vaker uitgedrukt in termen van ingestelde variabelen, in welk geval het de vorm aanneemt (bestaat Y / voor alle x (A (x) leftrightarrow x / in Y),) en beweert dat elke formule van de tweede orde, met parameters, definieert een set.in dat geval neemt het de vorm aan (bestaat Y / voor alle x (A (x) leftrightarrow x / in Y),) met de bewering dat elke tweede-ordeformule, met parameters, een set definieert.in dat geval neemt het de vorm aan (bestaat Y / voor alle x (A (x) leftrightarrow x / in Y),) met de bewering dat elke tweede-ordeformule, met parameters, een set definieert.

Analyse, of tweede-orde rekenkunde, is de uitbreiding van eerste-orde rekenkunde met het begripsschema voor willekeurige tweede-orde formules. De theorie is indringend in die zin dat men hiermee sets van natuurlijke getallen kan definiëren met behulp van kwantoren die zich uitstrekken over het hele universum van sets, inclusief, impliciet, de set die wordt gedefinieerd. Men kan predicatieve fragmenten van deze theorie verkrijgen door het type formules te beperken dat is toegestaan in het begrip axioma. De beperking die in verband met Ackermann hierboven is besproken, komt bijvoorbeeld overeen met het rekenbegripschema, waarin formules geen tweede-orde-kwantoren omvatten. Er zijn verschillende manieren om sterkere analysefragmenten te verkrijgen die niettemin predicatief gerechtvaardigd zijn. Men verkrijgt bijvoorbeeld een vertakte analyse door een ordinale rang te associëren om variabelen in te stellen;ruwweg, in de definitie van een set van een bepaalde rang, variëren kwantificatoren alleen over sets van lagere rang, dat wil zeggen degenen waarvan de definities logischerwijs voorafgaan.

Verder lezen. De vroege bewijzen van Hilbert en Ackermann worden besproken in Zach 2003; 2004. Het bewijs van Von Neumann is het onderwerp van Bellotti 2016. Het bewijs van Ackermann uit 1940 wordt besproken in Hilbert & Bernays 1970 en Wang 1963. Een moderne presentatie wordt gegeven door Moser 2006. Een vroege toepassing van epsilon-vervanging is de interpretatie zonder tegenvoorbeeld (Kreisel 1951).

6. Meer recente ontwikkelingen

In deze sectie bespreken we de ontwikkeling van de epsilon-substitutiemethode voor het verkrijgen van consistentie resultaten voor sterke systemen; deze resultaten zijn van wiskundige aard. We kunnen de details van de bewijzen hier helaas niet bespreken, maar zouden willen aangeven dat de epsilon-substitutiemethode niet stierf met het programma van Hilbert en dat een aanzienlijk deel van het huidige onderzoek wordt uitgevoerd in epsilon-formalismen.

Gentzen's consistentieproeven voor rekenkunde lanceerden een onderzoeksgebied dat bekend staat als ordinale analyse, en het programma voor het meten van de kracht van wiskundige theorieën met behulp van ordinale notaties wordt nog steeds voortgezet. Dit is met name relevant voor het uitgebreide Hilbert-programma, waar het doel is om klassieke wiskunde te rechtvaardigen ten opzichte van constructieve of quasi-constructieve systemen. Gentzen's verwijderingsmethoden (en uitbreidingen van de infinitaire logica ontwikkeld door Paul Lorentzen, Petr Novikov en Kurt Schütte) hebben voor een groot deel de vervangingsmethoden van epsilon in deze bezigheden verdrongen. Maar epsilon-calculusmethoden bieden een alternatieve benadering en er is nog steeds actief onderzoek naar manieren om Hilbert-Ackermann-methoden uit te breiden tot sterkere theorieën. Het algemene patroon blijft hetzelfde:

  1. Integreer de onderzochte theorie in een geschikte epsilon-calculus.
  2. Beschrijf een proces voor het bijwerken van opdrachten naar de epsilon-voorwaarden.
  3. Laat zien dat de procedure normaliseert, dat wil zeggen dat er, gezien elke set termen, een reeks updates is die resulteert in een opdracht 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 een ordinale analyse door ordinale notaties toe te kennen aan stappen in de procedure, zodanig dat de waarde van een notatie bij elke stap afneemt.

In de jaren zestig breidde Tait (1960, 1965, 2010) de methoden van Ackermann uit om een ordinale analyse te verkrijgen van uitbreidingen van rekenkunde met principes van transfinite inductie. Meer gestroomlijnde en moderne versies van deze aanpak zijn te vinden in Mints 2001 en Avigad 2002b. Meer recentelijk hebben Mints, Tupailo en Buchholz sterkere, maar nog steeds predicatief gerechtvaardigde, fragmenten van analyse overwogen, waaronder theorieën over rekenkundig begrip en een (Delta ^ {1} _1) - begripsregel (Mints, Tupailo & Buchholz 1996; Mints & Tupailo 1999; zie ook Mints 2016). Arai 2002 heeft de epsilon-substitutiemethode uitgebreid tot theorieën die het mogelijk maken om rekenkundig begrip te herhalen langs primitieve recursieve volgorde van putten. Vooral,zijn werk levert ordinale analyses op voor predicatieve analysefragmenten met transfinite hiërarchieën en transfinite inductie.

Er zijn enkele eerste stappen gezet in het gebruik van de epsilon-substitutiemethode bij de analyse van impredicatieve theorieën (zie Arai 2003, 2006 en Mints 2015).

Een variatie op stap 3 hierboven houdt in dat wordt aangetoond dat de normalisatieprocedure niet gevoelig is voor de keuze van updates, dat wil zeggen dat elke reeks updates wordt beëindigd. Dit wordt sterke normalisatie genoemd. Mints 1996 heeft aangetoond dat veel van de beschouwde procedures deze sterkere eigenschap hebben.

Naast de traditionele, fundamentele tak van bewijstheorie, is er tegenwoordig veel belangstelling voor structurele bewijstheorie, een tak van het onderwerp die zich richt op logische deductieve berekeningen en hun eigenschappen. Dit onderzoek is nauw verbonden met kwesties die relevant zijn voor informatica, die te maken hebben met geautomatiseerde aftrek, functionele programmering en computerondersteunde verificatie. Ook hier domineren Gentzen-achtige methoden (zie opnieuw de vermelding over bewijstheorie). Maar de epsilon-calculus kan ook waardevolle inzichten opleveren; vgl. bijvoorbeeld Aguilera & Baaz 2019, of de bespreking van de stelling van Herbrand hierboven.

Afgezien van de onderzoeken naar de epsilon-calculus in de bewijstheorie, moeten twee toepassingen worden genoemd. Een daarvan is het gebruik van epsilon-notatie in Bourbaki's Theorie des ensembles (1958). De tweede, misschien wel van groter belang, is het gebruik van de epsilon-operator in de stellingbevorderende systemen HOL en Isabelle, waar de expressieve kracht van epsilon-termen aanzienlijke praktische voordelen oplevert.

7. Epsilon-operators in taalkunde, filosofie en niet-klassieke logica

Het lezen van de epsilon-operator als een operator voor onbepaalde keuze ("an (x) zodat (A (x))")) suggereert dat het een nuttig hulpmiddel zou kunnen zijn bij de analyse van onbepaalde en bepaalde uitdrukkingen van zelfstandige naamwoorden in formele semantiek. De epsilon-notatie is in feite zo gebruikt en deze toepassing is met name nuttig gebleken bij het behandelen van anaforische referentie.

Beschouw het bekende voorbeeld

Elke boer die een ezel bezit, verslaat het

De algemeen aanvaarde analyse van deze zin wordt gegeven door de universele zin

(forall x / forall y (mathrm {Farmer} (x) wedge / mathrm {Donkey} (y) wedge / mathrm {Owns} (x, y)) rightarrow / mathrm {Beats} (x, y)))

Het nadeel is dat "een ezel" een existentiële kwantor suggereert, en dus moet de analyse op de een of andere manier parallel lopen aan de analyse van zin 3 gegeven door 4:

  1. Elke boer die een ezel bezit, is blij,
  2. (forall x (mathrm {Farmer} (x) wedge / bestaat y (mathrm {Donkey} (y) wedge / mathrm {Owns} (x, y)) rightarrow / mathrm {Happy} (x))),

maar de dichtst mogelijke formalisatie,

(forall x ((mathrm {Farmer} (x) wedge / bestaat y (mathrm {Donkey} (y) wedge / mathrm {Owns} (x, y)) rightarrow / mathrm {Beats} (x, y)))

bevat een gratis exemplaar van (y). Evans 1980 suggereert dat aangezien voornaamwoorden uitdrukkingen zijn, ze als definitieve beschrijvingen moeten worden geanalyseerd; en als het voornaamwoord voorkomt als gevolg van een voorwaardelijk, worden de beschrijvende voorwaarden bepaald door het antecedent. Dit leidt tot de volgende E-type analyse van (1): (begin {multline *} forall x ((mathrm {Farmer} (x) wedge / exist y (mathrm {Donkey} (y) wedge / mathrm {Owns} (x, y)) rightarrow \(mathrm {Beats} (x, / iota y (mathrm {Donkey} (y) wedge / mathrm {Owns} (x, y))) end {multline *}) Hier is (iota x) de operator voor de definitieve beschrijving, dus (iota y (mathrm {Donkey} (y) wedge / mathrm {Owns} (x, y))) is "de ezel die eigendom is van (x);". Het probleem hiermee is dat volgens de standaardanalyse de definitieve beschrijving een unieke voorwaarde heeft,en dus (5) zal onwaar zijn als er een boer is die meer dan één ezel bezit. Een uitweg hieruit is het introduceren van een nieuwe operator, whe (wie dan ook, wat dan ook) die werkt als een generaliserende kwantificeerder (Neale, 1990): (begin {multline *} forall x ((mathrm {Farmer} (x) wedge / bestaat y (mathrm {Donkey} (y) wedge / mathrm {Owns} (x, y)) rightarrow \(mathrm {Beats} (x, / mathrm {whe}, y (mathrm {Donkey} (y) wedge / mathrm {Owns} (x, y))) end {multline *})

Zoals opgemerkt door von Heusinger (1994), suggereert dit dat Neale zich ertoe verbindt om voornaamwoorden dubbelzinnig te maken tussen bepaalde omschrijvingen ((iota) - uitdrukkingen) en wee-uitdrukkingen. Heusinger stelt in plaats daarvan voor om epsilon-operatoren te gebruiken die zijn geïndexeerd door keuzefuncties (die afhankelijk zijn van de context). Volgens deze benadering is de analyse van (1)

Voor elke keuzefunctie (i): (begin {multline *} forall x ((mathrm {Farmer} (x) wedge / mathrm {Owns} (x, / varepsilon_i y / mathrm {Donkey} (y)) rightarrow \\\ mathrm {Beats} (x, / varepsilon_ {a ^ *} y / mathrm {Donkey} (y)) end {multline *})

Hier is (a ^ *) een keuzefunctie die afhankelijk is van (i) en het antecedent van het voorwaardelijke: Als (i) een keuzefunctie is die (varepsilon_i y / mathrm {Donkey} (y)) uit de set van alle ezels, dan selecteert (varepsilon_ {a ^ *} y / mathrm {Donkey} (y)) uit de set ezels die eigendom zijn van (x).

Deze benadering van het omgaan met voornaamwoorden met epsilon-operatoren geïndexeerd door keuzefuncties stelt von Heusinger in staat om met een grote verscheidenheid aan omstandigheden om te gaan (zie Egli en von Heusinger, 1995; von Heusinger, 2000).

Toepassingen van de epsilon-operator in formele semantiek, en keuzefuncties in het algemeen, hebben de afgelopen jaren veel belangstelling gekregen. Von Heusinger en Egli (2000a) vermelden onder meer: representaties van vragen (Reinhart, 1992), specifieke onbepaalde tijd (Reinhart 1992; 1997; Winter 1997), E-type voornaamwoorden (Hintikka en Kulas 1985; Slater 1986; Chierchia 1992, Egli en von Heusinger 1995) en bepaalde zelfstandige naamzinnen (von Heusinger 1997, 2004).

Voor een bespreking van de problemen en toepassingen van de epsilon-operator in de taal- en taalfilosofie, zie het artikel van BH Slater over epsilon calculi (geciteerd in de sectie Andere internetbronnen hieronder) en de collecties von Heusinger en Egli 2000 en von Heusinger en Kempson 2004.

Een andere toepassing van epsilon calculus is als algemene logica voor redeneren over willekeurige objecten. Meyer Viol (1995a) vergelijkt de epsilon-calculus met Fine's (1985) theorie van willekeurige objecten. De verbinding is inderdaad niet moeilijk te zien. Gezien de gelijkwaardigheid (forall x A (x) equiv) A ((varepsilon x (neg A))), is de term (varepsilon x (neg A)) een willekeurig object in die zin dat het een object is waarvan (A) waar is als f (A) in het algemeen waar is.

Meyer Viol (1995a, 1995b) bevatten verdere bewijs- en modeltheoretische studies van de epsilon-calculus; specifiek intuïtionistische epsilon calculi. Hier houden de stellingen van epsilon niet langer stand, dat wil zeggen dat de introductie van termen van epsilon niet-conservatieve uitbreidingen van intuïtionistische logica oplevert. Andere onderzoeken naar epsilon-operators in intuïtionistische logica zijn te vinden in Shirai (1971), Bell (1993a, 1993b) en DeVidi (1995). Voor epsilon-operators in veelgewaardeerde logica, zie Mostowski (1963), voor modale epsilon-calculus, Fitting (1975).

Verder lezen. Hieronder volgt een lijst van enkele publicaties op het gebied van taal en taalkunde die relevant zijn voor de epsilon calculus en zijn toepassingen. De lezer is met name gericht op de collecties von Heusinger & Egli (red.) 2000 en von Heusinger & Kempson (red.) 2004 voor verdere discussie en referenties: Bell 1993a, 1993b; Chierchia 1992; DeVidi 1995; Egli & von Heusinger 1995; Fine 1985; Fitting 1975; von Heusinger 1994, 1997, 2000, 2004; von Heusinger & Egli (red.) 2000; von Heusinger & Kempson (red.) 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; en Winter 1997.

Bibliografie

  • Aguilera, JP, Baaz, M., 2019, 'Ongezonde gevolgtrekkingen maken bewijzen korter'. Journal of Symbolische Logica 84: 102–122.
  • Ackermann, W., 1924, 'Begründung des' 'tertium non datur' 'wanten van Hilbertschen Theorie der Widerspruchsfreiheit', Mathematische Annalen, 93: 1–36.
  • –––, 1937–38, 'Mengentheoretische Begründung der Logik', Mathematische Annalen, 115: 1–22.
  • –––, 1940, 'Zur Widerspruchsfreiheit der Zahlentheorie', Mathematische Annalen, 117: 162–194.
  • Arai, T., 2002, 'Epsilon-substitutiemethode voor theorieën van spronghiërarchieën', Archive for Mathematical Logic, 2: 123–153.
  • –––, 2003, 'Epsilon-substitutiemethode voor ID (_ 1 (Pi ^ {0} _1 / vee / Sigma ^ {0} _1))', Annals of Pure and Applied Logic, 121: 163–208.
  • –––, 2006, 'Epsilon-substitutiemethode voor (Pi ^ {0} _2) - FIX. Journal of Symbolische Logica 71: 1155–1188
  • Avigad, J., 2002a, 'Verzadigde modellen van universele theorieën', Annals of Pure and Applied Logic, 118: 219–234.
  • –––, 2002b, 'Update-procedures en de 1-consistentie van rekenen', Mathematical Logic Quarterly, 48: 3–13.
  • Baaz, M., Leitsch, A., Lolic, A., 2018, 'A sequent-calculus based formulation of the extended first epsilon theorem', in: Artemov, S., Nerode, A. (red.), Logical Foundations of Computer Science, Berlin: Springer, 55–71.
  • Bell, JL, 1993a. 'Hilbert's epsilon-operator en klassieke logica', Journal of Philosophical Logic, 22: 1–18.
  • –––, 1993b. 'Hilbert's epsilon-operator in intuïtionistische typetheorieën', Mathematical Logic Quarterly, 39: 323–337.
  • Bellotti, L., 2016, 'Von Neumann's consistentie proof', Review of Symbolische logica, 9: 429–455.
  • Bourbaki, N., 1958, Theorie des ensembles, Paris: Hermann.
  • Buss, S., 1995, 'On Herbrand's theorem', Logic and Computational Complexity (Lecture Notes in Computer Science 960), Berlin: Springer, 195–209.
  • ––– 1998, 'Introduction to proof theory', in: Buss (red.), The Handbook of Proof Theory, Amsterdam: Noord-Holland, 1–78.
  • Chierchia, G., 1992. 'Anafora en dynamische logica'. Taalkunde en filosofie, 15: 111–183.
  • Davis, M. en R. Fechter, 1991, 'A free variable version of the first-order predicate calculus', Journal of Logic and Computation, 1: 431–451.
  • DeVidi, D., 1995. 'Intuitionistic (varepsilon) - and (tau) - calculi', Mathematical Logic Quarterly 41: 523–546.
  • Egli, U., von Heusinger, K., 1995, 'The epsilon operator and E-type pronouns', in U. Egli et al. (red.), Lexicale kennis in de organisatie van taal, Amsterdam: Benjamins, 121–141 (Actuele vraagstukken in de taaltheorie 114).
  • Evans, G., 1980, 'Pronouns', Linguistic Inquiry, 11: 337–362.
  • Ewald, WB (red.), 1996, From Kant to Hilbert. A Source Book in the Foundations of Mathematics, Vol. 2, Oxford: Oxford University Press.
  • Ferrari, PL, 1987, 'A note on a proof of Hilbert's second (varepsilon) - theorem', Journal of Symbolic Logic, 52: 214–215.
  • Fine, K., 1985. Redeneren met willekeurige objecten, Oxford: Blackwell.
  • Fitting, M., 1975. 'A modal logic epsilon-calculus', Notre Dame Journal of Formal Logic, 16: 1–16.
  • Flannagan, TB, 1975, 'On a extension of Hilbert's second (varepsilon) - theorem', Journal of Symbolic Logic, 40: 393–397.
  • Girard, J.-Y., 1982, 'Herbrand's stelling en bewijstheorie', Proceedings of the Herbrand Symposium, Amsterdam: North-Holland, 29-38.
  • Herbrand, J., 1930, Recherches sur la thèorie de la dèmonstration, Dissertation, University of Paris. Engelse vertaling in Herbrand 1971, blz. 44–202.
  • –––, 1971, Logical Writings, W. Goldfarb (red.), Cambridge, Mass.: Harvard University Press.
  • Hilbert, D., 1922, 'Neubegründung der Mathematik: Erste Mitteilung', Abhandlungen aus dem Seminar der Hamburgischen Universität, 1: 157–177, Engelse vertaling in Mancosu, 1998, 198–214 en Ewald, 1996, 1115–1134.
  • –––, 1923, 'Die logischen Grundlagen der Mathematik', Mathematische Annalen, 88: 151–165, Engelse vertaling in Ewald, 1996, 1134–1148.
  • Hilbert, D., Bernays, P., 1934, Grundlagen der Mathematik, Vol. 1, Berlijn: Springer.
  • –––, 1939, Grundlagen der Mathematik, Vol. 2, Berlijn: Springer.
  • –––, 1970, 'Grundlagen der Mathematik', Vol. 2e, 2e editie, Berlijn: Springer, Supplement V.
  • Hintikka, J., Kulas, J., 1985. Anaphora en definitieve beschrijvingen: twee toepassingen van speltheoretische semantiek, Dordrecht: Reidel.
  • Kempson, R., Meyer Viol, W., en Gabbay, D., 2001. Dynamische syntaxis: de stroom van taalbegrip, Oxford: Blackwell.
  • Kreisel, G, 1951, 'Over de interpretatie van niet-finitistische bewijzen - deel I', Journal of Symbolic Logic, 16: 241–267.
  • Leisenring, AC, 1969, Mathematical Logic en Hilbert's Epsilon-Symbol, London: Macdonald.
  • Luckhardt, H., 1989, 'Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken', Journal of Symbolic Logic, 54: 234–263.
  • Maehara, S., 1955, 'The predicate calculus with (varepsilon) - symbol', Journal of the Mathematical Society of Japan, 7: 323–344.
  • –––, 1957, 'Equality axiom on Hilbert's (varepsilon) - symbol', Journal of the Faculty of Science, University of Tokyo, Section 1, 7: 419–435.
  • Mancosu, P. (red.), 1998, Van Brouwer tot Hilbert. Het debat over de grondslagen van de wiskunde in de jaren 1920, Oxford: Oxford University Press.
  • Meyer Viol, WPM, 1995a, Instantial Logic. Een onderzoek naar redeneren met instanties, Ph. D. scriptie, Universiteit Utrecht. ILLC Dissertation Series 1995–11.
  • –––, 1995b. 'Een proof-theoretische behandeling van opdrachten', Bulletin van de IGPL, 3: 223–243.
  • Mints, G., 1994, 'Gentzen-achtige systemen en Hilbert's epsilon-substitutiemethode. I ', Logic, Methodology and Philosophy of Science, IX (Uppsala, 1991), Amsterdam: Noord-Holland, 91-122.
  • –––, 1996, 'Strong terminination for the epsilon substitution method', Journal of Symbolic Logic, 61: 1193–1205.
  • –––, 2001, 'The epsilon substitution method and continuity', in W. Sieg et al. (red.), Reflections on the Foundations of Mathematics: Essays ter Honour of Solomon Feferman, Lecture Notes in Logic 15, Association for Symbolic Logic.
  • –––, 2008, 'Cut Elimination for a simple formulation of epsilon calculus', Annals of Pure and Applied Logic, 152 (1–3): 148–160.
  • –––, 2013. 'Epsilon-vervanging voor predicaatlogica van de eerste en tweede orde', Annals of Pure en Applied Logic, 164: 733–739.
  • –––, 2015. 'Niet-deterministische epsilon-substitutiemethode voor PA en ID (_ 1)', in: Kahle, R., Rathjen, M. (Eds.), Gentzen's Centenary: The Quest for Consistency. Berlijn: Springer, pp. 479–500.
  • Mints, G., Tupailo, S., 1999, 'Epsilon-substitutiemethode voor de vertakte taal en (Delta ^ {1} _1) - begripsregel', in A. Cantini et al. (red.), Logica en grondslagen van de wiskunde (Florence, 1995), Dordrecht: Kluwer, 107–130.
  • Mints, G., Tupailo, S., Buchholz, W., 1996, 'Epsilon-substitutiemethode voor elementaire analyse', Archive for Mathematical Logic, 35: 103–130.
  • Moser, G., 2006, 'Ackermann's substitutiemethode (geremixed)', Annals of Pure and Applied Logic, 142 (1-3): 1-18.
  • Moser, G. en R. Zach, 2006, 'The epsilon calculus and Herbrand complexity', Studia Logica, 82 (1): 133–155.
  • Mostowski, A., 1963. 'De Hilbert epsilon-functie in veelgewaardeerde logica's', Acta Philosophica Fennica, 16: 169–188.
  • Neale, S., 1990, Beschrijvingen, Cambridge, MA: MIT Press.
  • Reinhart, T., 1992. 'WH-in-situ: een schijnbare paradox'. In: P. Dekker en M. Stokhof (redactie). Proceedings of the Eighth Amsterdam Colloquium, 17–20 december 1991. ILLC. Universiteit van Amsterdam, 483-491.
  • –––, 1997. 'Omvangbereik: hoe arbeid wordt verdeeld tussen QR en keuzefuncties'. Taalkunde en filosofie, 20: 335–397.
  • Shirai, K., 1971, 'Intuitionistic predicate calculus with (varepsilon) - symbol', Annals of the Japan Association for Philosophy of Science 4: 49–67.
  • Sieg, W., 1991, 'Herbrand analyses', Archive for Mathematical Logic, 30: 409–441.
  • Slater, BH, 1986, 'E-type voornaamwoorden en (varepsilon) - termen', Canadian Journal of Philosophy, 16: 27–38.
  • –––, 1988, 'Hilbertian reference', Noûs, 22: 283–97.
  • –––, 1994, 'The epsilon calculus' problematic ', Philosophical Papers, 23: 217–42.
  • –––, 2000, 'Quantifier / variable-binding', Linguistics and Philosophy, 23: 309–21.
  • Tait, WW, 1960, 'De vervangingsmethode.' Journal of Symbolische Logica, 30: 175–192.
  • –––, 1965, 'Functionals gedefinieerd door transfinite recursion', Journal of Symbolic Logic, 30: 155–174.
  • –––, 2010. 'De vervangingsmethode opnieuw bekeken.' in: S. Feferman en W. Sieg (red.), Proofs, Categories and Computations: Essays ter ere van Grigori Mints, London: College Publications, pp. 131–14.
  • von Heusinger, K., 1994, Review of Neale (1990). Taalkunde 32: 378–385.
  • –––, 1997. 'Bepaalde beschrijvingen en keuzefuncties'. In: S. Akama (red.). Logica, taal en berekening, Dordrecht: Kluwer, 61–91.
  • –––, 2000, 'The Reference of Indefinites', in von Heusinger en Egli, (2000), 265–284.
  • –––, 2004, 'Keuzefuncties en de anaforische semantiek van bepaalde NP's', Research in Language and Computation, 2: 309–329.
  • von Heusinger, K., Egli, U., (red.), 2000. Referentie en anaforische relaties, Dordrecht: Kluwer.
  • –––, 2000a. 'Inleiding: referentie en de semantiek van Anaphora', in von Heusinger en Egli (2000), 1–13.
  • von Heusinger, K., Kempson, R., (eds.), 2004. Keuzefuncties in semantiek, speciale uitgave van onderzoek naar taal en berekening 2 (3).
  • von Neumann, J., 1927, 'Zur Hilbertschen Beweistheorie', Mathematische Zeitschrift, 26: 1–46.
  • Wang, H., 1963, A Survey of Mathematical Logic, Peking: Science Press.
  • Winter, Y., 1997. 'Keuzefuncties en de scopale semantiek van onbepaalde tijd'. Taalkunde en filosofie, 20: 399–467.
  • Yasuhara, M., 1982, 'Cut elimination in (varepsilon) - calculi', Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28: 311–316.
  • Zach, R., 2003: 'De praktijk van het finitisme. Epsilon-calculus en consistentieproeven in Hilbert's Program ', Synthese, 137: 211–259.
  • –––, 2004. 'Hilbert's “Verunglückter Beweis”, de eerste epsilon-stelling, en consistentieproeven”. Geschiedenis en filosofie van de logica, 25, 79–94.
  • –––, 2017. 'Semantics and proof theory of the epsilon calculus', in: Ghosh, S., Prasad, S. (Eds.), Logic and Its Applications. ICLA 2017, LNCS. Springer, Berlin, Heidelberg, pp. 27–47.

Academische hulpmiddelen

sep man pictogram
sep man pictogram
Hoe deze vermelding te citeren.
sep man pictogram
sep man pictogram
Bekijk een voorbeeld van de PDF-versie van dit item bij de Vrienden van de SEP Society.
inpho icoon
inpho icoon
Zoek dit itemonderwerp op bij het Internet Philosophy Ontology Project (InPhO).
phil papieren pictogram
phil papieren pictogram
Verbeterde bibliografie voor dit item op PhilPapers, met links naar de database.

Andere internetbronnen

Epsilon Calculi door B. Hartley Slater (Internet Encyclopedia of Philosophy)

Neem contact op met de auteurs voor verdere suggesties.