Intuitionistička Logika

Sadržaj:

Intuitionistička Logika
Intuitionistička Logika

Video: Intuitionistička Logika

Video: Intuitionistička Logika
Video: Логика. Основы Логики. Логическое Мышление 2024, Ožujak
Anonim

Ulazna navigacija

  • Sadržaj unosa
  • Bibliografija
  • Akademske alate
  • Prijatelji PDF pregled
  • Podaci o autoru i citiranju
  • Povratak na vrh

Intuitionistička logika

Prvo objavljeno u srijedu 1. rujna 1999.; suštinska revizija Utorak, 4. rujna 2018

Intuicionistička logika obuhvaća opća načela logičkog rasuđivanja koja su logičari apstrahirali iz intuicijske matematike, kao što je to razvio LEJ Brouwer početkom [1907] i [1908]. Budući da ta načela vrijede i za rusku rekurzivnu matematiku i konstruktivnu analizu E. Bishopa i njegovih sljedbenika, intuicijska se logika može smatrati logičkom osnovom konstruktivne matematike. Iako se intuicionistička analiza sukobljava s klasičnom analizom, intuicijska Heyting aritmetika je podsustav klasične Peano-aritmetike. Iz toga slijedi da je intuicionistička propozicijska logika pravi podsustav klasične propozicijske logike, a čista intuicionistička predikatna logika pravilan podsustav čiste klasične predikatne logike.

Filozofski se intuicionizam razlikuje od logike tretirajući logiku kao dio matematike, a ne kao temelj matematike; iz finitizmaomogućujući konstruktivno rasuđivanje o nebrojivim strukturama (npr. monotonska indukcija šipki na drvetu potencijalno beskonačnih nizova prirodnih brojeva); i od platonizma gledajući matematičke predmete kao mentalne konstrukte bez neovisnog idealnog postojanja. Hilbertov formalistički program, opravdati klasičnu matematiku svodeći ga na formalni sustav čija bi se dosljednost trebala uspostaviti finitističkim (dakle konstruktivnim) sredstvima, bio je najmoćniji suvremeni suparnik Brouwerovom razvoju intuicionizma. U svom eseju iz 1912. Intucionizam i formalizam Brouwer ispravno je predvidio da će svaki pokušaj dokazivanja dosljednosti potpune indukcije na prirodnim brojevima dovesti do začaranog kruga.

Brouwer je sam po sebi odbacio formalizam, ali je priznao potencijalnu korisnost formuliranja općih logičkih principa koji izražavaju intuicionistički ispravne konstrukcije, poput modus ponens. Formalni sustavi za intuicionističku propozicijsku i predikatsku logiku i aritmetiku u potpunosti su razvili Heyting [1930], Gentzen [1935] i Kleene [1952]. Gödel [1933.] dokazao je ekvikoncionističnost intuicionističkih i klasičnih teorija. Beth [1956] i Kripke [1965] pružili su semantiku u kojoj je intuicionistička logika ispravna i cjelovita, mada dokazi cjelovitosti intuicijske predikatne logike zahtijevaju neko klasično zaključivanje.

  • 1. Odbijanje Tertiuma Non Datura
  • 2. Intuitionistička predikatna logika prvog reda

    • 2.1 Formalni sustavi (mathbf {H – IPC}) i (mathbf {H – IQC})
    • 2.2 Alternativni formalizmi i teorema dedukcije
  • 3. Intuitionistička teorija brojeva (Heyting Aithmetic) (mathbf {HA})
  • 4. Osnovna teorija dokazivanja

    • 4.1 Prevođenje klasične u intuicijsku logiku
    • 4.2. Dopuštena pravila intuicijske logike i aritmetike
  • 5. Osnovna semantika

    • 5.1 Kripke semantika za intuicijsku logiku
    • 5.2. Seantika realizacije za aritmetiku Heytinga
  • 6. Dodatne teme i daljnje čitanje

    • 6.1 Subintuitionistička i intermedijska logika
    • 6.2 Napredne teme
    • 6.3 Preporučeno čitanje
  • Bibliografija
  • Akademske alate
  • Ostali internetski resursi
  • Povezani unosi

1. Odbijanje Tertiuma Non Datura

Intuitionistička logika može se ukratko opisati kao klasična logika bez aristotelovskog zakona isključene sredine:

) tag {LEM} A / vee / neg A)

ili klasični zakon uklanjanja dvostruke negacije:

) oznaka {DNE} neg / neg A / rightarrow A)

ali sa zakonom suprotnosti:

[(A / rightarrow B) rightarrow ((A / rightarrow / neg B) rightarrow / neg A))

i ex falso sequitur quodlibet:

) neg A / rightarrow (A / pravica B).)

Brouwer [1908] je primijetio da je LEM apstrahiran od konačnih situacija, a zatim se bez opravdanja proširio na izjave o beskonačnim kolekcijama. Na primjer, neka se (x, y) kreće iznad prirodnih brojeva (0, 1, 2, / ldots) i neka (B (y)) skraćuje ((primepred (y) oldand) primepred (y + 2))), gdje (primepred (y)) izražava "(y) je primarni broj." Tada se (forall y (B (y) vee / neg B (y))) drži intuicijski i klasično, jer da bismo utvrdili je li prirodni broj primarni ili ne, trebamo samo provjeriti je li ili ne ima razdjelnik strogo između sebe i 1.

Ali ako skraćenica (A (x)) (postoji y (y / gt x / oldand B (y))), tada se treba tvrditi (forall x (A (x) vee / neg A (x))) intuicionistički trebat će nam učinkovita metoda (usp. Teza Crkve-Turinga) da bismo utvrdili postoji li par blizanaca koji su veći od proizvoljnog prirodnog broja (x), i dosad takva metoda nije poznata. Očigledna poluefikasna metoda je popis par glavnih brojeva koristeći preciziranje sita Eratostena (generiranje prirodnih brojeva jedan po jedan i brisanje svakog broja (y) koji ne zadovoljava (B (y))), a ako postoji par blizanaca koji su veći od (x), ova će metoda na kraju pronaći prvu. Međutim, (forall x A (x)) izražava Twin Primes konstituciju, koja još nije dokazana ili opovrgnuta,tako da u sadašnjem stanju našeg znanja ne možemo tvrditi ni (forall x (A (x) vee / neg A (x))) niti (forall x A (x) vee / neg / forall x Sjekira)).

Može se prigovoriti da ovi primjeri ovise o činjenici da još uvijek nije riješeno rješenje Twin Primesa. Brojni Brouwerovi izvorni „kontra-primjeri“ovisili su o problemima (kao što je Fermatova posljednja teorema) koji su otad riješeni. Ali Brouweru je opći LEM bio ekvivalentan apriori pretpostavci da svaki matematički problem ima rješenje - pretpostavku koju je odbacio, predviđajući Gödelovu teoremu nepotpunosti za četvrt stoljeća.

Odbacivanje LEM-a ima dalekosežne posljedice. Na jednoj ruci,

  • Intuicionistički gledano, reductio ad absurdum dokazuje samo negativne izjave, jer se (neg / neg A / rightarrow A) ne drži općenito. (Da je to tako, LEM slijedi modus ponens iz intuicijski provjerljivog (neg / neg (A / vee / neg A)).)
  • Intuitionistička propozicijska logika nema ograničenu interpretaciju tablice istine. Postoji bezbroj različitih aksiomatičnih sustava između intuicijske i klasične logike.
  • Nije svaka propozicijska formula ima intuitivno ekvivalentni disjunktivni ili konjunktivni normalni oblik, izgrađen iz primarnih formula i njihovih negacija koristeći samo (vee) i (oldand).
  • Nije svaka formula predikata intuitivno ekvivalentno normalnom obliku prenexa, sa prednjim kvantifikatima.
  • Dok je (forall x / neg / neg (A (x) vee / neg A (x))) teorem intuicijske predikatne logike, (neg / neg / forall x (A (x) vee / neg A (x))) nije; pa je (neg / forall x (A (x) vee / neg A (x))) u skladu s intuicijskom logikom predikata.

S druge strane,

  • Svaki intuicionistički dokaz zatvorene izjave obrasca (A / vee B) može se učinkovito transformirati u intuicijski dokaz (A) ili intuicionistički dokaz (B), a slično je i za zatvorene egzistencijalne izjave.
  • Intuicionistička propozicijska logika učinkovito je odlučujuća, u smislu da se konačni konstruktivni postupak primjenjuje jednoliko na svaku propozicijsku formulu, bilo da proizvede intuicijski dokaz formule ili demonstrira da takav dokaz ne može postojati.
  • Negativni fragment intuicijske logike (bez (vee) ili (postoji)) sadrži vjeran prijevod klasične logike, a slično je i za intuicionističku i klasičnu aritmetiku.
  • Intuitionistička aritmetika se dosljedno može proširiti aksiomima koji su u suprotnosti s klasičnom aritmetikom, što omogućava formalno proučavanje rekurzivne matematike.
  • Brouwerova kontroverzna intuicionistička analiza koja je u sukobu s LEM-om može se formalizirati i pokazati dosljednom u odnosu na klasično i intuicijski ispravnu podteoriju.

2. Intuitionistička predikatna logika prvog reda

Formalizirana intuicionistička logika prirodno je motivirana neformalnim objašnjenjem intuicijeističke istine Brouwer-Heyting-Kolmogorov iznesenim u zapisima o intuicionizmu u filozofiji matematike i razvoju intuicijske logike. Konstruktivna neovisnost logičkih operacija (oldand, / vee, / rightarrow, / neg, / forall, / postoji) u suprotnosti je s klasičnom situacijom, gdje je npr. (A / vee B) ekvivalent (neg (neg A / oldand / neg B)), a (postoji xA (x)) ekvivalent je (neg / forall x / neg A (x)). S gledišta BHK, rečenica obrasca (A / vee B) tvrdi da je izgrađen ili dokaz (A), ili dokaz (B);dok (neg (neg A / oldand / neg B)) tvrdi da je izgrađen algoritam koji bi efektivno pretvorio bilo koji par konstrukcija koje dokazuju (neg A) i (neg B), u dokaz poznate kontradikcije.

2.1 Formalni sustavi (mathbf {H – IPC}) i (mathbf {H – IQC})

Slijedi Hilbertovi formalizam (mathbf {H – IQC}) iz Kleenea [1952] (usp. Troelstra i van Dalen, 1988.) za intuicionističku logiku predikata prvog reda. Jezik (L) (mathbf {H – IQC}) ima predikatna slova (P, Q (.), / Ldots) svih ariteta i pojedinih varijabli (x, y, z, / ldots) (sa ili bez pretplata (1, 2, / ldots)), kao i simboli (oldand, / vee, / rightarrow, / neg, / forall, / postoji) za logičke poveznice i kvantifikatori i zagrade (,). Atomske (ili primarne) formule (L) izrazi su kao što su (P, Q (x), R (x, y, x)) gdje je (P, Q ({.}), R ({.} {.} {.})) su (0) - ari, (1) - ari i (3) - arirajuća predikatna slova; to jest, rezultat popunjavanja svakog praznog mjesta u predikatnom pismu pojedinačnim simbolom varijable glavna je formula.(Dobro oblikovane) formule (L) definirane su induktivno kako slijedi.

  • Svaka atomska formula je formula.
  • Ako su formule (A) i (B), tada su i ((A / stari i B), (A / vee B), (A / riđak B)) i (neg A).
  • Ako je (A) formula i (x) varijabla, onda su (forall xA) i (postoji xA) formule.

Općenito, koristimo (A, B, C) kao meta varijable za dobro oblikovane formule, a (x, y, z) kao metavarke za pojedinačne varijable. Anticipirajući aplikacije (na primjer intuitivističku aritmetiku) koristimo (s, t) kao meta varijable za pojmove; u slučaju čiste predikatne logike, pojmovi su jednostavno pojedinačne varijable. Pojava varijable (x) u formuli (A) je vezana ako je ona u okviru kvantifikatora (forall x) ili (postoji x), inače slobodna. Intuicionistički klasično, ((A / leftrightarrow B)) skraćenice (((A / rightarrow B) oldand (B / rightarrow A))), a zagrade će se izostaviti ako to ne uzrokuje zabunu.

Postoje tri pravila zaključivanja:

Modus Ponens

Iz (A) i (A / rightarrow B), zaključite (B).

(forall) - Uvod

Iz (C / rightarrow A (x)), gdje je (x) varijabla koja se ne pojavljuje besplatno u (C), zaključite (C / rightarrow / forall x A (x)).

(postoji) - uklanjanje

iz (A (x) rightarrow C), gdje je (x) varijabla koja se ne pojavljuje besplatno u (C), zaključi (postoji x A (x) rightarrow C).

Aksiomi su sve formule sljedećih oblika, pri čemu je u posljednje dvije sheme podformula (A (t)) rezultat zamjene pojave izraza (t) za svaki slobodan pojavljivanje (x) u (A (x)), a nijedna varijabla slobodna u (t) ne postaje vezana u (A (t)) kao rezultat zamjene.

) begin {array} {l} A / rightarrow (B / rightarrow A) (A / rightarrow B) rightarrow ((A / rightarrow (B / rightarrow C)) rightarrow (A / rightarrow C)) / A / rightarrow (B / rightarrow (A / oldand B)) (A / oldand B) rightarrow A \(A / oldand B) rightarrow B \\ A / rightarrow (A / vee B) / B / rightarrow (A / vee B) (A / rightarrow C) rightarrow ((B / rightarrow C) rightarrow ((A / vee B) rightarrow C)) (A / rightarrow B) rightarrow ((A / rightarrow / neg B) rightarrow / neg A) / \ neg A / rightarrow (A / rightarrow B) / \ forall xA (x) rightarrow A (t) / A (t) rightarrow / postoji xA (x) end {niz})

Dokaz je bilo koji konačni niz formula, od kojih je svaka aksiom ili neposredna posljedica, pravilom zaključivanja, (jedne ili dvije) prethodne formule niza. Kaže se da bilo koji dokaz dokazuje njegovu posljednju formulu, koja se naziva teoremom ili dokazivom formulom intuicijske logike predikata prvog reda. Izvod formule (E) iz zbirke pretpostavki je bilo koji slijed formula, od kojih svaka pripada (F) ili je aksiom ili neposredna posljedica, pravilom zaključivanja prethodnih formula slijeda, tako da je (E) zadnja formula slijeda. Ako takva izvedenica postoji, kažemo da je (E) izvedljiva iz (F).

Intuitionistička logika prijedloga (mathbf {H – IPC}) je podsustav (mathbf {H – IQC}) koji nastaje kada je jezik ograničen na formule izgrađene od slova prijedloga (P, Q, R, / ldots) koristeći propozicione veze (oldand, / vee, / rightarrow) i (neg), a koriste se samo propozicijski postulati. Dakle, posljednja dva pravila zaključivanja i posljednja dva shema aksioma nedostaju iz propozicijskog podsustava.

Ako je na zadanom popisu aksiomnih shema za intuicijsku propozicijsku ili prvobitnu logiku predikata, zakon koji izražava ex Falso sequitur quodlibet:

) neg A / rightarrow (A / jagnja B))

zamjenjuje se klasičnim zakonom uklanjanja dvostrukih negacija DNE:

) neg / neg A / rightarrow A)

(ili, što je ekvivalentno, ako je intuicijski zakon uvođenja negacije:

[(A / rightarrow B) rightarrow ((A / rightarrow / neg B) rightarrow / neg A))

zamjenjuje se LEM), formalni sustav (mathbf {H – CPC}) za klasičnu propozicijsku logiku ili (mathbf {H – CQC}) za klasične predikatne logičke rezultate. Budući da su ex falso i zakon kontradikcije klasični teoremi, intuicijska logika sadržana je u klasičnoj logici. U određenom smislu, klasična logika sadržana je i u intuicijističkoj logici; vidi Odjeljak 4.1 dolje.

Važno je napomenuti da iako su LEM i DNE ekvivalentni kao sheme nad (mathbf {H – IPC}), implikacija

[(neg / neg A / rightarrow A) rightarrow (A / vee / neg A))

nije shema teorema (mathbf {H – IPC}). Za teorije (mathbf {T}) zasnovane na intuicijističkoj logici, ako je (E) proizvoljna formula (L (mathbf {T})), onda je po definiciji:

(E) je odlučno u (mathbf {T}) ako i samo ako (mathbf {T}) dokaže (E / vee / neg E).

(E) je stabilna u (mathbf {T}) ako i samo ako se (mathbf {T}) dokaže (neg / neg E / rightarrow E).

(E) se može testirati u (mathbf {T}) ako i samo ako se (mathbf {T}) dokaže (neg E / vee / neg / neg E).

Mogućnost odlučivanja podrazumijeva stabilnost, ali ne i obrnuto. Spoj stabilnosti i testabilnosti jednak je odlučnosti. Sam Brouwer dokazao je da je "apsurdnost apsurda apsurda jednaka apsurdu" (Brouwer [1923C]), tako da je svaka formula oblika (neg A) stabilna; ali u osnovnim formulama (mathbf {H – IPC}) i (mathbf {H – IQC}) i njihove negacije nisu moguće odrediti, kao što je prikazano u odjeljku 5.1 niže.

2.2 Alternativni formalizmi i teorema dedukcije

Sustav Hilbertovog stila (mathbf {H – IQC}) koristan je za metamatematska istraživanja intuicijske logike, ali njegova prisilna linearna dedukcija dedukcija i sklonost aksiomima nad pravilima čine je neugodnim instrumentom za uspostavljanje izvedljivosti. Prirodni dedukcijski sustav (mathbf {N – IQC}) za intuicijsku predikatnu logiku proizlazi iz deduktivnog sustava (mathbf {D}), predstavljenog u odjeljku 3 unosa o klasičnoj logici u ovoj enciklopediji, izostavljanjem simbol i pravila za identitet i zamjena klasičnog pravila (DNE) dvostrukog uklanjanja negacije intuicijskim pravilom eliminacije negacije koje izražava ex falso:

(INE) Ako (F) podrazumijeva (A) i (F) podrazumijeva (neg A), tada (F) podrazumijeva (B)

Ključevi za dokazivanje da je (mathbf {H – IQC}) ekvivalent (mathbf {N – IQC}) su modusi porneta i obrnuto,:

Teorem dedukcije

Ako je (B) izvedljivo iz (A) i eventualno drugih formula (F), a sve varijable koje su slobodne u (A) održane konstantnim u izvodu (to jest, bez korištenja druge ili treće pravilo zaključivanja za bilo koju varijablu (x) koja se pojavljuje u (A), osim ako se pretpostavka (A) ne pojavi u izvodu prije dotičnog zaključka), tada je (A / rightarrow B) izveden iz (F).

Ovaj temeljni rezultat, otprilike izražavajući pravilo ((rightarrow I)) od (mathbf {I}), može se dokazati za (mathbf {H – IQC}) indukcijom na definiciji a derivacija. Druga pravila (mathbf {I}) vrijede za (mathbf {H – IQC}) u osnovi modus ponens, što odgovara ((rightarrow E)) u (mathbf {N -IQC}); i svi aksiomi (mathbf {H – IQC}) mogu se provjeriti u (mathbf {N – IQC}).

Da biste ilustrirali korisnost teoreme o odbitku, razmotrite (naizgled trivijalnu) shemu teorema ((A / rightarrow A)). Ispravan dokaz u (mathbf {H – IPC}) sadrži pet redaka:

  • 1. (A / prava zvijezda (A / prava zvijezda A))
  • 2. ((A / rightarrow (A / rightarrow A)) rightarrow ((A / rightarrow ((A / rightarrow A) rightarrow A)) rightarrow (A / rightarrow A)))
  • 3. ((A / rightarrow ((A / rightarrow A) rightarrow A)) rightarrow (A / rightarrow A))
  • 4. (A / rightarrow ((A / rightarrow A) rightarrow A))
  • 5. (A / pravica A)

pri čemu su 1, 2 i 4 aksiomi, a 3, 5 potječu iz ranijih linija pomoću modusa ponens. Međutim, (A) se može izvesti iz (A) (kao pretpostavke) u jednom očiglednom koraku, pa teorema o dedukciji omogućava zaključak da postoji dokaz o (A / rightarrow A). (Zapravo, formalni dokaz (A / rightarrow A) koji je upravo predstavljen dio je konstruktivnog dokaza Teoreme o odbitku!)

Važno je napomenuti da se u definiciji izvedbe iz pretpostavki u (mathbf {H – IQC}) formulama pretpostavki tretiraju kao da su sve njihove slobodne varijable univerzalno kvantificirane, tako da (forall x A (x)) proizlazi iz hipoteze (A (x)). Međutim, varijabla (x) će se u toj derivaciji mijenjati (a ne držati se konstantnom) primjenom pravila (forall) - uvođenja; i stoga se Teorem o odbitku ne može upotrijebiti za zaključak (lažno) da je (A (x) rightarrow / forall x A (x)) (i, prema tome, prema (postoji) - uklanjanje, (postoji x A (x) rightarrow / forall x A (x))) mogu se provjeriti u (mathbf {H – IQC}). Kao primjer ispravne upotrebe Teoreme o odbitku za logiku predikata uzmite u obzir implikaciju (postoji x A (x) rightarrow / neg / forall x / neg A (x)). Da biste to pokazali, dokazivo je u (mathbf {H – IQC}),prvo izvodimo (neg / forall x / neg A (x)) iz (A (x)) sa svim slobodnim varijablama koje se drže konstantno:

  • 1. (forall x / neg A (x) rightarrow / neg A (x))
  • 2. (A (x) rightarrow (forall x / neg A (x) rightarrow A (x)))
  • 3. (A (x)) (pretpostavka)
  • 4. (forall x / neg A (x) rightarrow A (x))
  • 5. ((forall x / neg A (x) rightarrow A (x)) rightarrow ((forall x / neg A (x) rightarrow / neg A (x)) rightarrow / neg / forall x / neg A (x)))
  • 6. ((forall x / neg A (x) rightarrow / neg A (x)) rightarrow / neg / forall x / neg A (x))
  • 7. (neg / forall x / neg A (x))

Ovdje su 1, 2 i 5 aksiomi; 4 potječe od 2 i 3 pomoću modusa ponens; i 6 i 7 dolaze iz ranijih redaka modusima ponens; pa ni varijable nisu varirane. Teorem o odbitku govori nam da u (mathbf {H – IQC}) postoji dokaz (P) o (A (x) rightarrow / neg / forall) x (neg A (x)), a jedna primjena (postoji) - eliminacija pretvara (P) u dokaz (postoji x A (x) rightarrow / neg / forall x / neg A (x)). Suprotno tome nije dokazano u (mathbf {H – IQC}), kao što je prikazano u odjeljku 5.1 niže.

Ostale važne alternative za (mathbf {H – IQC}) i (mathbf {N – IQC}) su različiti sekvencijalni proračuni za intuicionističku propozicijsku i predikatnu logiku. Prvi takav račun definirao je Gentzen [1934–5], usp. Kleene [1952]. Slijedni sustavi, koji dokazuju potpuno iste formule kao (mathbf {H – IQC}) i (mathbf {N – IQC}), eksplicitno prate sve pretpostavke i zaključke u svakom koraku dokaza, zamjenjujući modus ponens (koji eliminira intermedijarnu formulu) presječenim pravilom (koje se može pokazati da je dopušteno pravilo (usp. odjeljak 4.2) za podsustav koji ostaje kada je izostavljen).

Kad detalji formalizma nisu važni, od sada pratimo Troelstra i van Dalena [1988] u napuštanju riječi "(mathbf {IQC})" ili "(mathbf {IPC})" formalni sustav za intuicijsku logiku predikata odnosno prijedloga, i slično "(mathbf {CQC})" i "(mathbf {CPC})" za klasičnu predikat i logiku prijedloga.

Oba (mathbf {IPC}) i (mathbf {IQC}) zadovoljavaju interpolacijske teoreme, npr.: Ako su (A) i (B) prijedloge formule koje imaju najmanje jedno slovo prijedloga, i ako je (A / rightarrow B) dokaziv u (mathbf {IPC}), postoji formula (C), koja sadrži samo slova prijedloga koja se pojavljuju i u (A) i (B), tako da su i (A / rightarrow C) i (C / rightarrow B) dokazivi. Te su teme obrađene u Kleeneu [1952] i Troelstra i Schwichtenberg [2000].

Dok se identitet može naravno dodati intuicionističkoj logici, za primjene (npr. Aritmetiku) simbol jednakosti općenito se tretira kao istaknuta predikatna konstanta koja zadovoljava aksiome za odnos ekvivalencije (refleksivnost, simetrija i tranzitivnost) i dodatne nelogične aksiome (npr., primitivne rekurzivne definicije zbrajanja i množenja). Identitet je odlučujući, intuicionistički i klasično, ali intuicijska ekstenzijska jednakost nije uvijek odlučujuća; pogledajte raspravu Brouwerovih aksioma kontinuiteta u 3. odjeljku unosa o intuicionizmu u filozofiji matematike.

3. Intuitionistička teorija brojeva (Heyting Aithmetic) (mathbf {HA})

Intuitionistička (Heyting) aritmetika (mathbf {HA}) i klasična (peano) aritmetika (mathbf {PA}) dijele isti jezik prvog reda i iste nelogične aksiome; samo je logika drugačija. Uz logičke poveznice, kvantifikatore i zagrade te pojedinačne varijable (x, y, z, / ldots) (koristi se i kao metavarke), aritmetički jezik (L (mathbf {HA})) binarni predikatni simbol (=), pojedinačna konstanta (0), konstantna funkcija unara (S), te konačno ili brojčano beskonačno mnogo dodatnih konstanti za primitivne rekurzivne funkcije, uključujući zbrajanje i množenje; precizan izbor je stvar ukusa i praktičnosti. Pojmovi su izgrađeni od varijabli i (0) koristeći konstante funkcija; posebno,svaki prirodni broj (n) u jeziku se izražava brojem (mathbf {n}) dobivenim primjenom (S) (n) puta na (0) (npr. (S (S (0))) je broj za (2)). Osnovne formule su oblika ((s = t)) gdje su (s, t) izrazi, a složene formule dobivene su iz njih kao i obično.

Logični aksiomi i pravila (mathbf {HA}) su ona prvorazredne intuicijske logike predikata (mathbf {IQC}). Nelogični aksiomi uključuju refleksivna, simetrična i prijelazna svojstva (=):) forall x (x = x),)) forall x / forall y (x = y / rightarrow y = x),)) forall x / forall y / forall z ((x = y / oldand y = z) rightarrow x = z);) aksiom koji karakterizira (0) kao najmanji prirodni broj:

) forall x / neg (S (x) = 0),)

aksiom koji karakterizira (S) kao funkciju jedan na jedan:

) forall x / forall y (S (x) = S (y) rightarrow x = y),)

aksiom ekstenzijske jednakosti za (S):

) forall x / forall y (x = y / rightarrow S (x) = S (y));)

primitivne rekurzivne jednadžbe definiranja za svaku funkciju konstantu, posebno za zbrajanje:) forall x (x + 0 = x),)) forall x / forall y (x + S (y) = S (x + y));) i množenje:) forall x (x / cdot 0 = 0),)) forall x / forall y (x / cdot S (y) = (x / cdot y) + x);) i (univerzalno zatvaranje) shema matematičke indukcije, za proizvoljne formule (A (x)):

[(A (0) oldand / forall x (A (x) rightarrow A (S (x)))) rightarrow / forall x A (x).)

Aksiomi ekstenzijske jednakosti za sve funkcijske konstante dobivaju se matematičkom indukcijom iz aksioma jednakosti za (S) i primionih rekurzivnih aksioma funkcija.

Odnos prirodnog reda (x / lt y) može se definirati u (mathbf {HA}) pomoću (postoji z (S (z) + x = y)) ili bez kvantifikatora formula (S (x) dot {-} y = 0) ako su simbol i primitivna rekurzivna definirajuća jednadžba za prethodnika: [Pd (0) = 0,)) forall x (Pd (S (x)) = x)) i oduzimanje presjeka:) forall x (x / dot {-} 0 = 0),)) forall x (x / dot {-} S (y) = Pd (x / dot {-} y))) prisutni su u formalizmu. (mathbf {HA}) dokazuje komparativni zakon

) forall x / forall y (x / lt y / vee x = y / vee y / lt x))

i intuicionistički oblik principa najmanjeg broja za proizvoljne formule (A (x)):

) forall x) forall y (y / lt x / rightarrow (A (y) vee / neg A (y))) rightarrow \(postoji y ((y / lt x / oldand A (y)) oldand / forall z (z / lt y / rightarrow / neg A (z))) vee \\ / forall y (y / lt x / rightarrow / neg A (y))].)

Hipoteza je potrebna jer nisu sve aritmetičke formule moguće razlučiti u (mathbf {HA}). Međutim, (forall x / forall y (x = y / vee / neg (x = y))) se može dokazati izravno matematičkom indukcijom, i tako

Primarne formule (a time i sve formule bez kvantifikatora) su decidabilne i stabilne u (mathbf {HA}).

Ako je (A (x)) odrediv u (mathbf {HA}), tada je indukcijom na (x) isto tako (forall y (y / lt x / rightarrow A (y))) i (postoji y (y / lt x / old i A (y))). Stoga

Formule u kojima su svi kvantifikatori ograničeni su decidabilni i stabilni u (mathbf {HA}).

Zbir (Delta_0) aritmetičkih formula u kojima su ograničeni svi kvantifikatori najniža je razina klasične aritmetičke hijerarhije temeljene na obrascu izmjena kvantifikata u formulama prenexa. U (mathbf {HA}) ne postoji svaka formula preksinoćnog oblika, ali Burr [2004] je otkrio jednostavnu intuicionističku aritmetičku hijerarhiju koja odgovara nivou klasične. Samo za potrebe sljedeće dvije definicije, (forall x) označava blok konačnog broja kvantifikatora univerzalnog broja, a slično (postoji x) označava blok s konačnim brojem kvantifikatora egzistencijalnog broja. S ovim konvencijama Burrove klase (Phi_n) i (Psi_n) definiraju:

  • (Phi_0 = / Psi_0 = / Delta_0),
  • (Phi_1) je klasa svih formula formule (forall x A (x)) gdje je (A (x)) u (Psi_0). Za (n / ge 2), (Phi_n) je klasa svih formula formule (forall x [A (x) rightarrow / postoji y B (x, y)]) gdje (A (x)) je u (Phi_ {n-1}), a (B (x, y)) je u (Phi_ {n-2}),
  • (Psi_1) je klasa svih formula formule (postoji x A (x)) gdje je (A (x)) u (Phi_0). Za (n / ge 2), (Psi_n) je klasa svih formula formule (A / rightarrow B) gdje je (A) u (Phi_n) i (B) je u (Phi_ {n-1}).

Odgovarajuće klasične prenex klase definirane su jednostavnije:

  • (Pi_0 = / Sigma_0 = / Delta_0),
  • (Pi_ {n +1}) je klasa svih formula formule (forall x A (x)) gdje je (A (x)) u (Sigma_n),
  • (Sigma_ {n +1}) je klasa svih formula formule (postoji x A (x)) gdje je (A (x)) u (Pi_n).

Peano aritmetika (mathbf {PA}) dolazi od Heyting arithmetic (mathbf {HA}) dodavanjem LEM ili (neg / neg A / rightarrow A) na popis logičkih aksioma, tj. koristeći klasičnu umjesto intuicijsku logiku. Sljedeći rezultati vrijede čak i u fragmentima (mathbf {HA}) i (mathbf {PA}) s indukcijskom shemom ograničenom na (Delta_0) formule.

Burrova teorema:

  • Svaka aritmetička formula je u (mathbf {HA}) ekvivalentna formuli u jednoj od klasa (Phi_n).
  • Svaka formula u (Phi_n) je proverljivo jednaka u (mathbf {PA}) formuli u (Pi_n), i obratno.
  • Svaka formula u (Psi_n) je proverljivo jednaka u (mathbf {PA}) formuli u (Sigma_n), i obratno.

(mathbf {HA}) i (mathbf {PA}) su teoretski ekvivalentni, kao što će biti prikazano u odjeljku 4. Svaki je sposoban (brojčano) izraziti vlastiti dokaz predikata. Prema Gödelovoj poznatoj teoremi o nepotpunosti, ako je (mathbf {HA}) dosljedan, tada niti (mathbf {HA}) niti (mathbf {PA}) ne mogu dokazati vlastitu dosljednost.

4. Osnovna teorija dokazivanja

4.1 Prevođenje klasične u intuicijsku logiku

Temeljna činjenica o intuicijističkoj logici je da ima istu čvrstoću konzistentnosti kao i klasična logika. Za prijedlošku logiku to je prvi dokazao Glivenko [1929].

Glivenkov teorem

proizvoljna propozicijska formula (A) je klasično dokazana, ako i samo ako je (neg / neg A) intuitivno dokaziva.

Glivenkov teorem ne širi se na logiku predikata, mada je proizvoljna predikatna formula (A) klasično dokazana ako i samo ako je (neg / neg A) dokazana u intuicijističkoj predikatnoj logici plus shema "dvostrukog negacijskog pomaka".

) tag {DNS} forall x / neg / neg B (x) rightarrow / neg / neg / forall x B (x))

Sofisticiraniji negativni prijevod klasičnih u intuicionističke teorije, neovisno zbog Gödela i Gentzena, povezuje sa svakom formulom (A) jezika (L) drugu formulu (g (A)) (s ne (vee) ili (postoji)), tako da

  • (I) Klasična predikatna logika dokazuje (A / leftrightarrow g (A)).
  • (II) Intuitionistička predikatna logika dokazuje (g (A) leftrightarrow / neg / neg g (A)).
  • (III) Ako se klasična predikatna logika dokaže (A), tada se intuicijska predikatna logika dokazuje (g (A)).

Dokazi su jasni iz sljedeće induktivne definicije (g (A)) (koristeći Gentzen-ov izravni prijevod implikacija, a ne Gödelovih u smislu (neg) i (oldand)):

) početak {poravnati *} g (P) & / tekst {je} neg / neg P, / tekst {ako} P / tekst {je glavni}. \\ g (A / stari i B) & / tekst { je} g (A) old i g (B). \\ g (A / vee B) & / text {is} neg (neg g (A) oldand / neg g (B)). \\ g (A / rightarrow B) & / text {is} g (A) rightarrow g (B). \\ g (neg A) & / text {is} neg g (A). \\ g (forall xA (x)) & / text {is} forall xg (A (x)). \\ g (postoji xA (x)) & / text {is} neg / forall x / neg g (A (x)). / End {align *})

Za svaku formulu (A), (g (A)) se intuicijski može dokazati ako i samo ako je (A) klasično prenosiva. Konkretno, ako su (B / oldand / neg B) klasično dokazani za neku formulu (B), tada je (g (B) oldand / neg g (B)) (što je (g (B / oldand / neg B))) bi zauzvrat bio intuitivno dokaziv. Stoga

(IV) Klasična i intuicijska logika predikata su ujednačene

Negativni prijevod klasične u intuicionističku teoriju brojeva još je jednostavniji, jer su primarne formule intuicionističke aritmetike stabilne. Stoga se (g (s = t)) može uzeti kao (s = t), a ostale rečenice su nepromijenjene. Negativni prijevod bilo koje instance matematičke indukcije je drugi slučaj matematičke indukcije, a ostali nelogični aksiomi aritmetike su vlastiti negativni prijevodi, tako da

(I), (II), (III) i (IV) vrijede i za teoriju brojeva

Gödel [1933e] protumačio je te rezultate kao pokazujući da su intuicionistička logika i aritmetika bogatija od klasične logike i aritmetike, jer intuicionistička teorija razlikuje formule koje su klasično jednake i ima istu čvrstoću konzistencije kao i klasična teorija. Konkretno, Gödelovi teoremi o nepotpunosti vrijede za (mathbf {HA}) kao i za (mathbf {PA}).

Izravni pokušaji da se negativna interpretacija proširi na analizu ne uspijevaju, jer negativni prijevod izbornog aksioma izbora nije teorem intuicionističke analize. Međutim, u skladu je s intuicijskom analizom, uključujući Brouwerov princip kontroverznog kontinuiteta, funkcionalnom verzijom Kleeneove rekurzivne realizacije (usp. Odjeljak 6.2 dolje). Iz toga slijedi da je intuicijska matematika, koja se može izraziti samo korištenjem svih standardnih logičkih veza i kvantifikatora, u skladu s vjernim prijevodom klasične matematike izbjegavajući (vee) i (postoji).

Ovo je važno jer je Brouwerova intuicionistička analiza u neskladu s LEM-om. Međutim, ako je (A) bilo koja negativna formula (bez (vee) ili (postoji)) tada se (neg / neg A / rightarrow A) može dokazati pomoću intuicionističke logike. Pomirenje intuicijske i klasične analize u skladu s tim crtama, nadahnuto Kripkeovim pojmom redoslijeda izbora, predlaže se u Moschovakisu [2017].

4.2. Dopuštena pravila intuicijske logike i aritmetike

Gödel [1932] primijetio je da intuicijska propozicijska logika ima svojstvo disjunkcije:

(DP) Ako je (A / vee B) teorem, onda je (A) teorema ili je (B) teorema

Gentzen [1935.] uspostavio je svojstvo disjunkcije za zatvorene formule intuicijske logike predikata. Iz toga slijedi da ako je intuicionistička logika konzistentna, onda (P / vee / neg P) nije teorema ako je (P) atomska formula. Kleene [1945, 1952] dokazao je da intuicijska teorija brojeva prvog reda ima i srodno (usp. Friedman [1975]) svojstvo postojanja:

(EP) Ako je (postoji x A (x)) zatvorena teorema, onda je za neki zatvoreni pojam (t), (A (t)) teorem

Svojstva disjunkcije i egzistencije posebni su slučajevi opće pojave svojstvene neklasičnim teorijama. Dopuštena pravila teorije su pravila pod kojima je teorija zatvorena. Na primjer, Harrop [1960] je primijetio to pravilo

Ako je (neg A / rightarrow (B / vee C)) teorem, tako je i ((neg A / rightarrow B) vee (neg A / rightarrow C))

dopušteno je za intuicijsku logiku prijedloga (mathbf {IPC}) jer ako su (A), (B) i (C) bilo koje formule takve da (neg A / rightarrow (B / vee C)) je dokazivo u (mathbf {IPC}), tada je i ((neg A / rightarrow B) vee (neg A / rightarrow C)) dokazivo u (mathbf {IPC }). Harropovo pravilo nije izvedljivo u (mathbf {IPC}), jer ((neg A / rightarrow (B / vee C)) rightarrow (neg A / rightarrow B) vee (neg A / rightarrow C)) nije intuitivno dokazati. Drugi važan primjer dopuštenog nedopustivog pravila (mathbf {IPC}) je Mintovo pravilo:

Ako je ((A / rightarrow B) rightarrow (A / vee C)) teorem, tako je i (((A / rightarrow B) rightarrow A) vee ((A / rightarrow B) rightarrow C))).

Dvoredna interpretacija tablice istine klasične propozicione logike (mathbf {CPC}) daje jednostavan dokaz da je svako dopušteno pravilo (mathbf {CPC}) izvedljivo: u protivnom, neki zadatak dodijeliti (A), (B) itd. Učinili bi hipotezu istinitom, a zaključak lažnom, i zamjenom npr. (P / rightarrow P) za slova dodijeljena sa "istina" i (P / oldand / neg P) za one kojima je dodijeljen "lažni" jedan bi bio dokaziv hipoteza i nedorečiv zaključak. Činjenica da je intuicijska situacija zanimljivija dovodi do mnogih prirodnih pitanja, na koja su nedavno odgovorena.

Generaliziranjem Mintovog pravila, Visser i de Jongh identificirali su rekurzivno nabrojani niz uzastopno jačih dopuštenih pravila („Visserova pravila“) koja su, pretpostavljaju, tvorila osnovu za dopuštena pravila (mathbf {IPC}) u smislu da je svako dopušteno pravilo izvedeno iz svojstva disjunkcije i jednog od pravila niza. Nastavljajući na radu Ghilardija [1999], Iemhoff [2001] je uspio dokazati njihovu pretpostavku. Rybakov [1997] je dokazao da je zbirka svih dopuštenih pravila (mathbf {IPC}) odlučna, ali nema konačnu osnovu. Visser [2002] pokazao je da su njegova pravila također dopuštena prijedloška pravila (mathbf {HA}) i (mathbf {HA}) proširena Markovim principom MP (definiranim u odjeljku 5.2 dolje). Novije,Jerabek [2008] je našao neovisnu osnovu za dopuštena pravila (mathbf {IPC}), sa svojstvom koje nijedno pravilo u osnovi ne proizlazi iz drugog.

Mnogo manje se zna o dopuštenim pravilima intuicijske logike predikata. Čisto (mathbf {IQC}), bez pojedinačnih ili predikatskih konstanti, ima sljedeće izuzetno dopušteno dopušteno pravilo za (A (x)) bez varijabli koje nisu slobodne, ali (x):

Ako je (postoji x A (x)) teorem, tako je i (forall x A (x)).

Nije svako dopušteno predikatno pravilo (mathbf {IQC}) prihvatljivo za sve formalne sustave temeljene na (mathbf {IQC}); na primjer, (mathbf {HA}) očito krši upravo navedeno pravilo. Visser je [1999.] dokazao da je svojstvo dopuštenog predikatnog pravila (mathbf {HA}) cjelovito (Pi_2), a u 2002. godini da je ((mathbf {HA}) (+) MP ima ista predikat dopuštena pravila kao (mathbf {HA}). Plisko [1992] je dokazao da je predikatna logika (mathbf {HA}) (+) MP (skup rečenica na jeziku (mathbf {IQC}) svih čije uniformne zamjene postoje u jezik aritmetike je provjerljiv u (mathbf {HA}) (+) MP) je (Pi_2) cjelovit; Visser [2006] proširio je ovaj rezultat na neka konstruktivno zanimljiva konzistentna proširenja (mathbf {HA}) koja nisu sadržana u (mathbf {PA}).

Iako nisu u potpunosti klasificirani, poznato je da dopuštena pravila intuicijske predikatne logike uključuju Markovo pravilo za odlučujuće predikate:

Ako je (forall x (A (x) vee / neg A (x)) oldand / neg / forall x / neg A (x)) teorem, tako je i (postoji x A (x)).

i slijedeće pravilo neovisnosti prostora (gdje se pretpostavlja da se (y) ne pojavljuje u (A (x))):

Ako je (forall x (A (x) vee / neg A (x)) oldand (forall x A (x) rightarrow / postoji y B (y))) je teorem, tako je i ((postoji y (forall x A (x) rightarrow B (y))).

Oba su pravila također dopuštena za (mathbf {HA}). Odgovarajuće implikacije (MP odnosno IP), koje se ne mogu intuicijski dokazati, potvrđuju Gödelova interpretacija "Dialectica" (mathbf {HA}) (usp. Poglavlje 6.3 dolje). Dakle, da li implikacija (CT) odgovara jednom od najzanimljivijih dopuštenih pravila Heyit-ove aritmetike, nazovimo to crkvenim i Kleeneovim pravilom:

Ako je (forall x / postoji y A (x, y)) zatvorena teorema od (mathbf {HA}), tada postoji broj (n) takav da je, vjerojatno, u (mathbf {HA}), djelomična rekurzivna funkcija s Gödelovim brojem (n) je ukupna i preslikava svaki (x) u a (y) koji zadovoljava (A (x, y)) (i štoviše (A (mathbf {x}, / mathbf {y})) je dokaziv, gdje je (mathbf {x}) broj prirodnog broja (x) i (mathbf {y}) je broj za (y)).

Kombinacija Markovskog pravila s negativnim prijevodom rezultira time da klasična i intuicijska aritmetika dokazuju iste formulare oblika (forall x / postoji y A (x, y)) gdje je (A (x, y)) količnik-free. Općenito, ako je (A (x, y)) prikladno odlučiti u (mathbf {HA}) i ako je (forall x / postoji y A (x, y)) je zatvorena teorema od klasične aritmetike (mathbf {PA}), zaključak Crkveno-Kleeneovog pravila vrijedi čak i u intuicionističkoj aritmetici. Jer, ako (mathbf {HA}) dokaže (forall x / forall y (A (x, y) vee / neg A (x, y))) tada crkva-Kleene Pravilo karakteristična funkcija od (A (x, y)) ima Gödelov broj (m), što se može naći u (mathbf {HA}); pa (mathbf {HA}) dokazuje (forall x / postoji y A (x, y) leftrightarrow / forall x / postoji y / postoji z B (mathbf {m}, x, y, z)) pri čemu je (B) bez kvantifikata,a susjedni egzistencijalni kvantifikatori mogu se ugovoriti u (mathbf {HA}). Iz toga slijedi da (mathbf {HA}) i (mathbf {PA}) imaju iste rekurzivne funkcije.

Evo dokaza da je pravilo "Ako je (forall x (A / vee B (x))) teorem, tako je i ((vee / forall x B (x))" (gdje (x) nije slobodno u (A)) nije dopušteno za (mathbf {HA}), ako je (mathbf {HA}) dosljedan. Gödelovo numeriranje daje formulu bez kvantifikata (G (x)) koja (u brojevima) izražava predikat "(x) je kod dokaza u (mathbf {HA}) of ((0 = 1)). " Intuicionističkom logikom razlučivosti aritmetičkih formula bez kvantifikata, (mathbf {HA}) dokazuje (forall x (postoji y G (y) vee / neg G (x))). Međutim, ako se (mathbf {HA}) dokazao (postoji yG (y) vee / forall x / neg G (x)), tada svojstvom disjunkcije, (mathbf {HA}) mora dokazati ili (postoji yG (y)) ili (forall x / neg G (x)). Prvi je slučaj nemoguć,svojstvom postojanja s pretpostavkom dosljednosti i činjenicom da (mathbf {HA}) dokazuje sve rečenice bez kvantifikata. Ali drugi slučaj je također nemoguć, po Gödelovoj drugoj teoremi nepotpunosti, budući da (forall x / neg G (x)) izražava konzistentnost (mathbf {HA}).

5. Osnovna semantika

Intuitionistički sustavi potaknuli su različite interpretacije, uključujući Bethov stolni stol, Rasiowa i Sikorskijev topološki model, Heytingove algebre, formule kao tipove, Kleeneove rekurzivne realizacije, Kleene i Aczel reznice i modele temeljene na snopovima i topojima. Od svih tih interpretacija Kripkeova [1965.] semantika mogućeg svijeta, u odnosu na koje je intuicijska predikatna logika potpuna i konzistentna, najviše nalikuje klasičnoj teoriji modela. S druge strane, rekurzivne interpretabilne interpretacije pokušavaju učinkovito implementirati BHK objašnjenje intuicijske istine.

5.1 Kripke semantika za intuicijsku logiku

Kripke struktura (mathbf {K}) za (L) sastoji se od djelomično uređenog skupa (K) čvorova i funkcije domene D dodijeljene svakom čvoru (k) u (K) naseljeni skup (D (k)), tako da ako (k / le k '), tada (D (k) podseteq D (k')). Uz to (mathbf {K}) ima odnos prisiljavanja određen na sljedeći način.

Za svaki čvor (k) neka je (L (k)) jezik koji se proteže (L) novim konstantama za sve elemente (D (k)). Svakom čvoru (k) i svakom (0) - ariranom predikatnom slovu (svako slovo prijedloga) (P), bilo dodijeliti (f (P, k) =) true ili ostaviti (f (P, k)) nedefinirano, u skladu sa zahtjevom da ako su (k / le k ') i (f (P, k) =) istinite, tada je (f (P, k') =) true također. Kažu da je

(k) (vDash) (P) ako i samo ako je istina (f (P, k) =).

Svakom čvoru (k) i svakom ((n + 1)) - prerikatnom predikatu slovu (Q (ldots)) dodijelite (eventualno prazan) skup (T (Q, k)) od ((n + 1)) - zbirke elemenata (D (k)) na takav način da ako je (k / le k ') tada (T (Q, k) subseteq T (Q, k ')). Kažu da je

(k) (vDash) (Q (d_0, / ldots, d_n)) ako i samo ako ((d_0, / ldots, d_n) u T (Q, k)).

Sada definirajte (k) (vDash) (E) (koja se može čitati "(k) sile (E)") za složene rečenice (E) od (L (k)) induktivno kako slijedi:

(k) (vDash) ((A / old i B)) ako je (k) (vDash) (A) i (k) (vDash) (B).
(k) (vDash) ((A / vee B)) ako je (k) (vDash) (A) ili (k) (vDash) (B).
(k) (vDash) ((A / pravac B)) ako je za svaki (k '\ ge k) ako (k') (vDash) (A) tada (k ') (vDash) (B),
(k) (vDash) (neg A) ako za ne (k '\ ge k) zna (k') (vDash) (A).
(k) (vDash) (forall x A (x)) ako je za svaki (k '\ ge k) i svaki (d / u D (k')), (k ') (vDash) (A (d)).
(k) (vDash) (postoji x A (x)) ako je za neki (d / u D (k)), (k) (vDash) (A (d)).

Bilo koji takav prisilni odnos je dosljedan:

Bez rečenice (A) i bez (k) je li slučaj da i ((k) (vDash) (A) i (k) (vDash) (neg A).

i monotono:

Ako su (k / le k ') i (k) (vDash) (A), tada (k') (vDash) (A).

Kripkeove teoreme zvučnosti i cjelovitosti utvrđuju da je rečenica (L) dokazana u intuicijskoj logici predikata ako i samo ako je na to prisiljen svaki čvor svake Kripke strukture. Tako da se pokaže da je (neg / forall x / neg P (x) rightarrow / postoji x P (x)) intuicijski neprobavljiv, dovoljno je uzeti u obzir Kripkeovu strukturu s (K = {k, k '},) (k / lt k',) (D (k) = D (k ') = {0 }), (T (P, k)) prazno, ali (T (P, k ') = {0 }). A da bi se pokazalo suprotno, intuicionistički je izvodljivo (bez da se zapravo pokazuje dokaz), potrebna su samo svojstva dosljednosti i monotonosti proizvoljnih Kripkeovih modela, s definicijom (vDash).

Kripke modeli za jezike s jednakošću mogu interpretirati (=) na svakom čvoru proizvoljnim odnosom ekvivalencije, podložno monotonosti. Za aplikacije na intuitivističku aritmetiku dovoljni su normalni modeli (oni kod kojih se jednakost tumači identitetom na svakom čvorištu) jer je jednakost prirodnih brojeva odlučna.

Propoziciona Kripke semantika je posebno jednostavna, jer je proizvoljna propozicijska formula intuicijacijski dokazana ako i samo ako je prisiljena korijenom svakog Kripke modela čiji je okvir (skup (K) čvorova zajedno s njihovim djelomičnim redoslijedom) konačan stablo s najmanje elementa (korijen). Na primjer, Kripkeov model s (K = {k, k ', k' '}, k / lt k') i (k / lt k ''), a sa (P) istina samo u (k '), pokazuje da su i (P / vee / neg P) i (neg P / vee / neg / neg P) neprobavljivi u (mathbf {IPC}), Svaki terminalni čvor ili list Kripke modela je klasični model, jer list prisiljava svaku formulu ili njenu negaciju. Samo ona slova prijedloga koja se pojavljuju u formuli (E) i samo oni čvorovi (k ') takvi da su (k / le k') relevantni za odlučivanje da li će sile (k) biti sile ili ne (E). Takva razmatranja omogućuju nam da učinkovito povežemo svaku formulu (E) (L (mathbf {IPC})) konačnu klasu konačnih struktura Kripkea koja će uključivati kontmodel u (E) ako postoji. Budući da je klasa svih teorema (mathbf {IPC}) rekurzivno brojna, zaključujemo da

(mathbf {IPC}) je učinkovito razlučivo. Postoji rekurzivna procedura koja za svaku propozicijsku formulu (E) određuje je li ili ne (E) teorema (mathbf {IPC}), koja se zaključuje bilo s dokazom (E) ili (konačni) Kripke kontramodel.

Mogućnost (mathbf {IPC}) prvi je Gentzen dobio 1935. Neodređenost (mathbf {IQC}) proizlazi iz neodređenosti (mathbf {CQC}) negativnom interpretacijom, Poznate neintuitionističke logičke sheme odgovaraju, primjerice, strukturnim svojstvima Kripkeovih modela

  • DNS drži u svakom Kripke modelu s konačnim okvirom.
  • ((A / rightarrow B) vee (B / rightarrow A)) ima u svakom Kripke modelu s linearno uređenim okvirom. Suprotno tome, svaka formula prijedloga, koja nije izvedljiva u (mathbf {IPC} + (A / rightarrow B) vee (B / rightarrow A)), ima Kripke kontramodel s linearno uređenim okvirom (usp. Odjeljak 6.1 dolje).
  • Ako (x) nije slobodan u (A), tada (forall x (A / vee B (x)) rightarrow (A / vee / forall x B (x))) ima u svakoj Kripke model (mathbf {K}) s konstantnom domenom (tako da je (D (k) = D (k ')) za sve (k, k') u (K)). Isto vrijedi i za zastupnika u MP.

Kripkeovi modeli i Beth modeli (koji se po detaljima razlikuju od Kripkeovih modela, ali su intuicijski ekvivalentni) moćan su alat za uspostavljanje svojstava intuicionističkih formalnih sustava; usp Troelstra i van Dalen [1988], Smorynski [1973], de Jongh i Smorynski [1976], Ghilardi [1999] i Iemhoff [2001], [2005]. Međutim, ne postoji čisto intuicijski dokaz da je svaka rečenica koja vrijedi u svim Kripke i Beth modelima provjerljiva u (mathbf {IQC}). Nakon Gödelove opažanja, Kreisel [1958] potvrdio je da je potpunost intuicijske predikatne logike za Beth semantiku ekvivalentna Markovom načelu MP koji je Brouwer odbacio.

Štoviše, Dyson i Kreisel [1961] pokazali su da ako je (mathbf {IQC}) slabo kompletan za Beth semantiku (to jest, ako u svakom Beth modelu nema nedokazive rečenice), vrijedi sljedeća posljedica MP: [tag {GDK} forall / alpha_ {B (alfa)} neg / neg / postoji x R (alfa, x) rightarrow / neg / neg / forall / alpha_ {B (alfa)} postoji x R (alfa, x),) gdje se (x) kreće preko svih prirodnih brojeva, (alfa) raspon nad svim beskonačnim nizovima prirodnih brojeva, (B (alfa)) skraćenica (forall x (alpha (x) leq 1)), a (R) izražava primitivni rekurzivni odnos (alpha) i (x). Suprotno tome, GDK povlači za sobom slabu kompletnost (mathbf {IQC}). Ovaj zanimljivi princip, koji bi opravdao negativnu interpretaciju oblika Brouwerove teoreme obožavatelja,slabiji je od MP, ali neprobavljiv u sadašnjim sustavima intuicijske analize. Kreisel [1962] sugerirao je da se GDK na kraju može dokazati na temelju još uvijek neotkrivenih svojstava intuicijske matematike.

Izmijenivši definiciju Kripke modela kako bi se omogućilo "eksplodiranje čvorova" koji forsiraju svaku rečenicu, Veldman [1976] je pronašao dokaz potpunosti koristeći samo intuicijsku logiku, ali je doveo u pitanje jesu li Kripkeovi modeli s eksplodirajućim čvorovima intuicijski smisleni matematički objekti.

5.2. Seantika realizacije za aritmetiku Heytinga

Jedan od načina implementacije BHK-ovog objašnjenja intuitivističke istine za aritmetiku je povezivanje svake rečenice (E) od (mathbf {HA}) neke zbirke numeričkih kodova algoritama kojima se može utvrditi konstruktivna istina (E). Nakon Kleene [1945], broj (e) realizira rečenicu (E) jezika aritmetike indukcijom na logički oblik (E):

(e) ostvaruje (r = t) ako je istina (r = t).
(e) ostvaruje (A / stari i B) ako (e) kodira par ((f, g)) tako da (f) ostvaruje (A) i (g) realizira (B).
(e) ostvaruje (A / vee B) ako (e) kodira par ((f, g)) tako da ako (f = 0) tada (g) realizira (A), a ako (f / gt 0) tada (g) ostvaruje (B).
(e) ostvaruje (A / pravica B) ako, kad god (f) realizira (A), tada je (e) djelomična rekurzivna funkcija definirana na (f), a njena vrijednost realizira (B).
(e) ostvaruje (neg A) ako ne (f) ostvaruje (A).
(e) ostvaruje (forall x A (x)) ako je za svaki (n), djelomična rekurzivna funkcija (e) definirana na (n) i njena vrijednost realizira (A (mathbf {n})).
(e) ostvaruje (postoji x A (x)) ako (e) kodira par ((n, g)) i (g) realizira (A (mathbf {n})).

Proizvoljna formula je izvediv ako neki broj ostvaruje svoje univerzalno zatvaranje. Imajte na umu da nisu oba (A) i (neg A) ostvariva ni za jednu formulu (A). Temeljni rezultat je

Nelson teorem [1947]

Ako je (A) je dobivene u (mathbf {HA}) iz provedivih formula (F), a zatim (A) je ostvariti.

Neka neintuitionistička načela mogu se pokazati ostvarivim. Na primjer, Markov princip (za formule koje se mogu odlučiti) može se izraziti shemom

(MP) (forall x (A (x) vee / neg A (x)) oldand / neg / forall x / neg A (x) rightarrow / postoji x A (x))

Iako je neprobavljiv u (mathbf {HA}), MP je moguće realizirati argumentom koji neformalno koristi Markov princip. Ali ostvarivost je u osnovi neklasična interpretacija. U (mathbf {HA}) moguće je izraziti aksiom rekurzivnog izbora CT (za "Crkvenu tezu"), što je u suprotnosti s LEM-om, ali je (konstruktivno) ostvarivo. Dakle, prema Nelsonovom teoremu, (mathbf {HA}) (+) MP (+) CT je dosljedan.

Kleene je koristio varijantu realizacije broja kako bi dokazao da (mathbf {HA}) zadovoljava pravilo Church-Kleene; isti argument djeluje i za (mathbf {HA}) s MP ili CT i za (mathbf {HA}) (+) MP (+) CT. U Kleene i Vesley [1965] i Kleene [1969] funkcije zamjenjuju brojeve kao realizirajuće objekte, uspostavljajući dosljednost formalizirane intuicionističke analize i njezino zatvaranje u verziji crkve-Kleene pravila drugog reda.

Nelsonova teorema utvrđuje neizvodljivost u (mathbf {IQC}) nekih teorema klasične predikatne logike. Ako na svako (n) postavite predikatno slovo (P (ldots)), formulu (f (P)) od (L (mathbf {HA})) sa (n) dodjeljuju se slobodne varijable i ako formula (f (A)) of (L (mathbf {HA})) dolazi iz formule (A) od (L) zamjenom svake osnovna formula (P (x_1, / ldots, x_n)) by (f (P) (x_1, / ldots, x_n)), tada se (f (A)) naziva aritmetička institut zamjene (A). Kao primjer, ako formula (L (mathbf {HA})) koja izražava "(x) kodira dokaz u (mathbf {HA}) formule s kodom (y) "Je dodijeljen (P (x, y)), rezultirajuća aritmetička zamjenska instanca od (forall y (postoji x P (x, y) vee / neg / postoji x P (x, y))) je nemoguće realizirati i stoga je neprobavljivo u (mathbf {HA}), pa je to i dvostruka negacija. Iz toga slijedi da (neg / neg / forall y (postoji x P (x, y) vee / neg / postoji x P (x, y))) nije dokazano u (mathbf {IQC}).

De Jongh [1970] kombinirao je reabilnost s Kripkeovim modelom kako bi pokazao da su intuicijska logika prijedloga (mathbf {IPC}) i fragment (mathbf {IQC}) aritmetički potpuni za (mathbf {HA}). Dovoljno je dokazati jednoliko raspoređivanje jednostavnih egzistencijalnih formula za predikat slova

De Jonghova teorema (za IPC) [1970]

Ako prijedloška formula (A) jezika (L) nije dokaziva u (mathbf {IPC}), tada će se pojaviti neki aritmetički zamjenski primjerak (A) nije dokazati u (mathbf {HA}).

Dokaz ove verzije de Jonghove teoreme ne treba ostvarivost; usp Smorynski [1973]. Kao primjer, Rosserov oblik Gödelove teoreme o nepotpunosti daje rečenicu (C) od (L (mathbf {HA})) takvu da (mathbf {PA}) ne dokazuje ni (C) ni (neg C), tako da se svojstvom disjunkcije (mathbf {HA}) ne može dokazati ((C / vee / neg C)). Ali de Jonghov semantički dokaz također je utvrdio da svaka intuitivno neprobavljiva predikatna formula ograničene vrste ima aritmetičku supstitucijsku instancu koja je neupadljiva u (mathbf {HA}). Pomoću sintaktičke metode, Daniel Leivant [1979] proširio je de Jonghovu teoremu na sve intuitivno neprobavljive predikatne formule, dokazujući da je (mathbf {IQC}) aritmetički potpun za (bf {HA}). Vidi van Oosten [1991] za povijesni prikaz i jednostavniji dokaz cjelovite teoreme, koristeći apstraktnu reabilnost s Bethovim modelima umjesto Kripkeovih modela.

Ne tvrdeći da se realizacija broja podudara s intuitivističkom aritmetičkom istinom, Nelson je uočio da za svaku formulu (A) od (L (mathbf {HA})) predikat "(y) realizira (A) "Može se izraziti u (mathbf {HA}) drugom formulom (skraćeno" (y / realizerel A) "), a shema (A / lijeva glava / postoji y (y / realizerel A)) je u skladu s (mathbf {HA}). Troelstra [1973] pokazao je da je (mathbf {HA}) (+) ((A / lijeva svjetlost / postoji y (y / realizerel A))) ekvivalent (mathbf {HA}) (+) ECT, gdje je ECT ojačani oblik CT-a. U (mathbf {HA}) (+) MP (+) ECT, što Troelstra smatra formalizacijom ruske rekurzivne matematike (usp. Odjeljak 3.2. Unosa o konstruktivnoj matematici), svaka formula od obrazac ((y / realizuje A)) ima ekvivalentni "klasični" obrazac prenexa (A "(y)) koji se sastoji od podformula bez kvantifikata, kojima prethodi izmjena "klasičnih" kvantifikatora oblika (neg / neg / postoji x) i (forall z / neg / neg), i tako (postoji y A '(y)) je vrsta predpristojnog oblika (A).

6. Dodatne teme i daljnje čitanje

6.1 Subintuitionistička i intermedijska logika

Trenutno postoji nekoliko drugih unosa u ovoj enciklopediji koji obrađuju intuicijsku logiku u različitim kontekstima, ali čini se da nedostaje općeniti tretman slabijih i jačih propozicijskih i predikatskih logika. Identificirane su i proučavane mnoge takve logike. Evo nekoliko primjera.

Subintuitionistička prijedloška logika može se dobiti iz (mathbf {IPC}) ograničavanjem jezika ili slabljenjem logike ili oboje. Ekstremni primjer prvog je (mathbf {RN}), intuicijska logika s jednom propozicijskom varijablom (P), koja je dobila ime po svojim otkrivačima Riegeru i Nishimuri [1960]. (mathbf {RN}) karakterizira Rieger-Nishimura rešetka beskonačno mnogo nejednakih formula (F_n) tako da je svaka formula čija je jedina propozicijska varijabla jednaka intuicijiističkoj logici s nekim (F_n). Nishimurina verzija je

) početak {poravnati}} F _ { infty} & = P / rightarrow P. \\ F_0 & = P / oldand / neg P. \\ F_1 & = P. \\ F_2 & = / neg P. \\ F_ {2 n + 3} & = F_ {2 n + 1} vee F_ {2n + 2}. \\ F_ {2 n + 4} & = F_ {2 n + 3} riđokota F_ {2 n + 1}. / End {align *})

U (mathbf {RN}) niti (F_ {2 n + 1}) niti (F_ {2 n + 2}) podrazumijeva drugo; ali (F_ {2 n}) podrazumijeva (F_ {2 n + 1}), a (F_ {2 n + 1}) podrazumijeva svaki od (F_ {2 n + 3}) i (F_ {2 n + 4}).

Fragmenti (mathbf {IPC}) koji nedostaju jedan ili više logičkih veznika ograničavaju jezik i, slučajno, logiku, budući da intuicionističke veze (oldand), (vee), (rightarrow), (neg) logički su neovisni nad (mathbf {IPC}). Rose [1953] je dokazao da je fragment bez implikacije (bez (rightarrow) kompletan u pogledu reabilnosti, u smislu da ako je svaka aritmetička supstitucijska instanca prijedloga formule (E) bez (rightarrow) je (broj) -rezabilan, tada je (E) teorema (mathbf {IPC}). Ovaj rezultat je u suprotnosti sa

Roseov teorem [1953]

(mathbf {IPC}) je nepotpun u pogledu realizacije.

Neka je (F) prijedloga formula [((neg / neg D / rightarrow D) rightarrow (neg / neg D / vee / neg D)) rightarrow (neg / neg D / vee / neg D)) gdje je (D) ((neg P / vee / neg Q)) i (P), (Q) su glavni. Svaka aritmetička supstitucijska instanca od (F) je ostvariva (koristeći klasičnu logiku), ali (F) nije dokazivo u (mathbf {IPC}).

Iz toga slijedi da je (mathbf {IPC}) aritmetički nepotpuno za (mathbf {HA}) (+) ECT (usp. Odjeljak 5.2).

Minimalna logika (mathbf {ML}) dolazi iz intuicijske logike brisanjem ex falso-a. Kolmogorov [1925.] pokazao je da ovaj fragment već sadrži negativnu interpretaciju klasične logike zadržavajući oba kvantifikatora, usp. Leivant [1985]. Minimalna logika dokazuje poseban slučaj (neg A / rightarrow (A / rightarrow / neg B)) ex falso za negacije. Colacito, de Jongh i Vardas [2017] proučavaju različite subminimalne logike, svaka slabija od (mathbf {ML}).

Griss je osporio Brouwerovu upotrebu negacije, prigovarajući i zakonu suprotnosti i ex falso. Vrijedi napomenuti da negacija zapravo nije potrebna za intuicijsku matematiku, jer je (0 = 1) poznata suprotnost, pa se (neg A) može definirati s (A / rightarrow 0 = 1). Tada se ex falso može navesti kao (0 = 1 / rightarrow A), a zakon kontradikcije dokaziv je iz preostalih aksioma (mathbf {H}).

Prelazna logika prijedloga je svaka dosljedna zbirka prijedloga formula koja sadrži sve aksiome (mathbf {IPC}) i zatvorena pod modusom porneta i zamjenu proizvoljnih formula za slova prijedloga. Svaka posrednička logika prijedloga sadržana je u (mathbf {CPC}). Neke posebne intermedijarne logike prijedloga, karakterizirane dodavanjem jedne ili više klasično ispravnih, ali intuicijski neprobavljivih shema aksioma (mathbf {IPC}), detaljno su proučavane.

Jedna od najjednostavnijih logika posrednih prijedloga je Gödel-Dummettova logika (mathbf {LC}), dobivena dodavanjem (mathbf {IPC}) shemi ((A / rightarrow B) vee (B / rightarrow A)) koja vrijedi za sve i samo one Kripke okvire u kojima je djelomični redoslijed čvorova linearni. Gödel [1932.] koristio je beskonačni niz uzastopno jačih intermedijarnih logika kako bi pokazao da (mathbf {IPC}) nema konačnu interpretaciju tablice istine. Za svaki pozitivni cijeli broj (n) neka (mathbf {G_n}) bude (mathbf {LC}) plus shemu ((A_1 / rightarrow A_2) vee / ldots / vee (A_1 / oldand / ldots / oldand A_n / rightarrow A_ {n + 1})). Tada (mathbf {G_n}) vrijedi za sve i samo one linearno poredane Kripke okvire s ne više od (n) čvorova.

Jankova logika (mathbf {KC}) koja dodaje (mathbf {IPC}) princip testabilnosti (neg A / vee / neg / neg A), očito nema disjunkciju nekretnine. Kreisel-Putnam logika (mathbf {KP}), dobivena dodavanjem (mathbf {IPC}) sheme ((neg A / rightarrow B / vee C) rightarrow ((neg A / rightarrow B) vee (neg A / rightarrow C))) ima svojstvo disjunkcije, ali ne zadovoljava sva Visser pravila. Umesna logika dobivena dodavanjem sheme (((neg / neg D / rightarrow D) rightarrow (D / vee / neg D)) rightarrow (neg / neg D / vee / neg D)), odgovarajuće na Roseov suprotni primjer, da (mathbf {IPC}) također ima svojstvo disjunkcije. Iemhoff [2005] je dokazao da je (mathbf {IPC}) jedina posredna logika prijedloga sa svojstvom disjunkcije koja je zatvorena po svim Visser-ovim pravilima. Iemhoff i Metcalfe [2009] razvili su formalni račun za opću prihvatljivost za (mathbf {IPC}) i neke intermedijarne logike. Goudsmit [2015] temeljita je studija dopuštenih pravila intermedijarne logike, s opsežnom bibliografijom.

Kaže se da je posredna logika prijedloga (mathbf {L}) svojstvo konačnog okvira ako postoji klasa konačnih okvira na kojima su Kripke-važeće formule upravo teoreme (mathbf {L}), Mnoge intermedijarne logike, uključujući (mathbf {LC}) i (mathbf {KP}), imaju ovo svojstvo. Jankov [1968] koristio je beskonačni niz konačno ukorijenjenih Kripkeovih okvira kako bi dokazao da postoji kontinuitet mnogih međuprostornih logika. De Jongh, Verbrugge i Visser [2009] dokazali su da je svaka intermedijska logika (mathbf {L}) s svojstvom konačnog okvira propozicijska logika (mathbf {HA (L)}), to jest klasa svih formula na jeziku (mathbf {IPC}) svih čije su aritmetičke instance zamjene dokazane u logičkom produžetku (mathbf {HA}) pomoću (mathbf {L}).

Srednja logika prijedloga (mathbf {L}) strukturno je potpuna ako je svako pravilo koje je dopušteno za (mathbf {L}) izvedljivo u (mathbf {L}), a nasljedno je strukturno dovršeno ako svaka intermedijska logika koja se proteže (mathbf {L}) također je strukturno dovršena. Svaka intermedijska logika (mathbf {L}) ima strukturni završetak (mathbf { prekrivanje {L}}), dobiven dodavanjem svih njegovih dopuštenih pravila. (mathbf {LC}) i (mathbf {G_n}) su nasljedno strukturno dovršeni. Dok (mathbf {IPC}), (mathbf {RN}) i (mathbf {KC}) nisu strukturno dovršeni, njihovi strukturni kompleti su nasljedno strukturno dovršeni. Za ove rezultate i još mnogo toga, pogledajte Citkin [2016, Ostali internetski resursi].

Neke intermedijske predikatne logike, koje se prostiraju (mathbf {IQC}) i zatvorene pod zamjenom, su (mathbf {IQC}) (+) DNS (odjeljak 4.1), (mathbf {IQC}) (+) MP (usp. Odjeljak 5.2), (mathbf {IQC}) (+) MP (+) IP (usp. Odjeljak 4.2) i intuicionistička logika konstantnih domena (mathbf {CD}) dobiven je dodavanjem shemi (mathbf {IQC}) (forall x (A / vee B (x)) rightarrow (A / vee / forall x B (x))) za sve formule (A), (B (x)) s (x) koje se ne pojavljuju slobodne u (A). Mints, Olkhovikov i Urquhart [2012, Drugi internetski resursi] pokazali su da (mathbf {CD}) nema svojstvo interpolacije, pobijajući ranije objavljene dokaze drugih autora.

6.2 Napredne teme

Brouwerov utjecaj na Gödela bio je značajan, iako Gödel nikada nije postao intuicionist. Gödelov [1933f] prijevod intuicionističke propozicijske logike u modalnu logiku (mathbf {S4}) opisan je u odjeljku 2.5 unosa o Gödelu i u uvodnoj bilješci Troelstra o prijevodu [1933f] u svesku I Gödelove zbirke Djela. Vidi također Mints [2012]. Kripkeovi modeli modalne logike prethodili su onima za intuicijsku logiku.

Alternativa Kripke i Betsovoj semantičkoj intuicijističkoj propozicijskoj i predikatnoj logici uključuje topološku interpretaciju Stonea (1937.), Tarskog [1938.] i Mostowskog [1948.] (usp. Rasiowa i Sikorski [1963.], Rasiowa [1974.]), Koja je proširena na intuicionističku analizu Scotta [1968] i Krola [1978]. M. Hyland [1982] definirao je efektivni topos Eff i dokazao da je njegova logika intuicijska. Za vrlo informativnu raspravu semantike intuicijske logike i matematike W. Ruitenberga i zanimljivu novu perspektivu G. Bezhanishvili i W. Hollidaya pogledajte u odjeljku Ostali internetski resursi (dolje).

Jedna alternativa semantibilnosti ostvarenja za intuitivističku aritmetiku je Gödelova [1958] interpretacija "Dialectica" koja povezuje svaku formulu (B) od (L (mathbf {HA})) formula bez kvantifikata (B_D) jezikom intuicionističke aritmetike svih konačnih tipova. Tumačenje (B) "Dialectica", nazovite to (B ^ D), je (postoji Y / forall x B_D (Y, x)). Ako je (B) zatvorena teorema (mathbf {HA}), tada je (B_D (F, x)) dokaziv za neki pojam (F) u Gödelovoj teoriji (mathbf { T}) "primitivnih rekurzivnih" funkcija višeg tipa. Prijevod iz (B) u (B ^ D) zahtijeva aksiom izbora (kod svih konačnih vrsta), MP i IP, pa nije strogo konstruktivan; međutim,numeričke teoretske funkcije koje se mogu izraziti izrazima (F) iz (mathbf {T}) upravo su revarektivno rekurzivne funkcije (mathbf {HA}) (i od (mathbf {PA})). Tumačenje je proširio na analizu Spector [1962]; usp Howard [1973]. Jasna izlaganja i dodatne reference nalaze se u uvodu Troelstre u prijevod na engleski jezik u Gödel [1990] izvornog članka Dialectica, u Avigadu i Fefermanu (1998) i u Ferreiri [2008].

Dok je (mathbf {HA}) pravi dio klasične aritmetike, intuicijski stav prema matematičkim objektima rezultira teorijom realnih brojeva (usp. Odjeljke 3.4–3.7 unosa o intuicionizmu u filozofiji matematike). od klasičnog. Kleenova interpretacija funkcionalne realizacije, razvijena kako bi dokazala dosljednost njegove formalizacije (mathbf {FIM}) intuicionističke teorije sekvenci ("intuicijska analiza"), mijenja interpretaciju aritmetičkih formula; na primjer, (neg / neg / forall x (A (x) vee / neg A (x))) se može realizirati funkcija za svaku aritmetičku formulu (A (x)). Na jeziku analize,Markov princip i negativan prijevod izbornog aksioma izbora spadaju u mnoga neintuitionistička načela koja se mogu ostvariti funkcijom (klasičnim argumentima) i koja su u skladu s (mathbf {FIM}); usp Kleene [1965], Vesley [1972] i Moschovakis [2003].

Konkretnu i apstraktnu semantičnost realizacije za širok spektar formalnih sustava razvili su i proučavali logičari i informatičari; usp Troelstra [1998] i van Oosten [2002] i [2008]. Varijacije osnovnih pojmova osobito su korisne za uspostavljanje relativne konzistentnosti i relativne neovisnosti neloških aksioma u teorijama zasnovanim na intuicijističkoj logici; neki primjeri su Moschovakis [1971], Lifschitz [1979] i pojmovi realizacije za konstruktivne i intuicijske teorije skupa razvijeni od strane Rathjen [2006, 2012] i Chen [2012]. Rani apstraktni pojmovi realizacije uključuju kosine Kleene [1962, 1963] i Aczel [1968], i Läuchli [1970]. Kohlenbach, Avigad i drugi razvili su interpretacijske mogućnosti za dijelove klasične matematike.

Artemova logika opravdanja alternativna je interpretacija BHK-ovog objašnjenja intuicionističkih veza i kvantifikata, s (idealiziranim) dokazima koji igraju ulogu realizirajućih predmeta. Vidi također Artemov i Iemhoff [2007].

Druga linija istraživanja intuicionističke logike tiče se Brouwerovog vrlo kontroverznog „stvaranja kontra primjera predmeta“načelima klasične analize (kao što je Markov princip) koja se ne mogu opovrgnuti na temelju teorije (mathbf {FIM}) Kleena i Vesley [1965]. Slabeći Kleeneov oblik Brouwerovog principa kontinuiranog izbora i dodavanjem aksioma kojeg je nazvao Kripkeova shema (KP), Myhill je uspio formalizirati stvaranje argumenata za stvaranje. KP nije u skladu s (mathbf {FIM}), ali Vesley [1970] je pronašao alternativni princip (Veslejeva shema VS) koji se može dosljedno dodavati u (mathbf {FIM}) i podrazumijeva sve suprotne primjere za koje Brouwer je zahtijevao stvaranje predmeta. Krol [1978] i Scowcroft dali su dokaze topološke konzistentnosti za intuicijsku analizu s Kripkeovom shemom i slabim kontinuitetom.

6.3 Preporučeno čitanje

Unos o LEJ Brouweru govori o Brouwerovoj filozofiji i matematici, s kronologijom njegovog života i odabranim popisom publikacija, uključujući prijevode i sekundarne izvore. Najbolji način da saznate više je čitanje nekih originalnih radova. Engleski prijevodi Brouwerove doktorske disertacije i drugih radova koji su se izvorno pojavili na nizozemskom, zajedno s nizom članaka na njemačkom jeziku, mogu se naći u LEJ Brouwer: Collected Works (1975), uredio Heyting. Esencijalna izvorna knjiga Benacerrafa i Putnama sadrži Brouwer [1912] (u engleskom prijevodu), Brouwer [1949] i Dummett [1975]. Mancosu's [1998] pruža engleski prijevod mnogih temeljnih članaka Brouwera, Heytinga, Glivenka i Kolmogorova, iluminirajući uvodni materijal W. van Stigta, čiji je [1990] još jedan vrijedan izvor.

Treće izdanje [1971] Heytingovog klasika [1956] atraktivan je uvod u intuicijsku filozofiju, logiku i matematičku praksu. Kao dio nevjerojatnog projekta uređivanja i objavljivanja Brouwer's Nachlass-a, van Dalen [1981] pruža sveobuhvatan prikaz Brouwerove vlastite intuicijske filozofije. Engleski prijevod, u Van Heijenoortu (1969.), iz Brouwerove [1927] (s finim uvodom Parsonsa) još uvijek je neophodna referenca za Brouwerovu teoriju kontinuuma. Veldman [1990] i [2005] autentični su moderni primjeri tradicionalne intuicijske matematičke prakse. Troelstra [1991] intuicionističku logiku stavlja u svoj povijesni kontekst kao zajednički temelj konstruktivne matematike u dvadesetom stoljeću. Bezhanishvili i de Jongh [2005,Ostali internetski resursi] uključuje nedavna dostignuća u intuicijskoj logici.

Kleene i Vesley's [1965] daje pažljiv aksiomatski tretman intuicionističke analize, dokaz njegove dosljednosti u odnosu na klasično ispravnu podteoriju i proširenu primjenu na Brouwerovu teoriju stvaranja stvarnih brojeva. Kleene [1969] formalizira teoriju parcijalnih rekurzivnih funkcionalnosti, omogućujući precizne formalizacije interpretacije funkcije-realizacije koja je korištena u [1965] i srodne interpretacije q-realizabilnosti koja daje Church-Kleeneovo pravilo za intuicionističku analizu.

Troelstra [1973], Beesonova [1985] i Troelstra i van Dalenova [1988] (s ispravkama) ističu se kao najcjelovitije studije intuicionističkih i poluintuitionističkih formalnih teorija, koristeći obje konstruktivne i klasične metode, s korisnim bibliografijama. Troelstra i Schwichtenberg [2000] paralelno predstavljaju teoriju dokaza o klasičnoj, intuicionističkoj i minimalnoj logici, usredotočujući se na sekvencijalne sustave. Troelstra [1998] prikazuje formule kao vrste i (Kleene i Aczel) crte interpretacije za propozicijsku i predikatnu logiku, kao i apstraktne i konkretne realizacije za mnoštvo aplikacija. Martin-Löfova konstruktivna teorija tipova [1984] (usp. Odjeljak 3.4 unosa o konstruktivnoj matematici) pruža još jedan opći okvir unutar kojeg se nastavlja razvijati intuicijsko zaključivanje.

Bibliografija

  • Aczel, P., 1968, "Zasićene intuicijske teorije", u HA Schmidtu, K. Schütteu i H.-J. Thiele (ur.), Prilozi matematičkoj logici, Amsterdam: Sjeverna Holandija: 1–11.
  • Artemov, S. i Iemhoff, R., 2007, „Osnovna intuicijska logika dokaza“, časopis za logiku simbola, 72: 439–451.
  • Avigad, J. i Feferman, S., 1998, "Gödenova funkcionalna (" Dialectica ") interpretacija," Poglavlje V Buss-a (ur.) 1998: 337–405.
  • Bar-Hillel, Y. (ur.), 1965, logika, metodologija i filozofija znanosti, Amsterdam: Sjeverna Holandija.
  • Beeson, MJ, 1985, Temelji konstruktivne matematike, Berlin: Springer.
  • Benacerraf, P. i Hilary Putnam (ur.), 1983., Filozofija matematike: Izabrana čitanja, 2. izdanje, Cambridge: Cambridge University Press.
  • Beth, EW, 1956., „Semantička konstrukcija intuicijske logike“, Koninklijke Nederlandse Akad. von Wettenscappen, 19 (11): 357–388.
  • Brouwer, LEJ, 1907, „O osnovama matematike“, teza, Amsterdam; Prijevod s engleskog na Heyting (ur.) 1975: 11–101.
  • –––, 1908, „Nepouzdanost logičkih principa“, engleski prijevod u Heytingu (ur.) 1975: 107–111.
  • –––, 1912., „intuicionizam i formalizam“, engleski prijevod A. Dresdena, Bilten Američkog matematičkog društva, 20 (1913): 81–96, tiskano u Benacerraf i Putnam (ur.) 1983: 77–89; također ponovljeno u Heytingu (ur.) 1975: 123–138.
  • –––, 1923. [1954], „O značaju načela isključene sredine u matematici, posebno u teoriji funkcija,“„Dodaci i ispravke“, i „Daljnji dodaci i korekcije“, prijevod s engleskog na van Heijenoort (ur.) 1967: 334–345.
  • –––, 1923., „Intuitionistische Zerlegung matematičar Grundbegriffe“, Jahresbericht der Deutschen Mathematiker-Vereinigung, 33 (1925): 251-256; prepisano u Heytingu (ur.) 1975, 275–280.
  • –––, 1927., „Intuitionistička razmišljanja o formalizmu“, izvorno objavljena 1927., engleski prijevod u van Heijenoort (ur.) 1967: 490–492.
  • –––, 1948., „Svijest, filozofija i matematika“, izvorno objavljen (1948), tiskano u Benacerraf i Putnam (ur.) 1983: 90–96.
  • Burr, W., 2004., "Intuitionistička aritmetička hijerarhija", u J. van Eijcku, V. van Oostromu i A. Visseru (ur.), Logic Colloquium '99 (Bilješke predavanja u logici 17), Wellesley, MA: ASL i AK Peters, 51–59.
  • Buss, S. (ur.), 1998, Priručnik teorije dokaza, Amsterdam i New York: Elsevier.
  • Chen, RM. i Rathjen, M., 2012, „Lifschitzeva ostvarljivost za intuicionističku teoriju skupova Zermelo-Fraenkel“, Arhiv za matematičku logiku, 51: 789–818.
  • Colacito, A., de Jongh, D. i Vargas, A., 2017, „Subminimalna negacija“, Soft računarstvo, 21: 165–164.
  • Crossley, J. i MAE Dummett (ur.), 1965, Formalni sustavi i rekurzivne funkcije, Amsterdam: North-Holland Publishing.
  • van Dalen, D. (ur.), 1981, Brouwer's Cambridge Lectures on Intuitionism, Cambridge: Cambridge University Press.
  • Dummett, M., 1975, "Filozofska osnova intuicijske logike", prvotno objavljena (1975), tiskana u Benacerraf i Putnam (ur.) 1983: 97–129.
  • Dyson, V. i Kreisel, G., 1961,, Analiza Bethove semantičke konstrukcije intuicijske logike, Tehničko izvješće br. 3, Stanford: Laboratorija primijenjene matematike i statistike, Sveučilište Stanford.
  • Ferreira, F., 2008, „Umjetnički paket gomile ideja“, Dialectica, 62: 205–222.
  • Friedman, H., 1975, „Svojstvo razdvajanja podrazumijeva brojčano svojstvo postojanja“, Zbornik radova Nacionalne akademije znanosti, 72: 2877–2878.
  • Gentzen, G., 1934–5, „Untersuchungen Über das logische Schliessen,“Mathematische Zeitschrift, 39: 176–210, 405–431.
  • Ghilardi, S., 1999, "Ujedinjenje u intuicijističkoj logici", časopis za simboličku logiku, 64: 859–880.
  • Glivenko, V., 1929, „Sur quelques point of la logique de M. Brouwer“, Académie Royale de Belgique, Bilten of la classe des Sciences, 5 (15): 183–188.
  • Gödel, K., 1932, „Zum intuitionistischen Aussagenkalkül“, Anzeiger der Akademie der Wissenschaften u Beču, 69: 65–66. Reproducirano i prevedeno s uvodnom bilješkom AS Troelstra u Gödel 1986: 222–225.
  • –––, 1933., „Zur intuitionistischen Arithmetik und Zahlentheorie“, Ergebnisse eines mathematischen Kolloquiums, 4: 34–38.
  • –––, 1933f, „Eine Interpretation des intuitionistischen Aussagenkalküls“, reproducirano i prevedeno u uvodnoj bilješci AS Troelstra u Gödel 1986: 296–304.
  • –––, 1958., „Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes“, Dialectica, 12: 280–287. Prevedeno s engleskim prijevodom u Gödel 1990: 241–251.
  • –––, 1986, Zbornik radova, Vol. I, S. Feferman i sur. (ur.), Oxford: Oxford University Press.
  • –––, 1990, Zbornik radova, Vol. II, S. Feferman i sur. (ur.), Oxford: Oxford University Press.
  • Goudsmit, JP, 2015, intuicijska pravila: Dopuštena pravila intermedijarne logike, dr. Sc. disertacija, Sveučilište u Utrechtu.
  • Harrop R., 1960, „O formulama tipova (A / rightarrow B / vee C, A / rightarrow (Ex) B (x)) u intuicijskim formalnim sustavima,“Časopis Symbolic Logic, 25: 27–32,
  • van Heijenoort, J. (ur.), 1967, od Fregea do Gödela: Izvorna knjiga iz matematičke logike 1879–1931, Cambridge, MA: Harvard University Press.
  • Heyting, A., 1930, „Die formalen Regeln der intuitionistischen Logik“, u tri dijela, Sitzungsberichte der preussischen Akademie der Wissenschaften: 42–71, 158–169. Engleski prijevod dijela I u Mancosu 1998: 311–327.
  • –––, 1956., Intuicionizam: uvod, Amsterdam: Sjeverno-nizozemska izdavaštvo, 3. revidirano izdanje, 1971.
  • Heyting, A. (ur.), 1975, LEJ Brouwer: Zbornik radova (svezak 1: Filozofija i temelji matematike), Amsterdam i New York: Elsevier.
  • Howard, WA, 1973., "Nasljedno majorizirajuće funkcionalnosti konačnog tipa", u Troelstra (ur.) 1973: 454–461.
  • Hyland, JME, 1982., "Učinkoviti topos", u Troelstra i van Dalen (ur.) 1982: 165–216.
  • Iemhoff, R., 2001, "O dopuštenim pravilima intuicionističke logike prijedloga", časopis Symbolic Logic, 66: 281–294.
  • –––, 2005., „Srednja logika i Visserova pravila“, časopis Notre Dame za formalnu logiku, 46: 65–81.
  • Iemhoff, R. i Metcalfe, G., 2009, „Teorija dokaza o prihvatljivim pravilima“, Anali čiste i primijenjene logike, 159: 171–186.
  • Jankov, VA, 1968, „Izgradnja niza snažno neovisnih superintuitionističkih propozicijskih kalkulacija“, Sovjetska matematika. Doklady, 9: 801–807.
  • Jerabek, E., 2008, „Nezavisne osnove dopuštenih pravila“, Logički časopis IGPL-a, 16: 249-267.
  • de Jongh, DHJ, 1970., "Maksimalnost intuicionističkog prijedloga proračuna s obzirom na Heytingovu aritmetiku", Journal of Symbolic Logic, 6: 606.
  • de Jongh, DHJ, i Smorynski, C., 1976, „Kripke modeli i intuicionistička teorija vrsta“, Anali matematičke logike, 9: 157–186.
  • de Jongh, D., Verbrugge, R. i Visser, A., 2011, "Međusobna logika i svojstvo de Jongh", Arhiv za matematičku logiku, 50: 197–213.
  • Kino, A., Myhill, J. i Vesley, RE (ur.), 1970, intuicionizam i teorija dokaza: Zbornik radova o ljetnoj konferenciji u Buffalo, NY, 1968, Amsterdam: Sjever-Holland.
  • Kleene, SC, 1945, „O interpretaciji intuicijske teorije brojeva“, časopis Symbolic Logic, 10: 109–124.
  • –––, 1952., Uvod u metamatiku, Princeton: Van Nostrand.
  • –––, 1962., „Disjunkcija i postojanje pod implikacijom u elementarnim intuicionističkim formalizmima“, časopis za simboličku logiku, 27: 11–18.
  • –––, 1963., „Dodatak“, časopis za simboličku logiku, 28: 154–156.
  • –––, 1965, „Klasična proširenja intuicijske matematike“, u Bar-Hillelu (ur.) 1965: 31–44.
  • –––, 1969., Formalizirane rekurzivne funkcije i formalizirana realizacija, Memoari američkog matematičkog društva 89.
  • Kleene, SC i Vesley, RE, 1965, Temelji intuicijske matematike, posebno u odnosu na rekurzivne funkcije, Amsterdam: Sjever-Holland.
  • Kreisel, G., 1958, „Elementarna svojstva cjelovitosti intuicionističke logike s napomenom o negacijama formula pre-preksa“, časopis za simboličku logiku, 23: 317–330.
  • –––, 1962, „O slaboj cjelovitosti intuicijske logike predikata“, časopis za simboličku logiku, 27: 139–158.
  • Kripke, SA, 1965, „Semantička analiza intuicijske logike“, u J. Crossleyu i MAE Dummett (ur.) 1965: 92–130.
  • Krol, M., 1978, „Topološki model intuicionističke analize s Kripkeovom shemom“, Zeitschrift für Math. Logik und Grundlagen der Math., 24: 427–436.
  • Leivant, D., 1979, „Maksimalnost intuicijske logike“, Matematički centar traktati 73, Mathematisch Centrum, Amsterdam.
  • –––, 1985., „Sintaktički prijevodi i vidljivo rekurzivne funkcije“, časopis za simboličku logiku, 50: 682–688.
  • Läuchli, H., 1970, "Apstraktni pojam realizacije, za koji je intuicijski predikatski račun dovršen", u A. Kino i sur. (ur.) 1965: 227–234.
  • Lifschitz, V., 1979, "CT (_ 0) je jači od CT (_ 0)!", Zbornik Američkog matematičkog društva, 73 (1): 101–106.
  • Mancosu, P., 1998, Od Brouwer do Hilbert: Rasprava o osnovama matematike 1920-ih, New York i Oxford: Oxford University Press.
  • Martin-Löf, P., 1984., intuicionistička teorija tipa, Bilješke Giovannija Sambina iz niza predavanja održanih u Padovi, lipanj 1980, Napoli: Bibliopolis.
  • Mints, G., 2012, „Gödel-Tarski prijevodi intuicionističkih propozicijskih formula“, u „Ispravno rezoniranje“(Bilješke predavanja u računalnoj znanosti 7265), E. Erdem i sur. (ur.), Dordrecht: Springer-Verlag: 487–491.
  • Moschovakis, JR, 1971, „Mogu li postojati nerekurzivne funkcije?“, Časopis za simboličku logiku, 36: 309–315.
  • –––, 2003, „Klasične i konstruktivne hijerarhije u proširenom intuicionističkom analiziranju“, časopis za simboličku logiku, 68: 1015–1043.
  • –––, 2009., „Logika Brouwera i Heytinga“, u Logiku od Russell-a do Churchea (Priručnik povijesti logike, svezak 5), J. Woods i D. Gabbay (ur.), Amsterdam: Elsevier: 77 -125.
  • –––, 2017., „Intuitionistička analiza i kraj vremena“, Bilten simboličke logike, 23: 279–295.
  • Nelson, D., 1947, „Rekurzivne funkcije i teorija intuicionističkih brojeva“, Transakcije Američkog matematičkog društva, 61: 307–368.
  • Nishimura, I., 1960, „O formulama jedne varijable u intuicionističkom prijedložnom računu“, časopis za simboličku logiku, 25: 327–331.
  • van Oosten, J., 1991, „Semantički dokaz de Jonghove teoreme“, Arhiv za matematičku logiku, 31: 105–114.
  • –––, 2002, „Izvodljivost: povijesni esej“, Matematičke strukture u računarskoj znanosti, 12: 239–263.
  • –––, 2008, Izvodljivost: uvod u njegovu kategoričku stranu, Amsterdam: Elsevier.
  • Plisko, VE, 1992, „O aritmetičkoj složenosti pojedinih konstruktivnih logika“, Matematičke bilješke (1993): 701–709. Preveo s Matematicheskie Zametki, 52 (1992): 94–104.
  • Rasiowa, H., 1974, Algebraic Appriach to non Classical Logics, Amsterdam: North-Holland.
  • Rasiowa, H. i Sikorski, R., 1963., The Mathematics of Metamathematics, Varšava: Panstwowe Wydawnictwo Naukowe.
  • Rathjen, M., 2006, „Izvodljivost konstruktivne teorije skupova Zermelo-Fraenkel“, u Logic Colloquium 2003 (Bilješke predavanja u logici 24), J. Väänänen i sur. (ur.), AK Peters 2006: 282–314.
  • –––, 2012, „Od slabog do jakog svojstva postojanja“, Anali čiste i primijenjene logike, 163: 1400–1418.
  • Rose, GF, 1953, "Propozicioni proračun i realizacija", Transakcije Američkog matematičkog društva, 75: 1-19.
  • Rybakov, V., 1997, Prihvatljivost pravila logičkog zaključivanja, Amsterdam: Elsevier.
  • Scott, D., 1968, "Proširenje topološke interpretacije na intuicionističku analizu", Compositio Mathematica, 20: 194-210.
  • Smorynski, CA, 1973, "Primjene Kripke modela", u Troelstra (ur.) 1973: 324–391.
  • Spector, C., 1962, „Dokazno rekurzivne funkcionalnosti analize: dokaz dosljednosti analize nastavkom načela formuliranih u trenutnoj intuicijističkoj matematici,“Teorija rekurzivne funkcije: Zbornik simpozija u čistoj matematici, svezak 5, UZP Dekker (ur.), Providence, RI: Američko matematičko društvo, 1–27.
  • van Stigt, WP, 1990., Brouwerov intuicionizam, Amsterdam: Sjeverna Holandija.
  • Stone, MH, 1937, „Topološki prikaz distributivnih rešetki i braverovske logike“, Casopis Pest. Mat. Fys., 67: 1–25.
  • Tarski, A., 1938, „Der Aussagenkalkül und die Topologie“, Fundamenta Mathematicae, 31: 103–104.
  • Troelstra, AS, 1991., „Povijest konstruktivizma u dvadesetom stoljeću“, ITLI Prepublication Series ML – 1991–05, Amsterdam. Konačna verzija u Teoriji skupa, Aritmetika i temelji matematike (Bilješke predavanja iz logike 36), J. Kenney i R. Kossak (ur.), Udruženje za simboličku logiku, Ithaca, NY, 2011: 150–179.
  • –––, 1998, „Ostvarivost“, poglavlje VI Buss-a (ur.), 1998: 407–473.
  • –––, Uvodna napomena za 1958. i 1972., Gödel, 1990: 217–241.
  • Troelstra, AS (ur.), 1973, Metamathematičko istraživanje intuicijske aritmetike i analize (Bilješke predavanja iz matematike 344), Berlin: Springer-Verlag. Ispravci i dodaci dostupni u programu za uređivanje.
  • Troelstra, AS i Schwichtenberg, H., 2000, Temeljna teorija dokaza (Cambridge tracts in Theoretical Computer Science: svezak 43), drugo izdanje, Cambridge: Cambridge University Press.
  • Troelstra, AS i van Dalen, D., 1988., Konstruktivizam u matematici: uvod, 2 sveska, Amsterdam: North-Holland Publishing. [Vidi također Ispravke u drugim internetskim izvorima.]
  • Troelstra, AS i van Dalen, D. (ur.), 1982., LEJ Brouwer Centanary Symposium, Amsterdam: North-Holland Publishing.
  • Veldman, W., 1976., „Teorem intuicionističke cjelovitosti za intuicijsku logiku predikata“, časopis Symbolic Logic, 41: 159–166.
  • –––, 1990, „Istraživanje intuicijske teorije deskriptivnih skupova“, u PP Petkov (ur.), Matematička logika, Zbornik radova Heyting Conference, New York i London: Plenum Press, 155–174.
  • –––, 2005., „Dva jednostavna skupa koji nisu Borel pozitivno“, Anali čiste i primijenjene logike, 135: 151–209.
  • Vesley, RE, 1972, "Sekvence izbora i Markov princip", Compositio Mathematica, 24: 33–53.
  • –––, 1970, „Ugodna alternativa Kripkeovoj shemi“, u A. Kino i sur. (ur.) 1970: 197ff.
  • Visser, A., 1999., „Pravila i aritmetika“, časopis za formalnu logiku Notre Dame, 40: 116–140.
  • –––, 2002, „Zamjene rečenica (Sigma ^ {0} _1): istraživanja između intuicijske logike prijedloga i intuicionističke aritmetike“, Anali čiste i primijenjene logike, 114: 227–271.
  • –––, 2006., „Predikatna logika konstruktivnih aritmetičkih teorija“, časopis za simboličku logiku, 72: 1311–1326.

Akademske alate

sep man ikona
sep man ikona
Kako navesti ovaj unos.
sep man ikona
sep man ikona
Pregledajte PDF verziju ovog unosa na Društvu prijatelja SEP-a.
inpho ikona
inpho ikona
Pogledajte ovu temu unosa na projektu Internet Filozofska ontologija (InPhO).
ikona papira phil
ikona papira phil
Poboljšana bibliografija za ovaj unos na PhilPapersu, s vezama na njegovu bazu podataka.

Ostali internetski resursi

  • Bezhanishvili, G. i Holliday, W., 2018, „Semantička hijerarhija za intuicijsku logiku“, rukopis, publikacije Fakulteta Sveučilišta Berkeley.
  • Bezhanishvili, N. i de Jongh, DHJ, 2005., intuicijska logika, Bilješke predavanja predstavljene na ESSLLI, Edinburgh.
  • Brouwer, odlomci iz Brouwer's Cambridge predavanja.
  • Citkin, A., 2016, „Nasljedno strukturno dovršeni superintuitionistički deduktivni sustavi“, rukopis na arXiv.org.
  • Mints, G., Olkhovikov, G. i Urquhart, A., 2012, „Neuspjeh interpolacije u intuicijističkoj logici konstantnih domena“, rukopis, arXiv.org.
  • Troelstra, AS i JR Moschovakis, 2018, Ispravci AS Troelstra i D. van Dalen, 1988, Konstruktivizam u matematici.
  • Problemi u logici dokazivosti, koji drži Lev Beklemishev.
  • Bibliografija realizacije, koju vodi Lars Birkedal.
  • van Oosten 2000, i ostali prepisi koji se odnose na ostvarivost, a koje održava Jaap van Oosten.

Preporučeno: