Semantyka Dowodowo-teoretyczna

Spisu treści:

Semantyka Dowodowo-teoretyczna
Semantyka Dowodowo-teoretyczna

Wideo: Semantyka Dowodowo-teoretyczna

Wideo: Semantyka Dowodowo-teoretyczna
Wideo: 12b: Rozdział 2, Wprowadzenie do semantyki językoznawczej - Renata Grzegorczykowa 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

Semantyka dowodowo-teoretyczna

Pierwsza publikacja: środa, 5 grudnia 2012; rewizja merytoryczna Czw 1.02.2018

Semantyka dowodowo-teoretyczna jest alternatywą dla semantyki warunkowej. Opiera się ona na fundamentalnym założeniu, że głównym pojęciem, w jakim sens przypisuje się pewnym wyrażeniom naszego języka, w szczególności stałym logicznym, jest raczej dowód niż prawda. W tym sensie semantyka teorii dowodu jest semantyką w kategoriach dowodu. Semantyka dowodowo-teoretyczna oznacza również semantykę dowodów, tj. Semantykę bytów, która opisuje, jak dochodzimy do pewnych twierdzeń przy określonych założeniach. Obydwa aspekty semantyki teorii dowodu mogą się przeplatać, tj. Sama semantyka dowodów jest często podawana w kategoriach dowodów.

Semantyka dowodowo-teoretyczna ma kilka korzeni, z których najbardziej specyficznym są uwagi Gentzena, że reguły wprowadzające w jego rachunku dedukcji naturalnej definiują znaczenie stałych logicznych, podczas gdy w konsekwencji tej definicji można uzyskać reguły eliminacji (patrz sekcja 2.2.1). 1). Mówiąc szerzej, należy do tego, co Prawitz nazwał ogólną teorią dowodu (patrz sekcja 1.1). Mówiąc jeszcze szerzej, jest częścią tradycji, zgodnie z którą znaczenie terminu powinno być wyjaśniane poprzez odniesienie do sposobu jego użycia w naszym języku.

W filozofii semantyka teorii dowodu znajdowała się głównie pod hasłem „teoria znaczenia”. Ta terminologia podąża za Dummettem, który twierdził, że teoria znaczenia jest podstawą filozofii teoretycznej, pogląd, który przypisał Frege. Termin „semantyka teorii dowodu” został zaproponowany przez Schroedera-Heistera (1991; używany już w 1987 na wykładach w Sztokholmie), aby nie pozostawiać terminu „semantyka” wyłącznie denotacjonalizmowi - w końcu „semantyka” jest badania dotyczące znaczenia wyrażeń językowych. Co więcej, w przeciwieństwie do „teorii znaczenia”, termin „semantyka teorii dowodu” obejmuje również aspekty filozoficzne i techniczne. W 1999 roku pierwsza konferencja o tym tytule odbyła się w Tybindze, druga w 2013 roku. Pierwszy podręcznik pod tym tytułem ukazał się w 2015 roku.

  • 1. Tło

    • 1.1 Ogólna teoria dowodu: konsekwencja a dowody
    • 1.2 Inferencjalizm, intuicjonizm, antyrealizm
    • 1.3 Teoria dowodu w stylu Gentzena: redukcja, normalizacja, eliminacja cięć
  • 2. Niektóre wersje semantyki dowodowo-teoretycznej

    • 2.1 Semantyka implikacji: dopuszczalność, pochodna, reguły

      • 2.1.1 Logika operacyjna
      • 2.1.2 Semantyka Gentzena
      • 2.1.3 Odliczenie naturalne z regułami wyższego poziomu
    • 2.2 Semantyka derywacji w oparciu o reguły wprowadzenia

      • 2.2.1 Zasady inwersji i harmonia
      • 2.2.2 Wiarygodność teoretyczna
      • 2.2.3 Konstruktywna teoria typów
    • 2.3 Definicje klauzulowe i rozumowanie definicyjne

      • 2.3.1 Wyzwanie związane z programowaniem logicznym
      • 2.3.2 Refleksja definicji
    • 2.4 Strukturalna charakterystyka stałych logicznych
    • 2.5 Teoria dowodu kategorialnego
  • 3. Rozszerzenia i alternatywy dla standardowej semantyki teorii dowodu

    • 3.1 Zasady eliminacji jako podstawowe
    • 3.2 Negacja i zaprzeczenie
    • 3.3 Harmonia i odbicie w rachunku sekwencyjnym
    • 3.4 Struktura subatomowa i język naturalny
    • 3.5 Logika klasyczna
    • 3.6 Rozumowanie hipotetyczne
    • 3.7 Semantyka międzywymiarowo-teoretyczna
  • 4. Wnioski i perspektywy
  • Bibliografia
  • Narzędzia akademickie
  • Inne zasoby internetowe
  • Powiązane wpisy

Ten wpis obejmuje również następujące dokumenty uzupełniające, które są połączone z tekstem:

  • Przykłady trafności teoretycznej
  • Definicja refleksji i paradoksy

1. Tło

1.1 Ogólna teoria dowodu: konsekwencja a dowody

Termin „ogólna teoria dowodu” został wymyślony przez Prawitza. W ogólnej teorii dowodu „dowody są badane same w sobie w nadziei zrozumienia ich natury”, w przeciwieństwie do „redukcyjnej teorii dowodu” w stylu Hilberta, która jest „próbą przeanalizowania dowodów teorii matematycznych z zamiarem sprowadzając je do bardziej elementarnej części matematyki, takiej jak matematyka finitistyczna lub konstruktywna”(Prawitz, 1972, s. 123). W podobny sposób Kreisel (1971) prosi o przeorientowanie teorii dowodu. Chce wyjaśnić „ostatnie prace w teorii dowodu z zaniedbanego punktu widzenia. Dowody i ich reprezentacje za pomocą formalnych wyprowadzeń są traktowane jako główne przedmioty badań, a nie zwykłe narzędzia do analizy relacji konsekwencji”. (Kreisel, 1971, s.109) Podczas gdy Kreisel koncentruje się na dychotomii między teorią dowodów a teorią udowodnienia, Prawitz koncentruje się na różnych celach, do których może dążyć teoria dowodu. Obaj jednak podkreślają konieczność badania dowodów jako fundamentalnych bytów, za pomocą których zdobywamy wiedzę demonstracyjną (zwłaszcza matematyczną). Oznacza to w szczególności, że dowody są bytami epistemicznymi, których nie należy mylić z dowodami formalnymi lub wyprowadzeniami. Są raczej tym, co oznaczają derywacje, gdy uważa się je za reprezentacje argumentów. (Jednakże poniżej często używamy „dowodu” jako synonimu „derywacji”, pozostawiając czytelnikowi określenie, czy chodzi o formalne dowody lub dowody jako byty epistemiczne). Omawiając badanie Prawitza (1971), Kreisel (1971, s..111) wyraźnie mówi o „mapowaniu” między derywacjami a aktami umysłowymi i uważa, że wyjaśnienie tego odwzorowania, w tym badanie tożsamości dowodów, jest zadaniem teorii dowodu, który Prawitz i Martin-Löf umieścili w porządku obrad.

Oznacza to, że w ogólnej teorii dowodu nie interesuje nas wyłącznie to, czy B wynika z A, ale sposób, w jaki dochodzimy do B, zaczynając od A. W tym sensie ogólna teoria dowodu ma charakter intencjonalny i epistemologiczny, podczas gdy teoria modeli, która interesuje się relacją konsekwencji, a nie sposobem jej ustalania, jest ekstensjonalna i metafizyczna.

1.2 Inferencjalizm, intuicjonizm, antyrealizm

Semantyka dowodowo-teoretyczna jest z natury inferencyjna, ponieważ jest to działanie wnioskowania, które przejawia się w dowodach. Należy zatem do inferencjalizmu (zob. Brandom, 2000), zgodnie z którym wnioskowanie i reguły wnioskowania ustanawiają znaczenie wyrażeń, w przeciwieństwie do denotacjonalizmu, według którego denotacje są podstawowym rodzajem znaczeń. Inferencjalizm i pogląd semantyki „znaczenie jako użycie” to szerokie ramy filozoficzne semantyki opartej na teorii dowodu. Ta ogólna perspektywa filozoficzno-semantyczna połączyła się z konstruktywnymi poglądami wywodzącymi się z filozofii matematyki, zwłaszcza z matematycznego intuicjonizmu. Większość form semantyki opartej na teorii dowodu ma charakter intuicyjny,co oznacza w szczególności, że zasady klasycznej logiki, takie jak prawo wykluczonego środka lub prawo podwójnej negacji, są odrzucane lub przynajmniej uznawane za problematyczne. Wynika to częściowo z faktu, że główne narzędzie semantyki dowodowej, rachunek dedukcji naturalnej, jest nastawiony na logikę intuicjonistyczną w tym sensie, że proste sformułowanie reguł jej eliminacji jest intuicjonistyczne. Tam logika klasyczna jest dostępna tylko za pomocą pewnej reguły dowodu pośredniego, która przynajmniej w pewnym stopniu burzy symetrię zasad rozumowania (patrz sekcja 3.5). Jeśli przyjmiemy stanowisko naturalnej dedukcji, to logika intuicjonistyczna jest naturalnym systemem logicznym. Istotną rolę odgrywa również interpretacja znaków logicznych BHK (Brouwer-Heyting-Kolmogorov). Ta interpretacja nie jest unikalnym podejściem do semantyki, ale zawiera różne pomysły, które są często bardziej nieformalne niż formalnie opisane. Szczególnie ważny jest jego funkcjonalny pogląd na implikację, zgodnie z którym dowód A → B jest funkcją konstruktywną, która zastosowana do dowodu A daje dowód B. Ta funkcjonalna perspektywa leży u podstaw wielu koncepcji semantyki teorii dowodu, w szczególności tych Lorenzena, Prawitza i Martina Löfa (patrz rozdziały 2.1.1, 2.2.2, 2.2.3). Ta funkcjonalna perspektywa leży u podstaw wielu koncepcji semantyki teorii dowodu, w szczególności tych Lorenzena, Prawitza i Martina Löfa (patrz rozdziały 2.1.1, 2.2.2, 2.2.3). Ta funkcjonalna perspektywa leży u podstaw wielu koncepcji semantyki teorii dowodu, w szczególności tych Lorenzena, Prawitza i Martina Löfa (patrz rozdziały 2.1.1, 2.2.2, 2.2.3).

Według Dummetta logiczne stanowisko intuicjonizmu odpowiada filozoficznemu stanowisku antyrealizmu. Realistyczny pogląd na rzeczywistość niezależną od uznania jest metafizycznym odpowiednikiem poglądu, że wszystkie zdania są albo prawdziwe, albo fałszywe, niezależnie od naszych sposobów ich rozpoznania. Idąc za Dummettem, główne części semantyki teorii dowodu są związane z antyrealizmem.

1.3 Teoria dowodu w stylu Gentzena: redukcja, normalizacja, eliminacja cięć

Rachunek dedukcji naturalnej Gentzena i jego interpretacja przez Prawitza stanowi tło większości podejść do semantyki teorii dowodu. Naturalna dedukcja opiera się na co najmniej trzech głównych ideach:

  • Spełnienie założeń: Założenia mogą zostać „zwolnione” lub „wyeliminowane” w trakcie ich wyprowadzania, więc głównym pojęciem dedukcji naturalnej jest derywacja zależna od założeń.
  • Separacja: każdy schemat reguły pierwotnej zawiera tylko jedną stałą logiczną.
  • Wprowadzenia i wykluczenia: Reguły dla stałych logicznych występują w parach. Reguła (-y) wprowadzenia pozwala (-ą) wywnioskować formułę, której głównym operatorem jest dana stała, a reguła (-y) eliminacji (-e) pozwala (-ą) wyciągnąć konsekwencje z takiej formuły.

W systemie naturalnej dedukcji Gentzena dla wyprowadzeń logicznych pierwszego rzędu są zapisywane w formie drzewa i oparte na dobrze znanych regułach. Na przykład implikacja ma następujące zasady wprowadzania i eliminowania

[A]
b → Ja
A → B
A → BA → E.
b

gdzie nawiasy wskazują na możliwość rozładowania wystąpień założenia A. Otwarte założenia wyprowadzenia to te założenia, od których zależy formuła końcowa. Derywacja nazywana jest zamkniętą, jeśli nie ma otwartego założenia, w przeciwnym razie nazywana jest otwartą. Jeśli mamy do czynienia z kwantyfikatorami, musimy również rozważyć otwarte indywidualne zmienne (czasami nazywane „parametrami”). Cechy metalogiczne kluczowe dla semantyki dowodowej i po raz pierwszy systematycznie badane i publikowane przez Prawitza (1965) obejmują:

Redukcja: dla każdego objazdu składającego się z wprowadzenia, po którym bezpośrednio następuje eliminacja, istnieje etap redukcji, który usuwa ten objazd.

Normalizacja: poprzez kolejne stosowanie redukcji, wyprowadzenia można przekształcić w normalne formy, które nie zawierają objazdów.

Dla implikacji, standardowy krok redukcji usuwania objazdów jest następujący:

[A]
b |
A → B ZA
b
zmniejsza się do

|

A

B

Prosty, ale bardzo ważny wniosek normalizacji jest następujący: każde zamknięte wyprowadzenie w logice intuicjonistycznej można zredukować do wyprowadzenia przy użyciu reguły wprowadzenia w ostatnim kroku. Mówimy również, że intuicjonistyczna dedukcja naturalna spełnia „właściwość wprowadzenia formy”. W semantyce teorii dowodu wynik ten figuruje w czołówce pod nagłówkiem „fundamentalne założenie” (Dummett, 1991, s. 254). „Fundamentalne założenie” jest typowym przykładem filozoficznej reinterpretacji wyniku techniczno-teoretycznego.

Dalsze czytanie:

Dla ogólnej orientacji semantyki dowodowo-teoretycznej w specjalnym numerze Synthese (Kahle i Schroeder-Heister, 2006) czytelnik pod redakcją Piechy i Schroeder-Heistera (2016b), podręcznik Franceza (2015), Schroeder-Heister (2008b, 2016a) i Wansing (2000).

Na temat stanowiska filozoficznego i rozwoju teorii dowodu wpisy dotyczące programu Hilberta i rozwoju teorii dowodu oraz Prawitz (1971).

Dla intuicjonizmu pozycje z logiki intuicjonistycznej, intuicjonizmu w filozofii matematyki i rozwoju logiki intuicjonistycznej.

Dla antyrealizmu wpis o wyzwaniach dla realizmu metafizycznego oraz Tennant (1987); Tennant (1997), Tranchini (2010); Tranchini (2012a).

Dla teorii dowodu w stylu Gentzena i teorii dedukcji naturalnej: oprócz oryginalnej prezentacji Gentzena (1934/35) teoria przypuszczeń Jaśkowskiego (1934) i monografia klasyczna Prawitza (1965), Tennant (1978), Troelstra i Schwichtenberg (2000) oraz Negri i von Plato (2001).

2. Niektóre wersje semantyki dowodowo-teoretycznej

2.1 Semantyka implikacji: dopuszczalność, pochodna, reguły

Semantyka implikacji leży u podstaw semantyki teorii dowodu. W przeciwieństwie do klasycznej semantyki warunkowania prawdy, implikacja jest stałą logiczną samą w sobie. Cechuje go również to, że jest powiązany z pojęciem konsekwencji. Można to postrzegać jako wyrażanie konsekwencji na poziomie zdaniowym ze względu na modus ponens i to, co w systemach Hilberta nazywa się twierdzeniem o dedukcji, tj. Równoważność Γ, A ⊢ B i Γ ⊢ A → B.

Bardzo naturalnym rozumieniem implikacji A → B jest odczytanie jej jako wyrażenia reguły wnioskowania, która pozwala przejść od A do B. Licencjonowanie kroku od A do B na podstawie A → B jest dokładnie tym, co mówi modus ponens. A twierdzenie o dedukcji można postrzegać jako sposób na ustalenie reguły: wykazanie, że B można wydedukować z A, uzasadnia regułę, że z A możemy przejść do B. Oparta na regułach semantyka implikacji zgodna z takimi liniami leży u podstaw kilku koncepcji semantyki teorii dowodu, zwłaszcza tych opracowanych przez Lorenzena, von Kutschera i Schroeder-Heistera.

2.1.1 Logika operacyjna

Lorenzen w swoim wstępie do logiki operacyjnej i matematyki (1955) rozpoczyna od rachunków wolnych od logiki (atomowych), które odpowiadają systemom produkcji lub gramatykom. Nazywa regułę dopuszczalną w takim układzie, jeśli można ją do niej dodać bez powiększania zbioru atomów, które można wyprowadzić. Strzałka implikacji → jest interpretowana jako wyrażająca dopuszczalność. Implikacja A → B jest uznawana za ważną, jeśli czytana z reguły jest dopuszczalna (w odniesieniu do rachunku różniczkowego). Dla implikacji iterowanych (= reguł) Lorenzen rozwija teorię twierdzeń o dopuszczalności wyższych poziomów. Pewne stwierdzenia, takie jak A → A lub ((A → B), (B → C)) → (A → C), zachowują się niezależnie od rachunku różniczkowego. Nazywa się je powszechnie dopuszczalnymi [„allgemeinzulässig”]) i stanowią system pozytywnej logiki implikacyjnej. W podobny sposóbprawa dla kwantyfikacji uniwersalnej ∀ są uzasadniane twierdzeniami dopuszczalności dla reguł ze zmiennymi schematycznymi.

W celu uzasadnienia praw dla stałych logicznych ∧, ∨, ∃ i L Lorenzen używa zasady inwersji (termin, który ukuł). W bardzo uproszczonej formie, bez uwzględniania zmiennych w regułach, zasada inwersji mówi, że wszystko, co można uzyskać z każdego warunku definiującego A, można uzyskać z samego A. Na przykład, w przypadku dysjunkcji, niech A i B każdy będzie warunkiem definiującym A ∨ B wyrażonym przez reguły pierwotne A → A ∨ B i B → A ∨ B. Wtedy zasada inwersji mówi, że A ∨ B → C jest dopuszczalne przy założeniu A → C i B → C, co uzasadnia regułę eliminacji dla dysjunkcji. Z pozostałymi łącznikami postępuje się w podobny sposób. W przypadku ⊥ reguła absurdu ⊥ → A wynika z faktu, że nie ma warunku definiującego dla ⊥.

2.1.2 Semantyka Gentzena

W tym, co nazywa „semantyką Gentzena”, von Kutschera (1968) podaje, jako Lorenzen, semantykę logicznie złożonych zdań implikacyjnych A 1,…, A n → B w odniesieniu do rachunków K, które rządzą rozumowaniem zdaniami atomowymi. Podstawową różnicą w stosunku do Lorenzena jest fakt, że A 1,…, A n → B wyraża teraz raczej pochodną niż stwierdzenie dopuszczalności.

Aby przekształcić to w semantykę stałych logicznych logiki zdań, von Kutschera argumentuje w następujący sposób: Rezygnując z biwalencji, nie możemy już stosować klasycznych przypisań wartości prawdy do formuł atomowych. Zamiast tego możemy użyć rachunków, które potwierdzają lub odrzucają zdania atomowe. Co więcej, ponieważ rachunki nie tylko generują dowody lub obalenia, ale także dowolne relacje wyprowadzalności, chodzi o to, aby rozpocząć bezpośrednio od wyprowadzalności w systemie atomowym i rozszerzyć ją o reguły charakteryzujące łączniki logiczne. W tym celu von Kutschera podaje rachunek sekwencyjny z regułami wprowadzania n -arnych połączeń zdaniowych w następnych i poprzednikach, dając sekwencyjny system dla uogólnionych połączeń zdaniowych. Von Kutschera następnie pokazuje, że wszystkie tak zdefiniowane uogólnione łączniki można wyrazić za pomocą standardowych łączników intuicjonistycznej logiki (koniunkcja, dysjunkcja, implikacja, absurd).

2.1.3 Odliczenie naturalne z regułami wyższego poziomu

W ramach programu rozwijania ogólnego schematu reguł dla dowolnych stałych logicznych Schroeder-Heister (1984) zaproponował, że logicznie złożona formuła powinna wyrażać zawartość lub wspólną treść systemów reguł. Oznacza to, że nie zasady wprowadzenia są uważane za podstawowe, ale za konsekwencje zdefiniowania warunków. Reguła R jest albo formułą A, albo ma postać R 1,…, R n ⇒ A, gdzie R 1,…, R nsame są regułami. Te tak zwane „reguły wyższego poziomu” generalizują ideę, że reguły mogą przenosić założenia do przypadku, gdy te założenia same w sobie mogą być regułami. Dla standardowych stałych logicznych oznacza to, że A ∧ B wyraża zawartość pary (A, B); A → B wyraża treść reguły A ⇒ B; A ∨ B wyraża wspólną treść A i B; a absurd ⊥ wyraża wspólną treść pustej rodziny systemów reguł. W przypadku dowolnych n -arnych połączeń zdaniowych prowadzi to do naturalnego systemu dedukcji z uogólnionymi regułami wprowadzania i eliminacji. Okazało się, że te ogólne łączniki są definiowalne w kategoriach standardowych, ustanawiając ekspresyjną kompletność standardowych łączników intuicjonistycznych.

Dalsze czytanie:

Dla podejścia Lorenzena w odniesieniu do semantyki teorii dowodu w stylu Prawitza: Schroeder-Heister (2008a). Za przedłużenie ekspresyjnej kompletności w stylu von Kutschery: Wansing (1993a).

2.2 Semantyka derywacji w oparciu o reguły wprowadzenia

2.2.1 Zasady inwersji i harmonia

W swoich badaniach Investigations into Logical Deduction, Gentzen poczynił pewne, współcześnie bardzo często cytowane, programowe uwagi na temat semantycznego związku między wnioskami wprowadzającymi i eliminującymi w naturalnej dedukcji.

Wprowadzenia stanowią niejako „definicje” danych symboli, a eliminacje nie są w ostatecznym rozrachunku jedynie konsekwencjami tych definicji. Fakt ten można wyrazić następująco: eliminując symbol, możemy posłużyć się formułą, z której symbolem końcowym mamy do czynienia jedynie „w sensie, jaki nadaje mu wprowadzenie tego symbolu”. (Gentzen, 1934/35, s. 80)

Nie może to oczywiście oznaczać, że reguły eliminacji można wyprowadzić z reguł wprowadzających w dosłownym tego słowa znaczeniu; w rzeczywistości tak nie jest. Może to tylko oznaczać, że mogą być przez nich w jakiś sposób uzasadnione.

Uściślając te idee, powinno być możliwe wyświetlenie e-wnioskowania jako unikalnych funkcji odpowiadających im I-wnioskowań, na podstawie określonych wymagań. (tamże, s. 81)

Tak więc idea leżąca u podstaw programu Gentzena polega na tym, że mamy „definicje” w postaci reguł wprowadzających i pewnego rodzaju rozumowania semantycznego, które przy użyciu „pewnych wymagań” potwierdzają reguły eliminacji.

Przyjmując termin Lorenzena i dostosowując jego ideę do kontekstu naturalnej dedukcji, Prawitz (1965) sformułował „zasadę inwersji”, aby sprecyzować uwagi Gentzena:

Niech α będzie zastosowaniem reguły eliminacji, której konsekwencją jest B. Zatem dedukcje, które spełniają warunek wystarczający […] do wyprowadzenia głównej przesłanki α, w połączeniu z dedukcjami pomniejszych przesłanek α (jeśli istnieją), już „zawierają” odliczenie B; zatem odliczenie B można otrzymać bezpośrednio z podanych odliczeń bez dodawania α. (s. 33)

Tutaj warunki wystarczające są określone w przesłankach odpowiednich reguł wprowadzających. Zatem zasada inwersji mówi, że wyprowadzenie konkluzji reguły eliminacji można uzyskać bez zastosowania reguły eliminacji, jeśli jej główne założenie zostało wyprowadzone za pomocą reguły wprowadzenia w ostatnim kroku, co oznacza, że kombinacja

I-wnioskowanie
ZA
{D i } Wnioskowanie elektroniczne
b

kroków, gdzie {D i } oznacza (prawdopodobnie pustą) listę dedukcji pomniejszych przesłanek, można uniknąć.

Relacja między regułami wprowadzenia i eliminacji jest często opisywana jako „harmonia” lub jako rządzona „zasadą harmonii” (patrz np. Tennant, 1978, s. 74). Ta terminologia nie jest jednolita, a czasem nawet nie do końca jasna. Zasadniczo wyraża to, co oznacza również „inwersja”. Nawet jeśli „harmonia” jest terminem sugerującym relację symetryczną, często jest rozumiana jako wyrażająca koncepcję opartą na regułach wstępnych, jak np. W Read (2010) „ogólna harmonia eliminacji” (chociaż czasami zawiera się również koncepcje oparte na eliminacji). Czasami harmonia ma oznaczać, że łączniki są najsilniejsze lub najsłabsze w pewnym sensie, biorąc pod uwagę ich wprowadzenie lub zasady ich eliminacji. Ta idea leży u podstaw zasady harmonii Tennanta (1978),a także charakterystyki strukturalne Poppera i Koslowa (patrz sekcja 2.4). Konkretny związek między regułami wprowadzania i eliminacji sformułowanymi w zasadzie inwersji wyklucza domniemane definicje inferencyjne, takie jak definicja łącznika tonk, która łączy regułę wprowadzającą dla rozłączenia z regułą eliminacji dla koniunkcji i która dała początek wciąż toczącej się debacie na temat formatu definicji wnioskowania (patrz Humberstone, 2010).co dało początek wciąż toczącej się debacie na temat formatu definicji inferencyjnych (patrz Humberstone, 2010).co dało początek wciąż toczącej się debacie na temat formatu definicji inferencyjnych (patrz Humberstone, 2010).

2.2.2 Wiarygodność teoretyczna

Dominującym podejściem do semantyki dowodowo-teoretycznej jest trafność dowodowo-teoretyczna. Jako koncepcja techniczna została opracowana przez Prawitza (1971; 1973; 1974), przekształcając pojęcie trafności teorii dowodu oparte na ideach Taita (1967) i pierwotnie używane do udowodnienia silnej normalizacji w koncepcję semantyczną. Dummett dostarczył wielu filozoficznych podstaw dla tego pojęcia (patrz Dummett, 1991). Przedmioty, które są przede wszystkim poprawne, są dowodami jako reprezentacjami argumentów. W sensie drugorzędnym, pojedyncze reguły mogą być ważne, jeśli prowadzą od ważnych dowodów do ważnych dowodów. W tym sensie ważność jest pojęciem globalnym, a nie lokalnym. Odnosi się to do dowolnych wyprowadzeń w danym układzie atomowym, który definiuje pochodną dla atomów. Nazywając dowód, który wykorzystuje regułę wprowadzenia w ostatnim kroku jako kanoniczny, opiera się na następujących trzech ideach:

  1. Pierwszeństwo zamkniętych dowodów kanonicznych.
  2. Redukcja zamkniętych dowodów niekanonicznych do kanonicznych.
  3. Zastępczy pogląd na otwarte dowody.

Ad 1: Definicja trafności opiera się na koncepcji Gentzena, zgodnie z którą reguły wprowadzające „usprawiedliwiają się” i nadają stałym logicznym znaczenie. Ta cecha samouzasadniająca się jest używana tylko w przypadku zamkniętych odbitek próbnych, które są uważane za podstawowe w stosunku do otwartych.

Ad 2: Niekanoniczne dowody są usprawiedliwione poprzez zredukowanie ich do kanonicznych. Zatem procedury redukcyjne (redukcje objazdów) stosowane w dowodach normalizacyjnych odgrywają kluczową rolę. Ponieważ uzasadniają argumenty, Prawitz nazywa je również „uzasadnieniami”. Ta definicja ponownie ma zastosowanie tylko do zamkniętych dowodów, co odpowiada właściwości postaci wstępnej zamkniętych normalnych wyprowadzeń w naturalnej dedukcji (patrz sekcja 1.3).

Ad 3: Otwarte dowody są uzasadnione, biorąc pod uwagę ich zamknięte wystąpienia. Te zamknięte wystąpienia uzyskuje się przez zastąpienie ich otwartych założeń zamkniętymi dowodami ich istnienia, a ich otwarte zmienne zamkniętymi warunkami. Na przykład dowód B z A jest uważany za ważny, jeśli każdy zamknięty dowód, który uzyskuje się poprzez zastąpienie otwartego założenia A zamkniętym dowodem A, jest ważny. W ten sposób otwarte założenia są uważane za symbole zastępcze dla zamkniętych dowodów, z tego powodu możemy mówić o zastępczej interpretacji otwartych dowodów.

Daje to następującą definicję trafności teorii dowodu:

  1. Każdy zamknięty dowód w podstawowym systemie atomowym jest ważny.
  2. Zamknięty dowód kanoniczny jest uważany za ważny, jeśli jego bezpośrednie potwierdzenia są ważne.
  3. Zamknięty dowód niekanoniczny jest uważany za ważny, jeśli sprowadza się do ważnego zamkniętego dowodu kanonicznego lub do zamkniętego dowodu w systemie atomowym.
  4. Dowód otwarty jest uważany za ważny, jeśli każdy dowód zamknięty uzyskany przez zastąpienie jego otwartych założeń dowodami zamkniętymi, a zmienne otwarte terminami zamkniętymi jest ważny.

Formalnie definicja ta musi być relatywizowana do rozważanego systemu atomowego i rozważanego zbioru uzasadnień (redukcji dowodowych). Ponadto dowody są tutaj rozumiane jako kandydaci na ważne dowody, co oznacza, że reguły, z których są tworzone, nie są ustalone. Wyglądają jak drzewa dowodowe, ale ich poszczególne kroki mogą mieć dowolną (skończoną) liczbę przesłanek i mogą eliminować arbitralne założenia. Definicja ważności wyodrębnia te struktury dowodowe, które są „rzeczywistymi” dowodami na podstawie danych procedur redukcyjnych.

Trafność w odniesieniu do każdego wyboru systemu atomowego można postrzegać jako uogólnione pojęcie logicznej ważności. W rzeczywistości, jeśli weźmiemy pod uwagę standardowe redukcje logiki intuicjonistycznej, to wszystkie wyprowadzenia w logice intuicjonistycznej są ważne niezależnie od rozpatrywanego systemu atomowego. To jest poprawność semantyczna. Możemy zapytać, czy sytuacja odwrotna zachodzi, a mianowicie. czy, zakładając, że wyprowadzenie jest ważne dla każdego systemu atomowego, istnieje odpowiadające mu wyprowadzenie w logice intuicjonistycznej. Ta intuicjonistyczna logika jest kompletna w tym sensie, nazywana hipotezą Prawitza (patrz Prawitz, 1973; Prawitz, 2013). Jednak nie przedstawiono żadnego zadowalającego dowodu na to. Istnieją poważne wątpliwości co do słuszności tego przypuszczenia dla systemów, które wykraczają poza logikę implikacyjną. W każdym razie będzie to zależało od precyzyjnego sformułowania pojęcia ważności, w szczególności od sposobu, w jaki posługuje się układami atomowymi.

Bardziej formalna definicja i szczegółowe przykłady potwierdzające trafność, a także kilka uwag na temat hipotezy Prawitza można znaleźć w

Dodatek dotyczący przykładów trafności teoretycznej.

2.2.3 Konstruktywna teoria typów

Teoria typów Martina-Löfa (Martin-Löf, 1984) jest wiodącym podejściem w konstruktywnej logice i matematyce. Filozoficznie, podziela z Prawitzem trzy fundamentalne założenia standardowej semantyki teorii dowodu, o których mowa w sekcji 2.2.2: priorytet zamkniętych dowodów kanonicznych, redukcja zamkniętych niekanonicznych dowodów do kanonicznych oraz substytucyjny pogląd na otwarte dowody. Jednak teoria typów Martina-Löfa ma co najmniej dwie charakterystyczne cechy, które wykraczają poza inne podejścia w semantyce teorii dowodu:

  1. Rozważanie przedmiotów dowodu i odpowiadające mu rozróżnienie między dowodami jako przedmiotami a dowodami jako dowodami.
  2. Postrzeganie reguł tworzenia jako nieodłącznych elementów systemu dowodowego, a nie reguł zewnętrznych.

Pierwsza idea wywodzi się z korespondencji Curry-Howarda (por. De Groote, 1995; Sørensen i Urzyczyn, 2006), zgodnie z którą fakt, że formuła A ma pewien dowód, można skodyfikować jako fakt, że określony termin t jest typu A, przy czym formuła A jest identyfikowana z typem A. Można to sformalizować w rachunku przypisania typu, którego instrukcje mają postać t: A. Dowód t: A w tym systemie można odczytać jako pokazujący, że t jest dowodem A. Martin-Löf (1995; 1998) ujął to z perspektywy filozoficznej, wyróżniając ten podwójny sens dowodu w następujący sposób. Najpierw mamy dowody twierdzeń postaci t: A. Te stwierdzenia nazywane są sądami, a ich dowody nazywane są demonstracjami. W takich sądach termin t reprezentuje dowód twierdzenia A. Dowód w tym drugim sensie jest również nazywany przedmiotem dowodu. Demontując orzeczenie t: A, pokazujemy, że t jest dowodem (przedmiotem) dla zdania A. W tym dwuwarstwowym systemie warstwa demonstracyjna jest warstwą argumentacji. W przeciwieństwie do obiektów dowodowych, demonstracje mają znaczenie epistemiczne; ich sądy mają moc asertywną. Warstwa dowodowa to warstwa, na której wyjaśnione są znaczenia: znaczenie zdania A wyjaśnia się, mówiąc, co liczy się jako dowód (przedmiot) dla A. Rozróżnienie między dowodami kanonicznymi i niekanonicznymi jest rozróżnieniem na poziomie zdań, a nie na poziomie osądu. Oznacza to pewien wymóg jawności. Kiedy coś udowodnię, muszę mieć do dyspozycji nie tylko uzasadnienie dla mojego dowodu, jak w pojęciu ważności Prawitza,ale jednocześnie trzeba mieć pewność, że to usprawiedliwienie spełnia swoje zadanie. Tę pewność gwarantuje demonstracja. Matematycznie, to podwójne poczucie dowodu rozwija swoją prawdziwą moc tylko wtedy, gdy typy mogą zależeć od terminów. Typy zależne są podstawowym składnikiem teorii typów Martina-Löfa i podejść pokrewnych.

Druga idea sprawia, że podejście Martina-Löfa znacznie różni się od wszystkich innych definicji trafności teorii dowodu. Na przykład zasadnicza różnica w procedurze Prawitza polega na tym, że nie ma ona charakteru metajęzykowego, gdzie „metajęzykowa” oznacza, że najpierw określa się zdania i kandydatów na dowody, a następnie, za pomocą definicji w metajęzyku, ustala się, które są ważne, a które nie. Raczej twierdzenia i dowody wchodzą w grę tylko w kontekście demonstracji. Na przykład, jeśli założymy, że coś jest dowodem implikacji A → B, nie musimy koniecznie pokazywać, że zarówno A, jak i B są wprost dobrze sformułowanymi zdaniami, ale oprócz wiedzy, że A jest zdaniem, potrzebujemy tylko wiedzieć, że B jest twierdzeniem pod warunkiem, że A zostało udowodnione. Bycie zdaniem wyraża się w określonej formie sądu, która jest ustanowiona w tym samym systemie dowodzenia, który służy do stwierdzenia, że dowód zdania został osiągnięty.

W teorii Martina-Löfa semantyka teorii dowodu otrzymuje silnie ontologiczny komponent. Niedawna debata dotyczy tego, czy przedmioty dowodowe mają status czysto ontologiczny, czy też kodyfikują wiedzę, nawet jeśli same nie są aktami epistemicznymi.

Dalsze czytanie:

Zasady inwersji opisano w Schroeder-Heister (2007).

Warianty harmonii dowodowo-teoretycznej patrz Francez (2015) i Schroeder-Heister (2016a). Definicję trafności teorii dowodu Prawitza można znaleźć w Schroeder-Heister (2006).

Aby zapoznać się z teorią typów Matin-Löf, zobacz wpis dotyczący teorii typów oraz Sommaruga (2000).

2.3 Definicje klauzulowe i rozumowanie definicyjne

Semantyka dowodowo-teoretyczna zwykle koncentruje się na stałych logicznych. To skupienie praktycznie nigdy nie jest kwestionowane, najwyraźniej dlatego, że jest uważane za tak oczywiste. W teorii dowodu niewiele uwagi poświęcono układom atomowym, chociaż pojawiły się wczesne prace Lorenzena (patrz sekcja 2.1.1), w których uzasadnienie reguł logicznych jest osadzone w teorii reguł arbitralnych, a Martin-Löf (1971) teoria iterowanych definicji indukcyjnych, w których proponuje się zasady wprowadzania i eliminacji wzorów atomowych. Rozwój programowania logicznego rozszerzył tę perspektywę. Z punktu widzenia teorii dowodu, programowanie logiczne jest teorią rozumowania atomowego w odniesieniu do klauzulalnych definicji atomów. Refleksja definicyjna to podejście do semantyki dowodowej, które podejmuje to wyzwanie i próbuje zbudować teorię, której zakres zastosowania wykracza poza stałe logiczne.

2.3.1 Wyzwanie związane z programowaniem logicznym

W programowaniu logicznym mamy do czynienia z klauzulami programowymi postaci

A ⇐ B 1,…, B m

które definiują formuły atomowe. Takie klauzule można naturalnie interpretować jako opisujące reguły wprowadzania atomów. Z punktu widzenia semantyki dowodowo-teoretycznej istotne są dwa punkty:

(1) Reguły wprowadzenia (klauzule) dla formuł logicznie złożonych nie są zasadniczo rozróżniane od reguł wprowadzenia (klauzul) dla atomów. Interpretacja dowodu programowania logicznego teoretycznie motywuje rozszerzenie semantyki teorii dowodu na dowolne atomy, co daje semantykę o znacznie szerszej dziedzinie zastosowań.

(2) Klauzule programowe niekoniecznie są dobrze uzasadnione. Na przykład nagłówek klauzuli może występować w jej treści. Programy dobrze ugruntowane to tylko szczególny rodzaj programów. Stosowanie klauzul arbitralnych bez dalszych wymagań w programowaniu logicznym jest motywacją do kontynuowania tego samego pomysłu w semantyce dowodowej, dopuszczając wszelkiego rodzaju reguły wprowadzające, a nie tylko te o specjalnej formie, a zwłaszcza niekoniecznie dobrze -założony. To przenosi ideę wolności definicji, która jest kamieniem węgielnym programowania logicznego, do semantyki, ponownie poszerzając sferę zastosowania semantyki teorii dowodu.

Idea traktowania reguł wprowadzenia jako reguł nadających znaczenie atomom jest ściśle związana z teorią definicji indukcyjnych w jej ogólnej postaci, zgodnie z którą definicje indukcyjne są układami reguł (por. Aczel, 1977).

2.3.2 Refleksja definicji

Teoria refleksji definicyjnej (Hallnäs, 1991; Hallnäs, 2006; Hallnäs i Schroeder-Heister, 1990/91; Schroeder-Heister, 1993) podejmuje wyzwanie związane z programowaniem logicznym i przedstawia semantykę teorii dowodu nie tylko dla stałych logicznych, dla dowolnych wyrażeń, dla których można podać definicję klauzuli. Formalnie podejście to zaczyna się od listy klauzul, które są rozważaną definicją. Każda klauzula ma formę

A ⇐ Δ

gdzie głowa A jest wzorem atomowym (atomem). W najprostszym przypadku ciało Δ jest listą atomów B 1,…, B m, w którym to przypadku definicja wygląda jak określony program logiczny. Często rozważamy rozszerzony przypadek, w którym Δ może również zawierać pewną implikację strukturalną „⇒”, a czasami nawet jakąś strukturalną implikację uniwersalną, którą zasadniczo rozwiązuje się poprzez ograniczenie podstawiania. Jeśli definicja A ma postać

to A ma następujące zasady wprowadzenia i eliminacji

Δ 1 · · · Δ n A A

1] n]
ZA do · · · do
do

Zasady wprowadzające, zwane także regułami domknięcia definicji, wyrażają rozumowanie „wzdłuż” klauzul. Reguła eliminacji nazywana jest zasadą refleksji definicyjnej, ponieważ odzwierciedla definicję jako całość. Jeżeli Δ 1,…, Δ nwyczerp wszystkie możliwe warunki do wygenerowania A zgodnie z podaną definicją, a jeśli każdy z tych warunków pociąga za sobą ten sam wniosek C, to samo A pociąga za sobą ten wniosek. Jeśli definicja klauzuli jest postrzegana jako definicja indukcyjna, zasada ta może być postrzegana jako wyrażająca klauzulę ekstremalną w definicjach indukcyjnych: nic poza podanymi klauzulami nie definiuje A. Oczywiście refleksja definicyjna jest uogólnioną formą omawianych zasad inwersji. Rozwija swoją prawdziwą moc w kontekstach definicyjnych z wolnymi zmiennymi, które wykraczają poza rozumowanie czysto zdaniowe, oraz w kontekstach, które nie są dobrze uzasadnione. Przykładem nieuzasadnionej definicji jest definicja atomu R przez jego własną negację:

D R {R | )
D R {R | )

Ten przykład jest szczegółowo omówiony w

Dodatek dotyczący refleksji i paradoksów definicji.

Dalsze czytanie:

Odnośnie braku uzasadnienia i paradoksów, patrz wpisy dotyczące odniesień do samych siebie i paradoksu Russella, a także odniesienia cytowane w dodatku, do którego prowadzi.

2.4 Strukturalna charakterystyka stałych logicznych

Istnieje szerokie pole pomysłów i wyników dotyczących tego, co można by nazwać „strukturalną charakterystyką” stałych logicznych, gdzie „strukturalny” ma tu na myśli zarówno w teoretyczno-dowodowym sensie „reguł strukturalnych”, jak iw sensie ram, które ma pewną strukturę, w której ta struktura jest ponownie opisana teoretycznie. Niektórzy z jej autorów posługują się słownikiem semantycznym i przynajmniej w sposób dorozumiany sugerują, że ich temat należy do semantyki dowodowo-teoretycznej. Inni wprost zaprzeczają tym konotacjom, podkreślając, że interesuje ich charakterystyka, która ustanawia logiczność stałej. Pytanie „Co to jest stała logiczna?” można odpowiedzieć w kategoriach teorii dowodu, nawet jeśli semantyka samych stałych jest uwarunkowana prawdą:Mianowicie wymagając, aby stałe (być może warunkowo zdefiniowane przez prawdę) wykazywały określone zachowanie oparte na wnioskach, które można opisać za pomocą terminów teorii dowodu. Ponieważ jednak niektórzy autorzy traktują ich charakterystykę jednocześnie jako semantykę, należy tutaj wspomnieć o niektórych z tych podejść.

Najbardziej jawnym strukturalistą w odniesieniu do stałych logicznych, który wyraźnie siebie rozumie jako takiego, jest Koslow. W swojej Strukturalistycznej Teorii Logiki (1992) rozwija teorię stałych logicznych, w której charakteryzuje je pewnymi „relacjami implikacji”, gdzie relacja implikacji z grubsza odpowiada relacji konsekwencji skończonej w sensie Tarskiego (którą ponownie można opisać pewne zasady strukturalne systemu sekwencyjnego). Koslow rozwija teorię strukturalną w precyzyjnym sensie metamatematycznym, która nie określa domeny obiektów w żaden sposób poza podanymi aksjomatami. Jeśli podano język lub jakąkolwiek inną domenę obiektów wyposażonych w relację implikacji, podejście strukturalne można zastosować do wyodrębnienia związków logicznych poprzez sprawdzenie ich właściwości implikacyjnych.

W swoich wczesnych pracach na temat podstaw logiki Popper (1947a; 1947b) podaje inferencyjne charakterystyki stałych logicznych w terminach teorii dowodu. Posługuje się rachunkiem ciągów i charakteryzuje stałe logiczne pewnymi warunkami wyprowadzalności takich ciągów. Jego terminologia wyraźnie sugeruje, że zamierza zastosować semantykę teoretyczno-dowodową stałych logicznych, ponieważ mówi o „definicjach wnioskowania” i „trywializacji logiki matematycznej” osiągniętej poprzez definiowanie stałych w opisany sposób. Chociaż jego prezentacja nie jest wolna od pojęciowej nieprecyzyjności i błędów, był pierwszym, który wziął pod uwagę sekwencyjne zachowanie się stałych logicznych w celu ich scharakteryzowania. Jest to tym bardziej niezwykłe, że prawdopodobnie nie był wcale,i na pewno nie w pełni świadomy późniejszego rachunku Gentzena i dalszych osiągnięć Gentzena (choć korespondował z Bernaysem). Jednak wbrew jego opinii, jego dzieło można lepiej rozumieć jako próbę zdefiniowania logiczności stałych i ich strukturalnego scharakteryzowania, niż jako semantykę dowodowo-teoretyczną w sensie autentycznym. Niemniej jednak przewidział wiele idei, które są obecnie powszechne w semantyce teorii dowodu, takich jak charakteryzowanie stałych logicznych za pomocą pewnych warunków minimalności lub maksymalności w odniesieniu do reguł wprowadzania lub eliminacji.niż jako semantyka teorii dowodu w prawdziwym sensie. Niemniej jednak przewidział wiele idei, które są obecnie powszechne w semantyce teorii dowodu, takich jak charakteryzowanie stałych logicznych za pomocą pewnych warunków minimalności lub maksymalności w odniesieniu do reguł wprowadzania lub eliminacji.niż jako semantyka teorii dowodu w prawdziwym sensie. Niemniej jednak przewidział wiele idei, które są obecnie powszechne w semantyce teorii dowodu, takich jak charakteryzowanie stałych logicznych za pomocą pewnych warunków minimalności lub maksymalności w odniesieniu do reguł wprowadzania lub eliminacji.

Ważny wkład w debatę na temat logiki, który charakteryzuje stałe logiczne w kategoriach sekwencyjnych reguł rachunku różniczkowego, wnoszą Kneale (1956) i Hacking (1979). Dogłębne ujęcie logiczności proponuje Došen (1980; 1989) w swojej teorii stałych logicznych jako „znaki interpunkcyjne”, wyrażające cechy strukturalne na poziomie logicznym. Rozumie stałe logiczne jako charakteryzujące się pewnymi podwójnymi regułami dla sekwencji, które można odczytywać w obu kierunkach. Na przykład koniunkcja i dysjunkcja są (w logice klasycznej, z następcami wielokrotnych formuł) charakteryzują się regułami podwójnej linii

Γ⊢ A, Δ Γ⊢ B, Δ
Γ⊢ A ∧ B, Δ
Γ, A ⊢ Δ Γ, B ⊢ Δ
Γ⊢ A ∨ B, Δ

Došen jest w stanie przedstawić charakterystykę obejmującą systemy logiki modalnej. Wyraźnie traktuje swoją pracę jako przyczynek do debaty o logice, a nie do jakiejkolwiek koncepcji semantyki teorii dowodu. Sambin i wsp., W swojej Podstawowej logice (Sambin, Battilotti i Faggian, 2000), wyraźnie rozumieją to, co Došen nazywa regułami podwójnej linii jako podstawowe zasady nadające znaczenie. Reguły podwójnej linii dla koniunkcji i rozłączności są odczytywane jako niejawne definicje tych stałych, które za pomocą jakiejś procedury można przekształcić w jawne reguły w stylu sekwencyjnym, do których jesteśmy przyzwyczajeni. Więc Sambin i in. używają tego samego punktu wyjścia co Došen, ale interpretują go nie jako strukturalny opis zachowania stałych, ale semantycznie jako ich niejawną definicję (patrz Schroeder-Heister, 2013).

Istnieje kilka innych podejść do jednolitej charakterystyki teoretyczno-dowodowej stałych logicznych, z których wszystkie przynajmniej dotykają kwestii semantyki teorii dowodu. Takie teorie to Logika wyświetlania Belnapa (Belnap, 1982), Logika struktur informacji Wansinga (Wansing, 1993b), ogólne systemy edycji dowodów i ich implementacje, takie jak ramy logiczne Edynburga (Harper, Honsell i Plotkin, 1987) oraz wielu następców, pozwalają na specyfikację różnych systemów logicznych. Od czasu powstania logiki liniowej i, bardziej ogólnie, logiki podstrukturalnej (Di Cosmo i Miller, 2010; Restall, 2009), istnieją różne podejścia do logiki, które różnią się pod względem ograniczeń dotyczących ich reguł strukturalnych. Niedawny ruch odchodzący od wyodrębniania określonej logiki jako prawdziwej w kierunku bardziej pluralistycznego stanowiska (zob. Np. Beall i Restall, 2006), która jest zainteresowana tym, co łączy różne logiki bez preferencji dla określonej logiki, może być postrzegana jako odejście od semantycznego uzasadnienia w kierunku strukturalnej charakterystyki.

2.5 Teoria dowodu kategorialnego

Istnieje obszerna literatura na temat teorii kategorii w odniesieniu do teorii dowodu, a po przełomowych pracach Lawvere, Lambek i innych (patrz Lambek i Scott, 1986 oraz zawarte w nich odniesienia), sama kategoria może być postrzegana jako rodzaj abstrakcyjnego dowodu. teoria. Jeśli spojrzymy na strzałkę A → B w kategorii jako rodzaj abstrakcyjnego dowodu B z A, mamy reprezentację, która wykracza poza czystą wyprowadzalność B z A (jak strzała ma swoją indywidualność), ale nie zajmuje się szczególna struktura syntaktyczna tego dowodu. W przypadku systemów intuicjonistycznych semantyka dowodowo-teoretyczna w formie kategorialnej jest prawdopodobnie najbliższa temu, co semantyka denotacyjna w przypadku klasycznym.

Jednym z najlepiej rozwiniętych podejść do teorii dowodu kategorialnego jest Došen. Nie tylko dokonał postępów w stosowaniu metod kategorialnych w teorii dowodów (np. Došen i Petrić, 2004), ale także pokazał, jak metody teoretyczne można zastosować w samej teorii kategorii (Došen, 2000). Najważniejsze dla logiki kategorialnej w odniesieniu do semantyki teorii dowodu jest to, że w logice kategorialnej strzałki zawsze łączą się z relacją tożsamości, która w teorii dowodu odpowiada tożsamości dowodów. W ten sposób idee i wyniki teorii dowodu kategorialnego odnoszą się do tego, co można nazwać semantyką intencjonalno-teoretyczną, to znaczy badania dowodów jako odrębnych podmiotów, a nie tylko jako narzędzi do ustalania konsekwencji (Došen, 2006, 2016). Inną cechą teorii dowodu kategorialnego jest to, że ma ona z natury charakter hipotetyczny, co oznacza, że wychodzi od bytów hipotetycznych. W ten sposób przezwycięża paradygmat standardu, w szczególności opartą na walidacji semantykę opartą na teorii dowodu (patrz sekcja 3.6 poniżej).

Dalsze czytanie:

Aby zapoznać się z teorią stałych logicznych Poppera, patrz Schroeder-Heister (2005).

Aby uzyskać informacje o stałych logicznych i ich logiczności, zobacz wpis dotyczący stałych logicznych.

Podejścia kategorialne znajdują się we wpisie dotyczącym teorii kategorii.

3. Rozszerzenia i alternatywy dla standardowej semantyki teorii dowodu

3.1 Zasady eliminacji jako podstawowe

Większość podejść do semantyki teorii dowodu traktuje reguły wprowadzania jako podstawowe, dające znaczenie lub samo usprawiedliwiające, podczas gdy wnioskowania eliminujące są uzasadnione jako ważne w odniesieniu do podanych reguł wprowadzenia. Koncepcja ta ma co najmniej trzy korzenie: pierwszy to weryfikacjonistyczna teoria znaczenia, zgodnie z którą warunki stwierdzalności zdania stanowią jego znaczenie. Druga to idea, że musimy rozróżnić, co nadaje znaczenie, a jakie są konsekwencje tego znaczenia, ponieważ nie każda wiedza wnioskowa może składać się z zastosowania definicji. Trzecią z nich jest prymat asercji nad innymi aktami mowy, takimi jak przyjmowanie lub zaprzeczanie, co jest implicite we wszystkich rozważanych dotychczas podejściach.

Można by zbadać, jak daleko można się posunąć, rozważając raczej reguły eliminacji niż reguły wprowadzenia jako podstawę semantyki teorii dowodu. Dummett (1991, rozdz. 13) nakreślił kilka pomysłów na semantykę opartą na teorii eliminacji, a nie na wprowadzeniu, aczkolwiek w bardzo podstawowej formie. Bardziej precyzyjna definicja trafności oparta na wnioskach eliminacyjnych pochodzi od Prawitza (1971; 2007; zob. Także Schroeder-Heister 2015). Jego zasadniczą ideą jest to, że zamknięty dowód uważa się za ważny, jeśli wynik zastosowania reguły eliminacji do jego końcowego wzoru jest ważnym dowodem lub zmniejsza się do jednego. Na przykład, zamknięty dowód implikacji A → B jest ważny, jeśli dla dowolnego podanego zamkniętego dowodu A, wynik zastosowania modus ponens

A → BA
b

do tych dwóch dowodów jest ważny dowód B lub sprowadza się do takiego dowodu. Koncepcja ta zachowuje dwa z trzech podstawowych składników semantyki teorii dowodu w stylu Prawitza (patrz sekcja 2.2.2): rolę redukcji dowodów i substytucyjny pogląd na założenia. Dopiero kanoniczność dowodów kończących się wstępami zamienia się na kanoniczność dowodów kończących się eliminacjami.

3.2 Negacja i zaprzeczenie

Standardowa semantyka teorii dowodu koncentruje się na asercji, ponieważ warunki asertywności określają znaczenie stałych logicznych. Odpowiadając intuicjonistycznemu sposobowi postępowania, negacja ¬ A wzoru A jest zwykle rozumiana jako implikująca absurd A → ⊥, gdzie ⊥ jest stałą, której nie można stwierdzić, tj. Dla której nie określono warunku stwierdzalności. Jest to „pośredni” sposób rozumienia negacji. W literaturze dyskutowano o tym, co za von Kutscherą (1969) można nazwać negacją „bezpośrednią”. Rozumie się przez to jednopunktowy prymitywny operator negacji, którego nie można, a przynajmniej nie jest, sprowadzać do implikowania absurdu. Nie jest to też klasyczna negacja. Jest raczej posłuszny regułom, które dublują zwykłe reguły dla stałych logicznych. Czasami nazywa się to „zaprzeczeniem” wyroku,czasami także „silna negacja” (patrz Odintsov, 2008). Typowe zasady odmowy ~ A z A to

~ A ~ B ~ A ~ B.
~ (A ∨ B) ~ (A ∧ B) ~ (A ∧ B)

Zasadniczo reguły odmowy dla operatora odpowiadają regułom stwierdzenia dla operatora dualnego. Zbadano kilka logik zaprzeczania, w szczególności logikę „konstruowalnego fałszu” Nelsona, motywowaną najpierw przez Nelsona (1949) w odniesieniu do pewnej semantyki realizowalności. Główny nacisk położono na jego systemy nazwane później N3 i N4, które różnią się pod względem traktowania sprzeczności (N4 to N3 bez quodlibet ex contradictione). Stosując zaprzeczenie, każde podejście do semantyki teorii dowodu można zduplikować, po prostu wymieniając twierdzenie i zaprzeczanie oraz przechodząc od stałych logicznych do ich dualności. W ten sposób uzyskuje się system oparty raczej na obaleniu (= dowodzie zaprzeczenia) niż na dowodzie. Można to rozumieć jako zastosowanie popperowskiego poglądu do semantyki teorii dowodu.

Innym podejściem byłoby nie tylko zduplikowanie semantyki opartej na twierdzeniach i teorii dowodu na rzecz semantyki opartej na teorii refutacji, ale postrzeganie relacji między regułami twierdzenia i zaprzeczania jako rządzoną zasadą inwersji lub zasadą refleksji definicyjnej własny. Byłaby to zasada tego, co można by nazwać „harmonią asercji-zaprzeczenia”. Podczas gdy w standardowej semantyce teorii dowodu, zasady inwersji kontrolują związek między twierdzeniami a założeniami (lub konsekwencjami), taka zasada rządziłaby teraz relacją między stwierdzeniem a zaprzeczeniem. Biorąc pod uwagę pewne warunki definiujące A, można by powiedzieć, że odrzucenie każdego warunku definiującego A prowadzi do zaprzeczenia samego A. W przypadku koniunkcji i dysjunkcji prowadzi to do wspólnych par reguł twierdzenia i zaprzeczenia

ZA b ~ A ~ B
A ∨ B A ∨ B ~ (A ∨ B)
AB ~ A ~ B.
A ∧ B ~ (A ∧ B) ~ (A ∧ B)

Ideę tę można łatwo uogólnić na refleksję definicyjną, uzyskując system rozumowania, w którym przeplatają się twierdzenia i zaprzeczanie. Ma analogie do dedukcyjnych relacji między formami osądów badanymi na tradycyjnym placu opozycji (Schroeder-Heister, 2012a; Zeilberger, 2008). Należy podkreślić, że operator odmowy jest tutaj zewnętrznym znakiem wskazującym na formę oceny, a nie jako operator logiczny. Oznacza to w szczególności, że nie można go powtarzać.

3.3 Harmonia i odbicie w rachunku sekwencyjnym

Rachunek sekwencyjny Gentzena wykazuje symetrię między prawą i lewą regułą wprowadzania, co sugeruje poszukiwanie zasady harmonii, która czyni tę symetrię istotną dla semantyki teorii dowodu. Podążano za co najmniej trzema liniami, aby poradzić sobie z tym zjawiskiem. (i) Zasady wprowadzenia z prawej lub z lewej strony są uważane za zasady wprowadzenia. Odwrotne reguły (odpowiednio wprowadzenie po lewej i wprowadzenie po prawej) są następnie uzasadnione za pomocą odpowiednich reguł eliminacji. Oznacza to, że metody omówione wcześniej są stosowane do całych sekwencji, a nie formuł w sekwencjach. W przeciwieństwie do tych formuł sekwencje nie mają logicznej struktury. Dlatego podejście to opiera się na refleksji definicyjnej,który stosuje harmonię i inwersję do reguł dla jednostek o dowolnej strukturze, a nie tylko dla logicznych złożonych. Prowadzili go de Campos Sanz i Piecha (2009). (ii) Reguły wprowadzenia z prawej i lewej strony wywodzą się z charakterystyki w sensie reguł podwójnej linii Došena (sekcja 2.4), którą następnie czyta się jako pewnego rodzaju definicję. Kierunek od góry do dołu reguły podwójnej linii jest już regułą wprowadzającą w prawo lub w lewo. Drugi można wyprowadzić z kierunku oddolnego za pomocą pewnych zasad. Jest to podstawowy składnik teorii znaczeń w Podstawowej logice Sambina i wsp. (Sambin, Battilotti i Faggian, 2000). (iii) Reguły wprowadzenia w prawo i w lewo są postrzegane jako wyrażające interakcję między sekwencjami przy użyciu reguły cięcia. Biorąc pod uwagę prawa lub lewicę,Reguły komplementarne wyrażają, że wszystko, co wchodzi w interakcję z jej przesłankami w pewien sposób, tak samo jest z jej zakończeniem. Ta idea interakcji jest uogólnioną symetryczną zasadą refleksji definicyjnej. Można to uznać za uogólnienie zasady inwersji, posługując się raczej pojęciem interakcji niż wyprowadzalności konsekwencji (patrz Schroeder-Heister, 2013). Wszystkie trzy podejścia mają zastosowanie do rachunku sekwencyjnego w jego klasycznej formie, z prawdopodobnie więcej niż jedną formułą w następstwie sekwencji, w tym strukturalnie ograniczonymi wersjami badanymi w logice liniowej i innych. Można to uznać za uogólnienie zasady inwersji, posługując się raczej pojęciem interakcji niż wyprowadzalności konsekwencji (patrz Schroeder-Heister, 2013). Wszystkie trzy podejścia mają zastosowanie do rachunku sekwencyjnego w jego klasycznej formie, z prawdopodobnie więcej niż jedną formułą w następstwie sekwencji, w tym strukturalnie ograniczonymi wersjami badanymi w logice liniowej i innych. Można to uznać za uogólnienie zasady inwersji, posługując się raczej pojęciem interakcji niż wyprowadzalności konsekwencji (patrz Schroeder-Heister, 2013). Wszystkie trzy podejścia mają zastosowanie do rachunku sekwencyjnego w jego klasycznej formie, z prawdopodobnie więcej niż jedną formułą w następstwie sekwencji, w tym strukturalnie ograniczonymi wersjami badanymi w logice liniowej i innych.

3.4 Struktura subatomowa i język naturalny

Nawet jeśli, jak w refleksji definicyjnej, rozważamy reguły definicyjne dla atomów, warunki ich definiowania zwykle nie powodują rozkładu tych atomów. Podejście dowodowo-teoretyczne uwzględniające wewnętrzną strukturę zdań atomowych zostało zaproponowane przez Więckowskiego (2008; 2011; 2016). Używa reguł wprowadzania i eliminacji dla zdań atomowych, w których te zdania atomowe są zredukowane nie tylko do innych zdań atomowych, ale do wyrażeń subatomowych reprezentujących znaczenie predykatów i nazw indywidualnych. Można to postrzegać jako pierwszy krok w kierunku zastosowania semantyki teorii dowodu w języku naturalnym. Kolejny krok w tym kierunku podjął Francez, który opracował semantykę dowodowo-teoretyczną dla kilku fragmentów języka angielskiego (patrz Francez, Dyckhoff i Ben-Avi, 2010; Francez i Dyckhoff, 2010,Francez i Ben-Avi 2015).

3.5 Logika klasyczna

Semantyka teorii dowodowych jest intuicyjnie stronnicza. Wynika to z faktu, że naturalna dedukcja jako preferowana przez nią struktura ma pewne cechy, które czynią ją szczególnie dostosowaną do logiki intuicjonistycznej. W klasycznej dedukcji naturalnej ex falso quodlibet

ZA

zostaje zastąpiona zasadą klasycznej reductio ad absurdum

[A → ⊥]
ZA

Pozwalając wyprowadzić A → ⊥ w celu wywnioskowania A, reguła ta podważa zasadę podformuły. Ponadto, zawierając zarówno ⊥, jak i A → ⊥, odnosi się do dwóch różnych stałych logicznych w jednej regule, więc nie ma już separacji stałych logicznych. Wreszcie, jako reguła eliminacji dla ⊥ nie jest zgodna z ogólnym wzorcem wprowadzeń i eliminacji. W konsekwencji niszczy on właściwość formy wprowadzenia, że każde zamknięte wyprowadzenie można zredukować do takiej, która używa reguły wprowadzania w ostatnim kroku.

Logika klasyczna bardzo dobrze pasuje do rachunku wielosekwencyjnego sekwencyjnego. Nie potrzebujemy tam żadnych dodatkowych zasad poza tymi, które przyjęto w przypadku intuicjonistycznym. Tylko strukturalna cecha pozwalająca na więcej niż jedną formułę w następstwie wystarczy, aby uzyskać klasyczną logikę. Ponieważ istnieją wiarygodne podejścia do ustalenia harmonii między wprowadzeniem z prawej strony a wprowadzeniem z lewej w rachunku sekwencyjnym (patrz sekcja 3.3), logika klasyczna wydaje się być doskonale uzasadniona. Jest to jednak przekonujące tylko wtedy, gdy rozumowanie jest odpowiednio sformułowane jako proces z wieloma wnioskami, nawet jeśli nie odpowiada to naszej standardowej praktyce, w której skupiamy się na pojedynczych wnioskach. Można spróbować rozwinąć odpowiednią intuicję, argumentując, że rozumowanie w kierunku wielu wniosków wyznacza raczej obszar, w którym leży prawda, niż ustalanie jednego zdania jako prawdziwego. Jednak tę intuicję trudno jest utrzymać i nie można jej formalnie uchwycić bez poważnych trudności. Podejścia filozoficzne, takie jak te opracowane przez Shoesmith i Smiley (1978) oraz podejścia oparte na teorii dowodów, takie jak siatki dowodowe (patrz Girard, 1987; Di Cosmo i Miller, 2010) są próbami w tym kierunku.

Podstawową przyczyną niepowodzenia własności formy wstępnej w logice klasycznej jest indeterminizm tkwiący w prawach dysjunkcji. A ∨ B można wywnioskować zarówno z A, jak iz B. Dlatego też, gdyby prawa dysjunkcji były jedynym sposobem wywnioskowania A ∨ B, wyprowadzalność A ∨¬ A, która jest kluczową zasadą logiki klasycznej, pociągałaby za sobą zasadę A lub ¬ A, co jest absurdalne. Wyjściem z tej trudności jest zniesienie indeterministycznej dysjunkcji i użycie w zamian jej klasycznego odpowiednika de Morgana ¬ (¬ A ∧¬ B). Prowadzi to zasadniczo do logiki bez właściwego rozłączenia. W przypadku kwantyfikatora również nie byłoby właściwego kwantyfikatora egzystencjalnego, ponieważ ∃ xA byłoby rozumiane w znaczeniu ¬∀ x ¬ A. Jeśli ktoś jest gotów zaakceptować to ograniczenie, wówczas można sformułować pewne zasady harmonii dla logiki klasycznej.

3.6 Rozumowanie hipotetyczne

Standardowe podejście do semantyki teorii dowodu, zwłaszcza podejście Prawitza oparte na walidacji (sekcja 2.2.2), przyjmuje zamknięte wyprowadzenia jako podstawowe. Ważność otwartych pochodnych definiuje się jako przeniesienie ważności z zamkniętych pochodnych założeń do zamkniętego wyprowadzenia stwierdzenia, gdzie to ostatnie uzyskuje się przez zastąpienie otwartego założenia założeniem zamkniętym. Dlatego też, jeśli nazwać derywacje zamknięte „kategorycznymi”, a derywacje otwarte „hipotetycznymi”, to podejście to można scharakteryzować jako następujące dwie podstawowe idee: (I) prymat tego, co kategoryczne nad hipotetycznym, (II) transmisyjny pogląd konsekwencji. Te dwa założenia (I) i (II) można postrzegać jako dogmaty standardowej semantyki (patrz Schroeder-Heister 2012c). „Standardowa semantyka” oznacza tutaj nie tylko standardową semantykę teorii dowodu,ale także klasyczna semantyka modelowo-teoretyczna, w której również te dogmaty są przyjmowane. W tym miejscu zaczyna się od definicji prawdy, która jest pojęciem kategorycznym, i definiuje konsekwencję, pojęcie hipotetyczne, jako przenoszenie prawdy z warunków do następstwa. Z tego punktu widzenia semantyka konstruktywna, w tym semantyka dowodowo-teoretyczna, zamienia pojęcie prawdy na pojęcie konstrukcji lub dowodu i interpretuje „transmisję” w kategoriach konstruktywnej funkcji lub procedury, ale poza tym pozostawia ramy nietknięte.semantyka konstruktywna, w tym semantyka dowodowo-teoretyczna, zamienia pojęcie prawdy na pojęcie konstrukcji lub dowodu i interpretuje „transmisję” w kategoriach konstruktywnej funkcji lub procedury, ale poza tym pozostawia ramy nietknięte.semantyka konstruktywna, w tym semantyka dowodowo-teoretyczna, zamienia pojęcie prawdy na pojęcie konstrukcji lub dowodu i interpretuje „transmisję” w kategoriach konstruktywnej funkcji lub procedury, ale poza tym pozostawia ramy nietknięte.

W zasadzie nie ma nic złego w tych dogmatach. Są jednak zjawiska, z którymi trudno sobie poradzić w standardowym frameworku. Takim zjawiskiem jest brak uzasadnienia, zwłaszcza cykliczność, w przypadku której możemy mieć konsekwencje bez przekazywania prawdy i udowodnienia. Kolejnym zjawiskiem są podziały substrukturalne, w których kluczowe jest uwzględnienie strukturyzowania założeń od samego początku. Co więcej, i to jest najważniejsze, możemy definiować rzeczy w określony sposób, nie wiedząc z góry, czy nasza definicja lub łańcuch definicji jest dobrze uzasadniony, czy nie. Nie angażujemy się najpierw w metajęzykowe badanie definicji, od której zaczynamy, ale chcielibyśmy od razu zacząć rozumować. Problem ten nie występuje, jeśli ograniczymy się do przypadku stałych logicznych,gdzie reguły definiujące są trywialnie uzasadnione. Ale problem pojawia się natychmiast, gdy rozważymy bardziej skomplikowane przypadki, które wykraczają poza logiczne stałe.

Dlatego warto pójść w drugą stronę i zacząć od hipotetycznej koncepcji konsekwencji, czyli bezpośrednio scharakteryzować konsekwencję, nie sprowadzając jej do przypadku kategorycznego. Z filozoficznego punktu widzenia oznacza to, że pojęcie kategorialne jest pojęciem ograniczającym hipotetycznym. W klasycznym przypadku prawda byłaby ograniczającym przypadkiem konsekwencji, czyli konsekwencją bez hipotez. Program ten jest ściśle powiązany z podejściem teorii dowodu kategorialnego (sekcja 2.5), która opiera się na prymacie bytów hipotetycznych („strzałki”). Formalnie dałoby pierwszeństwo rachunekowi sekwencyjnemu nad naturalną dedukcją, ponieważ rachunek sekwencyjny pozwala na manipulację stroną założeń ciągu za pomocą reguł wprowadzenia w lewo.

3.7 Semantyka międzywymiarowo-teoretyczna

Jak wspomniano w pierwszej części (1.1), semantyka teorii dowodu ma charakter intencjonalny, ponieważ interesuje ją dowód, a nie tylko możliwość udowodnienia. Dla semantyki teorii dowodu istotne jest nie tylko to, czy B wynika z A, ale także, w jaki sposób możemy ustalić, że B wynika z A. Innymi słowy, tożsamość dowodów jest ważną kwestią. Jednakże, chociaż jest to prima facie oczywiste i semantyści teorii dowodu normalnie zgodziliby się z tym abstrakcyjnym twierdzeniem, praktyka semantyki teorii dowodu jest często inna, a temat tożsamości dowodów jest tematem znacznie zaniedbywanym. Bardzo często zdarza się, że identyfikowane są reguły, które są równie potężne. Na przykład, kiedy omawia się zasady harmonii i rozważa się standardową regułę wprowadzającą koniunkcję

AB
A ∧ B

Wielu semantyków zajmujących się teorią dowodu uznałoby za nieistotne, czy ktoś wybiera parę rzutów

A ∧ B A ∧ B
ZA b

lub para

A ∧ B A ∧ BA
ZA b

jako zasady eliminacji koniunkcji. Druga para reguł byłaby często uważana za bardziej skomplikowany wariant pary rzutów. Jednak z intensywnego punktu widzenia te dwie pary reguł nie są identyczne. Zidentyfikowanie ich odpowiada identyfikacji A ∧ B i A ∧ (A → B), które jest tylko w wymiarze, ale nie intencjonalnie poprawne. Jak często argumentował Došen (np. Došen 1997, 2006), wzory takie jak A ∧ B i A ∧ (A → B) są równoważne, ale nie są izomorficzne. Tutaj „izomorficzny” oznacza, że dowodząc jednej formuły od drugiej i odwrotnie, uzyskujemy, łącząc te dwa dowody, dowód tożsamości. W tym przykładzie tak nie jest.

Podążanie za tą ideą prowadzi do zasad harmonii i inwersji, które różnią się od standardowych. Ponieważ harmonia i inwersja leżą u podstaw semantyki opartej na teorii dowodu, wiele jej kwestii zostało poruszonych. Poważne potraktowanie tematu intencjonalności może zmienić wiele dziedzin semantyki opartej na teorii dowodu. A ponieważ tożsamość dowodów jest podstawowym tematem teorii dowodu kategorialnego, ta ostatnia będzie wymagała większej uwagi w semantyce teorii dowodu, niż ma to miejsce obecnie.

Dalsze czytanie

Zaprzeczanie i zaprzeczanie zob. Tranchini (2012b); Wansing (2001).

Dla semantyki języka naturalnego zobacz Francez (2015).

Aby zapoznać się z logiką klasyczną, zobacz wpis dotyczący logiki klasycznej.

Odnośnie do hipotetycznego rozumowania i semantyki teoretycznej dowodu intensywnego patrz Došen (2003, 2016) i Schroeder-Heister (2016a).

4. Wnioski i perspektywy

Standardowa semantyka teorii dowodu była praktycznie wyłącznie zajęta stałymi logicznymi. Stałe logiczne odgrywają centralną rolę w rozumowaniu i wnioskach, ale z pewnością nie są wyłącznymi, a być może nawet najbardziej typowym rodzajem bytów, które można zdefiniować wnioskując. Potrzebne są ramy, które zajmują się definicjami wnioskowymi w szerszym znaczeniu i obejmują zarówno definicje logiczne, jak i pozalogiczne. Idea refleksji definicyjnej w odniesieniu do arbitralnych reguł definicyjnych (patrz 2.3.2), a także zastosowania języka naturalnego (patrz 3.4) wskazują w tym kierunku, ale można sobie wyobrazić koncepcje sięgające dalej. Ponadto koncentracja na harmonii, zasadach inwersji, refleksji definicyjnej itp. Jest nieco myląca,ponieważ mogłoby to sugerować, że semantyka teorii dowodu składa się tylko z tego. Należy podkreślić, że już w przypadku arytmetyki oprócz inwersji potrzebne są silniejsze zasady. Jednak pomimo tych ograniczeń semantyka dowodowa uzyskała już bardzo znaczące osiągnięcia, które mogą konkurować z bardziej rozpowszechnionymi podejściami do semantyki.

Bibliografia

  • Aczel, Peter (1977). „An Introduction to Inductive Definitions”, w Handbook of Mathematical Logic, John Barwise (red.), Amsterdam: North-Holland, str. 739–782.
  • Beall, JC i Greg Restall (2006). Pluralizm logiczny, Oxford: Oxford University Press.
  • Belnap, Nuel D. (1982). „Display Logic”, Journal of Philosophical Logic, 11: 375–417.
  • Brandom, Robert B. (2000). Artykułowanie powodów: wprowadzenie do wnioskowania, Cambridge Mass.: Harvard University Press.
  • de Campos Sanz, Wagner i Thomas Piecha (2009). „Inversion by Definitional Reflection and the Admissibility of Logical Rules”, Review of Symbolic Logic, 2: 550–569.
  • –––, Thomas Piecha i Peter Schroeder-Heister (2014). „Konstruktywna semantyka, dopuszczalność reguł i ważność prawa Peirce'a”, Logic Journal of the IGPL, 22: 297–308.
  • de Groote, Philippe, wyd. (1995). Izomorfizm Curry-Howarda, tom 8, Cahiers du Centre de Logique, Academia-Bruyland.
  • Di Cosmo, Roberto i Dale Miller (2010). „Logika liniowa”, The Stanford Encyclopedia of Philosophy (wydanie jesień 2010), Edward N. Zalta (red.), URL =
  • Došen, Kosta (1980). Stałe logiczne: esej w teorii dowodu, D. Phil. Praca magisterska, Wydział Filozofii, Uniwersytet Oksfordzki.
  • ––– (1989). „Logical Constants as Punctuation Marks”, Notre Dame Journal of Formal Logic, 30: 362–381.
  • ––– (1997). „Logical Consequence: A Turn in Style”, w: Dalla Chiara, ML, K. Doets, D. Mundici, J. van Benthem (red.), Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florencja, sierpień 1995, Dordrecht: Kluwer, 289–311.
  • ––– (2000). Wytnij eliminację w kategoriach, Berlin: Springer.
  • ––– (2003). „Tożsamość dowodów opartych na normalizacji i ogólności”, Bulletin of Symbolic Logic, 9: 477–503.
  • ––– (2006). „Modele dedukcji”, w: Kahle i Schroeder-Heister, red. (2006), s. 639–657.
  • ––– (2016). „Na ścieżkach kategorii”, w: Piecha i Schroeder-Heister, red. (2016b), s. 65–77.
  • ––– i Zoran Petrić (2004). Proof-Theoretical Coherence, London: College Publications.
  • Dummett, Michael (1991). The Logical Basis of Metaphysics, London: Duckworth.
  • Francez, Nissim (2015). Proof-theoretic Semantics, London: College Publications.
  • ––– i Gilad Ben-Avi (2015). „A proof-teoretyczna rekonstrukcja uogólnionych kwantyfikatorów”, Journal of Semantics, 32: 313–371.
  • ––– i Roy Dyckhoff (2010). „Proof-theoretic Semantics for a Natural Language Fragment”, Linguistics and Philosophy, 33: 447–477.
  • –––, Roy Dyckhoff i Gilad Ben-Avi (2010). „Proof-Theoretic Semantics for Subsentential Phrases”, Studia Logica, 94: 381–401.
  • Gentzen, Gerhard (1934/35). „Untersuchungen über das logische Schließen”, Mathematische Zeitschrift, 39: 176–210, 405–431; Tłumaczenie na język angielski w The Collected Papers of Gerhard Gentzen, ME Szabo (red.), Amsterdam: North Holland, 1969, s. 68–131.
  • Girard, Jean-Yves (1987). „Logika liniowa”, Informatyka teoretyczna, 50: 1–102.
  • Hacking, Ian (1979). „Co to jest logika?”, Journal of Philosophy, 76: 285–319.
  • Hallnäs, Lars (1991). „Częściowe definicje indukcyjne”, Theoretical Computer Science, 87: 115–142.
  • ––– (2006). „O dowodowych podstawach teorii definicji ogólnej”, Synthese, 148: 589–602.
  • Hallnäs, Lars i Peter Schroeder-Heister (1990/91). „Teoretyczne podejście do programowania logicznego: I. Klauzule jako reguły. II. Programy jako definicje”, Journal of Logic and Computation, 1: 261–283, 635–660.
  • Harper, Robert, Furio Honsell i Gordon Plotkin (1987). „A Framework for Defining Logics”, Journal of the Association for Computing Machinery, 40: 194–204.
  • Humberstone, Lloyd (2010). „Sentence Connectives in Formal Logic”, The Stanford Encyclopedia of Philosophy (wydanie lato 2010), Edward N. Zalta (red.), URL =
  • Jaśkowski, Stanisław (1934). „On the Rules of Suppositions in Formal Logic”, Studia Logica, 1: 5–32 (przedruk w: S. McCall (red.), Polish Logic 1920–1939, Oxford 1967, s. 232–258.
  • Jäger, Gerhard i Robert F. Stärk (1998). „A Proof-Theoretic Framework for Logic Programming”, Handbook of Proof Theory, Samuel R. Buss (red.), Amsterdam: Elsevier, str. 639–682.
  • Kahle, Reinhard i Peter Schroeder-Heister, wyd. (2006). Semantyka dowodowo-teoretyczna, wydanie specjalne Synthese, tom 148.
  • Kneale, William (1956). „The Province of Logic”, Contemporary British Philosophy, HD Lewis (red.), Londyn: Allen and Unwin, s. 237–261.
  • Koslow, Arnold (1992). A Structuralist Theory of Logic, Cambridge: Cambridge University Press.
  • Kreisel, Georg (1971). „A Survey of Proof Theory II”, Proceedings of the Second Scandinavian Logic Symposium, JE Renstad (red.), Amsterdam: North-Holland, s. 109–170.
  • Kremer, Philip (2009). „The Revision Theory of Truth”, The Stanford Encyclopedia of Philosophy (wydanie wiosna 2009), Edward N. Zalta (red.), URL =
  • Kreuger, Per (1994). „Axioms in Definitional Calculi”, Extensions of Logic Programming: Proceedings of the 4th International Workshop, ELP'93, St. Andrews, Wielka Brytania, marzec / kwiecień 1993 (Lecture Notes in Computer Science, Voluem 798), Roy Dyckhoff (red.), Berlin: Springer, s. 196–205.
  • Lambek, J. i PJ Scott (1986). Wprowadzenie do logiki kategorialnej wyższego rzędu, Cambridge: Cambridge University Press.
  • Lorenzen, Paul (1955). Einführung in die operative Logik und Mathematik, Berlin: Springer; Wydanie 2, 1969.
  • Martin-Löf, Per (1971). „Hauptsatz dla intuicjonistycznej teorii iterowanych definicji indukcyjnych”, Proceedings of the Second Scandinavian Logic Symposium, JE Fenstad (red.), Amsterdam: North-Holland, str. 179–216.
  • ––– (1984). Intuitionistic Type Theory, Napoli: Bibliopolis.
  • ––– (1995). „Verificationism Once and Now”, The Foundational Debate: Complexity and Constructivity in Mathematics and Physics, Werner DePauli-Schimanovich, Eckehart Köhler i Friedrich Stadler (red.), Dordrecht: Kluwer, s. 187–196.
  • ––– (1998). „Truth and Knowability: On the Principles C and K of Michael Dummett”, Truth in Mathematics, Harold G. Dales i Gianluigi Oliveri (red.), Oxford: Clarendon Press, str. 105–114.
  • Negri, Sara i Jan von Plato (2001). Teoria dowodów strukturalnych, Cambridge: Cambridge University Press.
  • Nelson, David (1949). „Constructible Falsity”, Journal of Symbolic Logic, 14: 16–26.
  • Odintsov, Sergei P. (2008). Konstruktywne negacje i parakonsystencja, Berlin: Springer.
  • Piecha, Thomas (2016). „Kompletność w dowodowo-teoretycznej semantyce”. W: Piecha i Schroeder-Heister, wyd. (2016b), s. 231–251.
  • –––, Wagner de Campos Sanz i Peter Schroeder-Heister (2015). „Failure of Completeness in Proof-Theoretic Semantics”, Journal of Philosophical Logic, 44: 321–335.
  • ––– i Peter Schroeder-Heister (2016a). „Atomic Systems in Proof-Theoretic Semantics: Two Approaches”, w: Redmond, J., OP Martins, Á. N. Fernández Epistemology, Knowledge and the Impact of Interaction, Cham: Springer, str. 47–62.
  • ––– i Peter Schroeder-Heister, wyd. (2016b). Postępy w semantyce dowodowo-teoretycznej, Cham: Springer (otwarty dostęp)
  • Popper, Karl Raimund (1947a). „Logic without Assumptions”, Proceedings of the Aristotelian Society, 47: 251–292.
  • ––– (1947b). „New Foundations for Logic”, Mind, 56: 193–235; poprawki, Mind, 57: 69–70.
  • Prawitz, Dag (1965). Natural Deduction: A Proof-Theoretical Study, Stockholm: Almqvist & Wiksell; przedrukowano Mineola, NY: Dover Publications, 2006.
  • ––– (1971). „Ideas and Results in Proof Theory”, Proceedings of the Second Scandinavian Logic Symposium (Oslo 1970), Jens E. Fenstad (red.), Amsterdam: North-Holland, s. 235–308.
  • ––– (1972). „The Philosophical Position of Proof Theory”, Contemporary Philosophy in Scandinavia, RE Olson i AM Paul (red.), Baltimore, Londyn: John Hopkins Press, str. 123–134.
  • ––– (1973). „Towards a Foundation of a General Proof Theory”, Logic, Methodology and Philosophy of Science IV, Patrick Suppes i in. (red.), Amsterdam: Holandia Północna, s. 225–250.
  • ––– (1974). „O idei ogólnej teorii dowodu”, Synthese, 27: 63–77.
  • ––– (1985). „Remarks on some Approaches to the Concept of Logical Consequence”, Synthese, 62: 152–171.
  • ––– (2006). „Meaning Approached via Proofs”, Synthese, 148: 507–524.
  • ––– (2007). „Pragmatist and Verificationist Theories of Meaning”, The Philosophy of Michael Dummett, Randall E. Auxier and Lewis Edwin Hahn (red.), La Salle: Open Court, s. 455–481.
  • ––– (2013). „An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited”, Advances in Natural Deduction, Edward Hermann Haeusler, Luiz Carlos Pereira i Valeria de Paiva (red.), Berlin: Springer.
  • Przeczytaj, Stephen (2010). „General-Elimination Harmony and the Meaning of the Logical Constants”, Journal of Philosophical Logic, 39: 557–576.
  • Restall, Greg (2009). „Substructural Logics”, The Stanford Encyclopedia of Philosophy (wydanie lato 2009), Edward N. Zalta (red.), URL =.
  • Sambin, Giovanni, Giulia Battilotti i Claudia Faggian (2000). „Basic Logic: Reflection, Symmetry, Visibility”, Journal of Symbolic Logic, 65: 979–1013.
  • Sandqvist, Tor (2009). „Logika klasyczna bez biwalencji”, Analiza, 69: 211–218.
  • Schroeder-Heister, Peter (1984). „Naturalne rozszerzenie naturalnej dedukcji”, Journal of Symbolic Logic, 49: 1284–1300.
  • ––– (1991). „Uniform Proof-Theoretic Semantics for Logical Constants (Abstract)”, Journal of Symbolic Logic, 56: 1142.
  • ––– (1992). „Cut Elimination in Logics with Definitional Reflection”, Nonclassical Logics and Information Processing: Proceedings of the International Workshop, Berlin, listopad 1990 (Notatki do wykładu z informatyki: tom 619). David Pearce i Heinrich Wansing (red.), Berlin: Springer, str. 146–171.
  • ––– (1993). „Rules of Definitional Reflection”, Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science, Los Alamitos: IEEE Press, s. 222–232.
  • ––– (2004). „O pojęciu założenia w systemach logicznych”, Selected Papers Contribute the Sections of GAP5 (V Międzynarodowy Kongres Towarzystwa Filozofii Analitycznej, Bielefeld, 22-26 września 2003), R. Bluhm i C. Nimtz (red.), Paderborn: mentis dostępne w Internecie), s. 27–48.
  • ––– (2005). „Strukturalistyczna teoria logiki Poppera”, Karl Popper: A Centenary Assessment. Vol. III: Science, Ian Jarvie, Karl Milford i David Miller (red.), Aldershot: Ashgate, str. 17–36.
  • ––– (2006). „Validity Concepts in Proof-Theoretic Semantics”, Synthese, 148: 525–571.
  • ––– (2007). „Generalized Definitional Reflection and the Inversion Principle”, Logica Universalis, 1: 355–376.
  • ––– (2008a). „Operatywne uzasadnienie logiki intuicyjnej Lorenzena”, Sto lat intuicji (1907-2007): Konferencja Cerisy, Mark van Atten, et al. (red.), Bazylea: Birkhäuser, 214–240 [Odniesienia do całego tomu: 391–416].
  • ––– (2008b). „Proof-Theoretic versus Model-Theoretic Consequence”, The Logica Yearbook 2007, M. Peliš (red.), Praga: Filosofia, s. 187–200.
  • ––– (2012a). „Definitional Reasoning in Proof-Theoretic Semantics and the Square of Opposition”, The Square of Opposition: A General Framework for Cognition, Jean-Yves Béziau i Gillman Payette (red.), Berno: Peter Lang, s. 323–349.
  • ––– (2012b). „Semantyka dowodowo-teoretyczna, sprzeczność własna i format wnioskowania dedukcyjnego”. W: Topoi 31, s. 77–85.
  • ––– (2012c). „The Categorical and the Hypothetical: A Critique of some Fundamental Assumptions of Standard Semantics”. W: Synthese 187, s. 925–942.
  • ––– (2012d). „Paradoksy i reguły strukturalne”. W: Dutilh Novaes, Catarina and Ole T. Hjortland, red., Insolubles and Consequences. Eseje na cześć Stephena Read. London: College Publications, s. 203–211.
  • ––– (2013). „Definitional Reflection and Basic Logic”, Annals of Pure and Applied Logic, 164 (4): 491–501.
  • ––– (2015). „Wiarygodność teoretyczna oparta na regułach eliminacji”. W: Haeusler, Edward Hermann, Wagner de Campos Sanz i Bruno Lopes, red., Why is this a Proof? Festschrift dla Luiza Carlosa Pereiry. London: College Publications, s. 159–176.
  • ––– (2016a). „Open Problems in Proof-Theoretic Semantics”. W: Piecha i Schroeder-Heister, wyd. (2016b), s. 253–283.
  • ––– (2016b). „Ograniczanie sekwencji początkowych: kompromisy między tożsamością, kurczeniem się i cięciem”. W: Kahle, Reinhard, Thomas Strahm and Thomas Studer, red., Advances in Proof Theory Basel: Birkhäuser, s. 339–351.
  • Kowal, DJ i Timothy J. Smiley (1978). Logika wielu wniosków, Cambridge: Cambridge University Press.
  • Sommaruga, Giovanni (2000). Historia i filozofia teorii typu konstruktywnego, Dordrecht: Kluwer.
  • Sørensen, Morten Heine B. i Paweł Urzyczyn (2006). Wykłady na temat izomorfizmu Curry-Howarda, Amsterdam: Elsevier.
  • Tait, W. W: (1967). „Intensional Interpretations of Functionals of Finite Type I”, Journal of Symbolic Logic, 32: 198–212.
  • Tennant, Neil (1978). Natural Logic, Edynburg: Edinburgh University Press.
  • ––– (1982). „Proof and Paradox”, Dialectica, 36: 265–296.
  • ––– (1987). Antyrealizm i logika: prawda jako wieczna, Oxford: Clarendon Press.
  • ––– (1997). Poskromienie prawdy, Oxford: Clarendon Press.
  • Tranchini, Luca (2010). Dowód i prawda: perspektywa antyrealistyczna, Mediolan: Edizioni ETS, 2013; przedruk doktoratu rozprawa, Wydział Filozofii, Uniwersytet w Tybindze, 2010, dostępna online.
  • ––– (2012a). „Prawda z perspektywy dowodowo-teoretycznej”. W: Topoi 31, s. 47–57.
  • ––– (2012b). „Natural Deduction for Dual Intuitionistic Logic”, Studia Logica, 100: 631–648.
  • ––– (2016). „Proof-Theoretic Semantics, Paradoxes, and the Distinction between Sense and Denotation”, Journal of Logic and Computation, 26, s. 495–512.
  • Troelstra, Anne S. i Dirk van Dalen (1988). Konstruktywizm w matematyce: wprowadzenie, Amsterdam: Holandia Północna.
  • Troelstra, AS i H. Schwichtenberg (2000). Basic Proof Theory, Cambridge University Press, wydanie drugie.
  • von Kutschera, Franz (1968). „Die Vollständigkeit des Operatorensystems {¬, ∧, ∨, ⊃} für die intuitionistische Aussagenlogik im Rahmen der Gentzensemantik”, Archiv für mathematische Logik und Grundlagenforschung, 11: 3–16.
  • ––– (1969). »Ein verallgemeinerter Widerlegungsbegrifff für Gentzenkalküle«, Archiv für mathematische Logik und Grundlagenforschung, 12: 104–118.
  • Wansing, Heinrich (1993a). „Functional Completeness for Subsystems of Intuitionistic Propositional Logic”, Journal of Philosophical Logic, 22: 303–321.
  • ––– (1993b). Logika struktur informacyjnych (notatki z wykładów w sztucznej inteligencji, tom 681), Berlin: Springer Springer.
  • ––– (2000). „The Idea of a Proof-theoretic Semantics”, Studia Logica, 64: 3–20.
  • ––– (2001). „Negation”, The Blackwell Guide to Philosophical Logic, L. Goble (red.), Cambridge, MA: Blackwell, str. 415–436.
  • Więckowski, Bartosz (2008). „Predication in Fiction”, w The Logica Yearbook 2007, M. Peliš (red.), Praga: Filosofia, s. 267–285.
  • ––– (2011). „Rules for Subatomic Derivation”, Review of Symbolic Logic, 4: 219–236.
  • ––– (2016). „Subatomic Natural Deduction for a Naturalistic First-Order Language with Non-Primitive Identity”, Journal of Logic, Language and Information, 25: 215–268.
  • Zeilberger, Noam (2008). „On the Unity of Duality”, Annals of Pure and Applied Logic, 153: 66–96.

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

  • de Campos Sanz, Wagner i Thomas Piecha (2012). „Remarks on Constructive Semantics for Classical and Intuitionistic Logic”, rękopis online.
  • Tranchini, Luca (2012b). „Semantyka dowodowo-teoretyczna, paradoksy i rozróżnienie między sensem a denotacją”, rękopis online.

Zalecane: