Pagrindimas Logika

Turinys:

Pagrindimas Logika
Pagrindimas Logika

Video: Pagrindimas Logika

Video: Pagrindimas Logika
Video: #35 склеропластика у детей: за и против 2024, Kovo
Anonim

Tai yra failas Stanfordo filosofijos enciklopedijos archyvuose. Informacija apie autorius ir citata | Draugai PDF peržiūra | „InPho“paieška | „PhilPapers“bibliografija

Pagrindimas Logika

Pirmą kartą paskelbta 2011 m. Birželio 22 d., Trečiadienis; esminė peržiūra 2011 m. liepos 20 d., trečiadienis

Galite sakyti: „Aš žinau, kad Abraomas Linkolnas buvo aukštas žmogus. Savo ruožtu jūsų gali paklausti, kaip jūs žinote. Jūs beveik tikrai neatsakysite semantiškai, Hintikka stiliaus, kad Abraomas Linkolnas buvo aukštas visose situacijose, suderinamose su jūsų žiniomis. Geriau jūs sakysite: „Aš perskaičiau Abraomo Linkolno ūgį keliose knygose ir mačiau jo nuotraukas šalia kitų žmonių. „Žinias patvirtina pateikdamas priežastį, pagrindimą. Hintikka semantika žinias užfiksuoja kaip tikrąjį įsitikinimą. Pagrindimas Logika pateikia trūkstamą trečiąjį Platono žinių apibūdinimo komponentą kaip pagrįstą tikrąjį įsitikinimą.

  • 1. Kodėl logika?

    • 1.1 Episteminė tradicija
    • 1.2 Matematinės logikos tradicija
  • 2. Pagrindiniai logikos pagrindimo komponentai

    • 2.1 Paaiškinimo logikos kalba
    • 2.2 Pagrindinė logika J 0
    • 2.3 Loginis supratimas ir nuolatinės specifikacijos
    • 2.4 Funkcionalumas
    • 2.5 Teigiama savistaba
    • 2.6 Neigiama savistaba
  • 3. Semantika

    • 3.1 Galimas vieno agento pasaulinis pagrindimas J
    • 3.2 Silpnas ir ryškus išsamumas
    • 3.3 Vieno agento šeima
    • 3.4 Bendro pasaulio modeliai
  • 4. Realizacijos teoremos
  • 5. Apibendrinimai

    • 5.1 Aiškių ir numanomų žinių sumaišymas
    • 5.2 Galimi įvairių agentų pasaulio modeliai
  • 6. Russello pavyzdys: sukeltas veikimas
  • 7. Pateisinimų savireferencija
  • 8. Pateisinimo logikos kiekybiniai rodikliai
  • 9. Istorinės pastabos
  • Bibliografija
  • Akademinės priemonės
  • Susiję įrašai
  • Kiti interneto šaltiniai

1. Kodėl logika?

Pagrindimas Logika yra episteminė logika, leidžianti žinių ir įsitikinimų būdus „išskleisti“pateisinimo terminais: vietoj □ X rašoma t: X ir skaitoma kaip „X pateisinamas priežastimi t“. Galima galvoti apie tradicinius modalinius operatorius kaip netiesioginį modalumą, o pateisinimo terminus - kaip apie jų aiškų detalizavimą, papildantį modalinę logiką smulkesne epistemine mašina. Pateisinimo terminų šeima turi struktūrą ir operacijas. Pasirinkus operacijas atsiranda skirtinga pateisinimo logika. Visoms įprastoms episteminėms logikoms jų būdai gali būti visiškai išskleisti į aiškų pagrindimo pavidalą. Šiuo atžvilgiu Pagrindimas Logika atskleidžia ir naudoja aiškų, bet paslėptą tradicinės episteminės modinės logikos turinį.

Pagrindimas Logika atsirado kaip dalis sėkmingo projekto, pateikiančio konstruktyvią intuicionistinių loginių pagrindimų sąvokų semantiką, pašalinančią visas, išskyrus pačias pagrindines matematinių įrodymų savybes. Įrodymai yra pateisinimas gryniausia forma. Vėliau pagrindimo logika buvo įtraukta į formaliąją epistemologiją. Straipsnyje pateikiamas bendras šiuo metu suprantamas pagrindimo logikos spektras. Aptariami jų santykiai su įprastine modaline logika. Be techninės įrangos, straipsnyje nagrinėjama, kaip aiškių pagrindimo terminų vartojimas atspindi daugelį tradicinių filosofinių problemų. Visa tema vis dar aktyviai plėtojama. Tai, kas čia pateikiama, yra trumpas vaizdas rašymo metu.

Pateisinimo logikos šaknis galima atsekti daugelyje skirtingų šaltinių, iš kurių du išsamiai aptariami: epistemologija ir matematinė logika.

1.1 Episteminė tradicija

Žinių ir įsitikinimų savybės buvo formalios logikos objektas bent jau nuo von Wright ir Hintikka (Hintikka 1962, von Wright 1951). Tiek žinios, tiek įsitikinimai traktuojami kaip dabar labai gerai pažįstami būdai - episteminė logika. Tačiau iš trijų Platono žinių kriterijų, pagrįstų, teisingų, tikinčių (Gettier 1963, Hendricks 2005), episteminė logika iš tikrųjų veikia tik su dviem iš jų. Galimi pasauliai ir neišskiriamumo modelio įsitikinimas - žmogus tiki tuo, kas taip yra, bet kokiomis aplinkybėmis manoma. Veiksmingumas į žaidimą įtraukia tiesos komponentą - jei kažkas ne taip yra realiame pasaulyje, to negalima žinoti, tik tikėti. Tačiau pateisinimo sąlyga nepateikiama. Nepaisant to,modaliinis požiūris buvo nepaprastai sėkmingas, nes leido plėtoti turtingą matematikos teoriją ir pritaikymą (Fagin, Halpern, Moses ir Vardi, 1995, van Ditmarsch, van der Hoek ir Kooi 2007). Vis dėlto tai nėra visas vaizdas.

Modalinis požiūris į žinių logiką tam tikra prasme yra paremtas universaliu kiekybiniu rodikliu: X yra žinomas situacijoje, jei X yra teisingas visose situacijose, kurios nesiskiria nuo tos. Pateisinimai, kita vertus, atneša egzistencinį skaičių į paveikslėlį: X yra žinomas situacijoje, jei toje situacijoje yra X pateisinimas. Ši universali / egzistencinė dichotomija yra gerai žinoma logikams, formali logika egzistuoja X formulės įrodymu, jei ir tik tuo atveju, jei X yra teisinga visuose logikos modeliuose. Galima manyti, kad modeliai iš esmės nėra konstruktyvūs, o įrodymai - kaip konstruktyvūs dalykai. Niekur nesuklysime galvodami apie pagrindimus apskritai, kaip ir apie matematinius įrodymus. Iš tikrųjų pirmoji pateisinimo logika buvo aiškiai skirta matematiniams įrodymams fiksuoti aritmetinėje,tai, kas bus išsamiau aptarta 1.2 skyriuje.

Pagrindimas Logikoje, be formulių kategorijos, yra ir antra pateisinimo kategorija. Pateisinimas yra formalūs terminai, sudaryti iš konstantų ir kintamųjų, naudojant įvairius operacijos simbolius. Konstantos atspindi visuotinai priimtinų tiesų aksiomų tipus. Kintamieji žymi nepatikslintus pagrindimus. Skirtinga pateisinimo logika skiriasi tuo, kurios operacijos yra leidžiamos (taip pat ir kitais būdais). Jei t yra pateisinamasis terminas, o X yra formulė, t: X yra formulė ir yra skirta skaityti:

t yra X pateisinimas.

Viena operacija, bendra visoms pagrindimo logikoms, yra taikymas, parašytas kaip daugyba. Idėja yra, jei S yra pagrindimas A → B ir T yra pagrindimas A, tada [S ⋅ T] yra pagrindimas B [1]. T. y., Paprastai daroma prielaida:

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

Tai yra aiškus įprasto žinių operatorių pasiskirstymo ir apskritai įvairių transporto rūšių operatorių pasiskirstymo variantas:

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

Tiesą sakant, formulė (2) yra už daugelio loginio visažinio problemų problemų. Jis tvirtina, kad agentas žino viską, ką implikuoja agento žinios. Poveikis yra uždarytas. Nors iš principo žinomas, žinomumas yra uždaromas, to negalima pasakyti apie bet kokią įtikinamą faktinių žinių variantą. Skirtumą tarp (1) ir (2) galima panaudoti aptariant paradigminį Raudonojo svirno pavyzdį: Goldmanas ir Kripke; čia yra supaprastinta istorijos versija, paimta iš (Dretske 2005).

Tarkime, aš važiuoju per apylinkes, kuriose, man nežinant, papier-mâché tvartai yra išsibarstę ir matau, kad priešais mane esantis daiktas yra tvartas. Kadangi turiu suvokimą apie tvartą prieš mane, manau, kad priešais mane esantis daiktas yra tvartas. Mūsų intuicija rodo, kad aš nepažįstu tvarto. Bet dabar tarkime, kad kaimynystėje nėra netikrų raudonų tvartų, taip pat pastebiu, kad priešais mane esantis daiktas yra raudonas, todėl žinau, kad ten yra raudonas tvartas. Šis derinimas, būdamas raudonas tvartas, kurį aš žinau, reiškia, kad yra tvartas, kurio aš neturiu, „yra sumišimas“.

Pirmą kartą įforminus Raudonojo svirno pavyzdį, loginis išvedimas bus atliekamas pagal pagrindinę modalinę logiką, kurioje □ aiškinamas kaip „tikėjimo“modalumas. Tada kai kurie iš □ atvejų bus išoriškai interpretuojami kaip „žinios“pagal problemos aprašymą. Tegul B yra sakinys „objektas priešais mane yra tvartas“, o R - sakinys „objektas priešais mane yra raudonas“.

  1. □ B, „Manau, kad priešais mane esantis daiktas yra tvartas“;
  2. □ (B ∧ R), „Manau, kad priešais mane esantis daiktas yra raudonas tvartas“.

Meta lygmenyje 2 iš tikrųjų yra žinios, o problemos aprašyme 1 nėra žinios.

□ (B ∧ R → B), loginės aksiomos žinių tvirtinimas

Atliekant šį formalizavimą paaiškėjo, kad pažeidžiamas jo modifikuotos formos episteminis uždarymas: 2 eilutė, □ (B □ R) ir 3 eilutė, □ (B ∧ R → B) yra žinių atvejai, tuo tarpu □ B (linija) 1) nėra žinios. Atrodo, kad modalinė kalba nepadėjo išspręsti šios problemos.

Toliau apsvarstykite Raudonojo svirno pavyzdį logikoje, kur t: F yra suprantamas kaip „aš tikiu, kad F dėl t priežasties“. Tegul yra konkretus pateisinimas įsitikinimui, kad B, ir v, jei tikima, kad B ∧ R. Be to, leiskime pateisinti loginę tiesą B ∧ R → B. Tada prielaidų sąrašas yra:

  1. u: B, „u yra priežastis manyti, kad priešais mane esantis daiktas yra tvartas“;
  2. v:(B ∧ R), „v yra priežastis manyti, kad priešais mane esantis daiktas yra raudonas tvartas“;
  3. a:(B ∧ R → B).

Meta lygmenyje problemos aprašyme teigiama, kad 2 ir 3 yra ne tik tikėjimo, bet ir žinių atvejai, o 1 yra tikėjimas, o ne žinios. Štai kaip vyksta oficialūs samprotavimai:

  1. a:(B ∧ R → B) → (v:(B ∧ R) → [a ⋅ v]: B), pagal principą (1);
  2. v:(B ∧ R) → [a ⋅ v]: B, nuo 3 ir 4, pagal pasiūlymo logiką;
  3. [a ⋅ v]: B, nuo 2 ir 5, pagal pasiūlymo logiką.

Atkreipkite dėmesį, kad 6 išvada yra [a ⋅ v]: B, o ne u: B; episteminis uždarymas trunka. Motyvuojant pateisinimo logikoje buvo padaryta išvada, kad [a ⋅ v]: B yra žinių atvejis, ty „aš žinau B dėl priežasties a ⋅ v“. Tai, kad u: B nėra žinių atvejis, nepažeidžia uždarymo principo, nes pastarasis teigia, kad žino specialiai [a ⋅ v]: B. Taigi, pastebėjęs raudoną fasadą, aš iš tikrųjų žinau B, tačiau šios žinios neturi nieko bendra su 1, o tai lieka tikėjimo, o ne žinių pavyzdžiu. Pateisinimo logikos formalizavimas teisingai atspindi situaciją.

Stebėjimo pagrindimai atspindi Raudonojo svirno pavyzdžio struktūrą taip, kad jos neužfiksuotų tradiciniai episteminiai modaliniai įrankiai. Pagrindimas Loginis formalizavimas modeliuoja, kas tokiu atveju vyksta; Žinių uždarymas, atsižvelgiant į loginę prigimtį, išlaikomas, net jei „tvartas“nėra suvokiamas. [2]

1.2 Matematinės logikos tradicija

Anot Brouwerio, tiesa konstruktyvioje (intuicionistinėje) matematikoje reiškia įrodymo egzistavimą, plg. (Troelstra ir van Dalen 1988). 1931–34 Heytingas ir Kolmogorovas neoficialiai aprašė intuityvinės logikos semantiką, pagrįstą įrodymais (Kolmogorov 1932, Heyting 1934), kuri dabar vadinama Brouwer-Heyting-Kolmogorov (BHK) semantika. Remiantis BHK sąlygomis, formulė yra „teisinga“, jei ji turi įrodymą. Be to, jungtinio teiginio įrodymas yra sujungtas su jo komponentų įrodymais tokiu būdu:

  • A ∧ B įrodymą sudaro pasiūlymo A įrodymas ir pasiūlymo B įrodymas;
  • A ∨ B įrodymas pateikiamas pateikiant arba A, arba B įrodymą;
  • A → B įrodymas yra konstrukcija, paverčianti A įrodymus B įrodymais;
  • melagingumas ⊥ yra teiginys, neturintis įrodymų, ¬A yra santrumpa A → ⊥.

Kolmogorovas aiškiai užsiminė, kad jo aiškinime panašūs įrodymai („problemos sprendimai“) kilo iš klasikinės matematikos (Kolmogorovas 1932). Iš tikrųjų, žvelgiant iš pagrindų, nėra prasmės suprasti aukščiau pateiktus „įrodymus“kaip įrodymus intuicionistinėje sistemoje, kuriuos šios sąlygos turėtų nurodyti.

Pagrindinė BHK semantikos vertybė yra ta, kad neoficialiai, bet nedviprasmiškai siūloma pateisinimus, čia matematinius įrodymus, traktuoti kaip objektus su operacijomis.

(Gödel 1933), Gödel žengė pirmąjį žingsnį kuriant griežtą įrodymais pagrįstą intuicionizmo semantiką. Gödelis klasikinę modinę logiką S4 laikė skaičiavimo priemone, apibūdinančia patikimumo savybes:

  • Klasikinės teiginių logikos aksiomos ir taisyklės;
  • □ (F → G) → (□ F → □ G);
  • □ F → F;
  • □ F → □□ F;
  • Būtinumo taisyklė: jei ⊢ F, tada ⊢ □ F.

Remdamasis Brouwerio supratimu apie loginę tiesą kaip įrodomumą, Gödelis apibrėžė teigiamos formulės F vertimo tr (F) vertimą intuicionistine kalba į klasikinės modalinės logikos kalbą: tr (F) gaunamas priešdėliojant kiekvieną F podugnį su provokacija. modalumas □. Neoficialiai tariant, kai tr (F) atveju taikoma įprasta formulės klasikinės tiesos nustatymo procedūra, ji patikrins kiekvieno F pogrupio tikrumą (o ne tiesą), sutinkant su Brouwerio idėjomis. Remiantis Gödelio rezultatais ir McKinsey-Tarski atliktu modalinės logikos topologinės semantikos darbu, galima daryti išvadą, kad vertimas tr (F) leidžia tinkamai integruoti Intuitionistic Propositional Calculus (IPC) į S4, ty intuicionistinę logiką įterpti į klasikinę logiką. pratęsė patikimumo didinimo operatorius.

(3) Jei IPC įrodo F, tada S4 įrodo tr (F).

Vis dėlto pirminis Gödelio tikslas apibrėžti intuicionistinę logiką klasikinio įrodomumo prasme nebuvo pasiektas, nes nebuvo nustatytas S4 ryšys su įprasta matematiniu įrodomumo samprata. Be to, Gödelis pažymėjo, kad tiesi mintis interpretuoti modalumą □ F kaip F yra įrodyta tam tikroje formalioje sistemoje T, prieštaravo Gödelio antrajai neišsamumo teoremai. Iš tikrųjų □ (□ F → F) iš S4 gali būti išvedami pagal būtinumo taisyklę iš aksiomos □ F → F. Kita vertus, aiškindamas modalumą □ kaip T ir F teorinio formalumo įrodomumą kaip prieštaravimą, ši formulė virsta klaidingu teiginiu, kad T nuoseklumas T viduje yra įrodytas.

Padėtį po (Gödel 1933) galima apibūdinti tokiu paveikslu, kuriame „X ↪ Y“turėtų būti suprantamas kaip „X aiškinamas Y“

IPC ↪ S4 ↪? ↪ KLASIKINIAI ĮRODYMAI

1938 m. Vienoje vykusioje viešoje paskaitoje Gedelis pastebėjo, kad naudojant aiškių įrodymų formatą:

(4) t yra F įrodymas

gali padėti interpretuoti jo apskaičiavimo skaičiavimą S4 (Gödel 1938). Deja, Gödelio darbas (Gödel 1938) liko nepaskelbtas iki 1995 m., Iki to laiko jau buvo atrasta Gödelian aiškių įrodymų logika, aksiomatizuota kaip Proofs LP logika ir pateiktos išsamumo teoremos, jungiančios ją tiek su S4, tiek su klasikiniais įrodymais (Artemov). 1995).

Įrodymų logika LP tapo pirmąja Pagrindimas Logic šeimoje. Įrodomieji terminai LP yra ne kas kita, kaip BHK terminai, suprantami kaip klasikiniai įrodymai. Naudojant LP, intuityviosios logikos logika gavo norimą griežtą BHK semantiką:

IPC ↪ S4 ↪ LP ↪ KLASIKINIAI ĮRODYMAI

Norėdami išsamiau aptarti matematinės logikos tradicijas, skaitykite papildomo dokumento „Kai kurie daugiau techninių klausimų“1 skirsnį.

2. Pagrindiniai logikos pagrindimo komponentai

Šiame skyriuje pateikiama dažniausiai pasitaikančių pagrindimo logikos sistemų sintaksė ir aksiomatika.

2.1 Paaiškinimo logikos kalba

Norint sudaryti oficialią pateisinimo logikos ataskaitą, reikia padaryti pagrindinę struktūrinę prielaidą: pateisinimai yra abstraktūs objektai, kurie turi struktūrą ir operacijas. Gerą pateisinimų pavyzdį pateikia oficialūs įrodymai, kurie jau seniai yra matematinės logikos ir informatikos studijų objektas (plg. 1.2 skyrių).

Pagrindimas Logika yra oficiali loginė sistema, apimanti episteminius teiginius t: F, reiškiantis „t yra F pagrindimas“. Pagrindimas Logika tiesiogiai neanalizuoja, ką reiškia t pateisinti F, išskyrus t: F formatą, o bando apibūdinti šį ryšį aksiomatiškai. Tai yra panašu į tai, kaip Boole logika traktuoja savo jungiamuosius, tarkim, disjunkciją: neanalizuoja formulės p ∨ q, o greičiau prisiima tam tikras logines aksiomas ir tiesos lenteles apie šią formulę.

Priimti keli dizaino sprendimai. Pagrindimas Logika prasideda nuo paprasčiausio pagrindo: klasikinės loginės logikos ir dėl gerų priežasčių. Pateisinimas pateikia pakankamai rimtą iššūkį net paprasčiausiu lygmeniu. Raselo, Goldmano-Kripke'io, Gettier'io ir kitų paradigminius pavyzdžius galima nagrinėti naudojant Boolean Pagrindimas logiką. Episteminės logikos branduolį sudaro modalinės sistemos, turinčios klasikinę Boolean bazę (K, T, K4, S4, K45, KD45, S5 ir kt.), Ir kiekvienoje iš jų yra pateiktas atitinkamas loginio loginio pagrindo loginis papildymas.. Galiausiai ne visada manoma, kad pateisinimai yra faktiški. Tai leidžia užfiksuoti epistemologijos diskusijų, apimančių tikėjimo, o ne žinių, esmę.

Pagrindinė pagrindimo operacija yra taikymas ir suma. Taikymo operacija paima pagrindimus s ir t ir sukuria tokį pagrindimą s ⋅ t, kad jei s:(F → G) ir t: F, tada [s ⋅ t]: G. Simboliškai,

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

Tai yra pagrindimas, pateisinamas derinant logiką ir λ skaičiavimus (Troelstra ir Schwichtenberg 1996), Brouwer-Heyting-Kolmogorov semantika (Troelstra ir van Dalen 1988), Kleene įgyvendinamumas (Kleene 1945), Logic of Proofs LP ir kt..

Bet kuriuos du pagrindimus galima drąsiai sujungti į platesnio taikymo sritį. Tai atliekama naudojant operacijos sumą „+“. Jei s: F, tada kokie įrodymai gali būti t, jungtiniai įrodymai s + t išlieka F pateisinimu. Tiksliau tariant, „+“operacija priima pateisinimus s ir t ir sukuria s + t, tai yra pateisinimas viskuo, kas pateisinama s arba t.

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

Kaip motyvaciją galima manyti, kad s ir t yra du enciklopedijos tomai, o s + t - kaip šių dviejų tomų rinkinys. Įsivaizduokite, kad viename iš tomų, tarkim, s, yra pakankamas teiginio F pagrindimas, ty s: F. Tada didesnėje aibėje s + t taip pat pateikiamas pakankamas F, [s + t] pagrindimas: F. Įrodymų logikos LP 1.2 skyriuje „s + t“gali būti aiškinamas kaip įrodymų s ir t susikaupimas.

2.2 Pagrindinė logika J 0

Pagrindimas Terminai yra sudaryti iš pateisinamųjų kintamųjų x, y, z,… ir pagrindimo konstantos a, b, c,… (su indeksais i = 1, 2, 3,…, kurie praleidžiami, kai tik tai yra saugu) operacijų būdu “. ⋅ 'ir' + '. Išsamesnė logika, nagrinėjama toliau, taip pat leidžia atlikti papildomus veiksmus pagrindžiant. Konstantos žymi atomų pateisinimus, kurių sistema neanalizuoja; kintamieji žymi nepatikslintus pagrindimus. Pagrindinė pateisinimų logika J 0 aksiomatizuojama taip.

Klasikinė logika
Klasikinės teiginių aksiomos ir taisyklė Modusas Ponensas
Taikymo aksioma
s:(F → G) → (t: F → [s ⋅ t]: G),
Sumos aksiomos
s: F → [s + t]: F, s: F → [t + s]: F.

J 0 yra absoliučiai skeptiško agento, kuriam jokia formulė nėra pateisinama, bendrųjų (nebūtinai faktinių) pateisinimų logika, ty J 0 neišveda t: F bet kuriam t ir F. Tačiau toks agentas gali padaryti formos pagrindimo išvadas

Jei x: A, y: B,…, z: C palaikykite, tada t: F.

Turėdamas tokią galią J 0 gali tinkamai sekti kitas logikos sistemas savo kalba.

2.3 Loginis supratimas ir nuolatinės specifikacijos

Loginio supratimo principas teigia, kad loginės aksiomos yra pateisinamos ex officio: agentas priima logines aksiomas kaip pagrįstas (įskaitant tas, kurios susijusios su pateisinimais). Kaip ką tik minėjome, kai kuriose episteminėse situacijose loginis sąmoningumas gali būti per stiprus. Tačiau Pagrindimas „Logic“siūlo lankstų nuolatinių specifikacijų mechanizmą, kuris atspindi įvairius loginio sąmoningumo atspalvius.

Žinoma, galima atskirti prielaidą nuo pagrįstos prielaidos. Pagrindimas Logikos konstantos naudojamos prielaidoms pateisinti tais atvejais, kai jos daugiau neanalizuojamos. Tarkime, kad norima postuliuoti, kad A aksioma yra pagrįsta žinojui. Tiesiog postuluoja e 1: A tam tikriems įrodymams yra pastovi e 1 (su 1 rodykle). Be to, jei norima postuliuoti, kad šis naujas principas e 1: A taip pat pagrįstas, galima teigti, kad e 2:(e 1: A) yra pastovi e 2.(su 2 rodykle). Ir taip toliau. Stebėti indeksus nėra būtina, tačiau tai lengva ir padeda priimant sprendimus (Kuznets 2008). Visų šios rūšies prielaidų rinkinys tam tikrai logikai yra vadinamas Pastoviąja specifikacija. Čia yra oficialus apibrėžimas:

Pastovus Specifikacija CS už tam tikrą pagrindimas logika L yra formules nustatytą formą

e n: e n −1:…: e 1: A (n ≥ 1),

kur A yra L aksioma, o e 1, e 2,…, e n yra panašios konstantos su indeksais 1, 2,…, n. Manoma, kad CS yra visos tarpinės specifikacijos, ty kai n: e n − 1:…: e 1: A yra CS, tada e n − 1:…: e 1: A yra ir CS.

Literatūroje pateikiamos nuolatinės specifikacijos, susijusios su specialiomis sąlygomis. Dažniausiai pasitaiko šie dalykai.

Tuščia
CS = ∅. Tai atitinka absoliučiai skeptišką agentą. Tai prilygsta darbui su logika J 0.
Baigtinis
CS yra baigtinis formulių rinkinys. Tai visiškai reprezentatyvus atvejis, nes bet koks konkretus išaiškinimas Pagrindimas Logic bus susijęs tik su apibrėžtu konstantų rinkiniu.
Aksiomatiškai tinkama
Kiekviena aksioma, įskaitant tas, kurios naujai įgytos vykdant pačią nuolatinę specifikaciją, turi pagrindimą. Formaliame nustatyme kiekvienai aksiomai A yra pastovi e 1 tokia, kad e 1: A yra CS, o jei n: e n −1:…: e 1: A ∈ CS, tada e n +1: e n: e n −1:…: e 1: A ∈ CS kiekvienam n ≥ 1. Aksiomatiškai tinkamos pastovios specifikacijos yra būtinos norint užtikrinti internalizacijos savybę, aptariamą šio skyriaus pabaigoje.
Iš viso

Kiekvienai A aksiomai ir bet kurioms konstantoms e 1, e 2,… e n,

e n: e n −1:…: e 1: A ∈ CS.

Pavadinimas TCS rezervuotas visai konstantajai specifikacijai (tam tikrai logikai). Natūralu, kad bendra nuolatinė specifikacija yra aksiomatiškai tinkama.

Dabar galime nurodyti:

Pateisinimo logika, atsižvelgiant į nuolatinę specifikaciją:

Tegul CS yra nuolatinė specifikacija. J CS yra logika J 0 + CS; kartu su CS nariais yra J 0 aksiomos ir vienintelė išvadų taisyklė yra Modusas Ponensas. Atkreipkite dėmesį, kad J 0 yra J .

Teiginių logika

J yra logika J 0 + Aksiomų internalizacijos taisyklė. Naujojoje taisyklėje teigiama:

Kiekvienai A aksiomai ir bet kurioms konstantoms e 1, e 2,…, e n n e n e n e: −1:…: e 1: A.

Pastarasis įkūnija J. nevaržomo loginio supratimo idėją. Panaši taisyklė pasirodė LP logikoje „Logic of Proofs“, jos taip pat buvo numatyta ir Goldmano knygoje (Goldman 1967). Loginis sąmoningumas, išreikštas aksiomatiškai tinkamomis pastoviosiomis specifikacijomis, yra aiškus būtinybės taisyklės įkūnijimas modalinėje logikoje: ⊢ F ⇒ ⊢ □ F, bet apsiriboja aksiomomis. Atminkite, kad J sutampa su J TCS.

Pagrindinis logikos sistemų bruožas yra jų sugebėjimas internalizuoti savo išvestines kaip įrodomus teiginius jų kalbomis. Šis turtas buvo numatytas (Gödel 1938 m.).

1 teorema: Kiekviena aksiomatiškai tinkama nuolatinė specifikacija CS, J CS naudojasi internalizavimu:

Jei ⊢ F, tada ⊢ p: F tam tikram pagrindimo terminui p.

Įrodymas. Išvestinės ilgio indukcija. Tarkime, ⊢ F. Jei F yra J 0 narys arba CS narys, yra pastovi e n (kur n gali būti 1) tokia, kad e n: F yra CS, nes CS yra aksiomatiškai tinkama. Tada e n: F yra išvestinė. Jei F gauna Modusas Ponensas iš X → F ir X, tai pagal indukcijos hipotezę ⊢s:(X → F) ir ⊢ t: X kai kurioms s, t. Naudodami „Application Axiom“, ⊢ [s ⋅ t]: F.

Konkrečių sintaksinių darinių pateisinimo logikoje pavyzdžių ieškokite papildomo dokumento „Kai kurie daugiau techninių klausimų“2 skyriuje.

2.4 Funkcionalumas

Faktiškumas teigia, kad agentui pakanka pateisinimų, kad būtų galima padaryti išvadą apie tiesą. Tai aprašyta toliau.

Faktyvumo aksioma t: F → F.

Veiksmingumo aksioma turi panašią motyvaciją kaip ir episteminės logikos tiesos aksioma, □ F → F, kuri plačiai pripažįstama kaip pagrindinė žinių savybė.

Priešingai nei taikymo ir apibendrinimo principai, pagrindimo logiškumo sistemose pagrindimas nėra būtinas, todėl jos gali pateikti tiek dalinį, tiek faktinį pagrindimą. Faktiškumo aksioma pasirodė įrodymų logikos LP 1.2 skyriuje kaip pagrindinė matematinių įrodymų savybė. Iš tikrųjų šioje aplinkoje faktiškumas yra aiškiai pagrįstas: jei yra matematinis F įrodymas t, tada F turi būti tiesa.

Faktyvumo aksioma priimta siekiant pateisinimų, kurie veda prie žinių. Tačiau vien tik faktiškumas nereikalauja žinių, kaip parodė Gettier pavyzdžiai (Gettier 1963).

Faktinių pagrindimų logika

  • JT 0 = J 0 + Faktyvumas;
  • JT = J + Faktiškumas.

JT CS sistemos, atitinkančios nuolatinių specifikacijų CS, yra apibrėžtos kaip 2.3 skirsnyje.

2.5 Teigiama savistaba

Vienas iš bendrų žinių principų yra žinoti ir žinoti, kad žmogus žino. Modalinėje aplinkoje tai atitinka □ F → □□ F. Šis principas turi aiškų atitikmenį: faktas, kad agentas priima t kaip pakankamus įrodymus F, yra pakankamas įrodymas t: F. Dažnai tokie meta įrodymai turi fizinę formą: arbitro ataskaita, patvirtinanti, kad popieriuje pateiktas įrodymas yra teisingas; kompiuterio patikros išvestį, pateiktą kaip oficialų F kaip įvesties įrodymą; oficialus įrodymas, kad t yra F įrodymas ir tt Teigiama savistabos operacija '!' gali būti pridedamas prie šios kalbos kalbos; tada daroma prielaida, kad atsižvelgiant į t, agentas pateikia pagrindimą! t iš t: F toks, kad t: F →! t:(t: F). Teigiamas šios operatyvinės apžiūros būdas pirmą kartą pasirodė „Pro Logs of Proof LP“.

Teigiamos introspekcijos aksioma: t: F →! t:(t: F).

Tada mes apibrėžiame:

  • J4: = J + teigiama savistaba;
  • LP: = JT + teigiama savistaba. [3]

Logika J4 0, J4 CS, LP 0 ir LP CS yra apibrėžtos natūraliai (plg. 2.3 skyrių). Tiesioginis 1 teoremos analogas tinka ir J4 CS bei LP CS.

Esant pozityviosios savimonės aksiomai, aksiomos internalizacijos taisyklės taikymo sritį galima apriboti vidinėmis aksiomomis, kurios nėra e: A formos. Tai buvo padaryta LP: Axiom internalizacija gali būti modeliuojama naudojant !! e:(! e:(e: A)) vietoj e 3:(e 2:(e 1: A)) ir tt Pastovios specifikacijos sąvoka taip pat gali būti atitinkamai supaprastinta. Tokie pakeitimai yra nedideli ir jie neturi įtakos pagrindinėms „Logic“teoremoms ir taikymams.

2.6 Neigiama savistaba

(Pacuit 2006, Rubtsova 2006) neigiamos savistabos operaciją laikė „?“kuris patikrina, ar nurodytas pagrindimo teiginys yra klaidingas. Galima motyvacija apsvarstyti tokią operaciją yra ta, kad teigiama savistabos operacija '!' gali būti laikomas galinčiu pateikti įtikinamus patikrinimo sprendimus dėl pateisinimo teiginių t: F pagrįstumo, taigi, kai t nėra F pateisinimas, toks „!“turėtų daryti išvadą, kad ¬ t: F. Paprastai tai nutinka tikrinant kompiuterius, tikrinant oficialias teorijas ir tt. Ši motyvacija vis dėlto yra niuansuota: įrodymų tikrintojų ir tikrintojų pavyzdžiai veikia tiek su t, tiek su F kaip įvestimis, o Pacuit-Rubtsova formatas? t siūlo, kad vienintelis įvestis „?“yra pateisinimas t, o rezultatas? t turėtų pagrįsti teiginius ¬ t:F tolygiai visoms F, kurioms t: F nelaiko. Tokia operacija '?' neegzistuoja oficialiems matematiniams įrodymams, nes? t tada turėtų būti vienintelis be galo daug teiginių ¬ t: F įrodymas, o tai neįmanoma.

Neigiama introspekcijos aksioma ¬ t: F →? t: (¬ t: F)

Mes apibrėžiame sistemas:

  • J45 = J4 + neigiama savistaba;
  • JD45 = J45 + ¬ t: ⊥;
  • JT45 = J45 + savybė

ir natūraliai išplėsti šias apibrėžtis į J45 CS, JD45 CS ir JT45 CS. Tiesioginis 1 teoremos analogas tinka J45 CS, JD45 CS ir JT45 CS.

3. Semantika

Šiuo metu standartizuota pateisinimo logikos semantika kyla iš (Fitting 2005) - naudojami modeliai literatūroje paprastai yra vadinami tinkamais modeliais, tačiau čia bus vadinami galimais pasaulio pateisinimo modeliais. Galimi pasaulio pateisinimo modeliai yra Hintikka ir Kripke dėl žinomos galimos pasaulinės semantikos, susijusios su žinių ir įsitikinimų logika, sujungimas su pateisinimo terminams būdinga technika, kurią pristatė Mkrtychev (Mkrtychev 1997) (plg. 3.4 skyrių).

3.1 Galimas vieno agento pasaulinis pagrindimas J

Tiksliau tariant, reikia apibrėžti J CS semantiką, kur CS yra bet kokia nuolatinė specifikacija. Formaliai galimas J CS pasaulio pateisinimo logikos modelis yra M = ⟨G, R, E, V⟩ struktūra. Iš jų ⟨G, R⟩ yra standartinis K rėmelis, kur G yra galimų pasaulių rinkinys, o R yra dvejetainis santykis. V yra atvaizdavimas tarp siūlomų kintamųjų ir G pogrupių, nurodantis atominę tiesą galimuose pasauliuose.

Naujas elementas yra E, įrodymų funkcija, atsiradusi (Mkrtychev 1997). Tai pateisina pagrindų terminus ir formules į pasaulių rinkinius. Intuityvioji idėja yra, jei galimas pasaulis Γ yra E (t, X), tada t yra reikšmingas arba leistinas įrodymas X pasaulyje Γ. Nereikėtų galvoti apie svarbius įrodymus kaip įtikinamus. Geriau pagalvok apie tai kaip apie įrodymus, kurie gali būti pripažinti teisme: šis liudijimas, šis dokumentas yra kažkas, kurį turi įvertinti prisiekusieji, kažkas tinkamas, bet tai, apie kurio tiesą lemiantį statusą dar reikia atsižvelgti. Įrodymų funkcijos turi atitikti tam tikras sąlygas, tačiau jos yra aptariamos šiek tiek vėliau.

Atsižvelgiant į tai, J AP įmanoma pasaulis pagrindimas Modelis M = ⟨G, R, E, V⟩, tiesa formulė X: ne galimą pasaulio gama žymimas M, gama ⊩ X, ir privalo atitikti šiuos standartinėmis sąlygomis:

Kiekvienam ∈ ∈ G:

  1. M, ⊩ i P iff Γ ∈ V (P) P pasiūlymo raidei;
  2. nėra taip, kad M, Γ ⊩ ⊥;
  3. M, Γ ⊩ X → Y, jei nėra taip, kad M, Γ ⊩ X arba M, Γ ⊩ Y.

Jie tiesiog sako, kad atominė tiesa yra nurodoma savavališkai, o teiginiai jungiamieji principai funkciškai elgiasi kiekviename pasaulyje. Pagrindinis elementas yra kitas.

M, Γ ⊩ (t: X) tada ir tik tada, kai Γ ∈ E (t, X) ir kiekvienam Δ ∈ G su Γ R Δ turime tą M, Δ ⊩ X

Ši sąlyga suskaidoma į dvi dalis. Išlyga, reikalaujanti, kad M, Δ ⊩ X kiekvienam Δ ∈ G būtų toks, kad Γ R Δ yra pažįstama Hintikka / Kripke sąlyga, kad X būtų tikima arba būtų patikima at. Išlyga, reikalaujanti, kad Γ ∈ E (t, X), prideda, kad t turėtų būti tinkamas X įrodymas esant Γ. Tuomet neoficialiai t: X yra tikras galimo pasaulio atveju, jei X yra tikimas tame pasaulyje įprasta episteminės logikos prasme, o t yra tinkamas X tame pasaulyje įrodymas.

Svarbu suvokti, kad šioje semantikoje kažkas gali netikėti dėl tam tikros priežasties pasaulyje dėl to, kad paprasčiausiai nepatikima, arba dėl to, kad taip yra, bet priežastis nėra tinkama.

Įrodymų funkcijoms vis tiek reikia nustatyti tam tikras sąlygas, o vaizdas taip pat turi būti įtrauktas į nuolatinę specifikaciją. Tarkime, kad pateisinimas pateiktas s ir t. Tai galima derinti dviem skirtingais būdais: naudoti informaciją iš abiejų; arba naudokite tik vieno iš jų informaciją, bet pirmiausia pasirinkite kurį. Kiekviena iš jų yra pagrindinė operacija pagrįstaisiais terminais, ir +, kurie aksiomatiškai pateikiami 2.2 skirsnyje.

Tarkime, kad s yra reikšmingi įrodymai implikacijai ir t yra svarbūs įrodymai antecedentui. Tada s ir t kartu pateikia atitinkamus įrodymus. Daroma prielaida, kad įrodymų funkcijos yra tokios:

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

Pridedant šią sąlygą,

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

yra užtikrintas.

Jei s ir t yra įrodymai, galima sakyti, kad kažkas yra pateisinamas vienu iš s ar t, nesibaiminant patikslinti, kuris, ir tai vis tiek bus įrodymas. Šis reikalavimas taikomas įrodinėjimo funkcijoms.

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

Nenuostabu, kad abu

s: X → [s + t]: X

ir

t: X → [s + t]: X

dabar laikyk.

Galiausiai reikėtų atsižvelgti į nuolatinės specifikacijos CS. Prisiminkite, kad konstantos yra skirtos pagrindinėms prielaidoms, kurios yra akivaizdžiai priimtos, pagrįsti. M = ⟨G, R, E, V⟩ modelis atitinka nuolatinę CS specifikaciją, jei: c: X ∈ CS, tada E (c, X) = G.

Galimas pasaulio pateisinimo modelis Galimas J CS pasaulinio pateisinimo modelis yra M = ⟨G, R, E, V⟩ struktūra, atitinkanti visas aukščiau išvardytas sąlygas ir atitinkanti nuolatinės specifikacijos CS.

Nepaisant jų panašumų, galimi pasaulio pateisinimo modeliai leidžia atlikti tikslią analizę, kurios neįmanoma atlikti su Kripke modeliais. Norėdami gauti daugiau informacijos, žr. Papildomo dokumento 3 skirsnį „Kai kurie daugiau techninių klausimų“.

3.2 Silpnas ir ryškus išsamumas

X formulė galioja konkrečiame J CS modelyje, jei ji teisinga visuose įmanomuose modelio pasauliuose. Aksiomatiką J CS buvo suteiktas 2.2 ir 2.3 skirsniuose. Dabar išsamumo teorema įgauna numatytą formą.

2 teorema: X formulė yra įrodyta J CS tik tada, jei X galioja visuose J CS modeliuose.

Ką tik pasakyta išsamumo teorema kartais vadinama silpnu išsamumu. Galbūt šiek tiek stebina, kad žymėti „modalinę logiką K.“yra daug lengviau įrodyti nei išsamumą. Kita vertus, jis yra labai bendras, naudojamas pagal visas nuolatines specifikacijas.

(Fitting 2005) taip pat buvo pristatyta stipresnė semantikos versija. M = ⟨G, R, E, V⟩ modelis vadinamas visiškai paaiškinamuoju, jei jis atitinka šią sąlygą. Kiekvienam Γ ∈ G, jei M, Δ ⊩ X visiems Δ ∈ G taip, kad Γ R Δ, tada M, Γ ⊩ t: X tam tikram pateisinančiam žodžiui t. Atkreipkite dėmesį, kad sąlyga M, Δ ⊩ X visiems Δ ∈ G, kad Γ R Δ, yra įprasta sąlyga, kad X būtų patikimas at Hintikka / Kripke prasme. Taigi, aiškinantis iš tikrųjų, sakoma, kad jei formulė yra tikima galimame pasaulyje, ji yra pateisinama.

Ne visi silpni modeliai atitinka visiškai paaiškinamas sąlygas. Modeliai, kurie tai daro, yra vadinami stipriaisiais modeliais. Jei nuolatinė specifikacija CS yra pakankamai turtinga, kad atitiktų internalizacijos teoremą, tada ji yra išsami, atsižvelgiant į stiprius modelius, tenkinančius CS. Iš tiesų, tinkama prasme, išsamumas, susijęs su stipriais modeliais, yra lygus sugebėjimui įrodyti internalizaciją.

Tvirtų modelių išsamumo įrodymas yra panašus į išsamumo įrodymą, naudojant kanoninius modelius, pritaikomus modinei logikai K. Savo ruožtu, stiprūs modeliai gali būti naudojami norint pateikti semantinį Realizacijos teoremos įrodymą (plg. 4 skyrių)..

3.3 Vieno agento šeima

Iki šiol buvo kalbėta apie galimą vienos pateisinimo logikos pasaulio semantiką, J - K. atitikmuo. Dabar viskas praplečiama, kad apimtų ir kitų pažįstamų modalinės logikos pateisinimo analogus.

Paprasčiausiai pridedant prieinamumo santykio R refleksiškumą prie 3.1 skyriuje pateiktų sąlygų, įgyjamas t galiojimas: X → X kiekvienam t ir X ir gaunamas JT semantika - pateisinamosios loginės analogijos modinė logika. T, silpniausia žinių logika. Iš tikrųjų, jei M, Γ ⊩ t: X, tada X yra teisinga kiekvienoje būsenoje, prieinamoje iš Γ. Kadangi prieinamumo ryšys turi būti refleksinis, M, Γ ⊩ X. Silpnos ir stiprios išsamumo teoremos yra įrodomos naudojant tą pačią mašiną, kuri buvo taikoma ir J atveju, taip pat yra realizacijos teorijos, jungiančios JT ir T, semantinis įrodymas. Tas pats pasakytina ir apie toliau aptariamą logiką.

Norint pateisinti K4 analogą, papildomas vieningas operatorius '!' pridedamas prie termino kalba, žr. 2.5 skyrių. Prisiminkite, šis operatorius pateisina pateisinimus, kai mintis yra ta, kad jei t yra X pateisinimas, tada! t turėtų būti pateisinimas t: X. Semantiškai tai prideda tokias sąlygas M = ⟨G, R, E, V⟩ modeliui.

Pirmiausia, žinoma, R turėtų būti pereinamasis, bet nebūtinai atspindintis. Antra, būtina įrodymo funkcijų monotoniškumo sąlyga:

Jei Γ R Δ ir Γ ∈ E (t, X), tada Δ ∈ E (t, X)

Galiausiai reikia dar vienos įrodymų funkcijos sąlygos.

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

Šios sąlygos kartu lemia t galiojimą: X →! t: t: X ir sukurkite J4, K4 pagrindimo analogo, semantiką su juos jungiančia realizacijos teorema. Pridėjus refleksyvumą, atsiranda logika, kuri dėl istorinių priežasčių vadinama LP.

Taip pat galima pridėti neigiamą savianalizės operatorių „?“, Žr. 2.6 skyrių. Pateisinimo logikos, apimančios šį operatorių, modeliai prideda tris sąlygas. Pirmasis R yra simetriškas. Antra, pridedama sąlyga, kuri tapo žinoma kaip tvirtas įrodymas: M, Γ ⊩ t: X visiems Γ ∈ E (t, X). Galiausiai yra įrodymų funkcijos sąlyga:

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

Jei šios mašinos pridedamos prie J4, mes gauname logiką J45, K45 pagrindimą. Galima įrodyti aksiomatinį pagrįstumą ir išsamumą. Panašiu būdu gali būti suformuluota susijusi logika JD45 ir JT45.

Realizacijos teorema, kurioje atsižvelgiama į šį operatorių, buvo parodyta (Rubtsova 2006).

3.4 Bendro pasaulio modeliai

Vieno pasaulio pateisinimo modeliai buvo kuriami gerokai anksčiau nei bendresni galimi pasaulio pateisinimo modeliai, apie kuriuos mes diskutavome (Mkrtychev 1997). Šiandien jie paprasčiausiai gali būti sugalvoti kaip galimi pasaulio pateisinimo modeliai, kurie atsitiktų turintys vieną pasaulį. J išsamumo įrodymą ir kitą aukščiau paminėtą pagrindimo logiką galima lengvai modifikuoti siekiant nustatyti išsamumą atsižvelgiant į vieno pasaulio pagrindimo modelius, nors, žinoma, tai nebuvo pirminis argumentas. Tai, kas paaiškina vieno pasaulio pateisinimo modelių išsamumą, yra tai, kad informaciją apie galimą pateisinimo modelių pasaulio struktūrą galima visiškai užkoduoti priimtinų įrodymų funkcija, bent jau kol kas aptartai logikai. Mkrtychev naudojo vieno pasaulio pateisinimo modelius, kad nustatytų LP nuspręstamumą,ir kiti jais iš esmės pasinaudojo nustatydami pateisinimo logikos sudėtingumo ribas, taip pat norėdami pateisinti įsitikinimo logikos konservatyvumo rezultatus (Kuznets 2000, Kuznets 2008, Milnikel 2007, Milnikel 2009). Sudėtingumo rezultatai buvo toliau naudojami sprendžiant loginio visažiniškumo problemą.

4. Realizacijos teoremos

Natūralus modalinis episteminis įrodymų tvirtinimo atitikmuo t: F yra □ F, perskaitykite kai x, x: F. Šis pastebėjimas lemia nepamirštamo projekto projekciją, kuri kiekvieną t: F atvejį pakeičia □ F ir todėl paverčia loginį sakinį S atitinkamu modalinės logikos sakiniu S o. Pamirštama projekcija natūraliai tęsiasi nuo sakinių iki logikos.

Akivaizdu, kad skirtingi Pagrindimas Loginiai sakiniai gali būti vienodai užmaršūs, taigi S o praranda tam tikrą informaciją, esančią S. Tačiau nesunku pastebėti, kad užmarštinė projekcija visada suderina galiojančias logikos formules (pvz., J aksiomas) prie galiojančių atitinkamos episteminės logikos (šiuo atveju K) formulių. Taip pat priešingai: bet kuri galiojanti episteminės logikos formulė yra pamirštama tam tikros pagrįstos logikos formulės projekcija. Tai išplaukia iš 3 korespondencijos teoremos.

3 teorema: J o = K.

Šis susirašinėjimas galioja kitoms pateisinančių ir episteminių sistemų poroms, pavyzdžiui, J4 ir K4, LP ir S4 ir daugeliui kitų. Esant tokiai išplėstinei formai, korespondencijos teorema parodo, kad pagrindinės modalinės logikos, tokios kaip K, T, K4, S4, K45, S5 ir kai kurios kitos, turi tikslias logikos atitikmenis.

Korespondencijos teoremos esmė yra ši Realizacijos teorema.

4 teorema: Yra algoritmas, kuris kiekvienai K išvedamai modaliniai formulei F priskiria įrodymų terminus kiekvienam F modališkumo įvykiui taip, kad gauta formulė F r būtų išvestinė J. Be to, realizacija priskiria įrodymų kintamuosius. neigiamam modalinių operatorių pasireiškimui F, atsižvelgiant į egzistencinį episteminio modalumo skaitymą.

Žinomi realizavimo algoritmai, atkuriantys įrodymų terminus modalinėse teoremose, atitinkamose modalinėse logikose naudoja išpjaustinius. Kaip alternatyva, realizacijos teoremą galima nustatyti semantiškai, naudojant Fitingo metodą arba tinkamai jį modifikavus. Iš esmės šie semantiniai argumentai taip pat sukuria realizavimo procedūras, pagrįstas išsamia paieška.

Būtų klaidinga daryti išvadą, kad bet kokia modalinė logika turi pagrįstą pagrindimą logikos atžvilgiu. Pavyzdžiui, formaliojo įrodomumo logikoje, GL (Boolos 1993), yra Löb principas:

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

kuri, atrodo, neturi epistemiškai priimtinos aiškios versijos. Apsvarstykite, pavyzdžiui, atvejį, kai F yra pasiūlymo konstanta ⊥ klaidinga. Jei 4 teoremos analogas apimtų Löbo principą, pateisinimo terminai s ir t būtų tokie: x:(s: ⊥ → ⊥) → t: ⊥. Tačiau tai yra intuityviai klaidinga faktiškam pagrindimui. Iš tiesų, s: ⊥ → ⊥ yra Veiksmingumo aksiomos pavyzdys. Taikykite Axiom internalization, kad gautumėte c:(s: ⊥ → ⊥) tam tikrai konstanta c. Šis c pasirinkimas daro c pirmtaką:(s: ⊥ → ⊥) → t: ⊥ intuityviai teisinga, o išvada klaidinga [4]. Konkrečiai kalbant, įrodymui aiškinti negalioja Löbo principas (5) (plg. (Goris 2007), kuriame aprašoma, kurie GL principai yra įgyvendinami).

Korespondencijos teorema suteikia naujos įžvalgos apie episteminę modalinę logiką. Svarbiausia, kad tai pateikia naują pagrindinių modalinės logikos semantiką. Be tradicinio Kripke stiliaus „universalaus“□ F skaitymo, kaip F yra visose įmanomose situacijose, dabar yra ir griežta „egzistencinė“□ F semantika, kurią galima perskaityti, nes yra liudytojas (įrodymas, pagrindimas) F.

Pagrindimas Semantika vaidina panašų vaidmenį „Modal Logic“, kaip ir „Kleene“įgyvendinamumas „Intuitionistic Logic“. Abiem atvejais numatoma semantika yra egzistencinė: Brouwerio-Heytingo-Kolmogorovo intuicinės logikos interpretacija (Heytingas 1934, Troelstra ir van Dalenas 1988, van Dalenas 1986) ir Gödelio S4 įrodomumo skaitinys (Gödel 1933, Gödel 1938). Abiem atvejais yra įmanoma, pasaulio semantika universaluscharakteris, kuris yra labai stiprus ir dominuojantis techninis įrankis. Tačiau jame nekalbama apie numatomos semantikos egzistencinį pobūdį. Norint atskleisti intuityvinės logikos skaičiavimo semantiką ir įrodymų logiką, reikėjo Kleene'io realizavimo galimybių (Kleene 1945, Troelstra 1998), kad būtų galima pateikti tikslią intuicionistinės ir modinės logikos įrodymų semantiką BHK.

Episteminiame kontekste Pagrindimas Logika ir Korespondencijos teorema prideda naują „pagrindimo“komponentą žinių ir įsitikinimų modalinei logikai. Vėlgi, šis naujas komponentas iš tikrųjų buvo sena ir centrinė sąvoka, kurią plačiai aptarė pagrindiniai epistemologai, tačiau kuri nepateko į klasikinės episteminės logikos sritį. Korespondencijos teorema mums sako, kad pateisinimai yra suderinami su Hintikka stiliaus sistemomis ir todėl gali būti saugiai įtraukti į episteminės modulinės logikos pagrindą.

Norėdami sužinoti daugiau apie realizacijos teoremas, žiūrėkite papildomo dokumento 4 skyrių „Kai kurie daugiau techninių klausimų“.

5. Apibendrinimai

Iki šiol šiame straipsnyje buvo nagrinėjama tik vieno agento pagrindimo logika, analogiška vieno agento žinių logikai. Pagrindimas Logika gali būti laikoma aiškių žinių logika, susijusi su labiau įprasta numanomų žinių logika. Literatūroje yra ištirta keletas sistemų, išskyrus tas, kurios buvo aptartos aukščiau, apimančios kelis agentus arba turinčias netiesioginius ir tiesioginius operatorius, arba kai kuriuos iš jų derinius.

5.1 Aiškių ir numanomų žinių sumaišymas

Kadangi pateisinimo logika pateikia aiškų pagrindimą, o įprastinė žinių logika pateikia numanomą žinių operatorių, natūralu apsvarstyti galimybę sujungti du į vieną sistemą. Dažniausia bendra aiškių ir numanomų žinių logika yra S4LP (Artemov ir Nogina 2005). S4LP kalba yra tokia pati kaip LP, bet pridedant netiesioginį žinių operatorių, parašytą arba K, arba □. Aksiomatika yra tokia pati kaip LP, sujungta su numanomo operatoriaus S4 aksiomatika, kartu su jungiančiąja aksioma, t: X → □ X, viskas, kas turi aiškų pagrindimą, yra žinoma.

Seminatiškai galimų LP pateisinimo modelių pasaulyje nereikia modifikuoti, nes jie jau turi visą „Hintikka / Kripke“modelių techniką. Vienas modeliuoja operatorių □ įprastu būdu, naudodamas tik prieinamumo ryšį, ir vienas modeliuoja pagrindimo terminus, aprašytus 3.1 skyriuje, naudodamas ir prieinamumo, ir įrodymų funkciją. Kadangi įprasta sąlyga, kad □ X yra teisinga pasaulyje, yra viena iš dviejų sąlygų, skirtų t: X būti teisinga, sakinio, tai iš karto patvirtina t: X → □ X pagrįstumą, o tvirtumas seka lengvai. Aksiomatinis išsamumas taip pat yra gana aiškus.

S4LP pateikiamos tiek numanomos, tiek ir aiškios žinios, tačiau galimo pasaulio pateisinimo modelio semantikoje vienas prieinamumo ryšys tarnauja abiem. Tai nėra vienintelis būdas tai padaryti. Apskritai aiškus žinių prieinamumo ryšys galėtų būti tinkamas netiesioginių žinių išplėtimas. Tai atspindi aiškių žinių viziją, kad yra griežtesni standartai tam, kas laikoma žinoma, nei netiesioginių žinių. Skirtingų prieinamumo ryšių naudojimas aiškiam ir netiesioginiam žinojimui tampa būtinas, kai šios episteminės sąvokos paiso skirtingų loginių dėsnių, pvz., S5 reiškia netiesiogines žinias ir LP - aiškias. Kelių prieinamumo ryšių atvejis literatūroje yra plačiai žinomas kaip „Artemov-Fitting“modeliai, tačiau čia jis bus vadinamas galimu įvairių agentų pasaulio modeliu. (plg. 5.2 skyrių).

Įdomu, kad nors S4LP logika atrodo gana natūrali, realizacijos teorema jai buvo problematiška: tokios teoremos neįmanoma įrodyti, jei reikalaujama vadinamųjų normalių realizacijų (Kuznets 2010). Svarbus iššūkis šioje srityje tebėra realizuoti numanomus S4LP žinių būdus, pateikiant aiškius pagrindimus, kuriais būtų atsižvelgiama į episteminę struktūrą.

Netiesioginių ir aiškių žinių sąveika kartais gali būti gana subtili. Kaip pavyzdį apsvarstykite šį mišrų neigiamos savistabos principą (vėlgi □ reikėtų suprasti kaip numanomą episteminį operatorių),

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

Iš įrodomumo perspektyvos, tai yra teisinga neigiamos savistabos forma. Iš tikrųjų leiskime □ F aiškinti taip, kad F yra įrodyta, o t: F kaip t yra F įrodymas tam tikroje formaliojoje teorijoje T, pvz., Peano aritmetinėje PA. Tada (6) nurodomas įrodytinas principas. Iš tikrųjų, jei t nėra F įrodymas, tada, kadangi šis teiginys yra nuspręstas, jis gali būti nustatytas T viduje, taigi T sakinyje šis sakinys yra įrodomas. Kita vertus, įrodymas p „t nėra F įrodymas“priklauso ir nuo t, ir nuo F, p = p (t, F) ir negali būti apskaičiuojamas tik atsižvelgiant į t. Šiuo atžvilgiu □ negali būti pakeistas jokiu konkrečiu įrodomuoju žodžiu, priklausančiu tik nuo t ir (6) negali būti pateiktas visiškai aiškiu pagrindimo stiliaus formatu.

Pirmi aiškių / netiesioginių žinių sistemų pavyzdžiai pasirodė įrodomumo logikos srityje. (Sidon, 1997, Yavorskaya (Sidon) 2001), buvo pristatyta loginė LPP, apimanti GL patikimumo logiką su įrodymų logika LP, tačiau siekiant užtikrinti, kad gauta sistema turėtų pageidaujamų loginių savybių, kai kurios papildomos operacijos iš originalių kalbų ribų buvo pridėta GL ir LP. (Nogina 2006, Nogina 2007) buvo pasiūlyta išsami įrodymų ir įrodomumo loginė sistema GLA originalių GL ir LP kalbų suma. Tiek LPP, tiek GLA yra išsamūs, palyginti su aritmetinių modelių klase, taip pat palyginti su galimų pasaulio pateisinimo modelių klase.

Kitas įrodomumo principo, kurio negalima aiškiai išdėstyti, pavyzdys yra Löbo principas (5). Kiekvienam LPP ir GLA nesunku rasti įrodomąjį terminą l (x), kad

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

laiko. Tačiau nėra jokio supratimo, kuris aiškiai parodytų visus tris (5) taškus. Realiai įgyvendinamumo principų rinkinys yra GL ir S4 sankirtos (Goris 2007).

5.2 Galimi įvairių agentų pasaulio modeliai

Galimuose daugiaagentiniuose pasaulio pateisinimo modeliuose naudojami įvairūs prieinamumo santykiai, turintys ryšius tarp jų (Artemov 2006). Idėja yra ta, kad yra keli agentai, kurių kiekvienas turi netiesioginį žinių operatorių, ir yra pagrindimo terminai, kuriuos kiekvienas agentas supranta. Visi laisvai supranta aiškias priežastis; tai prilygsta įrodymais pagrįstam bendrajam žinojimui.

Galimas n-reagento pateisinimo pasauliu modelis yra ⟨G, R 1,…, R n, R, E, V⟩ struktūra, atitinkanti šias sąlygas. G yra galimų pasaulių rinkinys. Kiekvienas iš R 1, …, R n yra prieinamumą santykis, po vieną kiekvienam agento. Galima manyti, kad jie yra refleksyvūs, pereinantys arba simetriški. Jie naudojami modeliuojant implicitines agentų žinias agentų šeimai. Prieinamumo santykis R atitinka LP sąlygas, refleksyvumą ir pereinamumą. Jis naudojamas modeliuojant aiškias žinias. E yra įrodymų funkcija, tenkinanti tas pačias sąlygas, kurios 3.3 skirsnyje nurodytos LP. V, kaip įprasta, žymi siūlomas raides pasaulių rinkiniams. Yra nustatyta speciali sąlyga: kiekvienam i = 1,…, n, R i ⊆ R.

Jei M = ⟨G, R 1,…, R n, R, E, V⟩ yra daugiareikšmis įmanomas pasaulio pateisinimo modelis, tiesos pasaulyje santykis, M, Γ ⊩ X, apibūdinamas daugumoje įprastos išlygos. Ypač svarbios yra šios:

  • M, Γ ⊩ K i X tada ir tik tada, kai kiekvienam Δ ∈ G su Γ R i Δ turime tą M, Δ ⊩ X.
  • M, Γ ⊩ t: X tada ir tik tada, kai Γ ∈ E (t, X) ir kiekvienam Δ ∈ G su Γ R Δ mes turime tą M, Δ Δ X.

Sąlyga R i ⊆ R reiškia, kad kiekvienam agentui i galioja t: X → K i X. Jei yra tik vienas agentas, o to agento prieinamumo santykis yra refleksinis ir pereinamasis, tai suteikia kitą S4LP semantiką. Nepriklausomai nuo agentų skaičiaus, kiekvienas agentas priima aiškias priežastis, kodėl įgyja žinių.

LP versija su dviem agentais buvo pristatyta ir išnagrinėta (Yavorskaya (Sidon) 2008), nors ją galima apibendrinti su bet kokiu baigtinių agentų skaičiumi. Čia kiekvienas agentas turi savo pagrindimo operatorių, kintamųjų ir konstantų rinkinį, užuot turėjęs vieną visiems, kaip aprašyta aukščiau. Be to, gali būti leidžiama ribota komunikacija tarp atstovų, naudojant naują operatorių, kuris leidžia vienam agentui patikrinti kito agento pagrindimų teisingumą. Dviejų agentų logikai buvo sukurtos tiek vieno pasaulio, tiek bendresnės įmanomos pasaulio pagrindimo semantikos versijos. Tai apima įrodymų funkcijos sąvokos supratimo išplėtimą ir galimus pasaulio pateisinimo modelius, naudojant du prieinamumo ryšius. Realizacijos teoremos įrodytos sintaksiškai,nors, manytina, taip pat veiks semantinis įrodymas.

Neseniai buvo ištirtas viešųjų pranešimų vaidmuo daugiataškių pateisinimų logikoje (Renne 2008, Renne 2009).

Papildomame dokumente „Kai kurie daugiau techninių klausimų“5 skyriuje yra daugiau apie įrodymais pagrįstų žinių sąvoką.

6. Russello pavyzdys: sukeltas veikimas

Yra metodika, kaip naudoti logiką, skirtą analizuoti skirtingus to paties fakto pagrindimus, ypač kai kai kurie pagrindimai yra faktiški, o kiti ne. Norėdami parodyti techniką, atsižvelkite į gerai žinomą pavyzdį:

Jei vyras mano, kad vėliojo ministro pirmininko pavardė prasidėjo raide „B“, jis mano, kas yra tiesa, nes velionis ministras pirmininkas buvo seras Henris Campbellas Bannermanas [5]. Bet jei jis manys, kad ponas Balfour'as buvo vėlyvasis ministras pirmininkas [6], jis vis tiek tikės, kad vėliojo ministro pirmininko pavardė prasidėjo „B“, tačiau šis įsitikinimas, nors ir teisingas, nemanomas, kad yra žinios. (Russellas 1912 m.)

Kaip ir Raudonojo tvarto pavyzdyje, aptartame 1.1 skyriuje, čia reikia nagrinėti du tikrojo teiginio pagrindimus, iš kurių vienas yra teisingas, o kitas - ne. Tegul B yra sakinys (siūlomasis atomas), w yra paskirtas pagrindimo kintamasis dėl netinkamos B priežasties ir ra nurodomas pagrindimo kintamasis dėl B teisingos (taigi ir faktinės) priežasties. Tuomet Russello pavyzdys skatina šias prielaidas [7]:

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

Šiek tiek priešingai nei intuicija, galima logiškai išvesti w koeficientą iš R:

  1. r: B (prielaida)
  2. r: B → B (prielaida)
  3. B (nuo 1 ir 2 pateikė Modus Ponens)
  4. B → (w: B → B) (pasiūlymo aksioma)
  5. w: B → B (nuo 3 ir 4 Modus Ponens)

Tačiau šis išvestinis panaudojamas tuo, kad r yra faktinis B pagrindimas daryti išvadą w: B → B, kuris yra „sukeltos savybės“w: B atveju. Kyla klausimas, kaip galima atskirti „tikrąjį“r: B charakteristiką nuo „indukuotojo faktoriaus“w: B? Čia reikalingas tam tikras tiesos sekimas, ir Pagrindimas Logika yra tinkama priemonė. Natūralus požiūris yra atsižvelgti į prielaidų rinkinį be r: B, ty

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

ir nustatykite, kad w, ty w: B → B, negalima išvesti iš S. Čia yra galimas pasaulio pateisinimo modelis M = (G, R, E, V), kuriame S yra, bet w: B → B neturi:

  • G = { 1 },
  • R = ∅,
  • V (B) = ∅ (ir ne taip - 1 ⊩ B),
  • E (t, F) = { 1 } visoms poroms (t, F), išskyrus (r, B) ir
  • E (r, B) = ∅.

Nesunku pastebėti, kad įvykdytos paraiškos uždarymo sąlygos ir E suma. Esant 1, w: B sulaiko, ty

1 ⊩ w: B

nes w yra leistini įrodymai B taškui 1 ir nėra jokių galimų pasaulių, prieinamų iš 1. Be to,

not- 1 ⊩ r: B

nes, pasak E, r nėra leistini įrodymai, kai B yra 1. Taigi:

1 ⊩ r: B → B

Iš kitos pusės,

ne- 1 ⊩ w: B → B

nes B nelaiko 1.

7. Pateisinimų savireferencija

Realizacijos algoritmai kartais sukuria pastovias specifikacijas, kuriose pateikiami savaiminio pagrindimo teiginiai c: A (c), tai yra teiginiai, kuriuose pateisinimas (čia c) atsiranda teiginyje (čia A (c)).

Pateisinimų savireferencija yra naujas reiškinys, kurio nėra tradicinėje modalinėje kalboje. Šie savireferenciniai teiginiai, be intriguojančių episteminių objektų, yra ir ypatingas iššūkis semantiniu požiūriu, nes yra įmontuotas užburtas ratas. Iš tikrųjų, norint įvertinti c, pirmiausia reiktų įvertinti A, o paskui priskirti A pagrindimo objektą c. Tačiau to negalima padaryti, nes A yra c, kuris dar turi būti įvertintas. Svarbus atviras klausimas šioje srityje buvo tas, ar galima įgyvendinti loginę logiką, nenaudojant savireferencinių pagrindimų.

Pagrindinis „Kuznets“(Brežnev ir Kuznets 2006) rezultatas teigia, kad pateisinimo savaiminis pagrindimas yra neišvengiamas įgyvendinant S4 LP. Dabartinę dalykų būklę pateikia ši teorema dėl Kuznetso:

5 teorema: Savireferencionalumo galima išvengti realizuojant modalinę logiką K ir D. Savireferencijos negalima išvengti realizuojant modalinę logiką T, K4, D4 ir S4.

Ši teorema nustato, kad S4 pateisinimo terminų sistema būtinai turi remtis savimi. Tai sukuria rimtą, nors tiesiogiai nematytą, įrodomumo semantikos suvaržymą. Gödelio aritmetinių įrodymų kontekste problema buvo išspręsta bendru metodu, pagal kurį aritmetinė semantika buvo priskiriama savarankiškiems teiginiams c: A (c), teigiant, kad c yra A (c) įrodymas. Įrodymų logikoje LP buvo nagrinėjama ne trivialioji fiksuoto taško konstrukcija.

Savireferencija suteikia įdomią Moore'o paradokso perspektyvą. Išsamesnės informacijos žr. Papildomo dokumento 6 skirsnyje „Kai kurie daugiau techninių klausimų“.

8. Pateisinimo logikos kiekybiniai rodikliai

Nors pasiūlymo dėl logikos tyrimas dar toli gražu nėra baigtas, taip pat buvo nedaug darbo su pirmosios eilės versijomis. Kiekybinės „Modal Logic“versijos jau siūlo sudėtingesnių nei standartinė pirmosios eilės logika. Kiekybinis įvertinimas yra dar platesnis, kai kalbama apie logikos pagrindimą. Klasikine prasme kiekybiškai įvertinami „objektai“, o modeliuose yra domenas, per kurį skiriasi kiekybiniai rodikliai. Paprastai gali būti, kad vienas domenas yra bendras visiems įmanomiems pasauliams, arba kiekvienam pasauliui gali būti atskiri domenai. Čia gerai žinomas „Barcan“formulės vaidmuo. „Pagrindimas Logic“taip pat galimos tiek nuolatinės, tiek skirtingos srities galimybės. Be to, yra galimybė, neturinti „Modal Logic“analogo: kiekybiškai galima įvertinti pateisinimus.

Pradiniai rezultatai dėl kiekybiškai pagrįstos pagrindimo logikos buvo ypač nepalankūs. Aritmetinė „Logic of Pro LP“aritmetinė įrodomumo semantika natūraliai apibendrinama į pirmosios eilės variantą su įprastais kiekybiniais rodikliais, o į versiją su kiekybiniais rodikliais virš įrodymų. Abiem atvejais į aksiomatizuojamumo klausimus buvo atsakyta neigiamai.

6 teorema: Pirmos eilės įrodymų logika nėra rekursyviai įvardijama (Artemov ir Yavorskaya (Sidon) 2001). Įrodymų su kiekybiniais rodikliais įrodymų logika nėra rekursyviai įvardijama (Yavorsky 2001).

Nors aritmetinė semantika neįmanoma, (Fitting 2008) galimai pasaulio semantikai ir aksiomatinio įrodymo teorijai buvo pateikta LP versija su kiekybiniais rodikliais, pagrindžiančiais pagrįstumą. Buvo įrodytas pagrįstumas ir išsamumas. Šiuo metu galima pasaulio semantika atsiskiria nuo aritmetinės semantikos, kuri gali būti aliarmo priežastis. Taip pat buvo parodyta, kad S4 įeina į kiekybinę logiką išversdamas □ Z kaip „egzistuoja toks pateisinimas x, kad x: Z * “, kur Z * yra Z vertimas. Nors ši logika yra šiek tiek sudėtinga, ji rado programų, pvz., (Dean ir Kurokawa 2009b), ji naudojama Knower paradoksui analizuoti, nors šiai analizei buvo pareikšta prieštaravimų (Arlo-Costa ir Kishida 2009).

Taip pat buvo dirbama su Pagrindimas Logic versijomis su objektų kiekybiniais rodikliais, tiek su Barcan formulės analogu, tiek be jo. Nei vienas iš jų nebuvo paskelbtas, ir turėtų būti laikoma, kad jis vis dar vykdomas.

9. Istorinės pastabos

Pradinė logikos sistema, „Logic of Proofs LP“, buvo įvesta 1995 m. (Artemov 1995) (plg. Taip pat (Artemov 2001)), kur pirmiausia buvo nustatytos tokios pagrindinės savybės kaip internalizavimas, įgyvendinimas, aritmetinis išsamumas. LP pasiūlė numatytą Gödelio įrodomumo logikos S4 patikimumo semantiką, tokiu būdu pateikdama Brouwerio-Heytingo-Kolmogorovo semantikos įforminimą intuityvinės teiginio logika. Pirmą kartą LP buvo nustatyta episteminė semantika ir išsamumas („Fitting 2005“). Simbolinius modelius ir LP sprendimus lemia Mkrtychev (Mkrtychev 1997). Pirmiausia sudėtingumo įvertinimai pasirodė (Brežnevas ir Kuznets 2006, Kuznets 2000, Milnikel 2007). Išsamią visų sprendimų dėl sprendimų priėmimo ir sudėtingumo apžvalgą galima rasti (Kuznets 2008). J, J4 sistemosir JT pirmą kartą buvo svarstomi (Brežnevas 2001) skirtingais pavadinimais ir šiek tiek skirtinga aplinka. JT45 pasirodė savarankiškai (Pacuit 2006) ir (Rubtsova 2006), o JD45 pasirodė (Pacuit 2006). Vienos išvados įrodymų logika rasta (Krupski 1997). Bendresnis požiūris į bendras žinias, pagrįstas pagrįstomis žiniomis, buvo pasiūlytas (Artemov 2006). Žaidimo „Logika ir dinaminė episteminė logika“semantika su pateisinimais buvo nagrinėta (Renne 2008, Renne 2009). Logikos ir loginio visažiniškumo sąsajos buvo nagrinėjamos (Artemov ir Kuznets 2009, Wang 2009). Pavadinimas Pagrindimas Logika buvo pristatyta (Artemov 2008), kurioje buvo įforminti Kripke, Russell ir Gettier pavyzdžiai; šis įforminimas buvo naudojamas paradoksams išspręsti, patikrinti,paslėptos prielaidos analizė ir atleidimų pašalinimas. Straipsnyje (Dean ir Kurokawa, 2009a) Pagrindimas „Logika“buvo naudojama „Knower“ir „Knowledge“paradoksų analizei.

Bibliografija

  • Antonakos, E. (2007). „Pagrįstos ir bendros žinios: ribotas konservatyvumas“, S. Artemov ir A. Nerode (red. Past.), Kompiuterių mokslo loginiai pagrindai, Tarptautinis simpoziumas, LFCS 2007, Niujorkas, NY, JAV, 2007 m. Birželio 4–7 d., Proceedings (Paskaitų užrašai kompiuterių moksle: 4514 tomas), Berlynas: „Springer“, p. 1–11.
  • Arlo-Costa, H. ir K. Kishida (2009). „Trys įrodymai ir žinovas kiekybinėje įrodymų logikoje“oficialiame epistemologijos seminare / FEW 2009. Proceedings, Carnegie Mellon universitetas, Pitsburgas, PA, JAV.
  • Artemov, S. (1995). „Operatyvinė loginė logika“, techninė ataskaita MSI 95–29, Kornelio universitetas.
  • –––. (2001). „Aiškus įrodomumas ir konstruktyvi semantika“, Simbolinės logikos biuletenis, 7 (1): 1–36.
  • –––. (2006). „Pagrįstos bendros žinios“, teorinis kompiuterių mokslas, 357 (1–3): 4–22.
  • –––. (2008). „Pateisinimo logika“, Simbolinės logikos apžvalga, 1 (4): 477–513.
  • Artemov, S. ir R. Kuznets (2009). „Loginis visažiniškumas kaip skaičiavimo sudėtingumo problema“, A. Heifetz (red.), Racionalumo ir žinių teoriniai aspektai, Dvyliktosios konferencijos medžiaga (TARK 2009), „ACM Publishers“, p. 14–23.
  • Artemov, S. ir E. Nogina (2005). „Pateisinimo įvedimas į episteminę logiką“, žurnalas „Logic and Computation“, 15 (6): 1059–1073.
  • Artemovas, S. ir T. Yavorskaya (Sidonas) (2001). „Dėl pirmosios eilės įrodymų logikos“, Maskvos matematikos žurnalas, 1 (4): 475–490.
  • Boolos, G. (1993). Tikimybės logika, Kembridžas: Cambridge University Press.
  • Brežnevas, V. (2001). „Dėl įrodymų logikos“, K. Striegnitz (red.), Šeštosios ESSLLI studentų sesijos, 13-osios Europos logikos, kalbos ir informacijos vasaros mokyklos (ESSLLI'01), 35–46 p.
  • Brežnevas, V. ir R. Kuznetsai (2006). „Teikti aiškias žinias: kaip sunku“, Teorinis kompiuterių mokslas, 357 (1–3): 23–34.
  • Cubitt, RP ir R. Sugden (2003). „Bendros žinios, žinomumas ir tradicijos: Davido Lewiso žaidimo teorijos rekonstrukcija“, Ekonomika ir filosofija, 19: 175–210.
  • Dekanas, W. ir H. Kurokawa (2009a). „Nuo žinių paradokso iki įrodymų egzistavimo“, Synthese, 176 (2): 177–225.
  • –––. (2009b). „Žinios, įrodymas ir žinovas“, A. Heifetz (red.), Racionalumo ir žinių teoriniai aspektai, Dvyliktosios konferencijos (TARK 2009) medžiaga, ACM leidiniai, p. 81–90.
  • Dretske, F. (2005). „Ar žinios uždaromos pagal žinomą prievolę? Byla prieš uždarymą “, M. Steup ir E. Sosa (red.), Šiuolaikiniai epistemologijos debatai, Oksfordas: Blackwell, p. 13–26.
  • Faginas, R., J. Halpernas, Y. Mosesas ir M. Vardi (1995). Paaiškinimas apie žinias, Kembridžas, MA: MIT Press.
  • Montavimas, M. (2005). „Įrodymų logika semantiškai“, Grynos ir taikomosios logikos metraštis, 132 (1): 1–25.
  • –––. (2006). „Pakaitinė teorema LP “, techninė ataskaita TR-2006002, Niujorko miesto universiteto Kompiuterių mokslo katedra.
  • –––. (2008). „Kiekybinė įrodymų logika“, Grynos ir taikomosios logikos metraštis, 152 (1–3): 67–83.
  • –––. (2009). „Realizacijos ir LP “, Grynos ir taikomosios logikos metraščiai, 161 (3): 368–387.
  • Gettier, E. (1963). „Ar pagrįstos tikros žinios?“Analizė, 23: 121–123.
  • Girard, J.-Y., P. Taylor ir Y. Lafont (1989). Įrodymai ir tipai (Kembridžo traktatai kompiuterių moksle: 7 tomas), Kembridžas: Cambridge University Press.
  • Gödel, K. (1933). „Eine Interpretation des intuitionistischen Aussagenkalkuls“, Ergebnisse matematika. Kolloq., 4: 39–40. Vertimas į anglų kalbą: S. Feferman ir kt. (red.), Kurto Gödelio kolekciniai darbai (1 tomas), Oksfordas ir Niujorkas: Oxford University Press ir Clarendon Press, 1986, p. 301–303.
  • –––. (1938 m.). „Vortrag bei Zilsel / Paskaita Zilsel's“(* 1938a), S. Feferman, JJ Dawson, W. Goldfarb, C. Parsons ir R. Solovay (red.), Nepaskelbti esė ir paskaitos (Kurt Gödel kolekciniai darbai: tomas III), Oksfordas: Oxford University Press, 1995, p. 86–113.
  • Goldmanas, A. (1967). „Priežastinė prasmės teorija“, Žurnalas apie filosofiją, 64: 335–372.
  • Goodman, N. (1970). „Konstrukcijų teorija yra lygiavertė aritmetikai“, J. Myhill, A. Kino ir R. Vesley (red.), Intuicionizmas ir įrodymo teorija, Amsterdamas: Šiaurės Olandija, p. 101–120.
  • Goris, E. (2007). „Aiškūs oficialios įrodomumo logikos įrodymai“, S. Artemov ir A. Nerode (red.), Logical Computer Computer Foundations, International Symposium, LFCS 2007, Niujorkas, NY, JAV, 2007 m. Birželio 4–7 d., Proceedings (ecture Note of Computer Science: 4514 tomas), Berlynas: „Springer“, p. 241–253.
  • Hendrickas, V. (2005). Pagrindinė ir formali epistemologija, Niujorkas: Cambridge University Press.
  • Heytingas, A. (1934). „Mathematische Grundlagenforschung“. Intuicijos. Beweistheorie, Berlynas: „Springer“.
  • Hintikka, J. (1962). Žinios ir tikėjimas, Ithaca: Cornell University Press.
  • Kleene, S. (1945). „Dėl intuicionistinės skaičių teorijos aiškinimo“, Žurnalas apie simbolinę logiką, 10 (4): 109–124.
  • Kolmogorovas, A. (1932). „Zur Deutung der Intuitionistischen Logik“, Mathematische Zeitschrift, 35: 58–65. Vertimas į anglų kalbą VM Tikhomirov (ed.), Atrinkti AN Kolmogorovo darbai. I tomas: Matematika ir mechanika, Dordrecht: Kluwer, 1991, p. 151–158.
  • Kreisel, G. (1962). „Intuicionistinės logikos pagrindai“, E. Nagelis, P. Suppesas ir A. Tarski (red.), Logika, metodologija ir mokslo filosofija. 1960 m. Tarptautinio kongreso leidiniai, Stanfordas: Stanford University Press, 198–210 psl.
  • –––. (1965). „Matematinė logika“, T. Saaty (red.), III moderniosios matematikos paskaitos, Niujorkas: Wiley and Sons, p. 95–195.
  • Krupski, V. (1997). „Įrodžių operacinė logika su funkcinėmis sąlygomis įrodant predikatą“, S. Adian ir A. Nerode (red.), Logical Computer Computer Foundations, 4-asis tarptautinis simpoziumas, LFCS'97, Jaroslavlis, Rusija, 1997 m. Liepos 6–12 d., Straipsniai (Paskaitų užrašai kompiuterių moksle: 1234 tomas), Berlynas: „Springer“, p. 167–177.
  • Kurokawa, H. (2009). „Tableaux ir hipersekvencijos dėl logikos pagrindimo“, S. Artemov ir A. Nerode (red.), Logical Computer Computer Foundations, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, 2009 m. Sausio 3–6 d., Proceedings (Paskaitos užrašai kompiuterių moksle: 5407 tomas), Berlynas: „Springer“, p. 295–308.
  • Kuznets, R. (2000). „Dėl aiškios modulinės logikos sudėtingumo“, P. Clote ir H. Schwichtenberg (red.), Computer Science Logic, 14-asis tarptautinis seminaras, CSL 2000, EACSL metinė konferencija, Fischbachau, Vokietija, 2000 m. Rugpjūčio 21–26 d., Straipsniai (Paskaitų užrašai kompiuterių moksle: 1862 tomas), Berlynas: Springeris, p. 371–383.
  • –––. (2008). Niujorko miesto universiteto informatikos katedros informatikos katedros logikos pagrindimo sudėtingumo klausimai.
  • –––. (2010). „Pastaba apie S4LP realizacijos nenormalumą “, parašyta K. Brünnler ir T. Studer (red.), Įrodymas, skaičiavimas, PCC 2010 sudėtingumas, Tarptautinis seminaras, Proceedings, IAM techninės ataskaitos IAM-10-001, Kompiuterių institutas Mokslas ir taikomoji matematika, Berno universitetas.
  • McCarthy, J., M. Sato, T. Hayashi ir S. Igarishi (1978). „Dėl pavyzdinės žinių teorijos“, techninė ataskaita STAN-CS-78-667, Stanfordo universiteto Kompiuterių mokslo katedra.
  • Milnikel, R. (2007). „Tam tikrose įrodymų logikos posistemėse yra išvestinis Π 2 p - neišsamus“, „Grynos ir taikomosios logikos metraščiai“, 145 (3): 223–239.
  • –––. (2009). S. Artemovo ir A. Nerode'o (red.), „Kompiuterių mokslo loginiai pagrindai, Tarptautinis simpoziumas, LFCS 2009“, „Deerfield Beach“, FL, JAV, 2009 m. Sausio 3–6 d., Tema „Pateisinto įsitikinimo logikos konservatyvumas“. Paskaitų užrašai kompiuterių moksle: 5407 tomas), Berlynas: „Springer“, p. 354–364.
  • Mkrtychev, A. (1997). „Įrodymų logikos modeliai“, S. Adian ir A. Nerode (red. Past.), Kompiuterių mokslo loginiai pagrindai, 4-asis tarptautinis simpoziumas, LFCS'97, Jaroslavlis, Rusija, 1997 m. Liepos 6–12 d., Tema (paskaita) Pastabos kompiuterių moksle: 1234 tomas), Berlynas: „Springer“, p. 266–275.
  • Nogina, E. (2006). „Dėl įrodymų logikos ir įrodomumo logikos“, 2005 m. Simbolinės logikos asociacijos vasaros susirinkimas, Logikos kolokviumas'05, Atėnai, Graikija (2005 m. Liepos 28 d. – rugpjūčio 3 d.), Simbolinės logikos biuletenis, 12 (2): 356.
  • –––. (2007). „Episteminis GLA išsamumas “, 2007 m. Simbolinės logikos asociacijos metiniame susirinkime, Floridos universitetas, Gainesvilis, Florida (2007 m. Kovo 10–13 d.), Simbolinės logikos biuletenis, 13 (3): 407.
  • Pacuit, E. (2006). Amsterdamo universiteto Logikos, kalbos ir skaičiavimo instituto techninė ataskaita PP – 2006–29.
  • Plaza, J. (2007). „Viešųjų ryšių logika“, Sintezė, 158 (2): 165–179.
  • Renne, B. (2008). Dinaminė episteminė logika su pateisinimu, daktaro disertacija, Kompiuterių mokslo katedra, CUNY absolventų centras, Niujorkas, NY, JAV.
  • –––. (2009). „Įrodymų šalinimas naudojant daugelio veiksnių pagrindimo logiką“, A. Heifetz (red.), Racionalumo ir žinių teoriniai aspektai, Dvyliktosios konferencijos (TARK 2009), ACM publikacijos, 227–236 p.
  • Rose, G. (1953). „Propozicinis skaičiavimas ir įgyvendinamumas“, Amerikos matematikų draugijos sandoriai, 75: 1–19.
  • Rubtsova, N. (2006). „Dėl S5 modelio realizavimo įrodymais“, žurnalas „Logic and Computation“, 16 (5): 671–684.
  • Russell, B. (1912). Filosofijos problemos, Oksfordas: Oxford University Press.
  • Sidonas, T. (1997). „Įrodomumo logika su operacijomis su įrodymais“, S. Adian ir A. Nerode (red.), Logical Computer Computer Foundations, 4-asis tarptautinis simpoziumas, LFCS'97, Jaroslavlis, Rusija, 1997 m. Liepos 6–12 d., Darbai (paskaita Pastabos kompiuterių moksle: 1234 tomas), Berlynas: „Springer“, p. 342–353.
  • Troelstra, A. (1998). „Realizavimas“, S. Buss (red.), Proof Theory Handbook, Amsterdamas: Elsevier, p. 407–474.
  • Troelstra, A. ir H. Schwichtenberg (1996). Pagrindinė įrodymų teorija, Amsterdamas: Cambridge University Press.
  • Troelstra, A. ir D. van Dalen (1988). Matematikos konstruktyvizmas (1, 2 tomai), Amsterdamas: Šiaurės – Olandija.
  • van Dalen, D. (1986). „Intuicionistinė logika“, D. Gabbay ir F. Guenther (red.), „Filosofinės logikos vadovas“(3 tomas), Bordrecht: Reidel, p. 225–340.
  • van Ditmarsch, H., W. van der Hoek ir B. Kooi (red.) (2007). Dinaminė episteminė logika („Synthese Library“, 337 tomas), Berlynas: „Springer“..
  • von Wright, G. (1951). Esė „Modal Logic“, Amsterdamas: Šiaurės Olandija.
  • Wang, R.-J. (2009). „Žinios, laikas ir loginė visažinybė“, H. Ono, M. Kanazawa ir R. de Queiroz (red.), Logika, kalba, informacija ir skaičiavimas, 16-asis tarptautinis seminaras, WoLLIC 2009, Tokijas, Japonija, birželio 21 d. 2009 m. –24, darbai (Dirbtinio intelekto paskaitų užrašai: 5514 tomas), Berlynas: „Springer“, p. 394–407.
  • Yavorskaya (Sidonas), T. (2001). „Įrodymų ir įrodomumo logika“, Grynos ir pritaikytos logikos metraštis, 113 (1–3): 345–372.
  • –––. (2008). „Sąveikaujančios aiškių įrodymų sistemos“, Kompiuterių sistemų teorija, 43 (2): 272–293.
  • Yavorsky, R. (2001). „Tikimybių logika su įrodymų kiekybiniais rodikliais“, Grynos ir pritaikytos logikos metraštis, 113 (1–3): 373–387.

Akademinės priemonės

sep vyro ikona
sep vyro ikona
Kaip pacituoti šį įrašą.
sep vyro ikona
sep vyro ikona
Peržiūrėkite šio įrašo PDF versiją „Friends of the SEP“draugijoje.
info piktograma
info piktograma
Ieškokite šios įrašo temos Indianos filosofijos ontologijos projekte (InPhO).
„Phil Papers“piktograma
„Phil Papers“piktograma
Patobulinta šio įrašo „PhilPapers“bibliografija su nuorodomis į jo duomenų bazę.

Kiti interneto šaltiniai

Rekomenduojama: