Odôvodnenie Logika

2023 Autor: Noah Black | [email protected]. Naposledy zmenené: 2023-08-25 04:39

Toto je dokument v archívoch Stanfordskej encyklopédie filozofie. Informácie o autorovi a citácii Priatelia PDF Náhľad | Vyhľadávanie InPho PhilPapers Bibliography

Odôvodnenie Logika

Prvýkrát publikované St 22. júna 2011; podstatná revízia st 20. júla 2011

Môžete povedať: „Viem, že Abraham Lincoln bol vysoký muž. „Na druhej strane sa môžete opýtať, ako to viete. Takmer určite by ste neodpovedali sémanticky, v štýle Hintikka, že Abraham Lincoln bol vysoký vo všetkých situáciách kompatibilných s vašimi vedomosťami. Namiesto toho by ste skôr povedali: „Čítal som o výške Abrahama Lincolna v niekoľkých knihách a videl som jeho fotografie vedľa iných ľudí. „Jeden osvedčuje vedomosti poskytnutím dôvodu, odôvodnením. Sémantika Hintikka zachytáva vedomosti ako skutočnú vieru. Odôvodnenie Logika poskytuje chýbajúcu tretiu zložku Platovej charakterizácie vedomostí ako odôvodneného presvedčenia.

• 1. Prečo Odôvodnenie Logika?

  • 1.1 Epistemická tradícia
  • 1.2 Tradícia matematickej logiky

• 2. Základné komponenty logiky odôvodnenia

  • 2.1 Logika odôvodnenia
  • 2.2 Základné odôvodnenie Logika J ₀
  • 2.3 Logické povedomie a konštantné špecifikácie
  • 2.4 Faktivita
  • 2.5 Pozitívna inšpirácia
  • 2.6 Negatívna inšpirácia

• 3. Sémantika

  • 3.1 Možný svet pre jedného agenta Odôvodnenie Modely pre J
  • 3.2 Slabá a silná úplnosť
  • 3.3 Rodina s jedným zástupcom
  • 3.4 Modely jednotného sveta Odôvodnenie
• 4. Realizačné vety

• 5. Zovšeobecnenie

  • 5.1 Zmiešavanie explicitných a implicitných znalostí
  • 5.2 Modely možného sveta pre viacerých agentov
• 6. Russellov príklad: indukovaná skutočnosť
• 7. Vlastná referenčnosť odôvodnení
• 8. Kvantifikátory v odôvodnení logiky
• 9. Historické poznámky
• Bibliografia
• Akademické nástroje
• Súvisiace záznamy
• Ďalšie internetové zdroje

1. Prečo Odôvodnenie Logika?

Odôvodnenie logika je epistemická logika, ktorá umožňuje „rozvinúť“vedomostné a virálne modality do odôvodnenia: namiesto □ X sa píše t: X a znie to ako „X je odôvodnené dôvodom t“. Dalo by sa uvažovať o tradičných modálnych operátoroch ako o implicitných modalitách a odôvodňujúcich termínoch ako o ich explicitnom rozpracovaní, ktoré dopĺňa modálnu logiku o jemnejšie epistemické stroje. Skupina oprávnených výrazov má štruktúru a fungovanie. Výber operácií vedie k odlišnej logike odôvodnenia. Pre všetky bežné epistemické logiky sa ich modality dajú úplne rozvinúť do formy explicitného odôvodnenia. V tejto súvislosti Odôvodnenie Logika odhaľuje a používa výslovný, ale skrytý obsah tradičnej epistemickej modálnej logiky.

Odôvodnenie Logika vznikla ako súčasť úspešného projektu s cieľom poskytnúť konštruktívnu sémantiku pre intuicionistické logicko-logické odôvodňujúce pojmy, ktoré sú zbavené všetkých, ale najzákladnejších znakov matematických dôkazov. Dôkazy sú odôvodneniami v ich najčistejšej podobe. Následne bola do formálnej epistemológie zavedená logika odôvodnenia. Tento článok predstavuje všeobecný rozsah logiky odôvodnenia, ako sa v súčasnosti rozumie. Diskutuje ich vzťahy s konvenčnou modálnou logikou. Okrem technických mechanizmov sa v článku skúma, ako použitie výslovných odôvodňujúcich výrazov vrhá svetlo na množstvo tradičných filozofických problémov. Subjekt ako celok je stále v aktívnom vývoji. Tu sa uvádza jej stručný opis v čase písania správy.

Korene logiky odôvodnenia sa dajú vysledovať v mnohých rôznych zdrojoch, z ktorých dva sú podrobne rozobrané: epistemológia a matematická logika.

1.1 Epistemická tradícia

Vlastnosti vedomostí a viery sú predmetom formálnej logiky minimálne od von Wright a Hintikka (Hintikka 1962, von Wright 1951). Vedomosti a viera sa považujú za modality spôsobom, ktorý je v súčasnosti veľmi známy - Epistemická logika. Ale Platónove tri kritériá pre vedomosti, opodstatnené, pravdivé, presvedčené (Gettier 1963, Hendricks 2005), epistemická logika skutočne funguje iba s dvoma z nich. Možné svety a model nerozoznateľnosti viery - človek verí tomu, čo je za každých okolností považované za možné. Faktivita prináša do hry pravdivosť - ak niečo nie je tak v skutočnom svete, nemôže byť známe, iba verené. Neexistuje však žiadna reprezentácia podmienky odôvodnenia. Avšak,modálny prístup bol mimoriadne úspešný, keď umožnil rozvoj bohatej matematickej teórie a aplikácií (Fagin, Halpern, Moses a Vardi 1995, van Ditmarsch, van der Hoek a Kooi 2007). Stále to nie je celý obraz.

Modálny prístup k logike vedomostí je v istom zmysle postavený na univerzálnom kvantifikátore: X je známy v situácii, keď X je pravdivý vo všetkých situáciách, ktoré sa nedajú odlíšiť od tohto. Na druhej strane opodstatnenia privedú do obrazu existenciálny kvantifikátor: X je známe v situácii, ak v tejto situácii existuje X. Táto univerzálna / existenciálna dichotómia je pre logikov známa - vo formálnej logike existuje dôkaz pre vzorec X iba vtedy, ak je X pravdivý vo všetkých modeloch pre logiku. Jeden si myslí, že modely sú svojou podstatou nekonštruktívne a dôkazy ako konštruktívne veci. Jeden nebude mať zlé myslenie na zdôvodnenie všeobecne, rovnako ako matematické dôkazy. Prvá logika odôvodnenia bola výslovne navrhnutá tak, aby zachytávala matematické dôkazy v aritmetike,niečo, o čom sa bude ďalej diskutovať v oddiele 1.2.

V odôvodnení je okrem kategórie vzorcov aj druhá kategória odôvodnení. Zarovnania sú formálne termíny, zostavené z konštánt a premenných pomocou rôznych operačných symbolov. Konštanty predstavujú zdôvodnenie pre všeobecne akceptované pravdy - zvyčajne axiómy. Premenné označujú nešpecifikované odôvodnenie. Rôzne logiky odôvodnenia sa líšia v tom, ktoré operácie sú povolené (a tiež v iných ohľadoch). Ak t je ospravedlňujúci výraz a X je vzorec, t: X je vzorec a má sa čítať:

t je odôvodnenie pre X.

Jedna operácia spoločná pre všetky logiky odôvodnenia je aplikácia, písaná ako násobenie. Ide o to, že ak s je odôvodnenie pre A → B a t je odôvodnenie pre A, potom [s ⋅ t] je odôvodnením pre B ^[1]. To znamená, že sa všeobecne predpokladá nasledujúce:

(1)	s:(A → B) → (t: A → [s ⋅ t]: B).

Toto je explicitná verzia obvyklej distribúcie znalostných operátorov a modálnych operátorov vo všeobecnosti s dôsledkami:

(2)	□ (A → B) → (□ A → □ B).

V skutočnosti vzorec (2) stojí za mnohými problémami logickej vševedúcnosti. Tvrdí, že agent vie všetko, čo vyplýva z jeho vedomostných znalostí, čo je dôsledkom uzavretia. Aj keď je v zásade zrozumiteľná, zrozumiteľnosť uzavretá následkom, to isté sa nedá povedať o žiadnej hodnovernej verzii skutočných znalostí. Rozdiel medzi (1) a (2) možno využiť v diskusii o paradigmatickom príklade Červenej stodoly Goldmana a Kripka; tu je zjednodušená verzia príbehu prevzatého z (Dretske 2005).

Predpokladajme, že idem cez okolie, v ktorom, bez vedomia mňa, sú stodoly papiera-mâché roztrúsené a vidím, že objektom predo mnou je stodola. Pretože mám vnímanie stodoly predo mnou, domnievam sa, že objektom predo mnou je stodola. Naše intuície naznačujú, že neviem stodolu. Ale teraz predpokladajme, že okolie nemá falošné červené stodoly, a tiež si všimnem, že objekt predo mnou je červený, takže viem, že je tu červená stodola. Táto juxtapozícia, ktorá je červenou stodolou, o ktorej viem, znamená, že ide o stodolu, ktorú nemám, „je rozpaky“.

V prvej formalizácii príkladu Červenej stodoly sa logická derivácia uskutoční v základnej modálnej logike, v ktorej sa □ interpretuje ako modalita „viery“. Potom sa niektoré výskyty □ budú podľa popisu problému externe interpretovať ako „vedomosti“. Nech je B vetou „objekt predo mnou je stodola“a nech je R vetou „objekt predo mnou je červený“.

1. □ B: „Verím, že objektom predo mnou je stodola“;
2. □ (B ∧ R), „Verím, že predo mnou je červená stodola“.

Na kovovom poli je 2 vlastne znalosť, zatiaľ čo pri popise problému 1 nie je znalosť.

□ (B ∧ R → B), vedomostné tvrdenie logickej axiómy

V rámci tejto formalizácie sa zdá, že došlo k porušeniu epistemickej uzávery v jej modálnej podobe (2): riadok 2, □ (B ∧ R) a riadok 3, □ (B ∧ R → B) sú prípady vedomostí, zatiaľ čo □ B (riadok) 1) nie sú vedomosti. Zdá sa, že modálny jazyk tu nepomáha vyriešiť tento problém.

Ďalej zvážte príklad červenej stodoly v odôvodnení logiky, kde t: F sa interpretuje ako „ domnievam sa, že F je z dôvodu t“. Dovoliť u byť konkrétnym individuálnym odôvodnením viery, že B, a v, za presvedčenie, že B ∧ R. Okrem toho nech je ospravedlnenie logickej pravdy B ∧ R → B. Potom je zoznam predpokladov:

1. u: B, „u je dôvod domnievať sa, že objektom predo mnou je stodola“;
2. v:(B ∧ R), „v je dôvod domnievať sa, že objektom predo mnou je červená stodola“;
3. a:(B ∧ R → B).

Pokiaľ ide o metalevel, v popise problému sa uvádza, že 2 a 3 sú prípady poznania, nielen presvedčenie, zatiaľ čo 1 je presvedčenie, ktoré nie je poznaním. Formálne odôvodnenie je toto:

1. a:(B ∧ R → B) → (v:(B ∧ R) → [a ⋅ v]: B), v zásade (1);
2. v:(B ∧ R) → [a ⋅ v]: B od 3 a 4 pomocou výrokovej logiky;
3. [a ⋅ v]: B od 2 do 5 pomocou výrokovej logiky.

Všimnite si, že záver 6 je [a ⋅ v]: B, a nie u: B; držanie epistemických uzáverov. Logickým zdôvodnením sa dospelo k záveru, že [a ⋅ v]: B je prípad vedomostí, tj „viem B z dôvodu a ⋅ v“. Skutočnosť, že u: B nie je prípadom vedomosti, neporušuje zásadu uzavretia, pretože posledná uvedená si uplatňuje vedomosti konkrétne pre [a ⋅ v]: B. Preto po pozorovaní červenej fasády viem skutočne B, ale táto znalosť nemá nič spoločné s 1, čo zostáva skôr vecou viery ako poznania. Logická formalizácia odôvodnenia predstavuje situáciu spravodlivo.

Zdôvodnenia sledovania predstavujú štruktúru príkladu Červenej stodoly spôsobom, ktorý nie je zachytený tradičnými epistemickými modálnymi nástrojmi. Odôvodnenie Logické formalizačné modely, ktoré sa v takom prípade javia; zachováva sa uzavretie vedomostí za logických okolností, aj keď „stodola“nie je vnímaná percepčne. ^[2]

1.2 Tradícia matematickej logiky

Podľa Brouwera pravda v konštruktívnej (intuitionistickej) matematike znamená existenciu dôkazu, porovnaj (Troelstra a van Dalen 1988). V rokoch 1931 - 34 Heyting a Kolmogorov poskytli neformálny opis zamýšľanej sémantiky založenej na dôkazoch pre intuicionálnu logiku (Kolmogorov 1932, Heyting 1934), ktorá sa v súčasnosti označuje ako sémantika Brouwer-Heyting-Kolmogorov (BHK). Podľa podmienok BHK je vzorec „pravdivý“, ak má dôkaz. Ďalej je dôkaz zloženého vyhlásenia spojený s dôkazmi o jeho zložkách nasledovným spôsobom:

• dôkaz A ∧ B pozostáva z dôkazu o tvrdení A a dôkazu o tvrdení B;
• doklad o A A B sa predloží predložením dokladu A alebo dokladu B;
• dôkaz A → B je konštrukcia transformujúca dôkazy A na dôkazy B;
• klamstvo ⊥ je tvrdenie, ktoré nemá žiadny dôkaz, ¬ A je skratka pre A → ⊥.

Kolmogorov výslovne navrhol, že objekty, ktoré majú podobnú korektúru, sú interpretované („problémové riešenia“) z klasickej matematiky (Kolmogorov 1932). Vskutku, z hľadiska založenia nemá zmysel chápať vyššie uvedené „dôkazy“ako dôkazy v intuicionistickom systéme, ktoré sa tieto podmienky majú špecifikovať.

Základnou hodnotou sémantiky BHK je to, že neformálne, ale jednoznačne navrhuje zaobchádzať s odôvodneniami, tu matematickými dôkazmi, ako s objektmi s operáciami.

V roku (Gödel 1933) podnikol Gödel prvý krok k rozvoju prísnej sémantiky založenej na dôkazoch pre intuicionizmus. Gödel považoval klasickú modálnu logiku S4 za počet popisujúci vlastnosti preukázateľnosti:

• Axiómy a pravidlá klasickej výrokovej logiky;
• □ (F → G) → (□ F → □ G);
• □ F → F;
• □ F → □□ F;
• Pravidlo nevyhnutnosti: ak ⊢ F, potom ⊢ □ F.

Na základe Brouwerovho chápania logickej pravdy ako preukázateľnosti, Gödel definoval preklad tr (F) výrokového vzorca F v intuicionistickom jazyku do jazyka klasickej modálnej logiky: tr (F) sa získa predponou každého podformulu F s preukázateľnosťou modalita □. Neformálne povedané, keď sa na tr (F) použije obvyklý postup určovania klasickej pravdy vzorca, otestuje sa preukázateľnosť (nie pravda) každého z podformúl F, v zhode s Brouwerovými myšlienkami. Z Gödelových výsledkov a McKinsey-Tarského práce na topologickej sémantike pre modálnu logiku vyplýva, že preklad tr (F) poskytuje správne vloženie Intuitionistic Propositional Calculus, IPC, do S4, tj vloženie intuicionálnej logiky do klasickej logiky rozšírené prevádzkovateľom preukázateľnosti.

(3)	Ak IPC preukáže F, potom S4 preukáže tr (F).

Gödelov pôvodný cieľ definovať intuicionistickú logiku z hľadiska klasickej preukázateľnosti sa napriek tomu nedosiahol, pretože spojenie S4 s obvyklou matematickou predstavou o preukázateľnosti nebolo preukázané. Okrem toho Gödel poznamenal, že priama myšlienka interpretácie modality □ F ako F je preukázateľná v danom formálnom systéme T je v rozpore s Gödelovou druhou teóriou neúplnosti. Skutočne, □ (□ F → F) možno odvodiť v S4 pravidlom nevyhnutnosti z axiómu □ F → F. Na druhej strane interpretácia modality □ ako predikátu formálnej preukázateľnosti v teórii T a F ako rozporu prevádza tento vzorec na nepravdivé tvrdenie, že konzistencia T je vnútorne dokázateľná v T.

Situáciu po (Gödel 1933) možno opísať na nasledujúcom obrázku, kde „X ↪ Y“by sa malo interpretovať ako „X sa interpretuje v Y“

IPC ↪ S4 ↪? ↪ KLASICKÉ LÁTKY

Na verejnej prednáške vo Viedni v roku 1938 Gödel poznamenal, že použitím formátu jednoznačných dôkazov:

(4)	t je dôkazom F.

môže pomôcť pri interpretácii jeho počtu preukázateľnosti S4 (Gödel 1938). Gödelova práca (Gödel 1938) zostala až do roku 1995 nanešťastie neuverejnená. Dovtedy sa znovu objavila Gödelianova logika explicitných dôkazov a axiomatizovala sa ako Logika dôkazov LP a poskytla úplné vety, ktoré ju spájajú s S4 aj s klasickými dôkazmi (Artemov) 1995).

Logic of Proofs LP sa stal prvým v rodine Odôvodnenie Logic. Dôkazy v LP nie sú nič iné ako pojmy BHK chápané ako klasické dôkazy. S LP dostala výroková intuitionistická logika požadovanú prísnu sémantiku BHK:

IPC ↪ S4 ↪ LP ↪ KLASICKÉ LÁTKY

Podrobnejšie informácie o tradícii matematickej logiky nájdete v oddiele 1 doplnkového dokumentu Niektoré ďalšie technické záležitosti.

2. Základné komponenty logiky odôvodnenia

V tejto časti je uvedená syntax a axiomatika najbežnejších systémov logiky odôvodnenia.

2.1 Logika odôvodnenia

Aby sa vytvoril formálny účet logiky odôvodnenia, je potrebné urobiť základný štrukturálny predpoklad: odôvodnenia sú abstraktné objekty, ktoré majú štruktúru a operácie s nimi. Dobrým príkladom zdôvodnenia sú formálne dôkazy, ktoré sú už dlho predmetom štúdia matematickej logiky a informatiky (porovnaj časť 1.2).

Odôvodnenie Logika je formálny logický rámec, ktorý zahŕňa epistemické tvrdenia t: F, čo znamená „t je odôvodnenie pre F“. Odôvodnenie Logika priamo neanalyzuje, čo to znamená pre t, aby zdôvodnila F nad formátom t: F, ale skôr sa pokúša axiomaticky charakterizovať tento vzťah. Je to podobné spôsobu, akým logická logika zaobchádza so svojimi spojivami, povedzme, disjunkcia: neanalyzuje vzorec p ∨ q, ale skôr predpokladá určité logické axiómy a tabuľky pravdy o tomto vzorci.

Existuje niekoľko rozhodnutí o dizajne. Odôvodnenie Logika začína najjednoduchšou základňou: klasickou logickou logikou az dobrých dôvodov. Odôvodnenia poskytujú dostatočne závažnú výzvu aj na najjednoduchšej úrovni. Paradigmatické príklady Russella, Goldmana-Kripkeho, Gettiera a ďalších sa dajú spracovať pomocou logickej logiky Odôvodnenie. Jadro epistemickej logiky pozostáva z modálnych systémov s klasickou booleovskou základňou (K, T, K4, S4, K45, KD45, S5 atď.) A každému z nich bola poskytnutá zodpovedajúca sprievodná logika odôvodnenia založená na logickej logike., Nakoniec nie je vždy predpokladaná faktickosť odôvodnení. To umožňuje zachytiť podstatu diskusií v epistemológii, ktoré sa týkajú záležitostí viery a nie vedomostí.

Základnou operáciou odôvodnenia je aplikácia a súčet. Operácia aplikácie vezme zarovnania s at a vytvorí odôvodnenie s ⋅ t tak, že ak s:(F → G) at: F, potom [s ⋅ t]: G. symbolicky

s:(F → G) → (t: F → [s ⋅ t]: G)

Toto je základná vlastnosť odôvodnení predpokladaných v kombinatickej logike a λ-kalkuli (Troelstra a Schwichtenberg 1996), Brouwer-Heyting-Kolmogorov sémantika (Troelstra a van Dalen 1988), realizovateľnosť Kleene (Kleene 1945), logika dôkazov LP atď.,

Akékoľvek dve odôvodnenia sa dajú bezpečne spojiť do niečoho so širším rozsahom pôsobnosti. To sa vykonáva pomocou súčtu operácií '+'. Ak s: F, potom akýkoľvek dôkaz t môže byť, kombinovaný dôkaz s + t zostáva dôvodom pre F. Presnejšie povedané, operácia '+' berie odôvodnenia sa ta produkuje s + t, čo je odôvodnením všetkého odôvodneného s alebo t.

s: F → [s + t]: F at: F → [s + t]: F

Ako motiváciu by sa dalo uvažovať o s a t ako o dvoch zväzkoch encyklopédie a s + t ako o súbore týchto dvoch zväzkov. Predstavte si, že jeden zo zväzkov, napríklad s, obsahuje dostatočné odôvodnenie pre tvrdenie F, tj s: F je prípad. Potom väčšia množina s + t tiež obsahuje dostatočné odôvodnenie pre F, [s + t]: F. V časti Logic of Proofs LP, oddiel 1.2, možno výraz „s + t“vykladať ako zreťazenie dôkazov s at.

2.2 Základné odôvodnenie Logika J ₀

Pojmy odôvodnenia sú zostavené z odôvodňovacích premenných x, y, z, … a z odôvodňovacích konštánt a, b, c,… (s indexmi i = 1, 2, 3,…, ktoré sa vynechávajú vždy, keď je to bezpečné) prostredníctvom operácií “⋅ 'a' + '. Podrobnejšia logika, ktorá sa zvažuje ďalej, umožňuje ďalšie operácie odôvodnenia. Konštanty označujú atómové zdôvodnenia, ktoré systém neanalyzuje; premenné označujú nešpecifikované zdôvodnenia. Základná logika zdôvodnenie, J ₀ je axiomatized ktoré ďalej.

Klasická logika

Klasické výrokové axiómy a pravidlo Modus Ponens

Aplikácia Axiom

s:(F → G) → (t: F → [s ⋅ t]: G),

Súčet axiómov

s: F → [s + t]: F, s: F → [t + s]: F.

J ₀ je logika všeobecne (nie nutne Factiva) ospravedlnenie úplne skeptický činidlá, pre ktoré nie je vzorec preukázateľne oprávnený, tj, J ₀ neodvodzuje t: F pre každú t a F. Takýto prostriedok je však schopný vyvodiť relatívne opodstatnené závery formulára

Ak x: A, y: B, …, z: C drží, potom t: F.

Vďaka tejto kapacite dokáže J ₀ primerane napodobňovať ďalšie systémy logiky Odôvodnenie vo svojom jazyku.

2.3 Logické povedomie a konštantné špecifikácie

Zásada logického povedomia uvádza, že logické axiómy sú opodstatnené ex officio: agent akceptuje logické axiómy ako odôvodnené (vrátane tých, ktoré sa týkajú odôvodnení). Ako už bolo povedané, logické povedomie môže byť v niektorých epistemických situáciách príliš silné. Odôvodnenie Logika však ponúka flexibilný mechanizmus konštantných špecifikácií, ktorý predstavuje rôzne odtiene logického povedomia.

Jeden samozrejme rozlišuje medzi predpokladom a odôvodneným predpokladom. Odôvodnenie Odôvodnenie Logické konštanty slúžia na zdôvodnenie predpokladov v situáciách, keď sa už ďalej neanalyzujú. Predpokladajme, že je potrebné predpokladať, že axioma A je oprávnená pre znalca. Jeden jednoducho postuluje e ₁: A pre nejakú dôkazovú konštantu e ₁ (s indexom 1). Ak je ďalej potrebné predpokladať, že tento nový princíp e ₁: A je tiež opodstatnený, je možné predpokladať e ₂:(e ₁: A) pre konštantu e2.(s indexom 2). A tak ďalej. Sledovanie indexov nie je potrebné, ale je to ľahké a pomáha pri rozhodovacích postupoch (Kuznets 2008). Súbor všetkých predpokladov tohto druhu pre danú logiku sa nazýva konštantná špecifikácia. Tu je formálna definícia:

Constant Špecifikácie SK pre daný zdôvodnenie logiky L je množina formulou formulára

e _n: e _{n −1}:…: e ₁: A (n ≥ 1),

kde A je axióma L, a E ₁, E ₂, …, e _n sú podobné konštanty s indexmi 1, 2, …, n. Predpokladá sa, že CS obsahuje všetky prechodné špecifikácie, tj vždy, keď e _n: e _{n −1}:…: e ₁: A je v CS, potom e _{n −1}:…: e ₁: A je tiež v CS.

V literatúre sa uvádza konštantná špecifikácia. Nasledujú najbežnejšie.

prázdny

CS = ∅. To zodpovedá absolútne skeptickému agentovi. Znamená to prácu s logikou J ₀.

konečný

CS je konečný súbor vzorcov. Toto je plne reprezentatívny prípad, pretože akékoľvek konkrétne odvodenie v odôvodnení logiky bude zahŕňať iba konečný súbor konštánt.

Axiomaticky vhodné

Každá axióma vrátane tých, ktoré boli novo získané prostredníctvom samotnej konštantnej špecifikácie, má zdôvodnenie. Vo formálnom prostredí, pre každú axiómu A je konštanta e ₁ také, že e ₁: A je v CS, a ak e _n: e _{n -1}: …: e ₁: od A ∈ SK, potom e _{n +1}: e _n: e _{n −1}:…: e ₁: A ∈ CS, pre každé n ≥ 1. Na zabezpečenie vlastnosti Internalization sú potrebné axiomaticky vhodné konštantné špecifikácie, prediskutované na konci tejto časti.

Celkom

Pre každú axiómu A a akékoľvek konštanty e ₁, e ₂,… e _n,

e _n: e _{n −1}:…: e ₁: A ∈ CS.

Názov TCS je rezervovaný pre celkovú špecifikáciu konštanty (pre danú logiku). Celková konštantná špecifikácia je samozrejme axiomaticky vhodná.

Teraz môžeme uviesť:

Logika odôvodnení s danou konštantnou špecifikáciou:

Nech CS je konštantná špecifikácia. J _CS je logika J _° + CS; axiómy sú axiómy J ₀ spolu s členmi CS a jediné pravidlo odvodenia je Modus Ponens. Všimnite si, že J ₀ je J _∅.

Logika odôvodnení

J je logické pravidlo internalizácie J ₀ + Axiom. Nové pravidlo uvádza:

Pre každú axiómu A a akékoľvek konštanty e ₁, e ₂, …, e _n odvodíme _n: e _{n −1}: …: e ₁: A.

Ten stelesňuje myšlienku neobmedzeného Logického povedomia o J. Podobné pravidlo sa objavilo v Logic of Proofs LP, a bolo tiež predvídané v Goldmanovom (Goldman, 1967). Logické povedomie, vyjadrené axiomaticky vhodnými konštantnými špecifikáciami, je výslovnou inkarnáciou pravidla nevyhnutnosti v modálnej logike: ⊢ F ⇒ ⊢ □ F, ale obmedzuje sa na axiómy. Všimnite si, že J sa zhoduje s J _TCS.

Kľúčovou črtou systémov odôvodnenia logiky je ich schopnosť internalizovať svoje vlastné odvodenia ako preukázateľné odôvodňujúce tvrdenia vo svojich jazykoch. Táto nehnuteľnosť bola očakávaná v (Gödel 1938).

Veta 1: Pre každú axiomaticky vhodnú konštantnú špecifikáciu CS sa J _CS teší internalizácii:

Ak ⊢ F, potom ⊢ p: F pre nejaký zdôvodňovací termín p.

Dôkaz. Indikácia dĺžky derivácie. Predpokladajme, že ⊢ F. Ak F je člen J _° alebo člen CS, existuje konštanta e _n (kde n môže byť 1) tak, že e _n: F je v CS, pretože CS je axiomaticky vhodné. Potom e _n: F je odvoditeľná. Ak F získa Modus Ponens z X → F a X, potom pomocou indukčnej hypotézy ⊢ s:(X → F) a ⊢ t: X pre niektoré s, t. Pomocou aplikačného axiómu ⊢ [s ⋅ t]: F.

V oddiele 2 doplnkového dokumentu Niektoré ďalšie technické záležitosti sú uvedené príklady konkrétnych syntaktických derivácií v logike odôvodnenia.

2.4 Faktivita

Faktivita uvádza, že na to, aby agent uzavrel pravdu, stačí odôvodnenie. Toto je obsiahnuté v nasledujúcom texte.

Fakticita Axiom t: F → F.

Faktivita Axiom má podobnú motiváciu ako Pravdivý axiom epistemickej logiky, □ F → F, ktorý je všeobecne akceptovaný ako základná vlastnosť poznania.

Na rozdiel od zásad uplatňovania a súčtu sa v základných odôvodneniach nevyžadujú faktické odôvodnenia, čo ich robí schopnými reprezentovať čiastočné aj faktické odôvodnenia. Faktor Factivity Axiom sa objavil v Logic of Proofs LP, oddiel 1.2, ako hlavný znak matematických dôkazov. V tomto nastavení je fakticky jednoznačne platná: ak existuje matematický dôkaz t F, potom F musí byť pravdivý.

Faktor Factivity Axiom je prijatý pre odôvodnenia, ktoré vedú k znalostiam. Samotná skutočnosť však nezaručuje znalosti, ako sa ukázalo v príkladoch Gettiera (Gettier 1963).

Logika aktívnych oprávnení

• JT ₀ = J ₀ + Faktivita;
• JT = J + Factivity.

Systémy JT _CS zodpovedajúce _CS s konštantnými špecifikáciami sú definované ako v oddiele 2.3.

2.5 Pozitívna inšpirácia

Jedným zo spoločných princípov poznania je identifikácia poznania a poznania, ktoré človek pozná. V modálnom nastavení to zodpovedá □ F → □□ F. Táto zásada má primeraný výslovný náprotivok: skutočnosť, že zástupca akceptuje t ako dostatočný dôkaz pre F, slúži ako dostatočný dôkaz pre t: F. Takýto „meta-dôkaz“má často fyzickú podobu: správa rozhodcu, ktorá potvrdzuje správnosť dôkazu v papieri; výstup počítačového overovania, ktorý dostal formálny dôkaz t ako vstup; formálny dôkaz, že t je dôkazom F, atď. Pozitívna operácia infekcie '!' môžu byť na tento účel pridané do jazyka; potom sa predpokladá, že vzhľadom na t, agent poskytne odôvodnenie! t z t: F tak, že t: F →! t:(t: F). Pozitívna inšpekcia v tejto operatívnej podobe sa prvýkrát objavila v Logic of Proofs LP.

Axióma pozitívnej infekcie: t: F →! t:(t: F).

Potom definujeme:

• J4: = J + pozitívna Inšpekcia;
• LP: = JT + pozitívna Inšpekcia. ^[3]

Logika J4 ₀, J4 _CS, LP ₀ a LP _CS sú definované prirodzeným spôsobom (porovnaj oddiel 2.3). Priamy analóg vety 1 platí aj pre J4 _CS a LP _CS.

Za prítomnosti axiómu pozitívnej infekcie je možné obmedziť pôsobnosť pravidla internalizácie axiómu na internalizáciu axiómov, ktoré nie sú vo forme e: A. Takto sa to urobilo v LP: Internalizáciu Axiom je možné emulovať pomocou !! e:(! e:(e: A)) namiesto e ₃:(e ₂:(e ₁: A)) atď. Pojem konštantná špecifikácia sa môže tiež zodpovedajúcim spôsobom zjednodušiť. Takéto zmeny sú malé a nemajú vplyv na hlavné vety a aplikácie odôvodnenia logiky.

2.6 Negatívna inšpirácia

(Pacuit 2006, Rubtsova 2006) považovali operáciu negatívnej infekcie za „?“ktorý overuje, či je dané tvrdenie o odôvodnení nepravdivé. Možnou motiváciou pre zváženie takejto operácie je, že operácia pozitívnej introspekcie '!' môže byť považovaný za schopný poskytnúť presvedčivé verifikačné úsudky o platnosti tvrdení o odôvodnení t: F, takže keď t nie je dôvodom pre F, takéto „!“by mal dospieť k záveru, že F t: F. Toto je normálne prípad overovateľov počítačov, kontrolóri korektúr vo formálnych teóriách atď. Táto motivácia je však obťažná: príklady verifikátorov a kontrolóri korektúr pracujú s t aj F ako vstupy, zatiaľ čo formát Pacuit-Rubtsova? t naznačuje, že jediný vstup pre „?“je odôvodnenie t a výsledok? Má odôvodňovať návrhy:F rovnomerne pre všetky F s, pre ktoré t: F neplatí. Takáto operácia “?“neexistuje odvtedy formálne matematické dôkazy? t by potom mal byť jediným dôkazom nekonečne mnohých tvrdení F t: F, čo je nemožné.

Axiom negatívnej infekcie iom t: F →? t: (¬ t: F)

Definujeme systémy:

• J45 = J4 + negatívna inšpekcia;
• JD45 = J45 + ¬ t: ⊥;
• JT45 = J45 + Factivity

a prirodzene rozširujú tieto definície na J45 _CS, JD45 _CS a JT45 _CS. Priamy analóg vety 1 platí pre J45 _CS, JD45 _CS a JT45 _CS.

3. Sémantika

Dnešná štandardná sémantika pre logiku ospravedlnenia vychádza z (Fitting 2005) - použité modely sa v literatúre všeobecne nazývajú Fitting modely, ale tu sa budú nazývať možné modely svetového odôvodnenia. Možné modely svetového odôvodnenia sú zlúčením známej možnej svetovej sémantiky pre logiku vedomostí a viery, kvôli Hintikke a Kripkemu, so strojmi špecifickými pre pojmy ospravedlnenia, ktoré zaviedol Mkrtychev v (Mkrtychev 1997) (porovnaj časť 3.4).

3.1 Možný svet pre jedného agenta Odôvodnenie Modely pre J

Presnejšie povedané, je potrebné definovať sémantiku pre J _CS, kde CS je akákoľvek konštantná špecifikácia. Formálne je možným svetovým logickým modelom pre J _CS štruktúra M = ⟨G, R, E, V⟩. Z toho je „G, R“štandardný K rámec, kde G je množina možných svetov a R je binárny vzťah k nemu. V je mapovanie od výrokových premenných k podmnožinám G, špecifikujúce atómovú pravdu v možných svetoch.

Nová položka je E, dôkazová funkcia, ktorá vznikla v (Mkrtychev 1997). Toto mapuje termíny a vzorce odôvodnenia do skupín svetov. Intuitívna myšlienka je, že ak možný svet Γ je v E (t, X), potom t je relevantný alebo prípustný dôkaz pre X vo svete Γ. Človek by nemal považovať relevantné dôkazy za presvedčivé. Skôr si to predstavte skôr ako dôkazy, ktoré možno pripustiť na súde: toto svedectvo, tento dokument je niečo, čo by mala porota preskúmať, niečo, čo je relevantné, ale niečo, ktorého štatút určujúci pravdu sa ešte musí brať do úvahy. Funkcie preukazovania musia spĺňať určité podmienky, ale o týchto sa diskutuje trochu neskôr.

Vzhľadom na možný model svetelného oprávnenia J _CS M = ⟨G, R, E, V⟩ je pravda vzorca X v možnom svete M označená M, Γ ⊩ X a vyžaduje sa, aby spĺňal nasledujúce štandardné podmienky:

Pre každý Γ ∈ G:

1. M, Γ ⊩ P iff Γ ∈ V (P) pre P výrokový list;
2. nie je to tak, že M, Γ ⊩ ⊥;
3. M, Γ ⊩ X → Y, ak to tak nie je, M, Γ ⊩ X alebo M, Γ ⊩ Y.

Hovorí sa iba o tom, že atómová pravda je špecifikovaná svojvoľne a výrokové spojivá sa správajú pravdu funkčne v každom svete. Kľúčovou položkou je ďalšia.

M, Γ ⊩ (t: X) iba vtedy, ak Γ ∈ E (t, X) a pre každé Δ ∈ G s Γ R Δ máme toto M, ⊩ ⊩ X

Tento stav sa rozdelí na dve časti. Klauzula vyžadujúca, aby M, ⊩ X pre každý Δ ∈ G tak, že ΓR Δ je známa Hintikka / Kripkeho podmienka pre X, ktorá sa má veriť alebo byť uveriteľná v,. Doložka požadujúca, aby Γ ∈ E (t, X) dodáva, že t by malo byť relevantným dôkazom pre X v Γ. Neformálne potom platí, že t: X je pravdou v možnom svete, ak je X v tomto svete uveriteľné v obvyklom zmysle epistemickej logiky, a t je relevantným dôkazom X v tomto svete.

Je dôležité si uvedomiť, že v tejto sémantike človek nemusí veriť niečomu z konkrétneho dôvodu na svete, buď preto, že je jednoducho neuveriteľný, alebo preto, že je, ale dôvod nie je vhodný.

Niektoré funkcie musia byť stále stanovené pre funkciu dôkazov a do obrazu sa musí uviesť aj konštantná špecifikácia. Predpokladajme, že jeden je uvedený ako zdôvodnenie. Možno ich kombinovať dvoma rôznymi spôsobmi: súčasne využívať informácie z oboch; alebo použiť informácie iba od jedného z nich, ale najskôr si vyberte, ktorý z nich. Každá z nich vedie k základnej operácii za podmienok zdôvodnenia ⋅ a +, ktoré sú axiomaticky zavedené v oddiele 2.2.

Predpokladajme, že je to relevantný dôkaz pre implikáciu at je relevantný dôkaz pre predchodcu. Potom s a t spoločne poskytujú relevantné dôkazy o následkoch. Predpokladá sa nasledujúca podmienka týkajúca sa funkcií dôkazov:

E (s, X → Y) ∩E (t, X) ⊆ E (s ⋅ t, Y)

Po pridaní tejto podmienky platí platnosť

s:(X → Y) → (t: X → [s ⋅ t]: Y)

je zabezpečené.

Ak sú s a t dôkazy, možno povedať, že niečo je odôvodnené jedným alebo viacerými s, bez obťažovania sa špecifikovať, a to bude stále dôkaz. Na dôkazné funkcie sa ukladá táto požiadavka.

E (s, X) ∪ E (t, X) ⊆ E (s + t, X)

Niet divu, že oboje

s: X → [s + t]: X

a

t: X → [s + t]: X

teraz držte.

Nakoniec by sa mala zohľadniť CS s konštantnou špecifikáciou. Pripomeňme, že konštanty majú predstavovať dôvody pre základné predpoklady, ktoré sú priamo akceptované. Model M = ⟨G, R, E, V⟩ vyhovuje CS za predpokladu konštantnej špecifikácie: ak c: X ∈ CS, potom E (c, X) = G.

Možný svetový model odôvodnenia Možným svetovým odôvodňujúcim modelom pre J _CS je štruktúra M = ⟨G, R, E, V⟩, ktorá spĺňa všetky vyššie uvedené podmienky a spĺňa CS s konštantnou špecifikáciou.

Napriek svojim podobnostiam možné modely svetového odôvodnenia umožňujú jemnozrnnú analýzu, ktorá nie je možná u modelov Kripke. Ďalšie podrobnosti sa nachádzajú v oddiele 3 doplnkového dokumentu Niektoré ďalšie technické záležitosti.

3.2 Slabá a silná úplnosť

Vzorec X platí v konkrétnom modeli pre J _CS, ak je pravdivý vo všetkých možných svetoch modelu. Axiomatika pre J _CS bola uvedená v oddieloch 2.2 a 2.3. Veta o úplnosti má teraz očakávanú formu.

Veta 2: Vzorec X je preukázateľný v J _CS iba vtedy, ak X platí vo všetkých modeloch J _CS.

Veta o úplnosti, ako sa práve uviedla, sa niekedy označuje ako slabá úplnosť. Možno je trochu prekvapujúce, že pre modálnu logiku je dokázateľne ľahšie dokázať ako úplnosť K. Nasledujú komentáre k tomuto bodu. Na druhej strane je to veľmi všeobecné a pracuje pre všetky konštantné špecifikácie.

V (Fitting 2005) bola predstavená silnejšia sémantika. Model M = ⟨G, R, E, V⟩ sa nazýva plne vysvetľujúci, ak spĺňa nasledujúce podmienky. Pre každý Γ ∈ G, ak M, ⊩ ⊩ X pre všetky Δ ∈G, takže ΓR Δ, potom M, Γ ⊩t: X pre nejaký zdôvodňovací termín t. Všimnite si, že podmienka M, ⊩ ⊩ X pre všetky Δ ∈ G tak, že ΓR Δ, je obvyklou podmienkou toho, že X možno uveriť v at v zmysle Hintikka / Kripke. Úplne vysvetľujúce skutočnosti skutočne hovoria, že ak je vzorec v možnom svete uveriteľný, má to opodstatnenie.

Nie všetky slabé modely spĺňajú úplne vysvetľujúcu podmienku. Modely, ktoré sa nazývajú silné modely. Ak je CS s konštantnou špecifikáciou dostatočne bohatá na to, aby sa zachovala veta o internalizácii, potom je úplnosť s ohľadom na silné modely, ktoré spĺňajú CS. V pravom slova zmysle je úplnosť, pokiaľ ide o silné modely, skutočne rovnocenná schopnosti dokázať internalizáciu.

Dôkaz o úplnosti so zreteľom na silné modely je veľmi podobný dôkazu o úplnosti pomocou kanonických modelov pre modálnu logiku K. Na druhej strane možno silné modely použiť na poskytnutie sémantického dôkazu realizačnej vety (porovnaj oddiel 4).,

3.3 Rodina s jedným zástupcom

Doteraz sa diskutovalo o možnej svetovej sémantike pre jednu logiku ospravedlnenia, pre J, náprotivok K. Teraz sa veci rozširujú, aby zahŕňali ospravedlňujúce analógy iných známych modálnych logík.

Jednoducho pridaním reflexivity vzťahu dostupnosti R k podmienkam pre model v oddiele 3.1 získa človek platnosť t: X → X pre každé t a X a získa sémantiku pre JT, logiku odôvodnenia logickej analógie modálnej logiky T, najslabšia logika poznania. Ak je M, Γ ⊩ t: X, potom X platí najmä v každom stave prístupnom z Γ. Pretože sa vyžaduje, aby vzťah dostupnosti bol reflexný, M, ⊩ ⊩ X. Slabé a silné vety úplnosti sú preukázateľné pomocou rovnakého strojového zariadenia, aké sa použilo v prípade J, a je k dispozícii aj sémantický dôkaz realizačnej vety spájajúcej JT a T. To isté platí pre logiku diskutovanú nižšie.

V prípade odôvodňovacieho analógu K4 ďalší uársky operátor „!“sa pridáva do termínu jazyk, pozri oddiel 2.5. Pripomeňme si, že tento operátor mapuje odôvodnenia na odôvodnenia, pričom myšlienka je taká, že ak t je odôvodnenie pre X, potom! t by malo byť odôvodnením pre t: X. Sémanticky to pridáva podmienky k modelu M = ⟨G, R, E, V⟩ nasledovne.

Po prvé, R by samozrejme mal byť prechodný, ale nie nevyhnutne reflexný. Po druhé, je požadovaná podmienka monotónnosti funkcií dôkazov:

Ak ΓR Δ a Γ ∈ E (t, X), potom Δ ∈ E (t, X)

Nakoniec je potrebná ešte jedna podmienka funkcie dôkazu.

E (t, X) ⊆ E (! T, t: X)

Tieto podmienky spolu znamenajú platnosť t: X →! t: t: X a vytvoríme sémantiku pre J4, ospravedlňujúci analóg K4, s realistickou teorémou ich spojenia. Pridanie reflexivity vedie k logike, ktorá sa nazýva LP z historických dôvodov.

Dá sa tiež pridať negatívny operátor introspekcie, „?“, Pozri oddiel 2.6. Modely pre logiku odôvodnenia, ktoré zahŕňajú tohto operátora, pridávajú tri podmienky. Prvý R je symetrický. Po druhé, jeden dodáva stav, ktorý sa stal známym ako silný dôkaz: M, Γ ⊩ t: X pre všetky Γ ∈ E (t, X). Nakoniec je podmienkou funkcie dôkazov:

E (t, X) ⊆ E (? T, ¬ t: X)

Ak je toto strojné zariadenie pridané k stroju pre J4, dostaneme logiku J45, ktorá je opodstatnením náprotivku K45. Môže sa dokázať axiomatická spoľahlivosť a úplnosť. Podobným spôsobom sa môžu formulovať súvisiace logiky JD45 a JT45.

Realizačná veta zohľadňujúca tohto operátora bola uvedená v (Rubtsova 2006).

3.4 Modely jednotného sveta Odôvodnenie

Modely jednotného svetového odôvodnenia boli vyvinuté značne pred všeobecnejšími možnými modelmi svetového odôvodnenia, o ktorých diskutujeme, (Mkrtychev 1997). Dnes ich možno najjednoduchšie vymyslieť ako možné modely ospravedlnenia sveta, ktoré majú jednotný svet. Dôkaz úplnosti pre J a ďalšie uvedené logiky odôvodnenia sa dá ľahko upraviť tak, aby sa stanovila úplnosť s ohľadom na modely odôvodnenia jednotného sveta, hoci to samozrejme nebol pôvodný argument. Aká úplnosť, pokiaľ ide o modely ospravedlnenia jedného sveta, hovorí, že informácie o možnej svetovej štruktúre modelov ospravedlnenia môžu byť úplne zakódované funkciou prípustných dôkazov, aspoň pre doteraz diskutovanú logiku. Mkrtychev použil modely ospravedlnenia jednotného sveta na stanovenie rozhodovacej schopnosti LP,a iní ich zásadne využili pri stanovovaní hraníc komplexnosti pre logiku odôvodnenia, ako aj na preukázanie výsledkov konzervatívnosti pre logiku odôvodnenia viery (Kuznets 2000, Kuznets 2008, Milnikel 2007, Milnikel 2009). Výsledky zložitosti sa ďalej použili na riešenie problému logickej vševedúcnosti.

4. Realizačné vety

Prirodzený modálny epistemický náprotivok dôkazného tvrdenia t: F je □ F, odčítané pre niektoré x, x: F. Toto pozorovanie vedie k myšlienke zabudnutej projekcie, ktorá nahrádza každý výskyt t: F za □ F, a preto prevádza Odôvodnenie Logická veta S na zodpovedajúcu modálnu logickú vetu S ^o. Táto zabudnutá projekcia sa prirodzeným spôsobom rozširuje od viet až po logiku.

Je zrejmé, že rôzne Odôvodnenie Logika vety môžu mať rovnaký zábudlivý projekciu, teda S ^o stráca určité informácie, ktoré boli obsiahnuté v S. Je však ľahké pozorovať, že zabudnutá projekcia vždy mapuje platné vzorce odôvodnenia logiky (napr. Axiómy J) na platné vzorce zodpovedajúcej epistemickej logiky (v tomto prípade K). Platí to aj naopak: akýkoľvek platný vzorec Epistemic Logic je zabudnutou projekciou nejakého platného vzorca odôvodnenia Logic. Vyplýva to z korešpondenčnej vety 3.

Veta 3: J ^o = K.

Táto korešpondencia platí pre ďalšie dvojice systémov odôvodnenia a epistémie, napríklad J4 a K4 alebo LP a S4, a mnoho ďalších. V takejto rozšírenej podobe korešpondenčná veta ukazuje, že hlavné modálne logiky, ako sú K, T, K4, S4, K45, S5 a niektoré ďalšie, majú presné náprotivky logiky Odôvodnenie.

Jadrom korešpondenčnej vety je nasledujúca realizačná veta.

Veta 4: Existuje algoritmus, ktorý pre každý modálny vzorec F odvoditeľný v K priraďuje dôkazové termíny každému výskytu modality v F takým spôsobom, že výsledný vzorec ^Fr je odvoditeľný v J. Navyše realizácia priraďuje dôkazové premenné negatívnym výskytom modálnych operátorov v F, rešpektujúc tak existenčné čítanie epistemickej modality.

Známe realizačné algoritmy, ktoré obnovujú výrazy dôkazov v modálnych teorémoch, používajú v zodpovedajúcej modálnej logike derivácie bez prerušenia. Alternatívne môže byť realizačná veta stanovená sémanticky pomocou Fittingovej metódy alebo jej vhodnými úpravami. V zásade tieto sémantické argumenty vytvárajú aj realizačné postupy, ktoré sú založené na dôkladnom vyhľadávaní.

Bolo by chybné vyvodiť záver, že každá modálna logika má rozumný Odôvodnenie. Napríklad logika formálnej preukázateľnosti, GL (Boolos 1993) obsahuje Löbov princíp:

(5)	□ (□ F → F) → □ F,

ktorá nemá zrejme epistemicky prijateľnú výslovnú verziu. Zvážte napríklad prípad, keď F je výroková konštanta ⊥ pre false. Keby analóg analógovej vety 4 pokrýval Löbov princíp, boli by odôvodňujúce pojmy s a t tak, že x:(s: ⊥ → ⊥) → t: ⊥. Pre vecné odôvodnenie je to však intuitívne nesprávne. Skutočne s: ⊥ → ⊥ je príkladom Axiómu Factivity. Aplikujte Axiom Internalization na získanie c:(s: ⊥ → ⊥) pre nejakú konštantu c. Táto voľba c robí predchodcu c:(s: ⊥ → ⊥) → t: ⊥ intuitívne pravdivú a záver nepravdivý ^[4]. Najmä Löbov princíp (5) neplatí pre interpretáciu dôkazov (porovnaj (Goris 2007), v ktorej je uvedený úplný zoznam toho, ktoré princípy GL sú realizovateľné).

Korešpondenčná veta dáva nový pohľad na epistemickú modálnu logiku. Najmä poskytuje novú sémantiku pre hlavnú modálnu logiku. Okrem tradičného „univerzálneho“čítania □ F ako Kripkeho vo všetkých možných situáciách existuje teraz pre □ F prísna „existenciálna“sémantika, ktorú je možné prečítať, pretože existuje svedok (dôkaz, zdôvodnenie) F.

Odôvodnenie Sémantika zohráva v modálnej logike podobnú úlohu ako realizácia Kleene v intuitionistickej logike. V obidvoch prípadoch je zamýšľaná sémantika existenčná: Brouwer-Heyting-Kolmogorov interpretácia Intuitionistic Logic (Heyting 1934, Troelstra a van Dalen 1988, van Dalen 1986) a Gödelho čítanie S4 (Gödel 1933, Gödel 1938). V oboch prípadoch je možné, svet sémantika universalcharakter, ktorý je vysoko silným a dominantným technickým nástrojom. Nerieši však existenčný charakter zamýšľanej sémantiky. Realizácia Kleene realizovateľnosti (Kleene 1945, Troelstra 1998) odhalila výpočtovú sémantiku intuitívnej logiky a logiku dôkazov, aby poskytla presnú sémantiku dôkazov BHK pre intuitívnu a modálnu logiku.

V epistemickom kontexte Odôvodnenie Logika a Korešpondenčná veta pridávajú do modálnej logiky vedomostí a viery nový komponent „odôvodnenia“. Táto nová zložka bola opäť v skutočnosti starou a ústrednou predstavou, o ktorej sa všeobecne diskutovali epistemológovia hlavného prúdu, ale ktorá zostala mimo rámca klasickej epistemickej logiky. Korešpondenčná veta nám hovorí, že odôvodnenia sú kompatibilné so systémami v štýle Hintikka, a preto ich možno bezpečne začleniť do základu epistemickej modálnej logiky.

Viac informácií o realizačných vetách nájdete v časti 4 doplnkového dokumentu Niektoré ďalšie technické záležitosti.

5. Zovšeobecnenie

Doteraz sa v tomto článku uvažovalo iba o logike odôvodnenia jedného agenta, ktorá je analogická logike znalostí jedného agenta. Odôvodnenie Logiku možno považovať za logiku explicitných znalostí súvisiacich s konvenčnejšou logikou implicitných znalostí. V literatúre sa skúmalo množstvo systémov nad rámec systémov diskutovaných vyššie, ktoré zahŕňajú viac agentov alebo ktoré majú implicitných aj explicitných operátorov alebo ich kombináciu.

5.1 Zmiešavanie explicitných a implicitných znalostí

Pretože logika odôvodnenia poskytuje explicitné odôvodnenie, zatiaľ čo konvenčná logika znalostí poskytuje implicitného operátora znalostí, je prirodzené zvážiť kombináciu týchto dvoch prvkov do jedného systému. Najbežnejšou spoločnou logikou explicitných a implicitných znalostí je S4LP (Artemov a Nogina 2005). Jazyk S4LP je ako jazyk LP, ale s pridaním implicitného operátora znalostí napísaného buď K alebo □. Axiomatika je ako v prípade LP, kombinovaná s axiálnou hodnotou S4 pre implicitného operátora, spolu so spojovacou axiómou t: X → □ X, všetko, čo má explicitné odôvodnenie, je známe.

Sémanticky možné svetové modely oprávnenia na LP nepotrebujú žiadne úpravy, pretože už majú všetky modely modelov Hintikka / Kripke. Jeden modeluje operátora □ obvyklým spôsobom, pričom využíva iba vzťah prístupnosti, a jeden modeluje zdôvodňujúce výrazy, ako sú opísané v oddiele 3.1, pomocou funkcie prístupnosti a dôkazu. Pretože zvyčajná podmienka, že □ X je pravdivá vo svete, je jednou z dvoch klauzúl podmienky pre t: X je pravdivá, okamžite sa získa platnosť t: X → □ X, a spoľahlivosť ľahko vyplýva. Axiomatická úplnosť je tiež pomerne jednoduchá.

V S4LP sú zastúpené implicitné aj explicitné vedomosti, ale v možnej sémantike modelu svetového odôvodnenia slúži obom jediný vzťah dostupnosti. Toto nie je jediný spôsob, ako to dosiahnuť. Všeobecnejšie povedané, explicitný vzťah dostupnosti znalostí by mohol byť vhodným rozšírením vzťahu implicitných znalostí. Predstavuje to víziu explicitného poznania, ktorá má prísnejšie normy pre to, čo sa počíta ako známe, ako pre implicitné znalosti. Použitie odlišných vzťahov prístupnosti pre explicitné a implicitné znalosti je potrebné, keď sa tieto epistemické predstavy riadia rôznymi logickými zákonmi, napr. S5 pre implicitné znalosti a LP pre explicitné. Prípad viacnásobných prístupových vzťahov je v literatúre bežne známy ako Artemov-Fitting modely, tu sa však budú nazývať možné svetové modely s viacerými agentmi. (porovnaj oddiel 5.2).

Je zaujímavé, že zatiaľ čo logika S4LP sa zdá byť úplne prirodzená, realizačná veta je pre ňu problematická: žiadna takáto veta sa nedá dokázať, ak bude trvať na tom, čo sa nazýva normálna realizácia (Kuznets 2010). Realizácia implicitných modalít vedomostí v S4LP explicitným odôvodnením, ktoré by rešpektovalo epistemickú štruktúru, zostáva v tejto oblasti veľkou výzvou.

Interakcie medzi implicitnými a explicitnými znalosťami môžu byť niekedy dosť chúlostivé. Ako príklad uvážte nasledujúci zmiešaný princíp negatívnej introspekcie (opäť □ by sa mal chápať ako implicitný epistemický operátor),

(6)	¬ t: X → □ ¬ t: X.

Z hľadiska preukázateľnosti je to správna forma negatívnej introspekcie. Nech sa □ F interpretuje tak, že F je preukázateľné at: F ako t je dôkazom F v danej formálnej teórii T, napr. V Peano aritmetickej PA. Potom (6) sa uvádza preukázateľný princíp. Ak t nie je dôkazom F, potom, pretože toto tvrdenie je rozhodujúce, možno ho ustanoviť vo vnútri T, a preto v T je táto veta preukázateľná. Na druhej strane, dôkaz p 't nie je dôkazom F', závisí od ta t, F, p = p (t, F) a nedá sa vypočítať iba pre t. Z tohto hľadiska □ nemožno nahradiť žiadnym konkrétnym dôkazným pojmom v závislosti od iba ta 6) sa nedá prezentovať v úplne explicitnom formáte štýlu odôvodnenia.

Prvé príklady explicitných / implicitných znalostných systémov sa objavili v oblasti logiky preukázateľnosti. V (Sidon 1997, Yavorskaya (Sidon) 2001) bol zavedený logický LPP, ktorý kombinoval logiku preukázateľnosti GL s logikou dôkazov LP, ale s cieľom zabezpečiť, aby výsledný systém mal požadované logické vlastnosti, niektoré ďalšie operácie mimo pôvodných jazykov. GL a LP. V roku (Nogina 2006, Nogina 2007) bol ponúknutý kompletný logický systém, GLA, na dôkaz a preukázateľnosť, v súčte pôvodných jazykov GL a LP. LPP aj GLA majú úplnosť vo vzťahu k triede aritmetických modelov a tiež vo vzťahu k triede možných modelov svetového odôvodnenia.

Ďalším príkladom zásady preukázateľnosti, ktorú nie je možné úplne jednoznačne uviesť, je zásada Löb (5). Pre každý z LPP a GLA je ľahké nájsť dôkazový výraz l (x) taký

(7)	x: (□ F → F) → l (x): F

myslí si. Neexistuje však žiadna realizácia, ktorá by jednoznačne označila všetky tri □ s v (5). V skutočnosti je súborom realizovateľných princípov preukázateľnosti priesečník GL a S4 (Goris 2007).

5.2 Modely možného sveta pre viacerých agentov

V možných svetových modeloch odôvodnenia pre viacerých agentov sa používajú vzťahy s viacerými prístupmi, medzi ktorými sú prepojenia (Artemov 2006). Ide o to, že existuje viac agentov, z ktorých každý má implicitného operátora znalostí a existujú odôvodňujúce termíny, ktorým každý agent rozumie. Každý slobodne chápe explicitné dôvody; to predstavuje všeobecné vedomosti založené na dôkazoch.

N -agent možným modelom svet zdôvodnenie je štruktúra ⟨G, R ₁, …, R _n, R, E, V⟩ spĺňajú tieto podmienky. G je skupina možných svetov. Každá zo skupín R ₁, …, R _n je dostupnosť vzťah, jeden pre každý prostriedok. Tieto sa môžu podľa potreby považovať za reflexné, prechodné alebo symetrické. Používajú sa na modelovanie implicitných znalostí agentov pre rodinu agentov. Vzťah dostupnosti R spĺňa podmienky LP, reflexivitu a transitivitu. Používa sa pri modelovaní explicitných znalostí. E je dôkazová funkcia, ktorá spĺňa rovnaké podmienky ako podmienky uvedené v oddiele 3.3. V mapuje výrokové listy do skupín svetov, ako obvykle. Je stanovená osobitná podmienka: pre každé i = 1,…, n, R _i ⊆ R.

Ak M = ⟨G, R ₁, …, R _n, R, E, V⟩ je multi-agent možné Model svet zdôvodnenie pravda-na-a-svet vzťah, M, Γ ⊩ X, je definovaný u väčšiny obvyklé ustanovenia. Osobitne zaujímavé sú tieto:

• M, Γ _i K _i X iba vtedy, ak pre každé Δ ∈ G s Γ R _i Δ máme dané M, ⊩ ⊩ X.
• M, Γ ⊩ t: X iba vtedy, ak Γ ∈ E (t, X) a pre každé Δ ∈ G s ΓR Δ máme dané M, ⊩ X.

Podmienka R _i ⊆ R znamená platnosť t: X → K _i X pre každého agenta i. Ak existuje iba jediný agent a vzťah dostupnosti pre tohto agenta je reflexný a prechodný, poskytuje to ďalšiu sémantiku pre S4LP. Bez ohľadu na počet agentov, každý agent akceptuje výslovné dôvody na preukázanie vedomostí.

Verzia LP s dvoma agentmi bola predstavená a študovaná v (Yavorskaya (Sidon) 2008), hoci ju možno zovšeobecniť na akýkoľvek konečný počet agentov. V tomto má každý agent skôr svoju vlastnú množinu operátorov ospravedlnenia, premenných a konštánt, než aby mal pre každého jedného súboru, ako je uvedené vyššie. Okrem toho môže byť povolená určitá obmedzená komunikácia medzi agentmi pomocou nového operátora, ktorý umožňuje jednému agentovi overiť správnosť odôvodnení druhého agenta. Pre logiku dvoch agentov boli vytvorené verzie sémantiky jednotného sveta a všeobecnejších možných sémantických dôvodov. Zahŕňa to priame rozšírenie pojmu dôkaznej funkcie a možné modely svetového odôvodnenia pomocou dvoch vzťahov prístupnosti. Realizačné vety sa preukázali syntakticky,pravdepodobne by však fungoval aj sémantický dôkaz.

Nedávno sa preskúmala úloha verejných oznámení v logike odôvodnenia viacerých agentov (Renne 2008, Renne 2009).

V oddiele 5 doplnkového dokumentu Niektoré ďalšie technické záležitosti sa viac hovorí o spoločných znalostiach založených na dôkazoch.

6. Russellov príklad: indukovaná skutočnosť

Existuje technika na použitie logiky Odôvodnenie na analýzu rôznych zdôvodnení tej istej skutočnosti, najmä ak sú niektoré z odôvodnení faktické a niektoré nie. Na demonštráciu techniky zvážte dobre známy príklad:

Ak je človek presvedčený, že priezvisko posledného predsedu vlády sa začalo písmenom „B“, verí, čo je pravda, keďže posledným predsedom vlády bol sir Henry Campbell Bannerman ^[5]. Ak však verí, že pán Balfour bol neskoro predsedom vlády ^[6], bude stále veriť, že priezvisko posledného predsedu vlády sa začalo písmenom „B“, avšak táto viera, hoci je pravdivá, by sa nepovažovala za vedomosť. (Russell 1912)

Ako v príklade Červená stodola, ktorý je uvedený v oddiele 1.1, tu sa musíme zaoberať dvoma odôvodneniami pravdivého výroku, z ktorých jedno je správne a druhé nie. Nech B je veta (výrokový atóm), w je označená premenná odôvodnenia z nesprávneho dôvodu pre B a ra označená premenná odôvodnenia pre správny (teda skutočný) dôvod pre B. Potom Russellov príklad vyvolá nasledujúce predpoklady ^[7]:

R = {w: B, r: B, r: B → B}

Trochu v rozpore s intuíciou je možné logicky odvodiť faktivitu w z R:

1. r: B (predpoklad)
2. r: B → B (predpoklad)
3. B (od 1 do 2 od Modusa Ponensa)
4. B → (w: B → B) (výroková axióma)
5. w: B → B (od 3 do 4 od Modusa Ponensa)

Táto derivácia však využíva skutočnosť, že r je faktickým dôvodom pre B, aby sa dospelo k záveru w: B → B, čo predstavuje prípad „indukovanej faktivity“pre w: B. Otázka znie, ako je možné rozlíšiť „skutočnú“faktickosť r: B od „indukovanej faktivity“w: B? Je tu potrebný istý druh sledovania pravdy a Odôvodnenie Logika je vhodným nástrojom. Prirodzený prístup spočíva v zvážení súboru predpokladov bez r: B, tj

S = {w: B, r: B → B}

a stanovte, že faktickosť w, tj w: B → B nie je odvoditeľná od S. Tu je možný model svetového odôvodnenia M = (G, R, E, V), v ktorom S platí, ale w: B → B nie:

• G = { 1 },
• R = ∅,
• V (B) = ∅ (a teda nie - 1 ⊩ B),
• E (t, F) = { 1 } pre všetky páry (t, F) okrem (r, B) a
• E (r, B) = ∅.

Je ľahké vidieť, že podmienky na uzavretie žiadosti a súčet na E sú splnené. V 1, w: B platí, tj

1 ⊩ w: B

pretože w je prípustný dôkaz pre B na 1 a nie sú možné žiadne svety prístupné od 1. ďalej

nie - 1 ⊩ r: B

keďže podľa E r nie je prípustným dôkazom pre B na 1. Z toho dôvodu:

1 r: B → B

Na druhej strane,

nie - 1 ⊩ w: B → B

pretože B sa nedrží 1.

7. Vlastná referenčnosť odôvodnení

Realizačné algoritmy niekedy vytvárajú konštantné špecifikácie obsahujúce tvrdenia o autoreferenčnom opodstatnení c: A (c), to znamená, v ktorých sa zdôvodnenie (tu c) vyskytuje v tvrdenom tvrdení (tu A (c)).

Sebepreferencia ospravedlnení je nový jav, ktorý sa v konvenčnom modálnom jazyku nenachádza. Okrem zaujímavých epistemických predmetov, také samoštúdiové tvrdenia poskytujú zo sémantického hľadiska zvláštnu výzvu kvôli zabudovanému začarovanému kruhu. Na vyhodnotenie c sa skutočne očakáva, že najskôr vyhodnotí A a potom priradí objekt oprávnenia pre A až c. To však nie je možné, pretože A obsahuje c, ktorý sa ešte musí vyhodnotiť. Hlavnou otvorenou otázkou v tejto oblasti bola otázka, či je možné realizovať modálnu logiku bez použitia autoreferenčných odôvodnení.

Hlavný výsledok Kuznets v (Brežněv a Kuznets 2006) uvádza, že pri realizácii S4 v LP je nevyhnutná autoreferencia odôvodnení. Aktuálny stav vecí je daný Kuznetsovou vetou:

Veta 5: Pri realizácii modálnej logiky K a D sa možno vyhnúť autoreferenčnosti pri realizácii modálnej logiky T, K4, D4 a S4.

Táto veta potvrdzuje, že systém odôvodňujúcich výrazov pre S4 bude nevyhnutne samoreferenčný. To vytvára vážne, aj keď nie priamo viditeľné, obmedzenie sémantiky preukázateľnosti. V Gödelianskom kontexte aritmetických dôkazov sa problém vyrovnal všeobecnou metódou priradenia aritmetickej sémantiky k samoreferenčným tvrdeniam c: A (c) konštatovaním, že c je dôkazom A (c). V LP Logic of Proofs sa zaoberala netriviálnou konštrukciou s pevným bodom.

Sebepreferencia dáva zaujímavý pohľad na Mooreov paradox. Podrobnosti nájdete v oddiele 6 doplnkového dokumentu Niektoré ďalšie technické záležitosti.

8. Kvantifikátory v odôvodnení logiky

Zatiaľ čo skúmanie výrokovej odôvodnenia Logika nie je ani zďaleka ukončená, sporadické práce sa vyskytli aj vo verziách prvého poriadku. Kvantifikované verzie modálnej logiky už ponúkajú zložitosti nad rámec štandardnej logiky prvého poriadku. Kvantifikácia má ešte širšie pole, pokiaľ ide o odôvodnenie logiky. Klasicky jeden kvantifikuje „objekty“a modely sú vybavené doménou, v ktorej sa kvantifikátory pohybujú. Jeden môže mať jednu doménu spoločnú pre všetky možné svety alebo jeden môže mať samostatné domény pre každý svet. Úloha Barcanovej formule je tu dobre známa. Pre logiku Odôvodnenie sú k dispozícii aj konštantné aj rôzne možnosti domény. Okrem toho existuje možnosť, ktorá nemá žiadny analóg pre Modal Logic: človek by mohol kvantifikovať samotné zdôvodnenia.

Počiatočné výsledky týkajúce sa možnosti kvantifikovanej logiky odôvodnenia boli obzvlášť nepriaznivé. Sémantika aritmetickej preukázateľnosti pre Logic of Proofs LP sa prirodzene zovšeobecňuje na verziu prvého rádu s konvenčnými kvantifikátormi a na verziu s kvantifikátormi overenými nátlačkami. V obidvoch prípadoch boli otázky týkajúce sa axiomatizovateľnosti zodpovedané negatívne.

Veta 6: Logika dôkazov prvého poriadku nie je rekurzívne vyčísliteľná (Artemov a Yavorskaya (Sidon) 2001). Logika dôkazov s kvantifikátormi nad dôkazmi nie je rekurzívne vyčísliteľná (Yavorsky 2001).

Aj keď aritmetická sémantika nie je možná, v (Fitting 2008) bola možná verzia svetovej sémantiky a teória axiomatických dôkazov pre verziu LP s kvantifikátormi siahajúcimi nad odôvodnenia. Bola preukázaná spoľahlivosť a úplnosť. V tomto bode je možná svetová sémantika oddelená od aritmetickej sémantiky, ktorá môže alebo nemusí byť príčinou poplachu. Ukázalo sa tiež, že S4 vkladá do kvantifikovanej logiky prekladom □ Z ako „existuje odôvodnenie x také, že x: Z ^* “, kde Z ^* je preklad Z. Aj keď je táto logika trochu komplikovaná, našla aplikácie, napr. V (Dean a Kurokawa 2009b) sa používa na analýzu Knower Paradoxu, hoci v tejto súvislosti boli vznesené námietky (Arlo-Costa a Kishida 2009).

Uskutočnilo sa aj úsilie o verzie odôvodnenia logiky s kvantifikátormi nad objektmi, a to s analógom Barcanovho vzorca aj bez neho. Nič z toho nebolo zverejnené a malo by sa považovať za stále prebiehajúce práce.

9. Historické poznámky

Pôvodný systém logiky odôvodnenia, Logic of Proofs LP, bol zavedený v roku 1995 v (Artemov 1995) (porovnaj tiež (Artemov 2001)), kde boli prvýkrát zavedené také základné vlastnosti ako Internalizácia, Realizácia, aritmetická úplnosť. LP ponúkol zamýšľanú sémantiku vykonateľnosti pre Gödelovu logiku preukázateľnosti S4, čím poskytol formalizáciu Brouwer-Heyting-Kolmogorovovej sémantiky pre intuicionálnu výrokovú logiku. Epistemická sémantika a úplnosť (Fitting 2005) boli prvýkrát zavedené pre LP. Symbolické modely a rozhodnuteľnosť pre LP sú spôsobené Mkrtychevom (Mkrtychev 1997). Odhady zložitosti sa prvýkrát objavili v roku (Brežněv a Kuznets 2006, Kuznets 2000, Milnikel 2007). Komplexný prehľad všetkých výsledkov rozhodovania a zložitosti možno nájsť v (Kuznets 2008). Systémy J, J4,a JT sa prvýkrát posudzovali v roku (Brežněv 2001) pod rôznymi názvami av mierne odlišnom prostredí. JT45 sa objavil samostatne v (Pacuit 2006) a (Rubtsova 2006) a JD45 v (Pacuit 2006). Logika dôkazov proti jednému záveru bola nájdená v (Krupski 1997). Všeobecnejší prístup k spoločným znalostiam založený na odôvodnených znalostiach bol ponúknutý v (Artemov 2006). Herná sémantika odôvodnenia Logická a dynamická epistemická logika s odôvodneniami bola študovaná v (Renne 2008, Renne 2009). Prepojenia medzi odôvodnením a logikou a problémom logickej vševedúcnosti sa skúmali v (Artemov a Kuznets 2009, Wang 2009). Názov Odôvodnenie Logika bol zavedený v roku (Artemov 2008), v ktorom boli formalizované príklady Kripkeho, Russella a Gettiera; táto formalizácia sa použila na vyriešenie paradoxov, overenie,analýza skrytých predpokladov a odstránenie prepúšťania. V (Dean a Kurokawa 2009a) sa na analýzu paradoxov Knower a Knowability použila Odôvodnenie Logic.

Bibliografia

• Antonakos, E. (2007). „Oprávnené a spoločné znalosti: obmedzená konzervativita“, v S. Artemov a A. Nerode (eds.), Logické základy informatiky, medzinárodné sympózium, LFCS 2007, New York, NY, USA, 4. - 7. júna 2007, zborník. (Poznámky k prednáške v informatike: zväzok 4514), Berlín: Springer, s. 1–11.
• Arlo-Costa, H. a K. Kishida (2009). „Tri dôkazy a Knower v kvantifikovanej logike dôkazov“, na seminári o formálnej epistológii / FEW. Zborník, Carnegie Mellon University, Pittsburgh, PA, USA.
• Artemov, S. (1995). „Prevádzková modálna logika“, technická správa MSI 95–29, Cornell University.
• ---. (2001). „Explicitná preukázateľnosť a konštruktívna sémantika“, Bulletin of Symbolic Logic, 7 (1): 1-36.
• ---. (2006). „Oprávnené všeobecné znalosti“, Teoretická informatika, 357 (1–3): 4–22.
• ---. (2008). „Logika odôvodnenia“, Prehľad symbolickej logiky, 1 (4): 477–513.
• Artemov, S. a R. Kuznets (2009). „Logická vševeda ako problém výpočtovej zložitosti“, v A. Heifetz (ed.), Teoretické aspekty racionality a znalostí, zborník z 12. konferencie (TARK 2009), vydavatelia ACM, s. 14–23.
• Artemov, S. a E. Nogina (2005). „Zavádzanie odôvodnenia do epistemickej logiky“, Journal of Logic and Computation, 15 (6): 1059–1073.
• Artemov, S. a T. Yavorskaya (Sidon) (2001). „K logike dôkazov prvého poriadku“, Moscow Mathematical Journal, 1 (4): 475–490.
• Boolos, G. (1993). Logika zabezpečenia, Cambridge: Cambridge University Press.
• Brežněv, V. (2001). „O logike dôkazov“, v K. Striegnitz (ed.), Zborník zo šiesteho zasadnutia študentov ESSLLI, 13. Európska letná škola logiky, jazyka a informácií (ESSLLI'01), s. 35–46.
• Brežněv, V. a R. Kuznets (2006). „Zjednodušenie vedomostí: aké ťažké to je“, Teoretická informatika, 357 (1–3): 23–34.
• Cubitt, RP a R. Sugden (2003). „Spoločné znalosti, význam a konvencia: Obnova teórie hry Davida Lewisa“, Economics and Philosophy, 19: 175–210.
• Dean, W. a H. Kurokawa (2009a). „Od paradoxu poznateľnosti k existencii dôkazov“, Synthese, 176 (2): 177–225.
• ---. (2009b). „Znalosti, dôkazy a vedomosti“, v A. Heifetz (ed.), Teoretické aspekty racionality a znalostí, zborník z 12. konferencie (TARK 2009), ACM Publications, s. 81–90.
• Dretske, F. (2005). „Sú vedomosti uzavreté na základe známeho vedomia? Prípad proti zatvoreniu “, M. Steup a E. Sosa (ed.), Contemporary Debs in Epistemology, Oxford: Blackwell, s. 13–26.
• Fagin, R., J. Halpern, Y. Moses a M. Vardi (1995). Zdôvodnenie o znalostiach, Cambridge, MA: MIT Press.
• Fitting, M. (2005). „Logika dôkazov, sémanticky“, Annals of Pure and Applied Logic, 132 (1): 1–25.
• ---. (2006). „Náhradná veta za LP “, technická správa TR-2006002, Katedra počítačov, City University v New Yorku.
• ---. (2008). „Kvantifikovaná logika dôkazov“, Annals of Pure and Applied Logic, 152 (1–3): 67–83.
• ---. (2009). „Realizácie a LP “, Annals of Pure and Applied Logic, 161 (3): 368–387.
• Gettier, E. (1963). „Je ospravedlnenie skutočného vedomia viery?“Analýza, 23: 121 - 123.
• Girard, J.-Y., P. Taylor a Y. Lafont (1989). Dôkazy a typy (Cambridge Tracts in Computer Science: Zväzok 7), Cambridge: Cambridge University Press.
• Gödel, K. (1933). „Eine Interpretation des intuitionistischen Aussagenkalkuls“, Ergebnisse Math. Kolloq., 4: 39–40. Anglický preklad v: S. Feferman et al. (ed.), Kurt Gödel Collected Works (zväzok 1), Oxford a New York: Oxford University Press a Clarendon Press, 1986, s. 301 - 303.
• ---. (1938). „Vortrag bei Zilsel / prednáška v Zilsel's“(* 1938a), v S. Feferman, JJ Dawson, W. Goldfarb, C. Parsons a R. Solovay (ed.), Neuverejnené eseje a prednášky (Kurt Gödel Collected Works: Volume) III), Oxford: Oxford University Press, 1995, s. 86 - 113.
• Goldman, A. (1967). „Kauzálna teória významu“, Journal of Philosophy, 64: 335–372.
• Goodman, N. (1970). „Teória konštrukcií je ekvivalentná aritmetike“, v J. Myhill, A. Kino a R. Vesley (ed.), Intuitionism and Proof Theory, Amsterdam: North-Holland, s. 101–120.
• Goris, E. (2007). „Explicitné dôkazy vo formálnej logike vykonateľnosti“, v S. Artemov a A. Nerode (ed.), Logické základy informatiky, medzinárodné sympózium, LFCS 2007, New York, NY, USA, 4. - 7. júna 2007, zborník (ecture Notes in Computer Science: Zväzok 4514), Berlín: Springer, s. 241–253.
• Hendricks, V. (2005). Mainstreamová a formálna epistemológia, New York: Cambridge University Press.
• Heyting, A. (1934). Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, Berlín: Springer.
• Hintikka, J. (1962). Znalosť a viera, Ithaca: Cornell University Press.
• Kleene, S. (1945). „K interpretácii intuicionálnej teórie čísel“, The Journal of Symbolic Logic, 10 (4): 109–124.
• Kolmogorov, A. (1932). „Zur Deutung der Intuitionistischen Logik“, Mathematische Zeitschrift, 35: 58–65. Anglický preklad v VM Tikhomirov (ed.), Vybrané diela AN Kolmogorov. Zväzok I: Matematika a mechanika, Dordrecht: Kluwer, 1991, s. 151–158.
• Kreisel, G. (1962). „Základy intuicionistickej logiky“, v publikáciách E. Nagel, P. Suppes a A. Tarski (ed.), Logic, Methodology and Philosophy of Science. Zborník z medzinárodného kongresu 1960, Stanford: Stanford University Press, s. 198–210.
• ---. (1965). „Matematická logika“, v T. Saaty (ed.), Lectures in Modern Mathematics III, New York: Wiley and Sons, s. 95–195.
• Krupski, V. (1997). „Prevádzková logika dôkazov s podmienkou funkčnosti na predikáte dôkazov“, S. Adian a A. Nerode (ed.), Logické základy informatiky, 4. medzinárodné sympózium, LFCS'97, Jaroslavľ, Rusko, 6. - 12. júla 1997., Proceedings (Notes on Computer Science: Zväzok 1234), Berlin: Springer, pp. 167–177.
• Kurokawa, H. (2009). „Tabulky a hypersequenty na odôvodnenie logiky“, v S. Artemov a A. Nerode (eds.), Logické základy informatiky, medzinárodné sympózium, LFCS 2009, Deerfield Beach, FL, USA, 3. - 6. januára 2009, zborník (Poznámky k prednáškam z informatiky: Zväzok 5407), Berlín: Springer, s. 295–308.
• Kuznets, R. (2000). „O komplexnosti explicitnej modálnej logiky“, v P. Clote a H. Schwichtenberg (ed.), Počítačová veda, logika, 14. medzinárodný seminár, CSL 2000, výročná konferencia EACSL, Fischbachau, Nemecko, 21. - 26. augusta 2000., Proceedings (Notes on Computer Science: Zväzok 1862), Berlin: Springer, pp. 371–383.
• ---. (2008). Otázky zložitosti v odôvodnení Logika, dizertačná práca Ph.
• ---. (2010). „Poznámka k abnormalite realizácie S4LP “, v K. Brünnler a T. Studer (ed.), Dôkaz, výpočty, zložitosť PCC 2010, medzinárodný seminár, zborník, IAM-technické správy IAM-10-001, Ústav počítačov Veda a aplikovaná matematika, Univerzita v Berne.
• McCarthy, J., M. Sato, T. Hayashi a S. Igarishi (1978). „O modelovej teórii vedomostí“, Technická správa STAN-CS-78-667, Katedra počítačov, Stanfordská univerzita.
• Milnikel, R. (2007). „Odvoditeľnosť v určitých subsystémoch logiky dôkazov je Π ₂ ^p úplná“, Annals of Pure and Applied Logic, 145 (3): 223–239.
• ---. (2009). „Konzervativita pre logiku odôvodnenej viery“, v S. Artemov a A. Nerode (ed.), Logické základy informatiky, medzinárodné sympózium, LFCS 2009, Deerfield Beach, FL, USA, 3. - 6. januára 2009, zborník (Poznámky k prednáškam v informatike: Zväzok 5407), Berlín: Springer, s. 354–364.
• Mkrtychev, A. (1997). „Modely pre logiku dôkazov“, v S. Adian a A. Nerode (ed.), Logické základy informatiky, 4. medzinárodné sympózium, LFCS'97, Jaroslavľ, Rusko, 6. - 12. júla 1997, zborník (prednáška) Poznámky v informatike: zväzok 1234), Berlín: Springer, s. 266 - 275.
• Nogina, E. (2006). „K logike dôkazov a preukázateľnosti“, letné stretnutie Združenia pre symbolickú logiku v roku 2005, Logické kolokvium'05, Atény, Grécko (28. júla - 3. augusta 2005), Bulletin symbolickej logiky, 12 (2): 356,
• ---. (2007). „Epistemická úplnosť GLA “, na výročnom zasadnutí Asociácie pre symbolickú logiku, Florida University, Florida, Gainesville, Florida (10. - 13. marca 2007), Bulletin of Symbolic Logic, 13 (3): 407.
• Pacuit, E. (2006). „Poznámka k niektorej výslovnej modálnej logike“, technická správa PP – 2006–29, Inštitút pre logiku, jazyk a výpočet, University of Amsterdam.
• Plaza, J. (2007). „Logika verejných komunikácií“, Synthese, 158 (2): 165–179.
• Renne, B. (2008). Dynamická epistemická logika s odôvodnením, dizertačná práca, oddelenie informatiky, postgraduálne centrum CUNY, New York, NY, USA.
• ---. (2009). „Eliminácia dôkazov v logike viacerých agentov“, v A. Heifetz (ed.), Teoretické aspekty racionality a znalostí, zborník z 12. konferencie (TARK 2009), ACM Publications, s. 227–236.
• Rose, G. (1953). „Propozičný počet a realizovateľnosť“, Transactions of American Mathematical Society, 75: 1–19.
• Rubtsova, N. (2006). „O realizácii modality S5 podľa dôkazných podmienok“, Journal of Logic and Computation, 16 (5): 671–684.
• Russell, B. (1912). Problémy filozofie, Oxford: Oxford University Press.
• Sidon, T. (1997). „Logika zabezpečovania s operáciami na základe dôkazov“, S. Adian a A. Nerode (ed.), Logické základy informatiky, 4. medzinárodné sympózium, LFCS'97, Jaroslavľ, Rusko, 6. - 12. júla 1997, zborník (prednáška) Poznámky v informatike: zväzok 1234), Berlín: Springer, s. 342 - 353.
• Troelstra, A. (1998). „Realizability“, v S. Buss (ed.), Handbook of Proof Theory, Amsterdam: Elsevier, s. 407–474.
• Troelstra, A. a H. Schwichtenberg (1996). Basic Proof Theory, Amsterdam: Cambridge University Press.
• Troelstra, A. a D. van Dalen (1988). Konštruktivizmus v matematike (zväzky 1, 2), Amsterdam: Severné Holandsko.
• van Dalen, D. (1986). „Intuitionistická logika“, v D. Gabbay a F. Guenther (ed.), Handbook of Philosophical Logic (Zväzok 3), Bordrecht: Reidel, s. 225 - 340.
• van Ditmarsch, H., W. van der Hoek a B. Kooi (ed.), (2007). Dynamická epistemická logika (Synthese Library, zväzok 337), Berlín: Springer..
• von Wright, G. (1951). Esej v modálnej logike, Amsterdam: Severný Holland.
• Wang, R.-J. (2009). „Znalosti, čas a logická vševeda“, v H. Ono, M. Kanazawa a R. de Queiroz (ed.), Logic, Language, Information and Computation, 16. medzinárodný seminár, WoLLIC 2009, Tokio, Japonsko, 21. júna. -24, 2009, Zborník (Prednášky z umelej inteligencie: Zväzok 5514), Berlín: Springer, s. 394–407.
• Yavorskaya (Sidon), T. (2001). „Logika dôkazov a preukázateľnosti“, Annals of Pure and Applied Logic, 113 (1–3): 345–372.
• ---. (2008). „Interakcia systémov explicitného dôkazu“, Teória počítačových systémov, 43 (2): 272–293.
• Yavorsky, R. (2001). „Logika zabezpečiteľnosti s kvantifikátormi na dôkazoch“, Annals of Pure and Applied Logic, 113 (1–3): 373–387.

Akademické nástroje

	Ako citovať tento záznam.
	Ukážku verzie tohto príspevku vo formáte PDF si môžete pozrieť na stránke Friends of the SEP Society.
	Vyhľadajte túto vstupnú tému v projekte Indiana Philosophy Ontology Project (InPhO).
	Vylepšená bibliografia tohto záznamu vo PhilPapers s odkazmi na jeho databázu.

Ďalšie internetové zdroje