Tõestusteoreetiline Semantika

Sisukord:

Tõestusteoreetiline Semantika
Tõestusteoreetiline Semantika
Anonim

Sisenemise navigeerimine

  • Sissesõidu sisu
  • Bibliograafia
  • Akadeemilised tööriistad
  • Sõprade PDF-i eelvaade
  • Teave autori ja tsitaadi kohta
  • Tagasi üles

Tõestusteoreetiline semantika

Esmakordselt avaldatud 5. detsembril 2012; sisuline redaktsioon teisipäev, 1. veebruar 2018

Tõestusteoreetiline semantika on tõeseisundi semantika alternatiiv. See põhineb põhimõttelisel eeldusel, et keskne mõiste, milles tähendused omistatakse meie keele teatud väljenditele, eriti loogilistele konstantidele, on pigem tõend kui tõde. Selles mõttes on tõestusteoreetiline semantika tõenduse mõttes semantika. Tõestusteoreetiline semantika tähendab ka tõendite semantikat, st entiteetide semantikat, mis kirjeldavad, kuidas jõuame teatud väidetele teatud eelduste korral. Tõestusteoreetilise semantika mõlemad aspektid võivad olla omavahel läbi põimunud, st tõestuste semantika antakse sageli tõendite mõttes.

Tõestusteoreetilisel semantikal on mitu juuri, kõige täpsem on Gentzeni märkused, et sissejuhatusreeglid tema loomuliku deduktsiooni kalkulatsioonis määratlevad loogiliste konstantide tähendused, samas kui selle määratluse tagajärjel on võimalik saada eliminatsioonireegleid (vt punkt 2.2. 1). Laiemas plaanis kuulub see sellesse, mida Prawitz nimetas üldiseks tõestusteooriaks (vt punkt 1.1). Veel laiemalt on see osa traditsioonist, mille kohaselt termini tähendust tuleks selgitada viitega selle kasutamisele meie keeles.

Filosoofias on tõestusteoreetiline semantika enamasti mõelnud pealkirja all „tähendusteooria“. See terminoloogia järgib Dummettit, kes väitis, et tähendusteooria on teoreetilise filosoofia alus - vaade, mille ta omistas Frege'ile. Mõiste “tõenditeoreetiline semantika” pakkus välja Schroeder-Heister (1991; seda kasutati juba 1987. aasta Stockholmi loengutes), et mitte jätta terminit “semantika” ainuüksi denotationalismiks - lõppude lõpuks on “semantika” tavamõiste uurimised, mis käsitlevad keeleliste väljendite tähendust. Lisaks hõlmab mõiste "tõestusteoreetiline semantika" erinevalt "tähendusteooriast" ka filosoofilisi ja tehnilisi aspekte. 1999. aastal toimus esimene selle pealkirjaga konverents Tübingenis, teine 2013. aastal. Esimene selle pealkirjaga õpik ilmus 2015. aastal.

  • 1. Taust

    • 1.1 Üldine tõestusteooria: tagajärg vs tõestus
    • 1.2 Inferentsialism, intuitionism, antirealism
    • 1.3 Gentzen-stiilis tõestusteooria: redutseerimine, normaliseerimine, lõike eemaldamine
  • 2. Mõned tõenditeoreetilise semantika versioonid

    • 2.1 Mõjude semantika: lubatavus, tuletatavus, reeglid

      • 2.1.1 Operatiivne loogika
      • 2.1.2 Gentzen semantika
      • 2.1.3 Loomulik mahaarvamine kõrgema taseme reeglitega
    • 2.2. Tuletuste semantika sissejuhatuse reeglitel

      • 2.2.1 Inversiooni põhimõtted ja harmoonia
      • 2.2.2 Tõestatud teoreetiline paikapidavus
      • 2.2.3 Konstruktiivse tüübi teooria
    • 2.3 Clausali määratlused ja määratluspõhjendused

      • 2.3.1 Loogilise programmeerimise väljakutse
      • 2.3.2 Definitsiooniline peegeldus
    • 2.4 Loogiliste konstantide struktuuriline iseloomustus
    • 2.5 Kategoorikindluse teooria
  • 3. Laiendid ja alternatiivid tavapärasele tõenditeoreetilisele semantikale

    • 3.1 Kõrvaldamiseeskirjad on põhilised
    • 3.2 Eitamine ja eitamine
    • 3.3 Harmoonia ja peegeldus järjestikuses kivil
    • 3.4 Subatomiline struktuur ja loomulik keel
    • 3.5 Klassikaline loogika
    • 3.6 Hüpoteetiline arutluskäik
    • 3.7 Intensiivne tõenditeoreetiline semantika
  • 4. Järeldus ja väljavaated
  • Bibliograafia
  • Akadeemilised tööriistad
  • Muud Interneti-ressursid
  • Seotud kirjed

See kanne sisaldab ka järgmisi tekstiga seotud lisadokumente:

  • Näited tõestusteoreetilise kehtivuse kohta
  • Definitsiooniline peegeldus ja paradoksid

1. Taust

1.1 Üldine tõestusteooria: tagajärg vs tõestus

Termini “üldine tõestusteooria” lõi Prawitz. Üldises tõestusteoorias uuritakse „tõestusi iseseisvalt nende olemuse mõistmise lootuses”, erinevalt Hilberti stiilis „reduktiivse tõestusteooriast”, mis on „katse analüüsida matemaatiliste teooriate tõestusi eesmärgiga: taandades need matemaatika mõnele elementaarsele osale nagu finitistlik või konstruktiivne matemaatika”(Prawitz, 1972, lk 123). Sarnasel viisil palub Kreisel (1971) tõenditeooria ümberorienteerumist. Ta soovib selgitada hiljutist tõestusteooria tööd tähelepanuta jäetud vaatepunktist. Tõendeid ja nende esitusi formaalsete tuletiste abil käsitletakse peamiste uurimisobjektidena, mitte pelgalt tagajärje seose analüüsimise vahendina.” (Kreisel, 1971, lk.109) Kui Kreisel keskendub tõestamisteooria ja tõestatavuse teooria vahelisele dihhotoomiale, siis Prawitz keskendub erinevatele eesmärkidele, mille tõestamise teooria võib järgida. Mõlemad rõhutavad siiski tõendite uurimise olulisust kui põhiolemeid, mille abil omandame tutvustavaid (eriti matemaatilisi) teadmisi. See tähendab eriti seda, et tõendid on episteemilised üksused, mida ei tohiks seostada ametlike tõendite või tuletustega. Pigem on need, mida tuletised tähistavad, kui neid peetakse argumentide esitusviisiks. (Järgnevas kasutame sageli „tõestust” sünonüümina „tuletamisega”, jättes lugeja otsustada, kas mõeldakse formaalsete tõendite või tõendite kui episteemiliste üksuste all.) Prawitzi (1971) uuringu arutamisel rääkis Kreisel (1971, lk.111) räägib otsesõnu tuletamiste ja vaimsete toimingute „kaardistamisest” ning peab selle kaardistamise, sealhulgas tõendite identiteedi uurimise - tõenditeooria ülesandeks - teema, mille Prawitz ja Martin-Löf olid päevakorda seadnud, selgitamist.

See tähendab, et üldises tõestusteoorias ei huvita meid mitte ainult see, kas B järgneb A-st, vaid see, kuidas me jõuame B-ni A-st. Selles mõttes on üldine tõestusteooria oma olemuselt intentsionaalne ja epistemoloogiline, samas kui mudelteooria, mis on huvitatud tagajärgede seosest, mitte selle kehtestamise viisist, on ekstensiivne ja metafüüsiline.

1.2 Inferentsialism, intuitionism, antirealism

Tõestusteoreetiline semantika on oma olemuselt järelduslik, kuna tõestusmaterjalina ilmneb järeldatav tegevus. Seega kuulub see inferentialismi (vt Brandom, 2000), mille kohaselt järeldused ja järeldamisreeglid määravad väljendite tähenduse vastupidiselt denotationalismile, mille kohaselt denatsioonid on primaarsed tähendused. Inferentsialism ja semantika „tähendus kui kasutamine” vaade on tõenditeoreetilise semantika lai filosoofiline raamistik. See üldfilosoofiline ja semantiline vaatenurk ühines konstruktiivsete vaadetega, mis pärinesid matemaatikafilosoofiast, eriti matemaatilisest intuitsionismist. Enamik tõenditeoreetilise semantika vorme on oma olemuselt intuitiivsed,mis tähendab eriti seda, et sellised klassikalise loogika põhimõtted nagu välistatud keskmise või kahekordse eituse seadus lükatakse tagasi või peetakse vähemalt problemaatiliseks. Osaliselt on see tingitud asjaolust, et tõestamisteoreetilise semantika peamine tööriist, loodusliku deduktsiooni kalkulatsioon, on kallutatud intuitionistliku loogika poole, selles mõttes, et selle kõrvaldamise reeglite otsene sõnastus on intuitionistlik. Klassikaline loogika on kättesaadav ainult mõne kaudse tõestuse reegli abil, mis vähemalt mingil määral hävitab arutluspõhimõtete sümmeetria (vt punkt 3.5). Kui võtta omaks loomuliku deduktsiooni seisukoht, siis intuitiivne loogika on loomulik loogiline süsteem. Olulist rolli mängib ka loogiliste märkide BHK (Brouwer-Heyting-Kolmogorov) tõlgendus. See tõlgendus ei ole ainulaadne lähenemine semantikale, vaid hõlmab erinevaid ideesid, mis on sageli mitteametlikumad kui formaalselt kirjeldatud. Eriti oluline on selle funktsionaalne vaade implikatsioonile, mille kohaselt A → B tõend on konstruktiivne funktsioon, mis A tõendile kohaldamisel annab tõendi B kohta. See funktsionaalne vaatenurk põhineb paljudel tõestusteoreetilise semantika kontseptsioonidel, eriti Lorenzenil, Prawitzil ja Martin Löfil (vt jaotised 2.1.1, 2.2.2, 2.2.3). See funktsionaalne vaatenurk põhineb paljudel tõestusteoreetilise semantika kontseptsioonidel, eriti Lorenzenil, Prawitzil ja Martin Löfil (vt jaotised 2.1.1, 2.2.2, 2.2.3). See funktsionaalne vaatenurk põhineb paljudel tõestusteoreetilise semantika kontseptsioonidel, eriti Lorenzenil, Prawitzil ja Martin Löfil (vt jaotised 2.1.1, 2.2.2, 2.2.3).

Dummeti sõnul vastab intuitionismi loogiline positsioon antirealismi filosoofilisele positsioonile. Realistlik vaade iseseisvast reaalsusest on metafüüsiline vaste arvamusele, et kõik laused on kas õiged või valed, sõltumata meie äratundmisviisidest. Dummeti järel on tõestusteoreetilise semantika olulised osad seotud antirealismiga.

1.3 Gentzen-stiilis tõestusteooria: redutseerimine, normaliseerimine, lõike eemaldamine

Gentzeni loomuliku deduktsiooni arvutus ja selle renderdamine Prawitzi poolt on tõenditeoreetilise semantika enamiku lähenemisviiside taust. Looduslik mahaarvamine põhineb vähemalt kolmel peamisel ideel:

  • Eelduste täitmine: Eeldusi saab tuletuse käigus „täita” või „elimineerida”, seega on loomuliku deduktsiooni keskne mõiste tuletamine, mis sõltub eeldustest.
  • Eraldamine: iga primitiivne reegliskeem sisaldab ainult ühte loogilist konstanti.
  • Sissejuhatused ja eliminatsioonid: Loogiliste konstantide reeglid on paaris. Sissejuhatusreeglid võimaldavad tuletada valemi, mille põhioperaatoriks on konstant, kõrvaldamisreeglid lubavad järgmistel valemitel tagajärgi teha.

Gentzeni loomulikus esimese astme loogikavähendussüsteemis kirjutatakse tuletised puu kujul ja üldtuntud reeglite alusel. Näiteks implikatsioonil on järgmised sissejuhatuse ja kõrvaldamise reeglid

[A]
B → I
A → B
A → BA → E
B

kus sulud tähistavad võimalust kõrvaldada eelduse A esinemised. Tuletise avatud eeldused on eeldused, millest lõpp-valem sõltub. Tuletist nimetatakse suletudks, kui sellel pole avatud eeldust, vastasel juhul nimetatakse seda tuletiseks. Kvantifikaatorite käsitlemisel peame arvestama ka avatud üksikute muutujatega (mõnikord nimetatakse neid ka parameetriteks). Tõenditeoreetilise semantika jaoks üliolulised ja Prawitzi (1965) poolt süstemaatiliselt uuritud ja avaldatud metalloloogilised omadused on järgmised:

Vähendamine: Iga ümbersõidu jaoks, mis koosneb sissejuhatusest, millele järgneb kohe kõrvaldamine, on ümbersõidu eemaldamiseks ette nähtud vähendamise samm.

Normaliseerimine: Redutseerimiste järjestikuse kasutamisega saab tuletised muuta normaalseteks vormideks, mis ei sisalda ümbersõite.

Mõiste jaoks on ümbersõitude eemaldamise standardne vähendamise samm järgmine:

[A]
B |
A → B A
B
taandub

|

A

B

Lihtne, kuid väga oluline normaliseerimise järeldus on järgmine: Igasugust suletud tuletust intuitsioonilises loogikas saab taandada tuletuseks, kasutades sissejuhatuse reeglit viimases etapis. Samuti ütleme, et intuitionistlik loomulik deduktiivsus rahuldab sissejuhatuse vormi omadust. Tõenditeoreetilises semantikas on see tulemus silmatorkavalt pealkirja all “fundamentaalne eeldus” (Dummett, 1991, lk 254). Põhipõhine eeldus on tüüpiline näide tehnilise tõestusteoreetilise tulemuse filosoofilisest uuesti tõlgendamisest.

Lisalugemist:

Tõenditeoreetilise semantika üldiseks orienteerumiseks on Piecha ja Schroeder-Heisteri (2016b) toimetatud Synthese'i eriväljaanne (Kahle ja Schroeder-Heister, 2006), Francez (2015), Schroeder-Heister (2008b, 2016a) ja Wansing (2000).

Tõestusteooria filosoofilise positsiooni ja arendamise jaoks on nii sissekanded Hilberti programmist kui ka tõestusteooria väljatöötamine, samuti Prawitz (1971).

Intuitsionismi jaoks on sissekanded intuitionistlikust loogikast, intuitsionismist matemaatikafilosoofias ja intuitionistliku loogika arendamisest.

Realismivastasuse osas on sissejuhatus metafüüsilise realismi väljakutsetele ning ka Tennant (1987); Tennant (1997), Tranchini (2010); Tranchini (2012a).

Gentzeni stiilis tõestusteooria ja loodusliku deduktsiooni teooria jaoks: lisaks Gentzeni (1934/35) algupärasele esitlusele olid ka Jaśkowski (1934) oletuste teooria ja Prawitzi (1965) klassikaline monograafia, Tennant (1978), Troelstra ja Schwichtenberg (2000). ning Negri ja von Plato (2001).

2. Mõned tõenditeoreetilise semantika versioonid

2.1 Mõjude semantika: lubatavus, tuletatavus, reeglid

Implikatsiooni semantika on tõestusteoreetilise semantika keskmes. Vastupidiselt klassikalise tõe-seisundi semantikale on implikatsioon omaette loogiline konstant. Sellel on ka iseloomulik tunnus, et see on seotud tagajärje mõistega. Seda võib vaadelda kui ekstensiivse tagajärje avaldamist senentsiaalsel tasandil, mis tuleneb modus ponenssist ja sellest, mida Hilberti stiilis süsteemides nimetatakse deduktsiooniteoreemiks, st Γ, A ⊢ B ja Γ ⊢ A → B ekvivalentsiks.

Tähenduse A → B väga loomulik mõistmine on selle tõlgendamine järeldamisreegli väljendusena, mis võimaldab üle minna punktist A punkti B. Sammu A-st B-le litsentsimine A → B alusel on täpselt see, mida modus ponens ütleb. Ja deduktsiooni teoreemi võib vaadelda reegli kehtestamise vahendina: Näites, et B-st saab tuletada punkti A, õigustatakse reeglit, mille kohaselt A-st võime üle minna punktile B. Sellistel viisidel põhinev reeglitel põhinev implikatsiooni semantika põhineb mitmetel tõestusteoreetilise semantika kontseptsioonidel, eriti Lorenzeni, von Kutschera ja Schroeder-Heisteri kontseptsioonidel.

2.1.1 Operatiivne loogika

Lorenzen alustab oma sissejuhatuses operatiivsesse loogikasse ja matemaatikasse (1955) loogikavabadest (aatomi) kalkulitest, mis vastavad tootmissüsteemidele või grammatikatele. Ta nimetab reeglit, mis on sellises süsteemis vastuvõetav, kui seda saab sellele lisada, suurendamata selle tuletatavate aatomite komplekti. Kaasamise noolt → tõlgendatakse kui lubatavust. Järeldust A → B loetakse kehtivaks, kui see on reeglina lubatud (aluseks oleva kalkulatsiooni suhtes). Korduvate implikatsioonide (= reeglite) jaoks töötab Lorenzen välja kõrgemate astmete vastuvõetavuse teooria. Teatud väited, näiteks A → A või ((A → B), (B → C)) → (A → C), kehtivad aluspõhjast sõltumatult. Neid nimetatakse üldiselt aktsepteeritavaks [“allgemeinzulässig”]) ja need moodustavad positiivse implikatsiooniloogika süsteemi. Seotud viisil,seadused universaalse kvantifitseerimise jaoks justified on õigustatud, kasutades skemaatiliste muutujatega reeglite lubatavust.

Loogiliste konstantide ∧, ∨, ∃ ja ⊥ seaduste õigustamiseks kasutab Lorenzen inversiooni põhimõtet (termin, mille ta kehtestas). Inversiooniprintsiip ütleb väga lihtsustatud kujul, arvestamata reeglites esinevaid muutujaid, et A-st enesest saab kõike, mida saab A-st iga defineeriva tingimuse kohta. Näiteks disjunktsiooni korral olgu A ja B kumbki A ∨ B määratlev tingimus, mida väljendavad primitiivsed reeglid A → A ∨ B ja B → A ∨ B. Siis ütleb ümberpööramispõhimõte, et A ∨ B → C on lubatavad eeldusel, et A → C ja B → C, mis õigustab disjunktsiooni kõrvaldamise reeglit. Ülejäänud ühendusi käsitletakse sarnaselt. ⊥ puhul saadakse absurdsusreegel ⊥ → A sellest, et ⊥-le pole defineeritavat tingimust.

2.1.2 Gentzen semantika

Selles, mida ta nimetab „Gentzeni semantikaks”, annab von Kutschera (1968) Lorenzenina loogiliselt keerukate implikatsioonitaoliste lausete A 1,…, A n → B semantilisuse K-te suhtes, mis juhivad mõttekäiku aatomilausetega. Põhiline erinevus Lorenzenist on asjaolu, et A 1,…, A n → B väljendab nüüd tuletatavust, mitte lubatavust.

Selle muutmiseks propositsioonilise loogika loogiliste konstandite semantikaks väidab von Kutschera järgmist: Bivalentsusest loobumisel ei saa me enam kasutada klassikalisi tõe ja väärtuse määramisi aatomi valemitele. Selle asemel võime kasutada arvutusi, mis tõestavad või lükkavad ümber aatomi laused. Veelgi enam, kuna kalkulid ei tekita mitte ainult tõestusi või ümberlükkamisi, vaid ka meelevaldseid tuletatavussuhteid, on mõte alustada otseselt tuletussüsteemis tuletatavusega ja laiendada seda loogilisi ühendusi iseloomustavate reeglitega. Selle jaoks annab von Kutschera järjestikuse arvutuse reeglitega n -ariliste propositsiooniliste ühenduste sisseviimiseks pärimisse ja eelnevasse, saades järjestikuse süsteemi üldistatud propositsiooniliste ühenduste jaoks. Seejärel jätkub Von Kutschera näitel, et nii määratletud üldistatud ühendusi saab kõiki väljendada intuitionistliku loogika standardühenduste abil (konjunktsioon, disjunktsioon, implikatsioon, absurd).

2.1.3 Loomulik mahaarvamine kõrgema taseme reeglitega

Suvaliste loogiliste konstantide reeglite üldskeemi väljatöötamise programmis tegi Schroeder-Heister (1984) ettepaneku, et loogiliselt keeruline valem peaks väljendama reeglisüsteemide sisu või ühist sisu. See tähendab, et mitte sissejuhatuseeskirju ei peeta põhilisteks, vaid tingimuste määratlemise tagajärgedeks. Reegel R on kas valemiga A või on vormistatud R 1, …, R n ⇒ A, kus R 1, …, R non ise reeglid. Need niinimetatud “kõrgema taseme reeglid” üldistavad ideed, et reeglid võivad vabastada eeldused juhul, kui need eeldused võivad ise olla reeglid. Standardsete loogiliste konstantide jaoks tähendab see, et A ∧ B väljendab paari (A, B) sisu; A → B väljendab reegli A ⇒ B sisu; A ∨ B väljendab A ja B ühist sisu; ja absurdsus ⊥ väljendab reeglisüsteemide tühja perekonna ühist sisu. Suvaliste n -ariliste ettepanekuliste ühenduste korral saadakse loomulik deduktsioonisüsteem koos üldiste sissejuhatus- ja kõrvaldamisreeglitega. Need üldised ühendused näivad olevat standardsetena määratletavad, kinnitades intuitiivsete standardsete ühenduste väljenduslikku täielikkust.

Lisalugemist:

Lorenzeni lähenemisviisi kohta seoses Prawitzi stiilis tõenditeoreetilise semantikaga: Schroeder-Heister (2008a). Ekspressiivse terviklikkuse laienditeks von Kutschera stiilis: Wansing (1993a).

2.2. Tuletuste semantika sissejuhatuse reeglitel

2.2.1 Inversiooni põhimõtted ja harmoonia

Oma uurimustes loogilise deduktsiooni kohta teeb Gentzen mõned, tänapäeval väga sageli tsiteeritud programmilised märkused loomuliku deduktiivsuse sissejuhatuse ja elimineerimise järelduste vahelise semantilise seose kohta.

Sissejuhatused esindavad justkui asjaomaste sümbolite „määratlusi” ja elimineerimised pole lõppkokkuvõttes üksnes määratluste tagajärjed. Seda fakti võib väljendada järgmiselt: Sümboli elimineerimisel võime kasutada valemit, mille terminaalsümboliga me puutume, ainult „selles tähenduses, mis selle sümboli kasutuselevõtt võimaldab”. (Gentzen, 1934/35, lk 80)

See ei saa muidugi tähendada, et kõrvaldamisreeglid on sissejuhatuseeskirjadest tuletatavad selle sõna otseses tähenduses; tegelikult nad pole. See võib tähendada ainult seda, et neid saab mingil viisil õigustada.

Neid ideid täpsustades peaks olema võimalik E-järeldusi teatud nõuete alusel kuvada nende vastavate I-järelduste ainulaadsete funktsioonidena. (ibid., lk 81)

Gentzeni programmi aluseks on see, et meil on olemas sissejuhatusreeglite vormis määratlused ja mingisugune semantiline arutluskäik, mis „teatud nõuete” abil valideerib kõrvaldamise reeglid.

Võttes vastu Lorenzeni termini ja kohandades selle alusideed loodusliku deduktsiooni kontekstiga, sõnastas Prawitz (1965) “inversiooni põhimõtte”, et muuta Gentzeni märkused täpsemaks:

Olgu α elimineerimisreegli rakendamine, mille tagajärjel on B. Seejärel sisaldavad mahaarvamised, mis vastavad α peamise eelduse saamiseks piisavale tingimusele […], koos kombineeritud α väiksemate eeldustega (kui need on olemas), juba B lahusega; B lahutamine on seega saadav otse antud lahustest ilma a-d lisamata. (lk 33)

Piisavad tingimused antakse siin vastavate sissejuhatusreeglite eeldustes. Seega ütleb ümberpööramispõhimõte, et elimineerimisreegli järelduse võib saada ilma kõrvaldamisreeglit rakendamata, kui selle peamine eeldus on tuletatud sissejuhatuse reegli kasutamisel viimases etapis, mis tähendab, et kombinatsioon

Ma järeldan
A
{D i } E-järeldused
B

astmeid, kus {D i } tähistab (võib-olla tühja) väiksemate eelduste deduktsioonide nimekirja, saab vältida.

Sissejuhatuse ja kõrvaldamise reeglite suhet kirjeldatakse sageli kui “harmooniat” või kui seda reguleerib “harmoonia põhimõte” (vt nt Tennant, 1978, lk 74). See terminoloogia pole ühtne ja mõnikord isegi mitte täiesti selge. See väljendab sisuliselt seda, mida mõeldakse ka “ümberpööramise” all. Isegi kui “harmoonia” on mõiste, mis viitab sümmeetrilisele seosele, mõistetakse seda sageli sissejuhatuseeskirjadel põhineva kontseptsiooni väljendusena, näiteks Read'i (2010) “üldises elimineerimise harmoonias” (ehkki mõnikord hõlmab see ka eliminatsioonipõhiseid kontseptsioone)). Mõnikord tähendab harmoonia seda, et ühendused on nende kasutuselevõtu või kaotamise reegleid arvestades teatud mõttes tugevaimad või nõrgemad. See idee põhineb Tennanti (1978) harmooniaprintsiibil,ning ka Popperi ja Koslowi struktuuriomadused (vt punkt 2.4). Inversiooniprintsiibis sõnastatud sissejuhatuse ja kõrvaldamise reeglite vaheline konkreetne seos välistab väidetavad järelduslikud määratlused, näiteks ühendvärvi määratlus, mis ühendab disjunktsiooni sissejuhatuse reegli konjunktiivi eemaldamise reegliga ja mis on põhjustanud jätkuvat arutelu järelduslike määratluste formaadi kohta (vt Humberstone, 2010).ja mis on põhjustanud jätkuvaid arutelusid järelduslike määratluste formaadi üle (vt Humberstone, 2010).ja mis on põhjustanud jätkuvaid arutelusid järelduslike määratluste formaadi üle (vt Humberstone, 2010).

2.2.2 Tõestatud teoreetiline paikapidavus

Tõestusteoreetiline semantika on domineeriv tõestusteoreetiline paikapidavus. Tehnilise kontseptsioonina töötas selle välja Prawitz (1971; 1973; 1974), muutes tõenditeoreetilise kehtivusmõiste, mis põhines Taiti (1967) ideedel ja mida algselt kasutati tugeva normaliseerimise tõestamiseks, semantiliseks kontseptsiooniks. Dummett andis sellele ideele palju filosoofilisi aluseid (vt Dummett, 1991). Peamiselt kehtivad objektid on tõestused kui argumentide esitused. Teises tähenduses võivad üksikud reeglid kehtida, kui need viivad kehtivatest tõenditest kehtivate tõenditeni. Selles mõttes on kehtivus pigem globaalne kui kohalik mõiste. See kehtib suvalise tuletise kohta antud aatomisüsteemist, mis määratleb aatomite tuletatavuse. Kui helistate tõendile, mis kasutab sissejuhatusreeglit viimases etapis, kanooniliseks, põhineb see kolmel järgmisel ideel:

  1. Suletud kanooniliste tõendite prioriteet.
  2. Suletud mittekanooniliste tõendite taandamine kanoonilisteks.
  3. Asendatud vaade avatud tõenditele.

Kuulutus 1: kehtivuse määratlus põhineb Gentzeni ideel, et sissejuhatuseeskirjad on iseenesestmõistetavad ja annavad loogilistele konstantidele nende tähenduse. Seda iseenesestmõistetavat funktsiooni kasutatakse ainult suletud tõendite puhul, mida peetakse esmaseks võrreldes avatud dokumentidega.

Kuulutus 2: mittekanoonilised tõestused on õigustatud nende taandamisega kanoonilisteks. Seega mängivad normaliseerimistõendites kasutatavad vähendamisprotseduurid (ümbersõidu vähendamine) üliolulist rolli. Kuna need õigustavad argumente, nimetatakse neid ka Prawitzi poolt õigustamiseks. See määratlus kehtib jällegi ainult kinniste tõendite puhul, mis vastavad suletud normaaltuletuste sissejuhatusele loomuliku deduktsiooni korral (vt punkt 1.3).

Kuulutus 3: lahtised tõendid on õigustatud nende suletud eksemplare arvesse võttes. Need suletud juhtumid saadakse asendades nende avatud eeldused suletud tõenditega ja nende avatud muutujad suletud tingimustega. Näiteks A-st pärit B tõend loetakse kehtivaks, kui kehtiv on iga suletud tõend, mis saadakse asendades avatud eelduse A suletud A-tõendiga. Sel viisil peetakse avatud eeldusi kinniste tõendite kohahoidjateks, sel põhjusel võime rääkida avatud tõendite asendavast tõlgendamisest.

See annab järgmise tõenditeoreetilise kehtivuse määratluse:

  1. Iga suletud tõend selle aluseks olevas aatomisüsteemis on kehtiv.
  2. Suletud kanoonilist tõendit loetakse kehtivaks, kui selle vahetud alamkindlustused kehtivad.
  3. Suletud mittekanoonilist tõestust loetakse kehtivaks, kui see taandub kehtivaks suletud kanooniliseks tõestuseks või suletud tõestuseks aatomisüsteemis.
  4. Avatud tõend loetakse kehtivaks, kui kehtiv on iga suletud tõend, mis saadakse, asendades selle avatud eeldused suletud tõenditega ja avatud muutujad suletud tingimustega.

Formaalselt tuleb seda määratlust seostada vaadeldava aatomisüsteemiga ja kaaluda põhjenduste kogumit (tõendusvähendusi). Lisaks mõistetakse tõendite all siin kehtivate tõendite kandidaate, mis tähendab, et nende koostamise reegleid ei ole fikseeritud. Need näevad välja nagu tõestuspuud, kuid nende üksikute sammude eelduste arv võib olla suvaline (piiratud) ja need võivad meelevaldsed eeldused välistada. Kehtivuse määratlus eristab need tõendusstruktuurid, mis antud vähendamismenetluste alusel on „tõelised” tõendid.

Kehtivust aatomisüsteemi iga valiku suhtes võib vaadelda loogilise kehtivuse üldistatud mõistena. Tegelikult, kui arvestada intuitsioonilise loogika standardseid redutseerimisi, kehtivad kõik intuitionistliku loogika tuletused sõltumata vaadeldavast aatomisüsteemist. See on semantiline korrektsus. Võib küsida, kas vastupidine seisukoht kehtib, nimelt. kas arvestades, et tuletus kehtib igas aatomisüsteemis, on intuitiivses loogikas olemas ka vastav tuletus. Seda, et intuitsiooniline loogika on selles mõttes täielik, tuntakse Prawitzi oletusena (vt Prawitz, 1973; Prawitz, 2013). Selle kohta pole siiski rahuldavaid tõendeid esitatud. Selle oletuse paikapidavuse kohta süsteemides, mis ületavad implikatiivse loogika, on tõsiseid kahtlusi. Igal juhul sõltub see kehtivuse mõiste täpsest sõnastusest, eriti aatomisüsteemide käitlemisest.

Ametlikuma määratluse ja kehtivust tõendavate üksikasjalike näidete ning Prawitzi oletuse kohta märkuste saamiseks vt

Lisa tõenditeoreetilise kehtivuse näidete kohta.

2.2.3 Konstruktiivse tüübi teooria

Martin-Löfi tüübiteooria (Martin-Löf, 1984) on juhtiv lähenemisviis konstruktiivses loogikas ja matemaatikas. Filosoofiliselt jagab see Prawitziga standardse tõenditeoreetilise semantika kolme põhieeldust, mida on mainitud jaotises 2.2.2: suletud kanooniliste tõendite prioriteetsus, suletud mittekanooniliste tõendite taandamine kanoonilisteks ja avatud tõestuste asendusvaade. Martin-Löfi tüüptiteoorial on aga vähemalt kaks iseloomulikku tunnust, mis ületavad tõenditeoreetilise semantika muid lähenemisviise:

  1. Tõendusobjektide arvestamine ning tõendite objektina ja demonstreerimise tõendite vahelise eristamine.
  2. Vaade moodustamise reeglitele on pigem tõestussüsteemile omane kui väliste reegliteni kuuluv.

Esimene mõte ulatub tagasi Curry-Howardi kirjavahetusse (vt de Groote, 1995; Sørensen ja Urzyczyn, 2006), mille kohaselt võib valemi A teatud tõestuse olemasolu kodeerida tõsiasjaks, et teatud termin t on tüüpi A, kusjuures valem A identifitseeritakse tüübiga A. Selle saab vormistada tüübimääramise kalkulatsioonis, mille avaldused on kujul t: A. Tõend t: A-st selles süsteemis võib lugeda nii, et see näitab, et t on tõend A-st. Martin-Löf (1995; 1998) on pannud selle filosoofilisse perspektiivi, eristades seda kahetist tõestustunnet järgmiselt. Esiteks on meil tõendid avalduste kohta kujul t: A. Neid avaldusi nimetatakse kohtuotsusteks, nende tõestusi nimetatakse demonstratsioonideks. Sellistes kohtuotsustes tähistab termin t väidet A. Tõestust viimases tähenduses nimetatakse ka tõendusobjektiks. Kohtuotsuse t: A demonstreerimisel demonstreerime, et t on väite A tõend (objekt). Selles kahekihilises süsteemis on demonstreerimiskihiks argumentatsiooni kiht. Erinevalt tõendusobjektidest on demonstratsioonidel episteemiline tähendus; nende otsused kannavad kinnistavat jõudu. Tõestuskiht on kiht, milles tähendusi selgitatakse: Paigutuse A tähendust seletatakse sellega, et öeldakse, mida loetakse tõendiks (objektiks) A jaoks. Kanooniliste ja mittekanooniliste tõendite eristamine on eristus ettepanekul ja mitte kohtuotsuse kihil. See eeldab teatavat selguse nõuet. Kui olen midagi tõestanud, ei pea mul olema minu käsutuses mitte ainult tõendusmaterjali õigustus, nagu Prawitzi kehtivuse mõistes,kuid samal ajal peab olema kindel, et see õigustus täidab oma eesmärki. Selle kindluse tagab demonstratsioon. Matemaatiliselt arendab see kahetine tõestustunne oma tegelikku jõudu alles siis, kui tüübid võivad ise sõltuda terminitest. Sõltuvad tüübid on Martin-Löfi tüüpi teooria ja sellega seotud lähenemisviiside põhikomponent.

Teine mõte muudab Martin-Löfi lähenemisviisi tugevalt kõigist teistest tõestusteoreetilise kehtivuse määratlustest erinevaks. Kriitiline erinevus näiteks Prawitzi protseduuril on see, et see ei ole oma olemuselt metalingvistiline, kus “metalingvistiline” tähendab seda, et esmalt täpsustatakse tõendusmaterjali ettepanekud ja kandidaadid ning seejärel fikseeritakse metakeelse määratluse abil, milline neist need kehtivad ja mis mitte. Pigem tulevad väited ja tõendid mängu ainult demonstratsioonide käigus. Näiteks kui eeldada, et miski on implikatsiooni A → B tõend, siis ei pea me tingimata näitama, et nii A kui ka B on otse moodustatud väited, vaid lisaks teadmisele, et A on väide, on meil vaja ainult teada, et B on väide, kui A on tõestatud. Pakkumise olemust väljendab konkreetne kohtuotsuse vorm, mis kehtestatakse samas demonstratsioonisüsteemis, mida kasutatakse selle kinnitamiseks, et pakkumine on tõestatud.

Martin-Löfi teoorias võtab tõenditeoreetiline semantika tugevalt ontoloogilise komponendi. Hiljutine arutelu käsitles küsimust, kas tõendusobjektidel on puhtalt ontoloogiline staatus või kas nad kodifitseerivad teadmisi, isegi kui need pole ise episteemilised teod.

Lisalugemist:

Inversiooniprintsiipide kohta vaata Schroeder-Heister (2007).

Tõestusteoreetilise harmoonia variantide kohta vaata Francez (2015) ja Schroeder-Heister (2016a). Prawitzi tõenditeoreetilise kehtivuse määratluse leiate Schroeder-Heister (2006).

Matin-Löfi tüübiteooria kohta lugege tüüptoteooria alast sissekannet, samuti Sommaruga (2000).

2.3 Clausali määratlused ja määratluspõhjendused

Tõestusteoreetiline semantika keskendub tavaliselt loogilistele konstantidele. Seda fookust ei seata kunagi kahtluse alla, ilmselt seetõttu, et seda peetakse nii ilmseks. Tõestusteoorias on aatomisüsteemidele pööratud vähe tähelepanu, ehkki on olnud Lorenzeni varasemat tööd (vt punkt 2.1.1), kus loogiliste reeglite põhjendus on manustatud suvaliste reeglite teooriasse, ja Martin-Löfi (1971) itereeritud induktiivsete definitsioonide teooria, kus pakutakse välja aatomivalemite sissejuhatuse ja elimineerimise reeglid. Loogikaprogrammeerimise tõus on seda vaatenurka laiendanud. Tõenditeoreetilisest vaatepunktist on loogiline programmeerimine aatomi mõttekäigu teooria aatomite klausiaalsete määratluste osas. Definitsiooniline refleksioon on lähenemisviis tõenditeoreetilisele semantikale, mis võtab selle väljakutse vastu ja püüab üles ehitada teooria, mille rakendusala ületab loogilisi konstante.

2.3.1 Loogilise programmeerimise väljakutse

Loogilises programmeerimises käsitleme vormi programmisätteid

A ⇐ B 1,…, B m

mis määratlevad aatomi valemeid. Selliseid klausleid võib loomulikult tõlgendada nii, et need kirjeldavad aatomite sisseviimiseeskirju. Tõestusteoreetilise semantika seisukohast on olulised järgmised kaks punkti:

(1) Loogiliselt liitvalemite sissejuhatuseeskirju (klausleid) ei eristata põhimõtteliselt aatomite sissejuhatuseeskirjadest (klauslitest). Loogikaprogrammeerimise tõlgendamine tõestus teoreetiliselt motiveerib tõenditeoreetilise semantika laiendamist suvalistele aatomitele, mis annab semantika palju laiema rakendustevaldkonnaga.

(2) Programmklauslid ei ole tingimata põhjendatud. Näiteks võib selle kehas esineda klausli pea. Põhjendatud programmid on vaid teatud tüüpi programmid. Suvaliste lausete kasutamine ilma lisanõueteta loogikaprogrammeerimises on motivatsioon järgida sama ideed tõestusteoreetilises semantikas, tunnistades suvalisi sissejuhatuseeskirju ja mitte ainult erivormi reegleid ja eriti mitte tingimata neid, mis on hästi - leitud. See viib mõistese vabaduse idee, mis on loogilise programmeerimise nurgakivi, üle semantika, laiendades taas tõestusteoreetilise semantika rakendusala.

Idee pidada sissejuhatuse reegleid aatomite tähendust andvateks reegliteks on tihedalt seotud induktiivsete määratluste teooriaga selle üldisel kujul, mille kohaselt induktiivsed määratlused on reeglisüsteemid (vt Aczel, 1977).

2.3.2 Definitsiooniline peegeldus

Definitsioonilise peegelduse teooria (Hallnäs, 1991; Hallnäs, 2006; Hallnäs ja Schroeder-Heister, 1990/91; Schroeder-Heister, 1993) võtab loogikaprogrammeerimisest väljakutse ja pakub tõenditeoreetilist semantikat mitte ainult loogiliste konstantide jaoks, vaid suvaliste väljendite jaoks, mille jaoks võib anda klausli määratluse. Formaalselt algab see lähenemisviis klauslite loendiga, mis on vaadeldav määratlus. Igal klauslil on vorm

A ⇐ Δ

kus pea A on aatomivalem (aatom). Keha Δ on kõige lihtsamal juhul aatomite B 1,…, B m loetelu, sel juhul näeb määratlus välja kindla loogikaprogrammi. Me kaalume sageli laiendatud juhtumit, kus Δ võib sisaldada ka mõnda strukturaalset tähendust 'ja mõnikord isegi mõnda strukturaalset universaalset implikatsiooni, mida sisuliselt käsitletakse asendamise piiramisega. Kui definitsioonil A on vorm

siis A-l on järgmised sissejuhatuse ja eemaldamise reeglid

Δ 1 · · Δ n A A

1] n]
A C · · · C
C

Sissejuhatusreeglid, mida nimetatakse ka määratlusliku sulgemise reegliteks, väljendavad klausleid „piki“. Kõrvaldamise reeglit nimetatakse definitsioonilise peegelduse põhimõtteks, kuna see kajastab määratlust tervikuna. Kui Δ 1,…, Δ nkurnata kõik võimalikud tingimused, et genereerida A vastavalt antud määratlusele, ja kui igaüks neist tingimustest eeldab sama järeldust C, siis hõlmab A ka seda järeldust. Kui klausli määratlust peetakse induktiivseks määratluseks, võib seda põhimõtet vaadelda kui induktiivsetes määratlustes äärmusliku klausli väljendamist: A-d ei defineeri midagi muud peale antud klauslite. Ilmselt on definitsiooniline peegeldus käsitletud inversiooniprintsiipide üldistatud vorm. Ta arendab oma tõelist jõudu definitsioonikontekstides vabade muutujatega, mis lähevad kaugemale puhtalt propositsioonilistest arutluskäikudest, ja kontekstides, mis pole piisavalt põhjendatud. Mittetähendusliku määratluse näide on aatomi R määratlemine oma eituse abil:

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

Seda näidet käsitletakse üksikasjalikult dokumendis

Täiendav mõiste peegelduse ja paradokside kohta.

Lisalugemist:

Mittenõuetekohasuse ja paradokside kohta vaata sissekandeid eneseviidete ja Russelli paradokside kohta, samuti viidatud lisas esitatud viiteid.

2.4 Loogiliste konstantide struktuuriline iseloomustus

Loogiliste konstantide „struktuurseks iseloomustamiseks” võib olla palju ideesid ja tulemusi, kus „struktuurne” tähendab siin nii tõestusteoreetilist mõistet “struktuurireeglid” kui ka raamistikku, mis kannab teatud struktuuri, kus seda raamistikku kirjeldatakse taas teoreetiliselt. Mõned selle autorid kasutavad semantilist sõnavara ja arvavad vähemalt kaudselt, et nende teema kuulub tõenditeoreetilise semantika juurde. Teised eitavad neid varjundit sõnaselgelt, rõhutades, et neid huvitab iseloomustus, mis kinnitab konstandi loogilisust. Küsimus “Mis on loogiline konstant?” saab vastata tõenditeoreetiliselt, isegi kui konstantide endi semantika on tõepõhine:Nimelt nõudes, et (võib-olla tõega tinglikult määratletud) konstandid näitaksid teatavat järelduslikku käitumist, mida saab kirjeldada tõestusteoreetiliselt. Kuna mõned autorid käsitlevad nende iseloomustamist samal ajal semantikana, on kohane mainida mõnda neist lähenemisviisidest.

Loogiliste konstantide suhtes kõige sõnatuim struktureerija, kes mõistab end selgesõnaliselt sellisena, on Koslow. Oma struktuuriloolises loogika teoorias (1992) töötab ta välja loogiliste konstandite teooria, milles ta iseloomustab neid teatud „implikatsioonisuhetega”, kus implikatsioonisuhe vastab umbkaudu Tarski mõttes lõplikule tagajärjesuhtele (mida jällegi saab kirjeldada järkjärgulise stiili süsteemi teatud struktuurireeglid). Koslow töötab välja struktuuriteooria täpses metamaatikas, mis ei täpsusta mingil moel objektide domeeni väljaspool antud aksioome. Kui antakse keel või mõni muu implikatsioonisidemega varustatud objektide domeen, saab loogiliste ühendite eristamiseks kasutada struktuurilist lähenemisviisi, kontrollides nende implikatiivseid omadusi.

Popper (1947a; 1947b) on oma varasemates loogika aluseid käsitlevates artiklites loogiliste konstantide järeldavaid iseloomustusi tõestatud-teoreetiliselt. Ta kasutab jadade arvutamist ja iseloomustab loogilisi konstante selliste jadade teatud tuletatavuse tingimustega. Tema terminoloogia viitab selgelt sellele, et ta kavatseb loogiliste konstantide tõenditeoreetilist semantikat, kuna ta räägib “järeldusmõistetest” ja “matemaatilise loogika triviaalsusest”, mis saavutatakse konstandite kirjeldamise teel. Ehkki tema esitlus pole vaba kontseptuaalsest ebatäpsusest ja vigadest, kaalus ta esimesena nende iseloomustamiseks loogiliste konstantide järjestikuses stiilis järelduslikku käitumist. See on seda tähelepanuväärsem, et ta polnud tõenäoliselt üldse,ega ole kindlasti täielikult teadlik Gentzeni järgnenud arvutusest ja Gentzeni edasistest saavutustest (ta oli siiski Bernaysiga kirjavahetuses). Enda arvamuse vastaselt saab tema teost paremini mõista kui katset konstantide loogilisust määratleda ja neid struktuurselt iseloomustada kui tõestusteoreetilist semantikat ehtsas tähenduses. Sellegipoolest ootas ta paljusid praegu tõenditeoreetilises semantikas levinud ideesid, näiteks loogiliste konstantide iseloomustamist teatud minimaalsus- või maksimumtingimuste abil sissejuhatuse või kõrvaldamise reeglite osas.kui tõestus-teoreetilise semantika tegelikus tähenduses. Sellegipoolest ootas ta paljusid praegu tõenditeoreetilises semantikas levinud ideesid, näiteks loogiliste konstantide iseloomustamist teatud minimaalsus- või maksimumtingimuste abil sissejuhatuse või kõrvaldamise reeglite osas.kui tõestus-teoreetilise semantika tegelikus tähenduses. Sellegipoolest ootas ta paljusid praegu tõenditeoreetilises semantikas levinud ideesid, näiteks loogiliste konstantide iseloomustamist teatud minimaalsus- või maksimumtingimuste abil sissejuhatuse või kõrvaldamise reeglite osas.

Kneale (1956) ja Hacking (1979) on oluliseks panuseks loogilisuse arutellu, mis iseloomustavad loogilisi konstante järeldavalt järjestikuste arvutusreeglite osas. Põhjaliku ülevaate loogilisusest pakub Došen (1980; 1989) loogiliste konstantide teoorias kirjavahemärkidena, väljendades loogilisel tasandil struktuuriomadusi. Ta mõistab loogilisi konstante, mida iseloomustavad teatud järjestuste kaherealised reeglid, mida saab lugeda mõlemas suunas. Näiteks konjunktsiooni ja disjunktsiooni iseloomustavad (klassikalises loogikas, koos mitme valemiga järgnevusega) kaherealised reeglid

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

Došen oskab anda iseloomustusi, mis hõlmavad modaaloogika süsteeme. Ta peab oma tööd otsesõnu panuseks loogilisuse arutellu, mitte tõenditeoreetilise semantika kontseptsiooni kujundamisse. Sambin jt mõistavad oma põhiloogikas (Sambin, Battilotti ja Faggian, 2000) selgesõnaliselt seda, mida Došen nimetab topeltjoone reegliteks reeglite andmise põhimõttelise tähendusena. Konjunktsiooni ja disjunktsiooni kaherealisi reegleid loetakse nende konstantide kaudsete definitsioonidena, mida mõne protseduuri abil saab muuta selgesõnaliseks järgneva stiili reegliks, millega oleme harjunud. Nii Sambin jt. kasutage sama lähtepunkti nagu Došen, kuid tõlgendage seda mitte konstantide käitumise struktuurilise kirjeldusena, vaid semantiliselt nende kaudse määratlusena (vt Schroeder-Heister, 2013).

Loogiliste konstantide ühtsele tõenditeoreetilisele iseloomustamisele on veel mitmeid lähenemisviise, mis kõik vähemalt puudutavad tõenditeoreetilise semantika küsimusi. Sellisteks teooriateks on Belnapi ekraaniloogika (Belnap, 1982), Wansingi infostruktuuride loogika (Wansing, 1993b), üldised tõendite redigeerimise süsteemid ja nende rakendused, näiteks Edinburghi loogiline raamistik (Harper, Honsell ja Plotkin, 1987) ja paljud järglased, mis võimaldab täpsustada mitmesuguseid loogilisi süsteeme. Pärast lineaarse ja üldisemalt alamstrukturaalse loogika esilekutsumist (Di Cosmo ja Miller, 2010; Restall, 2009) on loogikaga seotud erinevad lähenemisviisid, mis erinevad nende struktuurireeglite piirangute osas. Hiljutine eemaldus konkreetse loogika tegelikust väljatoomisest pluralistliku hoiaku suunas (vt ntBeall ja Restall, 2006), keda huvitab see, mida erinevatel loogikatel on ühist ilma mingit loogikat eelistamata, võib pidada nihkeks semantilisest õigustusest struktuuri iseloomustamise poole.

2.5 Kategoorikindluse teooria

Kategooria teooria kohta tõenditeooria osas on arvestatav kirjandus ning Lawvere, Lambeki jt (vt Lambek ja Scott, 1986 ning nendes sisalduvaid viiteid) põhjaliku töö põhjal võib kategooriat ennast pidada omamoodi abstraktse tõestusmaterjalina. teooria. Kui vaadelda kategoorias noolt A → B kui teatud tüüpi abstraktset tõendit B-st punktist A, on meil esitus, mis ületab B-i puhta tuletatavuse A-st (kuna nool omab individuaalsust), kuid ei käsitle selle tõendi süntaktiline struktuur. Intuitsionistlike süsteemide puhul jõuab kategoorilises vormis tõenditeoreetiline semantika tõenäoliselt kõige lähemale sellele, mis denatsiooniline semantika on klassikalisel juhul.

Üks kõige arenenumaid lähenemisviise kategoorilise tõestuse teooriale tuleneb Došenist. Ta pole mitte ainult edendanud kategooriliste meetodite kasutamist tõestusteoorias (nt Došen ja Petrić, 2004), vaid ka näidanud, kuidas tõestusteoreetilisi meetodeid saab kasutada kategooriateoorias endas (Došen, 2000). Kategooriloogika jaoks on tõenditeoreetilise semantika seisukohast kõige olulisem see, et kategooriloogikas tulevad nooled alati kokku identiteedisuhtega, mis tõestusteoorias vastab tõendite identiteedile. Sel moel puudutavad kategoorilise tõestusteooria ideed ja tulemused nn intentsionaalset tõestusteoreetilist semantikat, see tähendab tõendite uurimist kui omaette üksusi, mitte ainult kui vahendeid tagajärgede tuvastamiseks (Došen, 2006, 2016). Teine kategoorilise tõestusteooria eripära on see, et see on oma olemuselt hüpoteetiline, mis tähendab, et see algab hüpoteetilistest üksustest. Sel moel ületab see standardse, eriti kehtivuspõhise, tõenditeoreetilise semantika paradigma (vt allpool punkt 3.6).

Lisalugemist:

Popperi loogiliste konstantide teooria kohta vt Schroeder-Heister (2005).

Loogiliste konstantide ja nende loogilisuse kohta vaata kannet loogiliste konstantide kohta.

Kategooriliste lähenemisviiside kohta vaata kategooriateooria kannet.

3. Laiendid ja alternatiivid tavapärasele tõenditeoreetilisele semantikale

3.1 Kõrvaldamiseeskirjad on põhilised

Enamik lähenemisi tõenditeoreetilisele semantikale peavad sissejuhatuse reegleid põhilisteks, tähendusi andvateks või ennast õigustavateks, samas kui kõrvaldamisjäreldused on õigustatud antud sissejuhatuseeskirjade osas kehtivatena. Sellel kontseptsioonil on vähemalt kolm juuri: esimene on verifitseeriv tähendusteooria, mille kohaselt lause kinnitatavuse tingimused moodustavad selle tähenduse. Teine on idee, et me peame eristama seda, mis selle tähenduse annab, ja mis on selle tähenduse tagajärjed, kuna mitte kõik järelduslikud teadmised ei pruugi koosneda määratluste rakendamisest. Kolmas on väidete ülimuslikkus muude kõnetoimingute suhtes, näiteks eeldamine või eitamine, mis on kaudselt esitatud kõigis seni vaadeldavates lähenemisviisides.

Võiks uurida, kui kaugele inimene jõuab, kui tõestamisteoreetilise semantika aluseks võtta pigem sissejuhatuse reeglid kui eliminatsioonireeglid. Dummett (1991, ptk. 13) visandas mõned ideed tõenditeoreetilise semantika kujundamiseks, mis põhinevad pigem kõrvaldamisel kui sissejuhatusel, kuigi väga algelisel kujul. Kehtivuse täpsem määratlus, mis põhineb elimineerimise järeldustel, tuleneb Prawitzist (1971; 2007; vt ka Schroeder-Heister 2015). Selle peamine mõte on see, et suletud tõendit loetakse kehtivaks, kui kõrvaldamisreegli kohaldamine selle lõppvalemi suhtes on kehtiv tõend või kui see väheneb ühega. Näiteks implikatsiooni A → B suletud tõend kehtib juhul, kui mis tahes antud suletud A tõendi korral on modus ponensi kohaldamise tulemus

A → BA
B

nendele kahele tõendile on kehtiv tõend B kohta või taandatakse selliseks tõendiks. See kontseptsioon säilitab kaks Prawitzi stiilis tõenditeoreetilise semantika kolmest põhikomponendist (vt punkt 2.2.2): tõestuse vähendamise roll ja eelduste asendusvaade. Ainult sissejuhatustega lõppevate tõendite kanoonilisus muutub tõendite kanoonilisuseks, mis lõpevad eliminatsioonidega.

3.2 Eitamine ja eitamine

Standardne tõenditeoreetiline semantika on väitekeskne, kuna kinnitatavuse tingimused määravad loogiliste konstantide tähenduse. Kooskõlas intuitiivse käitumisviisiga loetakse valemi A eitust ¬A tavaliselt absurdsuseks A → ⊥, kus ⊥ on konstant, mida ei saa väita, st mille jaoks ei ole kindlustuse tingimust määratletud. See on eituse mõistmise „kaudne” viis. Kirjanduses on arutatud, mida von Kutschera (1969) järel võib nimetada “otseseks eitamiseks”. Selle abil saab aru eituse ühe koha primitiivsest operaatorist, keda ei saa või vähemalt ei saa taandada absurdsusele. See pole ka klassikaline eitus. Pigem järgib see reegleid, mis dubleerivad loogiliste konstantide jaoks tavalisi reegleid. Mõnikord nimetatakse seda lause eitamiseks,mõnikord ka “tugev eitus” (vt Odintsov, 2008). Tüüpilised reeglid eituse ~ A keelamiseks on

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

Põhimõtteliselt vastavad operaatori keeldumisreeglid kahekordse operaatori väitereeglitele. Uuritud on mitmeid eitamise loogikaid, eriti Nelsoni „konstruktiivse võltsuse” loogikat, mille motiveeris esmalt Nelson (1949) seoses teatud realiseeritavuse semantikaga. Põhitähelepanu on pööratud tema süsteemidele, mida hiljem nimetatakse N3 ja N4, mis erinevad vastuolu käsitlemise osas (N4 on N3 ilma igasuguse vastuolulise quodlibetita). Keeldudes mis tahes lähenemisviisi tõestusteoreetilisele semantikale, saab seda dubleerida, vahetades lihtsalt väiteid ja eitust ning pöördudes loogilistest konstantidest nende duaalide poole. Seejuures saadakse süsteem, mis põhineb ümberlükkamisel (= eitamise tõend), mitte tõendusmaterjalil. Seda võib mõista popperianliku vaate rakendamisel tõestusteoreetilisele semantikale.

Teine lähenemisviis oleks väidetekeskse tõenditeoreetilise semantika mitte dubleerimine eituskeskse ümberlükkamise-teoreetilise semantika kasuks, vaid ka väidete ja eitamise reeglite seose nägemine, mida juhib ümberpööramispõhimõte või definitsioonilise peegelduse põhimõte. omaette. See oleks põhimõte, mida võiks nimetada “väite-eituse-harmooniaks”. Kui tavapärases tõenditeoreetilises semantikas kontrollivad ümberpööramise põhimõtted väidete ja eelduste (või tagajärgede) suhet, siis nüüd reguleerib selline põhimõte väite ja eituse vahelist suhet. Arvestades A teatud määratlevaid tingimusi, siis öeldakse, et kõigi A-d defineerivate tingimuste eitamine viib A enda eitamiseni. Konjunktsiooni ja disjunktsiooni jaoks toob see kaasa ühised väidete ja eitamise reeglite paarid

A B ~ A ~ B
A ∨ B A ∨ B ~ (A ∨ B)
AB ~ A ~ B
A ∧ B ~ (A ∧ B) ~ (A ∧ B)

Seda ideed saab hõlpsasti üldistada mõistetavaks peegelduseks, andes mõttesüsteemi, milles väide ja eitus on omavahel seotud. Sellel on paralleelid traditsioonilisel opositsiooniväljal uuritud kohtuotsuse vormide deduktiivsete suhetega (Schroeder-Heister, 2012a; Zeilberger, 2008). Tuleb rõhutada, et eitaja on siin väline märk, mis näitab kohtuotsuse vormi, mitte aga loogiline operaator. See tähendab eriti, et seda ei saa korrata.

3.3 Harmoonia ja peegeldus järjestikuses kivil

Gentzeni järkjärguline kalkulatsioon näitab sümmeetriat parema ja vasaku sissejuhatuse reeglite vahel, mis soovitab otsida harmoonia põhimõtet, mis muudab selle sümmeetria oluliseks tõenditeoreetilise semantika jaoks. Selle nähtusega tegelemiseks on võetud vähemalt kolm joont. i) Sissejuhatusreegliteks peetakse kas paremat sissejuhatust või vasakut sissejuhatust. Vastupidised reeglid (vastavalt vasakpoolsed sissejuhatused ja parempoolsed sissejuhatused) on siis õigustatud, kasutades vastavaid elimineerimiseeskirju. See tähendab, et eelnevalt käsitletud meetodeid rakendatakse pigem tervete jadade, mitte jadade siseste valemite korral. Erinevalt neist valemitest ei ole jadad loogiliselt üles ehitatud. Seetõttu toetub see lähenemisviis definitsioonilisele läbimõtlemisele,mis kohaldab harmooniat ja inversiooni reeglite suhtes suvaliselt struktureeritud üksuste, mitte ainult loogiliste komposiitide puhul. Seda on jälitanud de Campos Sanz ja Piecha (2009). (ii) Parema ja vasaku sissejuhatuse reeglid tulenevad iseloomustamisest Došeni topeltjoone reeglite tähenduses (punkt 2.4), mida seejärel loetakse mingisuguse määratlusena. Kaherealise reegli ülalt alla suund on juba parempoolse või vasakpoolse sissejuhatuse reegel. Teise saab tuletada alt-üles suunast teatud põhimõtete abil. See on Sambini jt põhiloogika põhiline tähendusteoreetiline koostisosa (Sambin, Battilotti ja Faggian, 2000). (iii) Parempoolse ja vasaku sissejuhatuse reegleid peetakse jadadevahelise interaktsiooni väljendamiseks lõikereeglit kasutades. Arvestades kas parem- või vasakpoolseid reegleid,täiendavad reeglid väljendavad, et kõik, mis mingil viisil suhestub tema eeldustega, vastab ka järeldusele. See interaktsiooni idee on definitsioonilise peegelduse üldistatud sümmeetriline põhimõte. Seda võib pidada inversiooniprintsiibi üldistavaks, kasutades pigem interaktsiooni mõistet kui tagajärgede tuletatavust (vt Schroeder-Heister, 2013). Kõik kolm lähenemisviisi kehtivad järjestikuse kuldkivi jaoks selle klassikalisel kujul, jadajärgmises järgus võib olla rohkem kui üks valem, sealhulgas struktuuriliselt piiratud versioonid, mida on uuritud lineaarses ja muus loogikas. Seda võib pidada inversiooniprintsiibi üldistavaks, kasutades pigem interaktsiooni mõistet kui tagajärgede tuletatavust (vt Schroeder-Heister, 2013). Kõik kolm lähenemisviisi kehtivad järjestikuse kuldkivi jaoks selle klassikalisel kujul, jadajärgmises järgus võib olla rohkem kui üks valem, sealhulgas struktuuriliselt piiratud versioonid, mida on uuritud lineaarses ja muus loogikas. Seda võib pidada inversiooniprintsiibi üldistavaks, kasutades pigem interaktsiooni mõistet kui tagajärgede tuletatavust (vt Schroeder-Heister, 2013). Kõik kolm lähenemisviisi kehtivad järjestikuse kuldkivi jaoks selle klassikalisel kujul, jadajärgmises järgus võib olla rohkem kui üks valem, sealhulgas struktuuriliselt piiratud versioonid, mida on uuritud lineaarses ja muus loogikas.

3.4 Subatomiline struktuur ja loomulik keel

Isegi kui kaalume sarnaselt määratlusliku peegeldusega aatomite määratlemise reegleid, ei lagunda nende määratlemistingimused neid aatomeid tavaliselt. Wieckowski (2008; 2011; 2016) on pakkunud välja tõenditeoreetilise lähenemisviisi, mis võtab arvesse aatomilausete sisemist struktuuri. Ta kasutab aatomilausete sissejuhatuse ja elimineerimise reegleid, kus neid aatomilauseid ei taandata pelgalt teistele aatomilausetele, vaid alamloomade väljenditele, mis tähistavad predikaatide ja üksikute nimede tähendust. Seda võib pidada esimese sammuna tõenditeoreetilise semantika loomulike keelerakenduste poole. Järgmise sammu selles suunas on astunud Francez, kes töötas välja mitme ingliskeelse fragmendi jaoks tõenditeoreetilise semantika (vt Francez, Dyckhoff ja Ben-Avi, 2010; Francez ja Dyckhoff, 2010,Francez ja Ben-Avi 2015).

3.5 Klassikaline loogika

Tõestusteoreetiline semantika on intuitiivselt kallutatud. Selle põhjuseks on asjaolu, et loomulikul deduktsioonil kui selle eelistatud raamistikul on teatud omadused, mis muudavad selle eriti sobivaks intuitionistliku loogika jaoks. Klassikalise loodusliku mahaarvamise korral on ex falso quodlibet

A

asendatakse klassikalise reductio ad absurdum reegliga

[A → ⊥]
A

Lubades A järeldada → → discharge tühjendamist, õõnestab see reegel alamvormi põhimõtet. Peale selle, sisaldades nii ⊥ kui ka A → ⊥, viitab see kahele erinevale loogilisele konstandile ühes reeglis, nii et loogilisi konstante enam ei eraldata. Lõpuks ei järgi see elim elimineerimise reeglina sissejuhatuste ja eliminatsioonide üldist mustrit. Selle tagajärjel hävitab see sissejuhatusvormi omaduse, et iga suletud tuletuse saab taandada selliseks, mis kasutab sissejuhatuse reeglit viimases etapis.

Klassikaline loogika sobib väga hästi mitme järjestikuse järjestikuse arvutusega. Seal ei vaja me täiendavaid põhimõtteid peale nende, mida eeldatakse intuitionistlikul juhul. Klassikalise loogika saamiseks piisab vaid strukturaalsest eripärast, mis lubab kasutada mitu valemit. Kuna parempoolsete sissejuhatuste ja vasakpoolsete sissejuhatuste vahelise harmoonia vahelise kooskõla loomiseks on usutavaid lähenemisviise (vt punkt 3.3), näib klassikaline loogika olevat täiesti õigustatud. Kuid see on veenev ainult siis, kui arutluskäik on sobivalt kujundatud mitme järeldusega protsessiks, isegi kui see ei vasta meie tavapraktikale, kus keskendume üksikutele järeldustele. Võiks proovida arendada sobivat intuitsiooni, väites, et mitmete järelduste põhjendamine piiritleb tõde peitvat valdkonda, selle asemel et luua ühtne väide tõeseks. Seda intuitsiooni on aga raske säilitada ja seda ei saa ilma tõsiste raskusteta ametlikult kinni hoida. Filosoofilised lähenemised, nagu näiteks Shoesmith ja Smiley (1978), ja tõenditeoreetilised lähenemised, näiteks tõestusvõrgud (vt Girard, 1987; Di Cosmo ja Miller, 2010), on katsed selles suunas.

Sissejuhatava vormi omaduse ebaõnnestumise põhiliseks põhjuseks klassikalises loogikas on disjunktsiooniseadustele omane indeterminism. A ∨ B võib tuletada nii A-st kui ka B-st. Seega, kui disjunktsiooniseadused oleksid A ∨ B järeldamise ainus viis, tähendaks klassikalise loogika põhiprintsiibiks oleva A ¬ ¬ A tuletatavus kas A või ¬ A, mis on absurdne. Väljapääs sellest raskusest on kaotada indeterministlik disjunktsioon ja kasutada selle asemel klassikalist de Morgani ekvivalenti ¬ (¬ A ¬ B). See viib sisuliselt loogikani ilma korraliku disjunktsioonita. Kvantifikaatori korral poleks olemas ka korralikku eksistentsiaalset kvantifikaatorit, kuna ∃ xA mõistetakse ¬∀ x ¬ A tähenduses. Kui keegi on valmis seda piirangut aktsepteerima, saab klassikalise loogika jaoks sõnastada teatud harmoonia põhimõtted.

3.6 Hüpoteetiline arutluskäik

Tõenditeoreetilise semantika standardsed lähenemisviisid, eriti Prawitzi kehtivuspõhine lähenemisviis (punkt 2.2.2), võtavad põhilistena suletud tuletusi. Avatud tuletuste kehtivust määratletakse kui kehtivuse ülekandmist eelduste suletud tuletistelt väite suletud tuletusteni, kus viimane saadakse asendades suletud tuletuse avatud oletusega. Seetõttu, kui suletud tuletisi nimetatakse kategoorilisteks ja avatud tuletisi hüpoteetilisteks, võib seda lähenemist iseloomustada kahe põhimõttelise ideena: (I) kategoorilise ülimuslikkus hüpoteetilise ees, (II) tagajärje ülekandevaade. Neid kahte eeldust (I) ja (II) võib vaadelda kui standardsemantika dogmasid (vt Schroeder-Heister 2012c). „Tavaline semantika” ei tähenda siin ainult standardset tõestusteoreetilist semantikat,aga ka klassikalist mudelteoreetilist semantikat, kus eeldatakse ka neid dogmasid. Alustatakse tõe määratlusega, mis on kategooriline mõiste, ja määratletakse tagajärg, hüpoteetiline kontseptsioon, kui tõe edastamine tingimustest tagajärjele. Sellest vaatenurgast vahetavad konstruktiivne semantika, sealhulgas tõenditeoreetiline semantika tõe kontseptsiooni ehituse või tõestuse mõistega ja tõlgendab “edastamist” konstruktiivse funktsiooni või protseduuri mõttes, kuid jätab raamistiku muul viisil puutumata.konstruktiivne semantika, sealhulgas tõenditeoreetiline semantika, vahetab tõe kontseptsiooni ehituse või tõestuse mõistega ja tõlgendab „edastamist” konstruktiivse funktsiooni või protseduuri mõttes, kuid jätab raamistiku muul viisil puutumata.konstruktiivne semantika, sealhulgas tõenditeoreetiline semantika, vahetab tõe kontseptsiooni ehituse või tõestuse mõistega ja tõlgendab „edastamist” konstruktiivse funktsiooni või protseduuri mõttes, kuid jätab raamistiku muul viisil puutumata.

Nendes dogmades pole põhimõtteliselt midagi valesti. Siiski on nähtusi, mida on tavaraamistikus keeruline käsitleda. Selliseks nähtuseks on põhjendamatus, eriti ringlus, kus meil võivad olla tõe ja tõestatavuse edastamata tagajärjed. Teine nähtus on strukturaalsed erinevused, mille puhul on ülioluline kaasata eelduste struktureerimine juba algusest peale. Veelgi enam, ja see on kõige olulisem, võiksime asju teatud viisil määratleda, teadmata ette, kas meie määratlus või määratluste ahel on hästi põhjendatud. Esiteks ei kaasata me endi algatatava definitsiooni metalingvistilisse uurimisse, vaid tahaksime kohe mõtlema hakata. See probleem ei muutu, kui piirduda loogiliste konstanditega,kus määratlevad reeglid on triviaalselt hästi põhjendatud. Kuid probleem ilmneb kohe, kui kaaluda keerulisemaid juhtumeid, mis ületavad loogilisi konstante.

Seetõttu on mõttekas liikuda teises suunas ja alustada hüpoteetilise tagajärje kontseptsiooniga, st iseloomustada tagajärge otse, taandamata seda kategooriliseks juhtumiks. Filosoofiliselt tähendab see, et kategooriline mõiste on hüpoteetilist piirav mõiste. Klassikalisel juhul oleks tõde tagajärgi piirav juhtum, nimelt tagajärg ilma hüpoteesideta. See programm on tihedalt seotud kategoorilise tõenditeooria lähenemisviisiga (punkt 2.5), mis põhineb hüpoteetiliste olemite (“nooled”) ülimuslikkusel. Formaalselt eelistaks see järjestikust arvutamist loodusliku deduktsiooni asemel, kuna järjestikune arvutus võimaldab vasakpoolse sissejuhatuse reeglite abil manipuleerida jada oletuskülge.

3.7 Intensiivne tõenditeoreetiline semantika

Nagu esimeses osas (1.1) mainitud, on tõenditeoreetiline semantika oma olemuselt intensiivne, kuna teda huvitavad tõendid, mitte ainult tõestatavus. Tõenditeoreetilise semantika jaoks pole oluline mitte ainult see, kas B tuleneb A-st, vaid ka see, kuidas saame kindlaks teha, et B tuleneb A-st. Teisisõnu on tõendite identiteet oluline küsimus. Ehkki see on esmapilgul ilmne ja tõenditeoreetilised semantikud nõustuvad selle abstraktse väitega tavaliselt, on tõenditeoreetilise semantika praktika sageli erinev ja tõendite identiteedi teema on palju unarusse jäetud. Väga sageli juhtub, et tuvastatakse võrdselt jõulised reeglid. Näiteks kui arutatakse harmoonia põhimõtteid ja peetakse silmas konjunktsiooni standardset sissejuhatusreeglit

AB
A ∧ B

paljud tõenditeoreetilised semantikud pidasid ebaoluliseks seda, kas keegi valib projektsioonide paari

A ∧ B A ∧ B
A B

või paar

A ∧ B A ∧ BA
A B

kui konjunktsiooni elimineerimise reeglid. Teist reeglipaari peetakse sageli projektsioonide paari keerukamaks variandiks. Intensiivsuse seisukohast pole need kaks reeglipaari siiski identsed. Nende tuvastamine vastab A ∧ B ja A ∧ (A → B) tuvastamisele, mis on ainult laiend, kuid mitte tahtlikult õige. Nagu Došen on sageli väitnud (nt Došen 1997, 2006), on sellised valemid nagu A ∧ B ja A ∧ (A → B) ekvivalentsed, kuid mitte isomorfsed. Siin tähendab „isomorfne” seda, et ühe valemi tõestamisel teisest ja vastupidi, saame nende kahe tõestuse kombineerimise teel identiteeditõendi. Selle näite puhul see nii pole.

Selle idee teostamine viib harmoonia ja inversiooni põhimõteteni, mis erinevad tavapärastest. Kuna harmoonia ja inversioon on tõenditeoreetilise semantika keskmes, puudutatakse paljusid selle küsimusi. Intensiivsuse teema tõsiseks võtmine võib muuta palju tõenditeoreetilise semantika valdkondi. Ja kuna tõendite identiteet on kategoorilise tõestuse teooria põhiteema, tuleb viimastele tõenditeoreetilise semantika osas pöörata suuremat tähelepanu kui praegu.

Lisalugemist

Eituse ja eituse kohta vaata Tranchini (2012b); Wansing (2001).

Looduskeele semantika kohta vaata Francez (2015).

Klassikalise loogika kohta vaata kirjet klassikalise loogika kohta.

Hüpoteetilise põhjenduse ja intensiivse tõestuse teoreetilise semantika kohta vaata Došen (2003, 2016) ja Schroeder-Heister (2016a).

4. Järeldus ja väljavaated

Standardne tõenditeoreetiline semantika on praktiliselt eranditult hõivatud loogiliste konstantidega. Loogikalistel konstantidel on keskne roll mõttekäikudes ja järeldustes, kuid need pole kindlasti ainuõiguslikud ja võib-olla isegi mitte kõige tüüpilisemad entiteedid, mida saab järeldada. Vaja on raamistikku, mis käsitleks järeldusmõisteid laiemas tähenduses ja hõlmaks nii loogilisi kui ka loogilisi väljundimääratlusi. Mõiste meelevaldsete definitsioonireeglite (vt punkt 2.3.2) ja ka loomuliku keele rakenduste (vt 3.4) määratluse peegelduse kohta osutab selles suunas, kuid võib ette kujutada ka kaugemaid mõisteid. Lisaks on harmooniale, ümberpööramispõhimõtetele, määratlusele tuginev peegeldus jms keskendumine mõnevõrra eksitav,kuna võib arvata, et tõenditeoreetiline semantika koosneb ainult sellest. Tuleb rõhutada, et juba aritmeetika osas on lisaks inversioonile vaja tugevamaid põhimõtteid. Vaatamata nendele piirangutele on tõenditeoreetiline semantika juba saavutanud väga olulisi saavutusi, mis suudavad võistelda semantika laiema lähenemisviisiga.

Bibliograafia

  • Aczel, Peter (1977). “Sissejuhatus induktiivsetesse mõistetesse”, Mathematical Logic Handbook, John Barwise (toim), Amsterdam: Põhja-Holland, lk 739–782.
  • Beall, JC ja Greg Restall (2006). Loogiline paljusus, Oxford: Oxford University Press.
  • Belnap, Nuel D. (1982). “Kuva loogika”, ajakiri Philosophical Logic, 11: 375–417.
  • Brandom, Robert B. (2000). Liigesepõhjused: sissejuhatus inferentsialismi, Cambridge Mass: Harvard University Press.
  • de Campos Sanz, Wagner ja Thomas Piecha (2009). “Inversioon mõisteliselt peegelduse ja loogiliste reeglite lubatavuse kaudu”, sümboolse loogika ülevaade, 2: 550–569.
  • –––, Thomas Piecha ja Peter Schroeder-Heister (2014). “Konstruktiivne semantika, reeglite lubatavus ja Peirce'i seaduse kehtivus”, IGPLi loogikaajakiri, 22: 297–308.
  • de Groote, Philippe, toim. (1995). Curry-Howardi isomorfism, Cahiers du Centre de Logique, 8. köide, Academia-Bruyland.
  • Di Cosmo, Roberto ja Dale Miller (2010). “Lineaarne loogika”, Stanfordi filosoofia entsüklopeedia (2010. aasta sügisel väljaanne), Edward N. Zalta (toim), URL =
  • Došen, Kosta (1980). Loogilised konstandid: essee tõestusteoorias, D. Phil. Lõputöö Oxfordi ülikooli filosoofia osakonnas.
  • ––– (1989). “Loogilised konstandid kui kirjavahemärgid”, Notre Dame Journal of Formal Logic, 30: 362–381.
  • ––– (1997). “Loogiline tagajärg: stiilimuutus”, autorid: Dalla Chiara, ML, K. Doets, D. Mundici, J. van Benthem (toim.), Loogika ja teaduslikud meetodid: kümnenda rahvusvahelise loogikakongressi esimene köide, metoodika ja teadusfilosoofia, Firenze, august 1995, Dordrecht: Kluwer, 289–311.
  • ––– (2000). Lõika eliminatsioon kategooriates, Berliin: Springer.
  • ––– (2003). “Tõestamiste identiteet, mis põhineb normaliseerimisel ja üldisusel”, Sümboolse loogika bülletään, 9: 477–503.
  • ––– (2006). “Mahaarvamise mudelid”, koosseisus: Kahle ja Schroeder-Heister, toim. (2006), lk 639–657.
  • ––– (2016). “Kategooriate radadel”, osades: Piecha ja Schroeder-Heister, toim. (2016b), lk 65–77.
  • ––– ja Zoran Petrić (2004). Tõestatud teoreetiline sidusus, London: kolledži väljaanded.
  • Dummett, Michael (1991). Metafüüsika loogiline alus, London: Duckworth.
  • Francez, Nissim (2015). Tõenditeoreetiline semantika, London: kolledži väljaanded.
  • ––– ja Gilad Ben-Avi (2015). “Üldistatud kvantifikaatorite tõestatud teoreetiline rekonstrueerimine”, Journal of Semantics, 32: 313–371.
  • ––– ja Roy Dyckhoff (2010). Looduskeele fragmendi tõestusteoreetiline semantika, keeleteadus ja filosoofia, 33: 447–477.
  • –––, Roy Dyckhoff ja Gilad Ben-Avi (2010). “Tõendav-teoreetiline substantsiaalsete fraaside semantika”, Studia Logica, 94: 381–401.
  • Gentzen, Gerhard (1934/35). “Untersuchungen über das logische Schließen”, Mathematische Zeitschrift, 39: 176–210, 405–431; Ingliskeelne tõlge Gerhard Gentzeni kogutud paberites, ME Szabo (toim), Amsterdam: Põhja-Holland, 1969, lk 68–131.
  • Girard, Jean-Yves (1987). “Lineaarne loogika”, teoreetiline arvutiteadus, 50: 1–102.
  • Häkkimine, Ian (1979). “Mis on loogika?”, Ajakiri Filosoofia, 76: 285–319.
  • Hallnäs, Lars (1991). “Osalised induktiivsed määratlused”, Teoreetiline arvutiteadus, 87: 115–142.
  • ––– (2006). “Üldmõisteteooria tõenditeoreetilise aluse kohta”, Synthese, 148: 589–602.
  • Hallnäs, Lars ja Peter Schroeder-Heister (1990/91). „Tõenditeoreetiline lähenemine loogikaprogrammeerimisele: I. Klauslid reeglina. II. Programmid määratlustena”, Journal of Logic and Computation, 1: 261–283, 635–660.
  • Harper, Robert, Furio Honsell ja Gordon Plotkin (1987). “Raamistik loogika määratlemiseks”, Arvutimasinate liidu ajakiri, 40: 194–204.
  • Humberstone, Lloyd (2010). “Lauseühendused formaalses loogikas”, Stanfordi filosoofia entsüklopeedia (2010. aasta suve väljaanne), Edward N. Zalta (toim.), URL =
  • Jaśkowski, Stanisław (1934). “Formaalse loogika suhet käsitlevate reeglite kohta”, Studia Logica, 1: 5–32 (kordustrükk S. McCall (toim)), Poola loogika 1920–1939, Oxford 1967, lk 232–258.
  • Jäger, Gerhard ja Robert F. Stärk (1998). “Loogikaprogrammide tõestatud teoreetiline raamistik”, tõestusteooria käsiraamat, Samuel R. Buss (toim), Amsterdam: Elsevier, lk 639–682.
  • Kahle, Reinhard ja Peter Schroeder-Heister, toim. (2006). Tõestusteoreetiline semantika, Synthese'i erinumber, köide 148.
  • Kneale, William (1956). „Loogika provints”, kaasaegne Briti filosoofia, HD Lewis (toim), London: Allen ja Unwin, lk 237–261.
  • Koslow, Arnold (1992). Struktuuristlik loogikateooria, Cambridge: Cambridge University Press.
  • Kreisel, Georg (1971). “Tõendusteooria II ülevaade”, Skandinaavia teise loogikasümpoosioni kogumikud, JE Renstad (toim), Amsterdam: Põhja-Holland, lk 109–170.
  • Kremer, Philip (2009). “Tõe revideerimise teooria”, Stanfordi filosoofia entsüklopeedia (2009. aasta kevade väljaanne), Edward N. Zalta (toim), URL =
  • Kreuger, Per (1994). “Aksioomid määratletavates kalkulites”, loogikaprogrammeerimise laiendid: 4. rahvusvahelise seminari toimetised, ELP'93, St. Andrews, Suurbritannia, märts / aprill 1993 (loenguteatised arvutiteaduses, Voluem 798), Roy Dyckhoff (toim), Berliin: Springer, lk 196–205.
  • Lambek, J. ja PJ Scott (1986). Sissejuhatus kõrgema järgu kategoorilisse loogikasse, Cambridge: Cambridge University Press.
  • Lorenzen, Paul (1955). Einführung in die operative Logik und Mathematik, Berliin: Springer; 2. trükk, 1969.
  • Martin-Löf, Per (1971). „Hauptsatz iteratiivsete induktiivsete määratluste intuitiivse teooria jaoks“, Teise Skandinaavia loogikasümpoosioni toimetused, JE Fenstad (toim), Amsterdam: Põhja-Holland, lk 179–216.
  • ––– (1984). Intuitionistlik tüüpi teooria, Napoli: Bibliopolis.
  • ––– (1995). “Verifikatsioon siis ja praegu”, aluspõhjaline arutelu: keerukus ja konstruktiivsus matemaatikas ja füüsikas, Werner DePauli-Schimanovich, Eckehart Köhler ja Friedrich Stadler (toim), Dordrecht: Kluwer, lk 187–196.
  • ––– (1998). “Tõde ja teadlikkus: Michael Dummeti C ja K põhimõttest”, Tõde matemaatikas, Harold G. Dales ja Gianluigi Oliveri (toim), Oxford: Clarendon Press, lk 105–114.
  • Negri, Sara ja Jan von Plato (2001). Struktuuride tõestusteooria, Cambridge: Cambridge University Press.
  • Nelson, David (1949). “Konstrukteeruv võltsing”, Journal of Symbolic Logic, 14: 16–26.
  • Odintsov, Sergei P. (2008). Konstruktiivsed eitus ja parakonsistentsus, Berliin: Springer.
  • Piecha, Thomas (2016). “Tõestusteoreetilise semantika terviklikkus”. Osades: Piecha ja Schroeder-Heister, toim. (2016b), lk 231–251.
  • –––, Wagner de Campos Sanz ja Peter Schroeder-Heister (2015). “Tõestusteoreetilise semantika täielikkuse ebaõnnestumine”, Journal of Philosophical Logic, 44: 321–335.
  • ––– ja Peter Schroeder-Heister (2016a). “Aatomisüsteemid tõestusteoreetilises semantikas: kaks lähenemisviisi”, autorid: Redmond, J., OP Martins, Á. N. Fernández Epistemoloogia, teadmised ja koostoime mõju, Cham: Springer, lk 47–62.
  • ––– ja Peter Schroeder-Heister, toim. (2016b). Tõestusteoreetilise semantika edasiminek, Cham: Springer (avatud juurdepääs)
  • Popper, Karl Raimund (1947a). “Loogika ilma oletusteta”, Aristotelese Seltsi Toimetised, 47: 251–292.
  • ––– (1947b). “Uued alused loogikale”, Mind, 56: 193–235; parandused, Mind, 57: 69–70.
  • Prawitz, Dag (1965). Looduslik mahaarvamine: tõestatud teoreetiline uuring, Stockholm: Almqvist & Wiksell; kordustrükk Mineola, NY: Dover Publications, 2006.
  • ––– (1971). „Ideed ja tulemused tõestamisteoorias”, Skandinaavia teise loogikasümpoosioni toimikud (Oslo 1970), Jens E. Fenstad (toim), Amsterdam: Põhja-Holland, lk 235–308.
  • ––– (1972). “Tõestusteooria filosoofiline positsioon”, kaasaegne filosoofia Skandinaavias, RE Olson ja AM Paul (toim), Baltimore, London: John Hopkins Press, lk 123–134.
  • ––– (1973). “Üldise tõestusteooria rajamise poole”, teaduse loogika, metoodika ja filosoofia IV, Patrick Suppes jt. (toim), Amsterdam: Põhja-Holland, lk 225–250.
  • ––– (1974). “Üldise tõestusteooria ideest”, Synthese, 27: 63–77.
  • ––– (1985). “Märkused mõne lähenemisviisi kohta loogilise tagajärje kontseptsioonile”, Synthese, 62: 152–171.
  • ––– (2006). “Tähendus on lähendatud tõendite kaudu”, Synthese, 148: 507–524.
  • ––– (2007). “Pragmaatikute ja verifitseerijate tähendusteooriad”, Michael Dummeti, Randall E. Auxieri ja Lewis Edwin Hahni (toim) filosoofia, La Salle: Open Court, lk 455–481.
  • ––– (2013). “Lähenemisviis üldisele tõendusteooriale ja uuesti läbi vaadatud intuitsioonilise loogika terviklikkuse oletus”, “Edusammud loomulikus mahaarvamises”, Edward Hermann Haeusler, Luiz Carlos Pereira ja Valeria de Paiva (toim), Berliin: Springer.
  • Loe, Stephen (2010). “Üldine elimineerimise harmoonia ja loogiliste konstantide tähendus”, Journal of Philosophical Logic, 39: 557–576.
  • Restall, Greg (2009). “Substructural Logics”, Stanfordi filosoofia entsüklopeedia (2009. aasta suve väljaanne), Edward N. Zalta (toim), URL =.
  • Sambin, Giovanni, Giulia Battilotti ja Claudia Faggian (2000). “Põhiloogika: peegeldus, sümmeetria, nähtavus”, ajakiri Symbolic Logic, 65: 979–1013.
  • Sandqvist, Tor (2009). „Klassikaline loogika ilma kahevalentsuseta“, analüüs, 69: 211–218.
  • Schroeder-Heister, Peter (1984). “Loodusliku deduktsiooni loomulik laiendus”, Journal of Symbolic Logic, 49: 1284–1300.
  • ––– (1991). „Loogiliste konstantide ühtne tõestamisteoreetiline semantika (abstraktne)”, Journal of Symbolic Logic, 56: 1142.
  • ––– (1992). „Lõikamise kõrvaldamine loogikas koos määratletava peegeldusega”, mitteklassikaline loogika ja infotöötlus: rahvusvahelise seminari toimetised, Berliin, november 1990 (loenguteatised arvutiteaduses: köide 619). David Pearce ja Heinrich Wansing (toim), Berliin: Springer, lk 146–171.
  • ––– (1993). “Mõistete peegeldamise reeglid”, IEEE 8. iga-aastase arvutiteaduse loogika sümpoosioni artiklid, Los Alamitos: IEEE Press, lk 222–232.
  • ––– (2004). “Loogiliste süsteemide eeldamise kontseptsiooni kohta”, valitud artiklid aitasid kaasa GAP5 sektsioonidele (Analüütilise Filosoofia Ühingu viies rahvusvaheline kongress, Bielefeld, 22. – 26. September 2003), R. Bluhm ja C. Nimtz (toim)., Paderborn: mentis on veebis saadaval), lk 27–48.
  • ––– (2005). “Popperi strukturalismi loogikateooria”, Karl Popper: Centenary Assessment. Vol. III: Teadus, Ian Jarvie, Karl Milford ja David Miller (toim), Aldershot: Ashgate, lk 17–36.
  • ––– (2006). “Kehtivuse kontseptsioonid tõestatud teoreetilises semantikas”, Synthese, 148: 525–571.
  • ––– (2007). “Üldistatud määratluspeegeldus ja ümberpööramispõhimõte”, Logica Universalis, 1: 355–376.
  • ––– (2008a). “Lorenzeni intuitsioonilise loogika operatiivne põhjendus”, intuitsiooni sada aastat (1907-2007): Cerisy konverents, Mark van Atten jt. (toim), Basel: Birkhäuser, 214–240 [Viited kogu köitele: 391–416].
  • ––– (2008b). “Tõestusteoreetiline versus mudelteoreetiline tagajärg”, Logica aastaraamat 2007, M. Peliš (toim), Praha: Filosofia, lk 187–200.
  • ––– (2012a). “Mõistete põhjendamine tõestatud teoreetilises semantikas ja opositsiooni ruut”, Opositsiooni väljak: üldine tunnetuse raamistik, Jean-Yves Béziau ja Gillman Payette (toim), Bern: Peter Lang, lk 323–349.
  • ––– (2012b). “Tõestatud teoreetiline semantika, enesekontroll ja deduktiivse mõttekäigu vorm”. In: Topoi 31, lk 77–85.
  • ––– (2012c). “Klassikaline ja hüpoteetiline: standardsemantika põhiliste eelduste kriitika”. In: Synthese 187, lk 925–942.
  • ––– (2012d). “Paradoksid ja struktuurireeglid”. Osades: Dutilh Novaes, Catarina ja Ole T. Hjortland, toim., Lahustumatud ja tagajärjed. Esseed Stephen Loe auks. London: College Publications, lk 203–211.
  • ––– (2013). „Definitsiooniline peegeldus ja põhiloogika”, Puhta ja rakendatud loogika ajakirjad, 164 (4): 491–501.
  • ––– (2015). „Tõenditeoreetiline kehtivus, mis põhineb kõrvaldamise reeglitel“. Osades: Haeusler, Edward Hermann, Wagner de Campos Sanz ja Bruno Lopes, toim., Miks see on tõestusmaterjal? Luiz Carlos Pereira festivali võit. London: College Publications, lk 159–176.
  • ––– (2016a). “Avatud probleemid tõestusteoreetilises semantikas”. Osades: Piecha ja Schroeder-Heister, toim. (2016b), lk 253–283.
  • ––– (2016b). „Algsete järjestuste piiramine: identiteedi, kokkutõmbumise ja tükeldamise vahelised kompromissid“. Osades: Kahle, Reinhard, Thomas Strahm ja Thomas Studer, toim., Progress Theory Theory Basels: Birkhäuser, lk 339–351.
  • Kingasepp, DJ ja Timothy J. Smiley (1978). Mitme järelduse loogika, Cambridge: Cambridge University Press.
  • Sommaruga, Giovanni (2000). Konstruktiivse tüübi teooria ajalugu ja filosoofia, Dordrecht: Kluwer.
  • Sørensen, Morten Heine B. ja Pawel Urzyczyn (2006). Loengud Curry-Howardi isomorfismist, Amsterdam: Elsevier.
  • Tait, W. W.: (1967). “I tüüpi lõplike funktsionaalide intensiivsed tõlgendused”, Journal of Symbolic Logic, 32: 198–212.
  • Tennant, Neil (1978). Looduslik loogika, Edinburgh: Edinburgh University Press.
  • ––– (1982). “Tõestus ja paradoks”, Dialectica, 36: 265–296.
  • ––– (1987). Antirealism ja loogika: tõde kui igavene, Oxford: Clarendon Press.
  • ––– (1997). Tõe taltsutamine, Oxford: Clarendon Press.
  • Tranchini, Luca (2010). Tõestus ja tõde: antirealistlik perspektiiv, Milano: Edizioni ETS, 2013; doktorikraadi kordustrükk väitekiri, Tuebingeni ülikooli filosoofia osakond, 2010, saadaval veebis.
  • ––– (2012a). “Tõde tõestatud-teoreetilisest vaatenurgast”. In: Topoi 31, lk 47–57.
  • ––– (2012b). “Looduslik deduktiivsus kahekordse intuitsioonilise loogika jaoks”, Studia Logica, 100: 631–648.
  • ––– (2016). “Tõestatud teoreetiline semantika, paradoksid ja mõistmise ning denotatsiooni eristamine”, Journal of Logic and Computation, 26, lk 495–512.
  • Troelstra, Anne S. ja Dirk van Dalen (1988). Konstruktivism matemaatikas: sissejuhatus, Amsterdam: Põhja-Holland.
  • Troelstra, AS ja H. Schwichtenberg (2000). Algteabe teooria, Cambridge University Press, teine trükk.
  • von Kutschera, Franz (1968). Die Die Vollständigkeit des Operatorensystems {¬, ∧, ∨, ⊃} für die intuitionistische Aussagenlogik im Rahmen der Gentzensemantik ", matemaatika logik ja Grundlagenforschung, 11: 3–16.
  • ––– (1969). “Ein verallgemeinerter Widerlegungsbegrifff für Gentzenkalküle”, Archiv fürhematische Logik und Grundlagenforschung, 12: 104–118.
  • Wansing, Heinrich (1993a). “Intuitionistliku propositsioonilise loogika alamsüsteemide funktsionaalne täielikkus”, ajakiri Philosophical Logic, 22: 303–321.
  • ––– (1993b). Infostruktuuride loogika (loengu märkused tehisintellekti kohta, köide 681), Berliin: Springer Springer.
  • ––– (2000). “Tõestatud teoreetilise semantika idee”, Studia Logica, 64: 3–20.
  • ––– (2001). “Negatsioon”, Blackwelli juhend filosoofilisse loogikasse, L. Goble (toim), Cambridge, MA: Blackwell, lk 415–436.
  • Wieckowski, Bartosz (2008). “Ennustamine ilukirjanduses”, The Logica aastaraamat 2007, M. Peliš (toim), Praha: Filosofia, lk 267–285.
  • ––– (2011). “Subatomieraldamise reeglid”, sümboolse loogika ülevaade, 4: 219–236.
  • ––– (2016). “Subatomaatiline looduslik mahaarvamine mitterealistliku identiteediga naturalistliku esmajärjekorra keele jaoks”, ajakiri Logic, Language and Information, 25: 215–268.
  • Zeilberger, Noam (2008). “Duaalsuse ühtsuse kohta”, Annals of Puhas ja rakendatud loogika, 153: 66–96.

Akadeemilised tööriistad

sep mehe ikoon
sep mehe ikoon
Kuidas seda sissekannet tsiteerida.
sep mehe ikoon
sep mehe ikoon
Vaadake selle sissekande PDF-versiooni SEP-i sõprade veebisaidil.
info ikoon
info ikoon
Otsige seda sisenemisteema Interneti-filosoofia ontoloogiaprojektilt (InPhO).
phil paberite ikoon
phil paberite ikoon
Selle kande täiustatud bibliograafia PhilPapersis koos linkidega selle andmebaasi.

Muud Interneti-ressursid

  • de Campos Sanz, Wagner ja Thomas Piecha (2012). “Märkused konstruktiivse semantika kohta klassikalisele ja intuitsioonilisele loogikale”, veebikäsikiri.
  • Tranchini, Luca (2012b). “Tõestatud teoreetiline semantika, paradoksid ning mõistmise ja denotatsiooni eristamine”, veebikäsikiri.

Soovitatav: