Rachunek Epsilon

Spisu treści:

Rachunek Epsilon
Rachunek Epsilon

Wideo: Rachunek Epsilon

Wideo: Rachunek Epsilon
Wideo: Весь курс мат. анализа. Часть 1. Теория пределов 2024, Marzec
Anonim

Nawigacja wejścia

  • Treść wpisu
  • Bibliografia
  • Narzędzia akademickie
  • Podgląd PDF znajomych
  • Informacje o autorze i cytacie
  • Powrót do góry

Rachunek epsilon

Po raz pierwszy opublikowano pt. 3 maja 2002; zmiana merytoryczna Poniedziałek 6 maja 2019 r

Rachunek epsilon jest logicznym formalizmem opracowanym przez Davida Hilberta w służbie jego programu z podstaw matematyki. Operator epsilon jest operatorem tworzącym termin, który zastępuje kwantyfikatory w zwykłej logice predykatów. W szczególności w rachunku różniczkowym termin (varepsilon x A) oznacza pewne (x) spełniające (A (x)), jeśli takie istnieje. W programie Hilberta terminy epsilon odgrywają rolę elementów idealnych; Celem dowodów o skończonej spójności Hilberta jest przedstawienie procedury, która usuwa takie terminy z formalnego dowodu. Procedury, według których ma to być przeprowadzone, oparte są na metodzie podstawienia epsilon Hilberta. Jednak rachunek epsilon ma również zastosowanie w innych kontekstach. Pierwsze ogólne zastosowanie rachunku epsilon było w twierdzeniach Hilberta o epsilonie,które z kolei stanowią podstawę pierwszego poprawnego dowodu twierdzenia Herbranda. Niedawno warianty operatora epsilon zostały zastosowane w językoznawstwie i filozofii językowej do radzenia sobie z zaimkami anaforycznymi.

  • 1. Przegląd
  • 2. Rachunek epsilon
  • 3. Twierdzenia epsilona
  • 4. Twierdzenie Herbranda
  • 5. Metoda podstawiania epsilonów i arytmetyka
  • 6. Nowsze wydarzenia
  • 7. Operatory epsilon w językoznawstwie, filozofii i logice nieklasycznej
  • Bibliografia
  • Narzędzia akademickie
  • Inne zasoby internetowe
  • Powiązane wpisy

1. Przegląd

Na przełomie wieków David Hilbert i Henri Poincaré zostali uznani za dwóch najważniejszych matematyków swojego pokolenia. Zakres zainteresowań matematycznych Hilberta był szeroki i obejmował zainteresowanie podstawami matematyki: jego Podstawy geometrii opublikowano w 1899 r., A na liście pytań zadanych na Międzynarodowym Kongresie Matematyków w 1900 r. Trzy dotyczyły wyraźnie fundamentalnych kwestii.

Po opublikowaniu paradoksu Russella, Hilbert wygłosił przemówienie na Trzecim Międzynarodowym Kongresie Matematyków w 1904 roku, gdzie po raz pierwszy naszkicował swój plan dostarczenia rygorystycznych podstaw matematyki poprzez dowody spójności składniowej. Jednak do tematu powrócił na poważnie dopiero w 1917 r., Kiedy pod opieką Paula Bernaysa rozpoczął cykl wykładów z podstaw matematyki. Chociaż Hilbert był pod wrażeniem pracy Russella i Whiteheada w ich Principia Mathematica, doszedł do przekonania, że próba sprowadzenia matematyki do logiki przez logika nie może się powieść, w szczególności ze względu na nielogiczny charakter ich aksjomatu redukowalności. Jednocześnie ocenił intuicjonistyczne odrzucenie prawa wyłączonego środka jako nie do przyjęcia dla matematyki. W związku z tym,Aby przeciwdziałać obawom wynikającym z odkrycia paradoksów logicznych i teorii mnogości, potrzebne było nowe podejście, aby uzasadnić nowoczesne metody matematyczne.

Do lata 1920 roku Hilbert sformułował takie podejście. Po pierwsze, nowoczesne metody matematyczne miały być reprezentowane w formalnych systemach dedukcyjnych. Po drugie, te systemy formalne miały zostać udowodnione pod względem składniowym, nie poprzez pokazanie modelu lub zredukowanie ich spójności do innego systemu, ale poprzez bezpośredni argument metatematyczny o wyraźnym, „finitarnym” charakterze. Podejście to stało się znane jako program Hilberta. Rachunek epsilon miał dostarczyć pierwszego składnika tego programu, podczas gdy jego metoda podstawienia epsilon miała zapewnić drugi.

Rachunek epsilon jest, w swojej najbardziej podstawowej formie, rozszerzeniem logiki predykatów pierwszego rzędu z „operacją epsilon”, która wybiera, dla każdej prawdziwej egzystencjalnej formuły, świadka egzystencjalnego kwantyfikatora. Rozszerzenie jest konserwatywne w tym sensie, że nie dodaje żadnych nowych konsekwencji pierwszego rzędu. Ale, odwrotnie, kwantyfikatory można zdefiniować w kategoriach epsilonów, więc logikę pierwszego rzędu można rozumieć w kategoriach rozumowania bez kwantyfikatorów, obejmującego operację epsilon. To właśnie ta ostatnia cecha sprawia, że rachunek różniczkowy jest wygodny w celu udowodnienia spójności. Odpowiednie rozszerzenia rachunku epsilon umożliwiają osadzenie silniejszych, ilościowych teorii liczb i zbiorów w obliczeniach wolnych od kwantyfikatorów. Hilbert spodziewał się, że możliwe będzie wykazanie spójności takich rozszerzeń.

2. Rachunek epsilon

W swoim wykładzie w Hamburgu w 1921 (1922) Hilbert po raz pierwszy przedstawił ideę wykorzystania funkcji wyboru do zajęcia się zasadą wykluczonego środka w formalnym systemie arytmetyki. Idee te zostały rozwinięte w rachunek epsilon i metodę substytucji epsilon w serii wykładów w latach 1921-1923 oraz w Hilbercie (1923). Ostatnią prezentację rachunku epsilon można znaleźć w rozprawie Wilhelma Ackermanna (1924).

Ta sekcja opisuje wersję rachunku różniczkowego odpowiadającą logice pierwszego rzędu, natomiast rozszerzenia do arytmetyki pierwszego i drugiego rzędu zostaną opisane poniżej.

Niech (L) będzie językiem pierwszego rzędu, czyli listą symboli stałych, funkcji i relacji z określonymi liczbami. Zbiór terminów epsilon i zbiór formuł (L) są zdefiniowane indukcyjnie jednocześnie w następujący sposób:

  • Każda stała (L) jest wyrazem.
  • Każda zmienna jest terminem.
  • Jeśli (s) i (t) są terminami, to (s = t) jest formułą.
  • Jeśli (s_1, / ldots, s_k) są terminami, a (F) to (k) - symbol funkcji ary (L, F (s_1, / ldots, s_k)) jest terminem.
  • Jeśli (s_1, / ldots, s_k) to wyrazy, a (R) to (k) - ary symbol relacji (L, R (s_1, / ldots, s_k)) to formuła.
  • Jeśli (A) i (B) są formułami, tak samo jak (A / wedge B, A / vee B, A / rightarrow B) i (neg A).
  • Jeśli (A) jest formułą, a (x) jest zmienną, (varepsilon x A) jest terminem.

Podstawienie i pojęcia zmiennej wolnej i związanej są zdefiniowane w zwykły sposób; w szczególności zmienna (x) zostaje związana w wyrazie (varepsilon x A). Zamierzona interpretacja jest taka, że (varepsilon x A) oznacza pewne (x) spełniające (A), jeśli istnieje. Zatem terminami epsilon rządzi następujący aksjomat („aksjomat pozaskończony” Hilberta): [A (x) rightarrow A (varepsilon x A)) Ponadto rachunek epsilon zawiera kompletny zestaw aksjomatów rządzących klasyczne łączniki zdań i aksjomaty rządzące symbolem równości. Jedyne zasady rachunku różniczkowego są następujące:

  • Modus ponens
  • Podstawienie: z (A (x)), zakończ (A (t)), dla dowolnego terminu (t.)

Wcześniejsze formy rachunku epsilon (takie jak przedstawiony u Hilberta 1923) używają podwójnej postaci operatora epsilon, w której (varepsilon x A) zwraca wartość falsyfikującą (A (x)). Powyższa wersja została wykorzystana w rozprawie Ackermanna (1924) i stała się standardem.

Zwróć uwagę, że właśnie opisany rachunek nie zawiera kwantyfikatorów. Kwantyfikatory można zdefiniować w następujący sposób: (begin {align} exist x A (x) & / equiv A (varepsilon x A) / \ forall x A (x) & / equiv A (varepsilon x (neg A)) end {align}) Można z nich wyprowadzić zwykłe aksjomaty i reguły kwantyfikatorów, więc powyższe definicje służą do osadzenia logiki pierwszego rzędu w rachunku epsilon. Odwrotność jest jednak nieprawdą: nie każda formuła w rachunku epsilon jest obrazem zwykłej formuły ilościowej w ramach tego osadzenia. W związku z tym rachunek epsilon jest bardziej wyrazisty niż rachunek predykatów, po prostu dlatego, że terminy epsilon można łączyć w bardziej złożony sposób niż kwantyfikatory.

Warto zauważyć, że terminy epsilon są niedeterministyczne, co stanowi formę aksjomatu wyboru. Na przykład w języku ze stałymi symbolami (a) i (b) (varepsilon x (x = a / vee x = b)) to (a) lub (b), ale rachunek różniczkowy pozostawia całkowicie otwarte pytanie, który przypadek ma miejsce. Do rachunku różniczkowego można dodać schemat rozszerzalności, (forall x (A (x) leftrightarrow B (x)) rightarrow / varepsilon x A = / varepsilon x B), który stwierdza, że operator epsilon przypisuje to samo świadek do równoważnych formuł (A) i (B). Jednak w przypadku wielu aplikacji ten dodatkowy schemat nie jest konieczny.

3. Twierdzenia epsilona

Drugi tom Hilberta i Bernaysa Grundlagen der Mathematik (1939) zawiera opis wyników rachunku epsilon, które zostały udowodnione do tego czasu. Obejmuje to omówienie pierwszego i drugiego twierdzenia epsilon z zastosowaniami do logiki pierwszego rzędu, metody podstawienia epsilon dla arytmetyki z indukcją otwartą oraz rozwinięcie analizy (czyli arytmetyki drugiego rzędu) za pomocą rachunku epsilon.

Pierwsze i drugie twierdzenia epsilon są następujące:

Pierwsze twierdzenie epsilon: Załóżmy, że (Gamma / cup {A }) jest zbiorem formuł pozbawionych kwantyfikatorów, które nie obejmują symbolu epsilon. Jeśli (A) można wyprowadzić z (Gamma) w rachunku epsilon, to (A) można wyprowadzić z (Gamma) w logice predykatów bez kwantyfikatorów.

Drugie twierdzenie epsilon: Załóżmy, że (Gamma / cup {A }) jest zbiorem formuł nie obejmujących symbolu epsilon. Jeśli (A) można wyprowadzić z (Gamma) w rachunku epsilon, to (A) można wyprowadzić z (Gamma) w logice predykatów.

W pierwszym twierdzeniu epsilon „logika predykatów pozbawiona kwantyfikatorów” ma obejmować powyższą regułę podstawiania, więc aksjomaty bez kwantyfikatorów zachowują się jak ich uniwersalne domknięcia. Ponieważ rachunek epsilon zawiera logikę pierwszego rzędu, pierwsze twierdzenie epsilon implikuje, że można ostatecznie uniknąć wszelkich objazdów przez logikę predykatów pierwszego rzędu używaną do wyprowadzenia twierdzenia wolnego od kwantyfikatorów z aksjomatów wolnych od kwantyfikatorów. Drugie twierdzenie Epsilon pokazuje, że można również uniknąć wszelkich objazdów przez rachunek różniczkowy epsilon używany do wyprowadzenia twierdzenia w języku rachunku predykatów z aksjomatów w języku rachunku predykatów.

Mówiąc bardziej ogólnie, pierwsze twierdzenie epsilon ustala, że kwantyfikatory i epsilony można zawsze wyeliminować z dowodu wzoru wolnego od kwantyfikatorów z innych wzorów bez kwantyfikatorów. Ma to szczególne znaczenie dla programu Hilberta, ponieważ epsilony odgrywają rolę elementów idealnych w matematyce. Jeśli formuły pozbawione kwantyfikatorów odpowiadają „rzeczywistej” części teorii matematycznej, to pierwsze twierdzenie epsilon pokazuje, że elementy idealne można wyeliminować z dowodów rzeczywistych twierdzeń, pod warunkiem, że aksjomaty są również twierdzeniami rzeczywistymi.

Idea ta jest sprecyzowana w pewnym ogólnym twierdzeniu o zgodności, które Hilbert i Bernays wyprowadzają z pierwszego twierdzenia epsilon, które mówi, co następuje: Niech (F) będzie dowolnym systemem formalnym, który wynika z rachunku predykatów przez dodanie stałej, funkcji i symbole predykatów oraz prawdziwe aksjomaty, które są wolne od kwantyfikatorów i epsilonów i zakładają, że prawdziwość formuł atomowych w nowym języku jest rozstrzygalna. Wtedy (F) jest spójne w tym silnym sensie, że każda dająca się wyprowadzić formuła bez kwantyfikatorów i epsilonów jest prawdziwa. Hilbert i Bernays używają tego twierdzenia, aby dać ostateczny dowód zgodności elementarnej geometrii (1939, sekcja 1.4).

Trudność w dostarczaniu dowodów zgodności dla arytmetyki i analizy polega na rozszerzeniu tego wyniku na przypadki, w których aksjomaty zawierają również elementy idealne, tj. Wyrażenia epsilon.

Dalsza lektura. Oryginalne źródła dotyczące rachunku epsilon i twierdzeń epsilon (Ackermann 1924, Hilbert & Bernays 1939) pozostają dostępne tylko w języku niemieckim. Leisenring 1969 jest stosunkowo nowoczesnym, książkowym wprowadzeniem do rachunku epsilon w języku angielskim. Pierwsze i drugie twierdzenie epsilon zostały szczegółowo opisane w Zach 2017. Moser i Zach 2006 podają szczegółową analizę przypadku bez równości. Oryginalne dowody podano dla aksjomatycznych prezentacji rachunku epsilon. Maehara 1955 jako pierwszy rozważał rachunek różniczkowy z terminami epsilon. Pokazał, jak udowodnić drugie twierdzenie epsilon za pomocą eliminacji przecięcia, a następnie wzmocnił twierdzenie, aby uwzględnić schemat ekstensjonalności (Maehara 1957). Baaz i in. 2018 podają ulepszoną wersję pierwszego twierdzenia epsilon. Poprawki błędów w literaturze (w tym w książce Leisenringa) można znaleźć w Flannagan 1975; Ferrari 1987; i Yasuhara 1982. Odmiana rachunku epsilon oparta na funkcjach Skolema, a zatem zgodna z logiką pierwszego rzędu, została omówiona w Davis i Fechter 1991.

4. Twierdzenie Herbranda

Hilbert i Bernays wykorzystali metody rachunku epsilon do ustalenia twierdzeń o logice pierwszego rzędu, które nie odnoszą się do samego rachunku epsilon. Jednym z takich przykładów jest twierdzenie Herbranda (Herbrand 1930; patrz Buss 1995, Girard 1982 i sekcja 2.5 Buss 1998). Jest to często formułowane jako stwierdzenie, że jeśli formuła egzystencjalna (istnieje x_1 / ldots / istnieje x_k A (x_1, / ldots, x_k)) jest wyprowadzalna w logice predykatów pierwszego rzędu (bez równości), gdzie (A) nie zawiera kwantyfikatorów, to istnieją sekwencje terminów (t_ {1} ^ 1, / ldots, t_ {k} ^ 1, / ldots, t_ {1} ^ n, / ldots, t_k ^ n), takie, że [A (t_ {1} ^ 1, / ldots, t_k ^ 1) vee / ldots / vee A (t_ {1} ^ n, / ldots, t_k ^ n)) jest tautologią. Jeśli ktoś ma do czynienia z logiką pierwszego rzędu z równością,trzeba zastąpić „tautologię” „tautologiczną konsekwencją podstawienia przypadków aksjomatów równości”; będziemy używać terminu „quasi-tautologia” do opisania takiej formuły.

Wersja właśnie opisanego twierdzenia Herbranda wynika bezpośrednio z rozszerzonego pierwszego twierdzenia Epsilona Hilberta i Bernaysa. Korzystając z metod związanych z dowodem drugiego twierdzenia epsilon, Hilbert i Bernays uzyskali jednak silniejszy wynik, który, podobnie jak oryginalne sformułowanie Herbranda, dostarcza więcej informacji. Aby zrozumieć dwie części poniższego twierdzenia, warto rozważyć konkretny przykład. Niech (A) będzie wzorem

(istnieje x_1 / forall x_2 / istnieje x_3 / forall x_4 B (x_1, x_2, x_3, x_4)) gdzie (B) nie zawiera kwantyfikatorów. Negacja (A) jest równoważna (forall x_1 / istnieje x_2 / forall x_3 / istnieje x_4 / neg B (x_1, x_2, x _3, x_4).) Skolemizując, czyli używając symboli funkcji jako świadków egzystencjalnych kwantyfikatorów, otrzymujemy (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)).) Przyjmując negację tego, widzimy, że pierwotna formuła jest „równoważna” z (forall f_2, f_4 / istnieje x_1, x_3 B (x_1, f_2 (x_1), x_3, f_4 (x_1, x_3)).)

Pierwsza klauzula poniższego twierdzenia, w tym konkretnym przypadku, mówi, że powyższy wzór (A) jest wyprowadzalny w logice pierwszego rzędu wtedy i tylko wtedy, gdy istnieje ciąg terminów (t_ {1} ^ 1, t_ {3} ^ 1, / ldots, t_ {1} ^ n, t_ {3} ^ n) w rozszerzonym języku z (f_2) i (f_4) takimi, że [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))) jest quasi-tautologią.

Druga klauzula poniższego twierdzenia, w tym konkretnym przypadku, mówi, że powyższy wzór (A) jest wyprowadzalny w logice pierwszego rzędu wtedy i tylko wtedy, gdy istnieją sekwencje zmiennych (x_ {2} ^ 1, x_ { 4} ^ 1, / ldots, x_2 ^ n, x_4 ^ n) i terminy (s_ {1} ^ 1, s_ {3} ^ 1, / ldots, s_1 ^ n, s_3 ^ n) w oryginale język taki, że [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)) jest quasi-tautologią i taką, że (A) można wyprowadzić z tego wzoru przy użyciu jedynie kwantyfikatora i reguł idempotencji opisanych poniżej.

Bardziej ogólnie, załóżmy, że (A) to dowolna formuła przedrostka, w postaci (mathbf {Q} _1 x_1 / ldots / mathbf {Q} _n x_n B (x_1, / ldots, x_n),) gdzie (B) nie zawiera kwantyfikatorów. Wtedy mówi się, że (B) jest macierzą (A), a wystąpienie (B) uzyskuje się przez podstawienie terminów w języku (B) dla niektórych jej zmiennych. Normalną postać Herbranda (A ^ H) z (A) uzyskuje się przez

  • usunięcie każdego uniwersalnego kwantyfikatora i
  • zastąpienie każdej zmiennej ilościowej ujętej powszechnie (x_i) przez (f_i (x_ {i} ^ 1, / ldots, x_ {i} ^ {k (i)})), gdzie (x_ {i} ^ 1, / ldots, x_ {i} ^ {k (i)}) to zmienne odpowiadające egzystencjalnym kwantyfikatorom poprzedzającym (mathbf {Q} _i) w (A) (w kolejności) i (f_i) to nowy symbol funkcji przeznaczony dla tej roli.

Kiedy odnosimy się do wystąpienia macierzy (A ^ H), mamy na myśli wzór otrzymany przez podstawienie wyrażeń w języku rozwiniętym do macierzy (A ^ H). Możemy teraz podać sformułowanie Hilberta i Bernaysa

Twierdzenie Herbranda. (1) Formuła przedrostka (A) jest wyprowadzalna w rachunku predykatów wtedy i tylko wtedy, gdy istnieje dysjunkcja wystąpień macierzy (A ^ H), która jest quasi-tautologią.

(2) Formuła przedrostka (A) jest wyprowadzalna w rachunku predykatów wtedy i tylko wtedy, gdy istnieje dysjunkcja (bigvee_j B_j) wystąpień macierzy (A), tak że (bigvee_j B_j) jest quasi-tautologią, a (A) można wyprowadzić z (bigvee_j B_j), stosując następujące zasady:

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

    conclude (C_1 / vee / ldots / vee / exist x C_i (x) vee / ldots / vee C_m) i

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

    conclude (C_1 / vee / ldots / vee / forall xC_i (x) vee / ldots / vee C_m) (jeśli (x) nie w (C_j) dla (j / ne i)),

jak również idempotencja (vee) (z (C / vee C / vee D) conclude (C / vee D)).

Twierdzenie Herbranda można również uzyskać, stosując eliminację cięć, za pomocą „twierdzenia o środkowej sekwencji” Gentzena. Jednak dowód wykorzystujący drugie twierdzenie epsilon wyróżnia się tym, że jest pierwszym kompletnym i poprawnym dowodem twierdzenia Herbranda. Co więcej, i rzadko jest to rozpoznawane, podczas gdy dowód oparty na eliminacji cięcia zapewnia ograniczenie długości dysjunkcji Herbranda tylko w funkcji rangi cięcia i złożoności formuł ciętych w dowodzie, długość uzyskana z dowodu oparty na rachunku epsilon zapewnia ograniczenie jako funkcję liczby zastosowań aksjomatu pozaskończonego oraz rangi i stopnia występujących w nim terminów epsilon. Innymi słowy, długość dysjunkcji Herbranda zależy tylko od ilościowej złożoności zaangażowanych podstawień i np.wcale nie chodzi o strukturę zdania lub długość dowodu.

Wersja twierdzenia Herbranda podana na początku tej sekcji jest zasadniczo szczególnym przypadkiem (2), w którym formuła (A) jest egzystencjalna. W świetle tego szczególnego przypadku (1) jest równoważne stwierdzeniu, że formuła (A) jest wyprowadzalna w logice predykatów pierwszego rzędu wtedy i tylko wtedy, gdy (A ^ H) jest. Dalszy kierunek tej równoważności jest znacznie łatwiejszy do udowodnienia; w rzeczywistości dla dowolnej formuły (A, A / rightarrow A ^ H) można wyprowadzić w logice predykatów. Udowodnienie odwrotnego kierunku wymaga wyeliminowania dodatkowych symboli funkcji w (A ^ H) i jest znacznie trudniejsze, szczególnie w przypadku równości. To tutaj metody epsilon odgrywają kluczową rolę.

Biorąc pod uwagę formułę przedrostkową, normalna postać Skolema (A ^ S) jest podwójnie definiowana jako (A ^ H), tj. Poprzez zastąpienie egzystencjalnie ujętych ilościowo zmiennych funkcjami obserwującymi. Jeśli (Gamma) jest zbiorem zdań poprzedzających, niech (Gamma ^ S) oznacza zbiór ich normalnych form Skolema. Korzystając z twierdzenia o dedukcji i twierdzenia Herbranda, nietrudno wykazać, że poniższe są równoważne parom: (begin {align} Gamma & / text {proves} A \\ / Gamma & / text {proves} A ^ H \\ / Gamma ^ S & / text {proves} A \\ / Gamma ^ S & / text {proves} A ^ H / end {align})

Uderzające zastosowanie twierdzenia Herbranda i powiązanych metod znajduje się w analizie twierdzenia Rotha Luckhardta (1989). Omówienie przydatnych rozszerzeń metod Herbranda, patrz Sieg 1991. Teoretyczna wersja tego modelu jest omówiona w Avigad 2002a.

5. Metoda podstawiania epsilonów i arytmetyka

Jak wspomniano powyżej, z historycznego punktu widzenia głównym przedmiotem zainteresowania rachunkiem epsilon był sposób uzyskiwania dowodów zgodności. Już w wykładach Hilberta z lat 1917–1918 zauważono, że można łatwo udowodnić spójność logiki zdań, przyjmując zmienne i formuły zdaniowe w zakresie powyżej wartości prawdziwości 0 i 1 oraz interpretując łączniki logiczne jako odpowiadające im operacje arytmetyczne. Podobnie, można dowieść spójności logiki predykatów (lub czystego rachunku epsilon), specjalizując się w interpretacjach, w których wszechświat dyskursu ma jeden element. Te rozważania sugerują następujący, bardziej ogólny program potwierdzania spójności:

  • Rozszerz rachunek epsilon w taki sposób, aby przedstawić większe fragmenty matematyki.
  • Pokaż, używając metod finitarnych, że każdy dowód w rozszerzonym systemie ma spójną interpretację.

Na przykład weźmy pod uwagę język arytmetyki z symbolami (0), (1), (+), (times), (lt). Wraz z aksjomatami bez kwantyfikatorów definiującymi podstawowe symbole, można określić, że terminy epsilon (varepsilon x A (x)) wybierają najmniejszą wartość spełniającą (A), jeśli istnieje, z następującym aksjomatem: (tag {*} A (x) rightarrow A (varepsilon x A (x)) wedge / varepsilon x A (x) le x) Wynikiem jest system, który jest wystarczająco silny, aby zinterpretować jako pierwszy -order (Peano) arytmetyka. Alternatywnie, można przyjąć symbol epsilon, aby spełnić następujący aksjomat: [A (y) rightarrow A (varepsilon x A (x)) wedge / varepsilon x A (x) ne y + 1.)

Innymi słowy, jeśli istnieje świadek (y) spełniający (A (y)), termin epsilon zwraca wartość, której poprzednik nie ma tej samej właściwości. Oczywiście termin epsilon opisany przez (*) spełnia alternatywny aksjomat; odwrotnie, można sprawdzić, czy przy danym (A) wartość (varepsilon x (exist z / le x A (x))) spełniająca alternatywny aksjomat może być użyta do interpretacji (varepsilon x A (x)) w (*). Można dalej ustalić znaczenie terminu epsilon za pomocą aksjomatu (varepsilon x A (x) ne 0 / rightarrow A (varepsilon x A (x))), który wymaga, aby jeśli nie ma świadka (A), termin epsilon zwraca 0. Jednak w poniższej dyskusji najwygodniej jest skupić się wyłącznie na (*).

Załóżmy, że chcemy pokazać, że powyższy system jest spójny; innymi słowy, chcemy pokazać, że nie ma dowodu na wzór (0 = 1). Przesuwając wszystkie podstawienia do aksjomatów i zastępując wolne zmienne stałą 0, wystarczy wykazać, że nie ma zdaniowego dowodu (0 = 1) ze skończonego zbioru zamkniętych wystąpień aksjomatów. W tym celu wystarczy pokazać, że mając skończony zbiór zamkniętych wystąpień aksjomatów, można przypisać wartości liczbowe terminom w taki sposób, że wszystkie aksjomaty są prawdziwe w interpretacji. Ponieważ operacje arytmetyczne (+) i (times) można interpretować w zwykły sposób, jedyną trudnością jest znalezienie odpowiednich wartości do przypisania do terminów epsilon.

Metodę podstawienia epsilon Hilberta można z grubsza opisać następująco:

  • Mając skończony zbiór aksjomatów, zacznij od interpretacji wszystkich terminów epsilon jako 0.
  • Znajdź przykład aksjomatu (*) powyżej, który jest fałszywy w interpretacji. Może się to zdarzyć tylko wtedy, gdy wyraz t jest taki, że (A (t)) jest prawdziwe w interpretacji, ale albo (A (varepsilon x A (x))) jest fałszywe, albo wartość (t) jest mniejsza niż wartość (varepsilon x A (x)).
  • „Napraw” przypisanie, przypisując do (varepsilon x A (x)) wartość (t) i powtórz proces.

Dowód ostatecznej spójności uzyskuje się, gdy zostanie wykazane w ostatecznie możliwy do zaakceptowania sposób, że proces kolejnych „napraw” dobiegł końca. Jeśli tak, wszystkie krytyczne formuły są prawdziwymi formułami bez terminów epsilon.

Ta podstawowa idea („Hilbertsche Ansatz”) została po raz pierwszy przedstawiona przez Hilberta w przemówieniu z 1922 r. (1923) i rozwinięta na wykładach w latach 1922–23. Podane tam przykłady dotyczą jednak tylko dowodów, w których wszystkie wystąpienia aksjomatu pozaskończonego odpowiadają pojedynczemu terminowi epsilon (varepsilon x A (x)). Wyzwaniem było rozszerzenie podejścia na więcej niż jeden człon epsilon, na zagnieżdżone terminy epsilon, a ostatecznie na epsilony drugiego rzędu (w celu uzyskania dowodu spójności nie tylko w zakresie arytmetyki, ale także analizy).

Trudność w radzeniu sobie z zagnieżdżonymi terminami epsilon można opisać w następujący sposób. Załóżmy, że jednym z aksjomatów w dowodzie jest aksjomat pozaskończony [B (y) rightarrow B (varepsilon y B (y))) (varepsilon y B (y)) może oczywiście wystąpić w inne wzory w dowodzie, w szczególności w innych aksjomatach pozaskończonych, np. [A (x, / varepsilon y B (y)) rightarrow A (varepsilon x A (x, / varepsilon y B (y)), / varepsilon y B (y))) Więc najpierw wydaje się konieczne znalezienie prawidłowej interpretacji dla (varepsilon y B (y)), zanim spróbujemy znaleźć jedną dla (varepsilon x A (x, / varepsilon y B (y))). Istnieją jednak bardziej skomplikowane wzorce, w których terminy epsilon mogą występować w dowodzie. Przykładem aksjomatu, który odgrywa rolę w określaniu prawidłowej interpretacji dla (varepsilon y B (y)) może być [B (varepsilon x A (x,\ varepsilon y B (y))) rightarrow B (varepsilon y B (y))) Jeśli (B) (0) jest fałszem, to w pierwszej rundzie procedury (varepsilon y B (y)) będzie interpretowane przez 0. Późniejsza zmiana interpretacji (varepsilon x A (x, 0)) z 0 na, powiedzmy, (n), spowoduje interpretację tego wystąpienia as (B (n) rightarrow B) (0), co będzie fałszywe, jeśli (B (n)) jest prawdą. Zatem interpretacja (varepsilon y B (y)) będzie musiała zostać skorygowana do (n), co z kolei może skutkować interpretacją (varepsilon x A (x, / varepsilon y B (y))) nie będzie już prawdziwą formułą.spowoduje interpretację tego wystąpienia jako (B (n) rightarrow B) (0), co będzie fałszywe, jeśli (B (n)) jest prawdziwe. Zatem interpretacja (varepsilon y B (y)) będzie musiała zostać skorygowana do (n), co z kolei może skutkować interpretacją (varepsilon x A (x, / varepsilon y B (y))) nie będzie już prawdziwą formułą.spowoduje interpretację tego wystąpienia jako (B (n) rightarrow B) (0), co będzie fałszywe, jeśli (B (n)) jest prawdziwe. Zatem interpretacja (varepsilon y B (y)) będzie musiała zostać skorygowana do (n), co z kolei może skutkować interpretacją (varepsilon x A (x, / varepsilon y B (y))) nie będzie już prawdziwą formułą.

To tylko szkic trudności związanych z rozszerzeniem idei Hilberta na przypadek ogólny. Ackermann (1924) dokonał takiego uogólnienia stosując procedurę, która „cofa się”, ilekroć nowa interpretacja na danym etapie pociąga za sobą konieczność skorygowania interpretacji znalezionej już na poprzednim etapie.

Procedura Ackermanna dotyczyła systemu arytmetyki drugiego rzędu, w którym jednak wyrażenia drugiego rzędu zostały ograniczone, aby wykluczyć wiązanie krzyżowe epsilonów drugiego rzędu. Sprowadza się to z grubsza do ograniczenia do rozumienia arytmetycznego jako dostępnej zasady tworzenia zbiorów (patrz dyskusja na końcu tej sekcji). Pojawiły się dalsze trudności z terminami epsilon drugiego rzędu i szybko stało się jasne, że dowód w obecnej postaci był błędny. Jednak nikt w szkole Hilberta nie zdawał sobie sprawy z rozmiarów trudności aż do 1930 roku, kiedy Gödel ogłosił swoje wyniki niekompletności. Do tej pory uważano, że dowód (przynajmniej z pewnymi modyfikacjami wprowadzonymi przez Ackermanna,niektóre z nich dotyczyły pomysłów z wersji metody podstawienia epsilon von Neumanna (1927)), które przejdą przynajmniej w części pierwszego rzędu. Hilbert i Bernays (1939) sugerują, że zastosowane metody zapewniają dowód spójności jedynie dla arytmetyki pierwszego rzędu z indukcją otwartą. W 1936 roku Gerhard Gentzen zdołał wykazać spójność arytmetyki pierwszego rzędu w sformułowaniu opartym na logice predykatów bez symbolu epsilon. Ten dowód używa indukcji pozaskończonej do (varepsilon_0). Ackermann (1940) był później w stanie zaadaptować idee Gentzena, aby dać poprawny dowód spójności arytmetyki pierwszego rzędu przy użyciu metody podstawiania epsilon. Gerhardowi Gentzenowi udało się udowodnić spójność arytmetyki pierwszego rzędu w sformułowaniu opartym na logice predykatów bez symbolu epsilon. Ten dowód używa indukcji pozaskończonej do (varepsilon_0). Ackermann (1940) był później w stanie zaadaptować idee Gentzena, aby dać poprawny dowód spójności arytmetyki pierwszego rzędu przy użyciu metody podstawiania epsilon. Gerhardowi Gentzenowi udało się udowodnić spójność arytmetyki pierwszego rzędu w sformułowaniu opartym na logice predykatów bez symbolu epsilon. Ten dowód używa indukcji pozaskończonej do (varepsilon_0). Ackermann (1940) był później w stanie zaadaptować idee Gentzena, aby dać poprawny dowód spójności arytmetyki pierwszego rzędu przy użyciu metody podstawiania epsilon.

Mimo że próby Ackermanna w celu udowodnienia spójności dla arytmetyki drugiego rzędu zakończyły się niepowodzeniem, zapewniły one jaśniejsze zrozumienie stosowania terminów epsilon drugiego rzędu w formalizacji matematyki. Ackermann użył terminów epsilon drugiego rzędu (varepsilon f / A (f)), gdzie (f) jest zmienną funkcji. Analogicznie do przypadku pierwszego rzędu, (varepsilon f / A (f)) jest funkcją, dla której (A (f)) jest prawdziwe, np. (Varepsilon f (x + f (x) = 2x)) to funkcja tożsamości (f (x) = x). Ponownie, analogicznie do przypadku pierwszego rzędu, do interpretacji kwantyfikatorów drugiego rzędu można używać epsilonów drugiego rzędu. W szczególności dla dowolnej formuły drugiego rzędu (A (x)) można znaleźć wyraz (t (x)) taki, że [A (x) leftrightarrow t (x) = 1) jest wyprowadzalne w rachunku różniczkowym (wzór (A) może mieć inne wolne zmienne,w takim przypadku pojawiają się one również w wyrazie (t)). Fakt ten można następnie wykorzystać do interpretacji zasad rozumienia. W języku z symbolami funkcyjnymi przyjmują one postać (exist f / forall x (A (x) leftrightarrow f (x) = 1)) dla dowolnej formuły (A (x)). Zrozumienie jest częściej wyrażane w postaci zbioru zmiennych, w którym to przypadku przyjmuje postać (istnieje Y / forall x (A (x) leftrightarrow x / in Y),) twierdząc, że co drugi wzór z parametrami, definiuje zestaw.w takim przypadku przyjmuje postać (istnieje Y / forall x (A (x) leftrightarrow x / in Y),) twierdząc, że co drugi wzór rzędu, z parametrami, definiuje zbiór.w takim przypadku przyjmuje postać (istnieje Y / forall x (A (x) leftrightarrow x / in Y),) twierdząc, że co drugi wzór rzędu, z parametrami, definiuje zbiór.

Analiza lub arytmetyka drugiego rzędu jest rozszerzeniem arytmetyki pierwszego rzędu ze schematem rozumienia dla dowolnych formuł drugiego rzędu. Teoria jest nieredukowana, ponieważ pozwala zdefiniować zbiory liczb naturalnych za pomocą kwantyfikatorów, które obejmują cały wszechświat zbiorów, w tym, w sposób dorozumiany, definiowany zbiór. Fragmenty predykatywne tej teorii można uzyskać, ograniczając typ formuł dozwolonych w aksjomacie rozumienia. Na przykład ograniczenie omówione powyżej w związku z Ackermannem odpowiada schematowi rozumienia arytmetycznego, w którym wzory nie obejmują kwantyfikatorów drugiego rzędu. Istnieją różne sposoby uzyskania mocniejszych fragmentów analizy, które są jednak predykcyjnie uzasadnione. Na przykład, można uzyskać analizę rozgałęzioną, łącząc rangę porządkową z ustawionymi zmiennymi;z grubsza, w definicji zbioru o danej randze kwantyfikatory obejmują jedynie zbiory o niższej randze, tj. takie, których definicje są logicznie wcześniejsze.

Dalsze czytanie. Wczesne dowody Hilberta i Ackermanna są omówione w Zach 2003; 2004. Dowód von Neumanna jest tematem Bellotti 2016. Dowód Ackermanna z 1940 r. Omówiono w Hilbert & Bernays 1970 i Wang 1963. Nowoczesną prezentację podaje Moser 2006. Wczesnym zastosowaniem podstawienia epsilon jest interpretacja bez kontrprzykładu (Kreisel 1951).

6. Nowsze wydarzenia

W tej sekcji omówimy rozwój metody zastępowania epsilon w celu uzyskania spójności wyników dla silnych systemów; wyniki te mają charakter matematyczny. Nie możemy niestety omawiać tutaj szczegółów dowodów, ale chcielibyśmy wskazać, że metoda zastępowania epsilon nie zginęła wraz z programem Hilberta, a znaczna część obecnych badań jest przeprowadzana w formalizmach epsilon.

Dowody spójności Gentzena dla arytmetyki zapoczątkowały dziedzinę badań znaną jako analiza porządkowa, a program pomiaru siły teorii matematycznych przy użyciu notacji porządkowej jest nadal realizowany. Jest to szczególnie istotne w przypadku rozszerzonego programu Hilberta, którego celem jest uzasadnienie matematyki klasycznej w odniesieniu do systemów konstruktywnych lub quasi-konstruktywnych. Metody eliminacji cięcia przez Gentzena (i rozszerzenia logiki nieskończonej opracowanej przez Paula Lorentzena, Petra Novikova i Kurta Schütte) w dużej mierze wyparły w tych dążeniach metody substytucji epsilon. Ale metody rachunku epsilon zapewniają alternatywne podejście i nadal trwają aktywne badania nad sposobami rozszerzenia metod Hilberta-Ackermanna na silniejsze teorie. Ogólny wzór pozostaje ten sam:

  1. Osadź badaną teorię w odpowiednim rachunku epsilon.
  2. Opisz proces aktualizacji przydziałów do warunków epsilon.
  3. Pokaż, że procedura normalizuje, tj. Przy danym zestawie terminów istnieje sekwencja aktualizacji, która skutkuje przypisaniem, które spełnia aksjomaty.

Ponieważ ostatni krok gwarantuje spójność oryginalnej teorii, z fundamentalnego punktu widzenia interesują nas metody dowodzenia normalizacji. Na przykład, można uzyskać analizę porządkową, przypisując notacje porządkowe do kroków procedury w taki sposób, że wartość notacji maleje z każdym krokiem.

W latach sześćdziesiątych Tait (1960, 1965, 2010) rozszerzył metody Ackermanna w celu uzyskania porządkowej analizy rozszerzeń arytmetyki o zasady indukcji pozaskończonej. Bardziej usprawnione i nowoczesne wersje tego podejścia można znaleźć w Mints 2001 i Avigad 2002b. Niedawno Mints, Tupailo i Buchholz rozważali silniejsze, ale wciąż predykcyjnie uzasadnione fragmenty analizy, w tym teorie rozumienia arytmetycznego i (Delta ^ {1} _1) - regułę rozumienia (Mints, Tupailo & Buchholz 1996; Mints & Tupailo 1999; patrz także Mints 2016). Arai 2002 rozszerzył metodę podstawiania epsilon na teorie, które pozwalają iterować rozumienie arytmetyczne wzdłuż prymitywnych rekurencyjnych porządków studni. W szczególności,jego praca dostarcza analizy porządkowe dla predykatywnych fragmentów analizy obejmującej hierarchie pozaskończone i indukcję pozaskończoną.

Podjęto pewne pierwsze kroki w stosowaniu metody substytucji epsilon w analizie teorii impredykatywnych (patrz Arai 2003, 2006 i Mints 2015).

Odmiana kroku 3 powyżej polega na pokazaniu, że procedura normalizacji nie jest wrażliwa na wybór aktualizacji, co oznacza, że każda sekwencja aktualizacji kończy się. Nazywa się to silną normalizacją. Mints 1996 pokazał, że wiele z rozważanych procedur ma tę silniejszą właściwość.

Oprócz tradycyjnej, fundamentalnej gałęzi teorii dowodu, obecnie istnieje duże zainteresowanie teorią dowodu strukturalnego, gałęzią przedmiotu, która koncentruje się na logicznych rachunkach dedukcyjnych i ich właściwościach. Badania te są ściśle powiązane z zagadnieniami związanymi z informatyką, związanymi z automatyczną dedukcją, programowaniem funkcjonalnym i weryfikacją wspomaganą komputerowo. Tutaj również dominują metody w stylu Gentzena (zobacz ponownie wpis dotyczący teorii dowodu). Ale rachunek epsilon może również dostarczyć cennych informacji; por. na przykład Aguilera & Baaz 2019, czy omówienie powyższego twierdzenia Herbranda.

Oprócz badań rachunku epsilon w teorii dowodu, należy wspomnieć o dwóch zastosowaniach. Jednym z nich jest użycie notacji epsilon w Theorie des ensembles Bourbaki (1958). Drugim, być może obecnie bardziej interesującym, jest użycie operatora epsilon w systemach dowodzenia twierdzeń HOL i Isabelle, gdzie siła wyrazowa terminów epsilon daje znaczące korzyści praktyczne.

7. Operatory epsilon w językoznawstwie, filozofii i logice nieklasycznej

Czytanie operatora epsilon jako operatora wyboru nieokreślonego („an (x) takiego, że (A (x))”) sugeruje, że może to być przydatne narzędzie w analizie fraz rzeczownikowych nieokreślonych i określonych w semantyce formalnej. W rzeczywistości zastosowano w ten sposób notację epsilon i ta aplikacja okazała się przydatna w szczególności w przypadku odniesień anaforycznych.

Rozważmy znany przykład

Każdy rolnik, który posiada osła, bije go

Powszechnie przyjętą analizę tego zdania podaje zdanie uniwersalne

(forall x / forall y (mathrm {Farmer} (x) wedge / mathrm {Osioł} (y) wedge / mathrm {Właściciele} (x, y)) rightarrow / mathrm {Beats} (x, y)))

Wadą jest to, że „osioł” sugeruje egzystencjalny kwantyfikator, a zatem analiza powinna być w jakiś sposób równoległa do analizy zdania 3 podanego przez 4:

  1. Każdy rolnik, który posiada osła, jest szczęśliwy,
  2. (forall x (mathrm {Farmer} (x) wedge / exist y (mathrm {Osioł} (y) wedge / mathrm {Właściciele} (x, y)) rightarrow / mathrm {Szczęśliwy} (x))),

ale najbliższa możliwa formalizacja,

(forall x ((mathrm {Farmer} (x) wedge / exist y (mathrm {Donkey} (y) wedge / mathrm {Właściciele} (x, y)) rightarrow / mathrm {Beats} (x, y)))

zawiera dowolne wystąpienie (y). Evans 1980 sugeruje, że skoro zaimki odnoszą się do wyrażeń, należy je analizować jako opisy określone; a jeśli zaimek występuje w następniku warunku, warunki opisowe są określane przez poprzednik. Prowadzi to do następującej analizy typu E (1): (begin {multline *} forall x ((mathrm {Farmer} (x) wedge / exist y (mathrm {Donkey} (y)) wedge / mathrm {Właściciele} (x, y)) rightarrow \(mathrm {Beats} (x, / iota y (mathrm {Osioł} (y) wedge / mathrm {Właściciele} (x, y))) end {multline *}) Tutaj (iota x) jest określonym operatorem opisu, więc (iota y (mathrm {Donkey} (y) wedge / mathrm {Właściciele} (x, y))) to „osioł, którego właścicielem jest (x);”. Problem polega na tym, że w analizie standardowej opis określony zawiera warunek niepowtarzalności,i tak (5) będzie fałszywe, jeśli jest rolnik, który posiada więcej niż jednego osła. Wyjściem z tego jest wprowadzenie nowego operatora, whe (ktokolwiek, cokolwiek), który działa jako uogólniający kwantyfikator (Neale, 1990): (begin {multline *} forall x ((mathrm {Farmer} (x) wedge / exist y (mathrm {Osioł} (y) wedge / mathrm {Właściciele} (x, y)) rightarrow \(mathrm {Beats} (x, / mathrm {whe}, y (mathrm {Osioł} (y) wedge / mathrm {Właściciele} (x, y))) end {multline *})

Jak zauważył von Heusinger (1994), sugeruje to, że Neale jest zaangażowany w zaimki, które są niejednoznaczne między opisami określonymi ((iota) - wyrażeniami) a wyrażeniami whe. Heusinger sugeruje zamiast tego użycie operatorów epsilon indeksowanych przez funkcje wyboru (które zależą od kontekstu). Zgodnie z tym podejściem analiza (1) jest

Dla każdego wyboru funkcja (i): (begin {multline *} forall x ((mathrm {Farmer} (x) wedge / mathrm {Właściciele} (x, / varepsilon_i y / mathrm {Osioł} (y)) rightarrow \\\ mathrm {Beats} (x, / varepsilon_ {a ^ *} y / mathrm {Donkey} (y)) end {multline *})

Tutaj (a ^ *) jest funkcją wyboru, która zależy od (i) i poprzednika warunku: Jeśli (i) jest funkcją wyboru, która wybiera (varepsilon_i y / mathrm {Donkey} (y)) ze zbioru wszystkich osłów, a następnie (varepsilon_ {a ^ *} y / mathrm {Donkey} (y)) wybiera ze zbioru osłów należących do (x).

Takie podejście do postępowania z zaimkami za pomocą operatorów epsilon indeksowanych przez funkcje wyboru umożliwia von Heusingerowi radzenie sobie w wielu różnych okolicznościach (patrz Egli i von Heusinger, 1995; von Heusinger, 2000).

Zastosowania operatora epsilon w semantyce formalnej i ogólnie funkcje wyboru spotkały się w ostatnich latach z dużym zainteresowaniem. Von Heusinger i Egli (2000a) wymieniają między innymi: reprezentacje pytań (Reinhart, 1992), konkretne nieokreślone (Reinhart 1992; 1997; Zima 1997), zaimki typu E (Hintikka i Kulas 1985; Slater 1986; Chierchia 1992, Egli i von Heusinger 1995) oraz wyrażenia rzeczownikowe określone (von Heusinger 1997, 2004).

Omówienie zagadnień i zastosowań operatora epsilon w językoznawstwie i filozofii języka można znaleźć w artykule BH Slatera na temat rachunków epsilon (cytowany w sekcji Inne zasoby internetowe poniżej) oraz w zbiorach von Heusinger i Egli 2000 oraz von Heusinger i Kempson 2004.

Innym zastosowaniem rachunku epsilon jest ogólna logika wnioskowania o dowolnych obiektach. Meyer Viol (1995a) przedstawia porównanie rachunku epsilon z teorią dowolnych obiektów Fine'a (1985). Rzeczywiście, połączenie nie jest trudne do zauważenia. Biorąc pod uwagę równoważność (forall x A (x) equiv) A ((varepsilon x (neg A))), termin (varepsilon x (neg A)) jest dowolnym obiektem w tym sensie, że jest to przedmiot, którego (A) jest prawdziwe, jeśli (A) jest ogólnie prawdziwe.

Meyer Viol (1995a, 1995b) zawierają dalsze badania dowodowe i teoretyczne modelowania rachunku epsilon; szczególnie intuicjonistyczne rachunki epsilon. Tutaj twierdzenia epsilon już nie obowiązują, tj. Wprowadzenie terminów epsilon prowadzi do niekonserwatywnych rozszerzeń logiki intuicjonistycznej. Inne badania operatorów epsilon w logice intuicjonistycznej można znaleźć u Shirai (1971), Bell (1993a, 1993b) i DeVidi (1995). Dla operatorów epsilon w logikach wielowartościowych, patrz Mostowski (1963), dla modalnego rachunku epsilon, Fitting (1975).

Dalsze czytanie. Poniżej znajduje się lista niektórych publikacji z zakresu języka i lingwistyki mających znaczenie dla rachunku epsilon i jego zastosowań. Czytelnik jest kierowany w szczególności do zbiorów von Heusinger & Egli (red.) 2000 oraz von Heusinger & Kempson (red.) 2004 do dalszej dyskusji i odniesień: Bell 1993a, 1993b; Chierchia 1992; DeVidi 1995; Egli & von Heusinger 1995; Fine 1985; Dopasowanie 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; i zima 1997.

Bibliografia

  • Aguilera, JP, Baaz, M., 2019, „Wnioski Unsound sprawiają, że dowody są krótsze”. Journal of Symbolic Logic 84: 102–122.
  • Ackermann, W., 1924, „Begründung des” „tertium non datur” „mittels der 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, „Metoda substytucji Epsilon dla teorii hierarchii skoków”, Archive for Mathematical Logic, 2: 123–153.
  • –––, 2003, 'Epsilon substitution method for ID (_ 1 (Pi ^ {0} _1 / vee / Sigma ^ {0} _1))', Annals of Pure and Applied Logic, 121: 163–208.
  • –––, 2006, 'Metoda podstawienia epsilon dla (Pi ^ {0} _2) - NAPRAW. Journal of Symbolic Logic 71: 1155–1188
  • Avigad, J., 2002a, „Nasycone modele teorii uniwersalnych”, Annals of Pure and Applied Logic, 118: 219–234.
  • –––, 2002b, „Aktualizuj procedury i 1-spójność arytmetyki”, Mathematical Logic Quarterly, 48: 3–13.
  • Baaz, M., Leitsch, A., Lolic, A., 2018, 'A sequent-calcus based formulation of the extended first epsilon theorem', w: Artemov, S., Nerode, A. (red.), Logical Foundations Informatyki, Berlin: Springer, 55–71.
  • Bell, JL, 1993a. „Hilbert's epsilon operator and classical logic”, Journal of Philosophical Logic, 22: 1–18.
  • –––, 1993b. „Operator epsilon Hilberta w intuicjonistycznych teoriach typów”, Mathematical Logic Quarterly, 39: 323–337.
  • Bellotti, L., 2016, „Von Neumann's consency proof”, Review of Symbolic Logic, 9: 429–455.
  • Bourbaki, N., 1958, Theorie des ensembles, Paryż: Hermann.
  • Buss, S., 1995, „On Herbrand's theorem”, Logic and Computational Complexity (Lecture Notes in Computer Science 960), Berlin: Springer, 195–209.
  • ––– 1998, „Wprowadzenie do teorii dowodu”, w: Buss (red.), The Handbook of Proof Theory, Amsterdam: North-Holland, 1–78.
  • Chierchia, G., 1992. „Anafora i logika dynamiczna”. Linguistics and Philosophy, 15: 111–183.
  • Davis, M. i R. Fechter, 1991, „Wolna zmienna wersja rachunku predykatów pierwszego rzędu”, Journal of Logic and Computation, 1: 431–451.
  • DeVidi, D., 1995. „Intuitionistic (varepsilon) - and (tau) - rachunki”, Mathematical Logic Quarterly 41: 523–546.
  • Egli, U., von Heusinger, K., 1995, „Operator epsilon i zaimki typu E”, w: U. Egli et al. (red.), Lexical Knowledge in the Organization of Language, Amsterdam: Benjamins, 121–141 (Current Issues in Linguistic Theory 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, tom. 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. Reasoning with Arbitrary Objects, Oxford: Blackwell.
  • Fitting, M., 1975. „A modal logic epsilon-calcus”, Notre Dame Journal of Formal Logic, 16: 1–16.
  • Flannagan, TB, 1975, „On an extension of Hilbert's second (varepsilon) - theorem”, Journal of Symbolic Logic, 40: 393–397.
  • Girard, J.-Y., 1982, „Herbrand's theorem and dowód teoria”, 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. Tłumaczenie angielskie w Herbrand 1971, s. 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, angielskie tłumaczenie w Mancosu, 1998, 198–214 i Ewald, 1996, 1115–1134.
  • –––, 1923, „Die logischen Grundlagen der Mathematik”, Mathematische Annalen, 88: 151–165, tłumaczenie angielskie w Ewald, 1996, 1134–1148.
  • Hilbert, D., Bernays, P., 1934, Grundlagen der Mathematik, Vol. 1, Berlin: Springer.
  • –––, 1939, Grundlagen der Mathematik, t. 2, Berlin: Springer.
  • –––, 1970, „Grundlagen der Mathematik”, t. 2, 2, wydanie, Berlin: Springer, Suplement V.
  • Hintikka, J., Kulas, J., 1985. Anaphora and Definite Descriptions: Two Applications of Game-Theoretical Semantics, Dordrecht: Reidel.
  • Kempson, R., Meyer Viol, W., and Gabbay, D., 2001. Dynamic Syntax: The Flow of Language Understanding, Oxford: Blackwell.
  • Kreisel, G, 1951, „O interpretacji dowodów niefinitistycznych - część I”, Journal of Symbolic Logic, 16: 241–267.
  • Leisenring, AC, 1969, Mathematical Logic and Hilbert's Epsilon-Symbol, Londyn: 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 calculator with (varepsilon) - symbol”, Journal of the Mathematical Society of Japan, 7: 323–344.
  • –––, 1957, „Aksjomat równości na symbolu Hilberta (varepsilon) -”, Journal of the Faculty of Science, University of Tokyo, Section 1, 7: 419–435.
  • Mancosu, P. (red.), 1998, From Brouwer to Hilbert. Debata o podstawach matematyki w latach dwudziestych XX wieku, Oxford: Oxford University Press.
  • Meyer Viol, WPM, 1995a, Instantial Logic. Badanie dotyczące rozumowania za pomocą instancji, Ph. D. praca magisterska, Uniwersytet w Utrechcie. ILLC Dissertation Series 1995–11.
  • –––, 1995b. „A proof-theoretic treatment of assignment”, Biuletyn IGPL, 3: 223–243.
  • Mints, G., 1994, „Gentzen-type systems and Hilbert's epsilon substitution method. I ', Logic, Methodology and Philosophy of Science, IX (Uppsala, 1991), Amsterdam: North-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”, w: W. Sieg et al. (red.), Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, Association for Symbolic Logic.
  • –––, 2008, „Eliminacja cięcia dla prostego sformułowania rachunku epsilon”, Annals of Pure and Applied Logic, 152 (1–3): 148–160.
  • –––, 2013. „Zastępowanie epsilon dla logiki predykatów pierwszego i drugiego rzędu”, Annals of Pure and Applied Logic, 164: 733–739.
  • –––, 2015. „Non-deterministic epsilon substitution method for PA and ID (_ 1)”, w: Kahle, R., Rathjen, M. (red.), Gentzen's Centenary: The Quest for Consistency. Berlin: Springer, s. 479–500.
  • Mints, G., Tupailo, S., 1999, „Epsilon-substitution method for the ramified language and (Delta ^ {1} _1) - compension rule”, w: A. Cantini et al. (red.), Logic and Foundations of Mathematics (Florencja, 1995), Dordrecht: Kluwer, 107–130.
  • Mints, G., Tupailo, S., Buchholz, W., 1996, „Epsilon substitution method for elementary analysis”, Archive for Mathematical Logic, 35: 103–130.
  • Moser, G., 2006, „Ackermann's substitution method (remiksed)”, Annals of Pure and Applied Logic, 142 (1–3): 1–18.
  • Moser, G. i R. Zach, 2006, „The epsilon calcus and Herbrand complexity”, Studia Logica, 82 (1): 133–155.
  • Mostowski, A., 1963. „Funkcja Hilberta epsilon w logikach wielowartościowych”, Acta Philosophica Fennica, 16: 169–188.
  • Neale, S., 1990, Opisy, Cambridge, MA: MIT Press.
  • Reinhart, T., 1992. „Wh-in-situ: pozorny paradoks”. W: P. Dekker i M. Stokhof (red.). Materiały z VIII Kolokwium w Amsterdamie, 17–20 grudnia 1991 r. ILLC. University of Amsterdam, 483–491.
  • –––, 1997. „Zakres kwantyfikatora: podział pracy między funkcje QR i wyboru”. Linguistics and Philosophy, 20: 335–397.
  • Shirai, K., 1971, „Intuitionistic predicate calcus with (varepsilon) - symbol”, Annals of the Japan Association for Philosophy of Science 4: 49–67.
  • Sieg, W., 1991, „Herbrand analysis”, Archive for Mathematical Logic, 30: 409–441.
  • Slater, BH, 1986, „Zaimki typu E i (varepsilon) - terminy”, Canadian Journal of Philosophy, 16: 27–38.
  • –––, 1988, „Hilbertian reference”, Noûs, 22: 283–97.
  • –––, 1994, „The epsilon calcus 'problematic”, Philosophical Papers, 23: 217–42.
  • –––, 2000, „Quantifier / variable-binding”, Linguistics and Philosophy, 23: 309–21.
  • Tait, WW, 1960, „Metoda substytucji”. Journal of Symbolic Logic, 30: 175–192.
  • –––, 1965, „Funkcjonały zdefiniowane przez rekurencję pozaskończoną”, Journal of Symbolic Logic, 30: 155–174.
  • –––, 2010. „The substitution method revisited”. w: S. Feferman i W. Sieg (red.), Proofs, Categories and Computations: Essays in Honor of Grigori Mints, London: College Publications, str. 131–14.
  • von Heusinger, K., 1994, Review of Neale (1990). Linguistics 32: 378–385.
  • –––, 1997. „Określone opisy i funkcje wyboru”. W: S. Akama (red.). Logic, Language and Computation, Dordrecht: Kluwer, 61–91.
  • –––, 2000, „The Reference of Indefinites”, w: von Heusinger i Egli, (2000), 265–284.
  • –––, 2004, „Funkcje wyboru i anaforyczna semantyka określonych NP”, Research in Language and Computation, 2: 309–329.
  • von Heusinger, K., Egli, U., (red.), 2000. Referencje i stosunki anaforyczne, Dordrecht: Kluwer.
  • –––, 2000a. „Wprowadzenie: odniesienie i semantyka Anafory”, w: von Heusinger i Egli (2000), 1–13.
  • von Heusinger, K., Kempson, R., (red.), 2004. Choice Functions in Semantics, Special Issue of Research on Language and Computation 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. „Funkcje wyboru i semantyka zakresu nieokreśloności”. Linguistics and Philosophy, 20: 399–467.
  • Yasuhara M., 1982, „Cut elimination in (varepsilon) - calci”, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28: 311–316.
  • Zach, R., 2003, „Praktyka finityzmu. Rachunek epsilona i dowody spójności w Programie Hilberta, Synthese, 137: 211–259.
  • –––, 2004. „Hilbert's„ Verunglückter Beweis”, pierwsze twierdzenie epsilon i dowody zgodności”. Historia i filozofia logiki, 25, 79–94.
  • –––, 2017. „Semantyka i teoria dowodu rachunku epsilon”, w: Ghosh, S., Prasad, S. (red.), Logic and Its Applications. ICLA 2017, LNCS. Springer, Berlin, Heidelberg, s. 27–47.

Narzędzia akademickie

człowiek ikona
człowiek ikona
Jak cytować ten wpis.
człowiek ikona
człowiek ikona
Zobacz wersję PDF tego wpisu w Friends of the SEP Society.
ikona Inpho
ikona Inpho
Poszukaj tego tematu wpisu w Internet Philosophy Ontology Project (InPhO).
ikona dokumentów phil
ikona dokumentów phil
Ulepszona bibliografia tego wpisu na PhilPapers, z linkami do jego bazy danych.

Inne zasoby internetowe

Epsilon Calculi autorstwa B. Hartley Slater (Internetowa Encyklopedia Filozofii)

Prosimy o kontakt z autorami w celu uzyskania dalszych sugestii.

Zalecane: