Konstruktiivne Matemaatika

2023 Autor: Noah Black | [email protected]. Viimati modifitseeritud: 2023-05-24 11:17

Sisenemise navigeerimine

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

Konstruktiivne matemaatika

Esmakordselt avaldatud teisipäeval 18. novembril 1997; sisuline redaktsioon ke 30. mai 2018

Konstruktiivset matemaatikat eristab selle traditsioonilisest vasteest, klassikalisest matemaatikast, fraasi „olemas” range tõlgendusega kui „me saame ehitada”. Konstruktiivse töö tagamiseks peame mitte ainult eksistentsiaalset kvantifikaatorit, vaid kõiki loogilisi ühendusi ja kvantifikaatoreid tõlgendama kui juhiseid selle kohta, kuidas luua nende loogiliste avaldistega väite tõestus.

Selles artiklis tutvustame tänapäevast konstruktiivset matemaatikat, mis põhineb loogiliste ühenduste ja kvantifikaatorite BHK-tõlgendusel. Arutleme konstruktiivse matemaatika nelja peamise variandi üle, pöörates erilist tähelepanu kahele variandile, mis on seotud Errett Bishopi ja Per Martin-Löfiga ning mida võib pidada minimaalseteks konstruktiivseteks süsteemideks. Seejärel visandame edusammud (mitteametlikus) konstruktiivses pöördtemaatikas - uurimisprogrammis, mille eesmärk on tuvastada põhimõtteid, näiteks Brouweri fänniteoreem, mis lisaks minimaalsetele konstruktiivsetele variantidele hõlbustavad oluliste analüütiliste teoreemide tõestamist. Pärast lühikest arutelu konstruktiivse algebra, majanduse ja rahanduse üle lõpeb sissekanne kahe lisaga: ühega teatud loogilistest põhimõtetest, mis kehtivad klassikalises, intuitionistlikus ja rekursiivses matemaatikas ning millele lisas piiskop "konstruktiivne matemaatika, hõlbustab teatud kasulike analüüsi teooriate tõestamist; ja üks arutab lähenemisi üldise topoloogia konstruktiivseks arendamiseks.

• 1. Sissejuhatus
• 2. Loogika konstruktiivne tõlgendamine

• 3. Konstruktiivse matemaatika sordid

  • 3.1 Intuitionistlik matemaatika
  • 3.2 Rekursiivne konstruktiivne matemaatika
  • 3.3 Piiskopi konstruktiivne matemaatika
  • 3.4 Martin-Löfi konstruktiivse tüübi teooria
• 4. Valiku aksioom

• 5. Konstruktiivne vastupidine matemaatika

  5.1 Fänniteoreemid CRM-is

• 6. Konstruktiivne topoloogia
• 7. Konstruktiivne matemaatiline majandus ja rahandus
• 8. Lõppmärkused

• Bibliograafia

  • Viited
  • Seotud kirjandus
• Akadeemilised tööriistad
• Muud Interneti-ressursid
• Seotud kirjed

1. Sissejuhatus

Enne kui matemaatikud väidavad midagi (peale aksioomi), peaksid nad olema tõesed. Mida tähendavad matemaatikud siis, kui nad väidavad disjunktsiooni (P \ vee Q), kus (P) ja (Q) on mõnes (formaalses või mitteametlikus) matemaatikakeeles süntaktiliselt õiged väited? Selle disjunktsiooni loomulik - ehkki, nagu näeme, mitte ainulaadne - tõlgendus seisneb selles, et mitte ainult (vähemalt) ühte lauset (P, Q) ei oma, vaid ka me saame otsustada, kumba neist peetakse. Nii nagu matemaatikud väidavad (P) ainult siis, kui nad on otsustanud, et (P) kehtib selle tõestamise teel, saavad nad väita, et (P \ vee Q) ainult siis, kui nad mõlemad suudavad esitada tõendi (P) või looge üks järgmistest: (Q).

Selle tõlgenduse abil on meil aga erijuhtum, kus (Q) on (P) eitamine, (neg P), tõsine probleem. Väita, et (neg P) tähendab, et (P) tähendab vastuolu (näiteks (0 = 1)). Kuid sageli juhtub, et matemaatikutel pole (P) ega (neg P) tõestust. Selle nägemiseks peame mõtlema ainult järgmistele Goldbachi oletustele (GC):

Iga paarisarv (gt 2) võib olla kirjutatud kahe algarve summana, mida ei ole tõestatud ega ümber lükatud, vaatamata paljude juhtivate matemaatikute parimatele pingutustele alates sellest, kui seda esmakordselt tõstatati Goldbachi kirjas Eulerile 1742. Oleme sunnitud järeldama, et P (vee Q), ainult kangekaelne optimist suudab säilitada usu tõrjutud keskosa seadusesse (LEM):

Iga väljavõtte (P) kohta kehtib kas (P) või (neg P).

Klassikaline loogika saab selle ümber, laiendades disjunktsiooni tõlgendamist: see tõlgendab (P \ vee Q) kui (neg (neg P \ kiil \ neg Q)) ehk teisisõnu: “on vastuoluline, et nii (P) kui (Q) on valed”. See viib omakorda eksistentsi idealistliku tõlgenduseni, milles (eksisteerib xP (x)) tähendab (neg \ forall x \ neg P (x)) (“on vastuoluline, et (P (x)) ole vale iga (x) kohta). Just nende disjunktsiooni ja olemasolu tõlgenduste põhjal on matemaatikud ehitanud klassikalise matemaatika suurejoonelise ja ilmselt immutamatu ehitise, mis loob aluse füüsilistele, sotsiaalsetele ja (üha enam) bioloogilistele teadustele. Laiemad tõlgendused lähevad siiski maksma: näiteks kui läheme (P \ vee Q) algsest loomulikust tõlgendusest idealistliku tõlgenduse piiramatu kasutamiseni,(neg (neg P \ kiil \ neg Q)), ei saa saadud matemaatikat üldiselt tõlgendada arvutuslike mudelite, näiteks rekursiivse funktsiooni teooria raames.

Seda punkti illustreerib hästi kulunud näide, väide:

On olemas irratsionaalseid numbreid (a, b), nii et (a ^ b) on ratsionaalne.

Lihtne klassikaline tõestusmaterjal on järgmine. Mõlemad (sqrt {2} ^ { sqrt {2}}) on ratsionaalsed, sel juhul võtame (a = b = \ sqrt {2}); või siis (sqrt {2} ^ { sqrt {2}}) on irratsionaalne, sel juhul võtame (a = \ sqrt {2} ^ { sqrt {2}}) ja (b = \ sqrt {2}) (vt Dummett 1977 [2000], 6). Kuid praeguses vormis ei võimalda see tõend täpselt kindlaks teha, kummal paaril kahest valikust ((a, b)) on nõutav omadus. ((A, b)) õige valiku määramiseks peame otsustama, kas (sqrt {2} ^ { sqrt {2}}) on ratsionaalne või irratsionaalne, mis on täpselt kasutada meie esialgset tõlgendust koosseisust (P) väitega „(sqrt {2} ^ { sqrt {2}}) on ratsionaalne“.

Siin on veel üks näide tõlgenduste erinevusest. Mõelge reaalarvude hulga (bR) kohta järgmisele lihtsale väitele:

) silt {*} jätkub x x sisse \ bR (x = 0 \ vee x \ ne 0),)

kus põhjustel, mida varsti avaldame, tähendab (x \ ne 0), et leiame ratsionaalse arvu (r), kasutades klahvi (0 \ lt r \ lt \ abs {x}). (*) Loomulik arvutuslik tõlgendus on see, et meil on protseduur, mida rakendatakse mis tahes reaalarvu (x) korral, kas öeldes, et (x = 0) või öeldes, et (x \ ne 0). (Näiteks võib selline protseduur väljastada 0 juhul, kui (x = 0), ja 1, kui (x = ne 0).) Kuna arvuti saab reaalarvu käsitleda ainult piiratud ratsionaalsete lähenduste abil, siis on alavoolu probleem, mille korral piisavalt väike positiivne arv võib arvuti poolt valeks lugeda 0; nii et avaldust õigustavat otsustusmenetlust ei saa olla (*). Teisisõnu, me ei saa oodata, et (*) peab kvantitaatori (forall) ja sideühenduse (vee) loomulikku arvutuslikku tõlgendust.

Uurime seda teise nurga alt. Las (G (n)) toimib lühendina väitele „(2n + 2) on kahe algarvu summa”, kus (n) ulatub üle positiivsete täisarvude ja määratleb lõpmatu kahendjada (ba = (a_1, a_2, \ ldots)) järgmiselt:

[a_n = \ alusta {juhtumeid} 0 & \ tekst {kui} G (n) tekst {kehtib kõigi jaoks} k \ le n \\ 1 & \ tekst {kui} neg G (n) tekst {hoiab mõnede jaoks} k \ le n \\ \ lõpp {juhtumid})

Pole kahtlust, et (ba) on arvutuslikult hästi määratletud jada, selles mõttes, et meil on iga (n) jaoks arvutamise algoritm (a_n): kontrollige paarisarvu (4, 6,8, ldots, 2n + 2), et teha kindlaks, kas igaüks neist on kahe alge summa; sel juhul määrake (a_n = 0) ja vastasel juhul määrake (a_n = 1). Nüüd arvestama tegelikku arvu, kelle (n) ^th kahendnumbri on (a_n):

) alusta {joonda *} x & = (0 \ cdot a_1 a_2 \ cdots) _ {2} & = 2 ^ {- 1} a_1 + 2 ^ {- 2} a_2 + \ cdots \& = \ summa_ {n = 1} ^ { infty} 2 ^ {- n} a_n. \ lõpeta {joonda *})

Kui (*) kehtib meie arvutusliku tõlgenduse kohaselt, siis võime valida kahe järgmise variandi vahel:

• (2 ^ {- 1} a_1 + 2 ^ {- 2} a_2 + \ cdots = 0), mis tähendab, et (a_n = 0) iga (n) kohta;
• võime leida positiivse täisarvu (N) selliselt, et (2 ^ {- 1} a_1 + 2 ^ {- 2} a_2 + \ cdots \ gt 2 ^ {- N}).

Viimasel juhul, testides (a_1, \ ldots, a_N), leiame (n \ le N) sellise, et (a_n = 1). Seega võimaldab (*) arvutuslik tõlgendus otsustada, kas eksisteerib (n) selline, et (a_n = 1); teisisõnu, see võimaldab meil otsustada Goldbachi oletuse staatuse üle. Seda tüüpi näide, mis näitab, et mõne klassikalise tulemuse konstruktiivne tõestus (P) võimaldab meil lahendada Goldbachi oletuse (ja sarnaste argumentide abil paljusid muid seni avatud probleeme, näiteks Riemann'i hüpoteesi), nimetatakse Brouweri näide või isegi brouweri vastanäide avaldusele (P) (ehkki see pole selle sõna tavapärases tähenduses vastunäide).

Goldbachi oletuse kasutamine siin on puhtalt dramaatiline. Eelmise lõigu argumenti saab muuta, et näidata, et meie arvutusliku tõlgenduse kohaselt tähendab (*) piiratud kõiketeadvuse (LPO) põhimõtet:

Iga binaarse jada ((a_1, a_2, \ ldots)) jaoks on (a_n = 0) kõigi (n) jaoks või on olemas (n) selline, et (a_n = 1), mida peetakse mitmel põhjusel põhimõtteliselt mittekonstruktiivseks põhimõtteks. Esiteks, selle rekursiivne tõlgendus, On olemas rekursiivne algoritm, mida rakendatakse igale rekursiivselt määratletud binaarsele järjestusele ((a_1, a_2, \ ldots)), väljundiks 0, kui (a_n = 0) kõigi (n) jaoks, ja väljundiks 1, kui (a_n = 1) mõne (n) jaoks, on rekursiivse funktsiooni teoorias tõestatavalt vale, isegi klassikalise loogikaga (vt Bridges & Richman [1987], 3. peatükk); nii et kui me tahame lubada kogu meie matemaatika rekursiivset tõlgendamist, siis ei saa me LPO-d kasutada. Teiseks on olemas mudeliteooria (Kripke mudelid), milles saab näidata, et LPO pole konstruktiivselt tuletatav (Bridges & Richman [1987], 7. peatükk).

2. Loogika konstruktiivne tõlgendamine

Nüüdseks peaks olema selge, et matemaatika täisvereline arvutuslik areng välistab disjunktsiooni ja olemasolu idealistlikud tõlgendused, millest enamik klassikalist matemaatikat sõltub. Konstruktiivse töö tagamiseks peame naasma klassikaliste tõlgenduste juurest loomulike konstruktiivsete juurde:

(vee) (või):	(P \ vee Q) tõestamiseks peab meil olema (P) või (Q) tõend.
(kiil) (ja):	(P \ kiilu Q) tõestamiseks peavad meil olema nii (P) kui ka (Q) tõendid.
(Parempoolne) (eeldab):	(P \ paremnool Q) tõend on algoritm, mis teisendab kõik (P) tõendid (Q) tõestuseks.
(neg) (mitte):	(neg P) tõestamiseks peame näitama, et (P) tähendab (0 = 1).
(olemas) (olemas):	tõestamiseks (eksisteerib xP (x)) peame konstrueerima objekti (x) ja tõestama, et (P (x)) omab.
(forall) (kõigi / kõigi kohta):	tõend (forall x \ SP (x)) on algoritm, mida rakendatakse mis tahes objekti (x) ja andmete jaoks, mis tõestavad, et (x \ S \ -s), tõestab, et (P (x)) hoiab.

Neid BHK-tõlgendusi (nimi peegeldab nende päritolu Brouweri, Heytingi ja Kolmogorovi loomingus) saab täpsustada, kasutades Kleene realiseeritavuse mõistet; vt (Dummett [1977/2000], 222–234; Beeson [1985], VII peatükk).

Milliseid asju otsime, kui mõtleme tõsiselt matemaatika arendamisele nii, et kui teoreem kinnitab objekti (x) olemasolu omadusega (P), siis kehastab selle tõestus algoritmid (x) konstrueerimiseks ja vajalike arvutuste abil tõestamaks, et (x) omab omadust (P). Siin on mõned teoreemide näited, millele igaühele järgneb selle konstruktiivse tõestuse nõuete mitteametlik kirjeldus.

1. Iga reaalarvu (x) jaoks on (x = 0) või (x \ ne 0). Tõendusnõue: Algoritm, mis rakendatakse antud reaalarvule (x), otsustab, kas (x = 0) või (x \ ne 0). Pange tähele, et selle otsuse tegemiseks võib algoritm kasutada mitte ainult andmeid, mis kirjeldavad (x), vaid ka andmeid, mis näitavad, et (x) on tegelikult reaalarv.

2. Kõigil ülalpool piiratud alamhulkadel (S) (bR) on minimaalselt ülaosa.

   Tõendusnõue: algoritm, mida rakendatakse reaalarvude hulgale (S), (S) liikmele (s) ja (S) ülemisele piirile,

   1. arvutab objekti (b) ja näitab, et (b) on reaalarv;
   2. näitab, et (x \ le b) iga (x \ S \ korral); ja
   3. antud reaalarv (b '\ lt b), arvutab (S) elemendi (x) selliselt, et (x \ gt b').

3. Kui (f) on suletud intervalli ([0,1]) pidev reaalväärtusega kaardistamine selliselt, et (f (0) cdot f (1) lt 0), siis on olemas (x) selliselt, et (0 \ lt x \ lt 1) ja (f (x) = 0).

   Tõendusnõue: algoritm, mida rakendatakse funktsioonile (f), (f) pidevusmoodulile ja väärtustele (f (0)) ja (f (1)),

   1. arvutab objekti (x) ja näitab, et (x) on reaalarv vahemikus 0 kuni 1; ja
   2. näitab, et (f (x) = 0).

4. Kui (f) on suletud intervalli ([0,1]) pidev reaalväärtusega kaardistamine selliselt, et (f (0) cdot f (1) lt 0), siis iga (varepsilon \ gt 0) on olemas (x) nii, et (0 \ lt x \ lt 1) ja (abs {f (x)} lt \ varepsilon).

   Tõendusnõue: algoritm, mida rakendatakse funktsioonile (f), (f) pidevusmoodulile, väärtustele (f (0)) ja (f (1)) ning a positiivne arv (varepsilon),

   1. arvutab objekti (x) ja näitab, et (x) on reaalarv vahemikus 0 kuni 1; ja
   2. näitab, et (abs {f (x)} lt \ varepsilon).

Meil on juba põhjust kahelda, kas A-l on konstruktiivne tõend. Kui punkti B tõestamisnõuded on täidetud, saame matemaatilist lauset (P) arvestades kasutada tõendit (B), et arvutada ülipõhja ratsionaalne lähend (z) (sigma) komplekti

[S = {0 } tass {x \ in \ bR: P \ kiil x = 1 })

veaga (lt \ bfrac {1} {4}). Seejärel saame kindlaks teha, kas (z \ gt \ bfrac {1} {4}), sel juhul (sigma \ gt 0) või (z \ lt \ bfrac {3} {4}), kui (sigma \ lt 1). Esimesel juhul on olemas (x \ S \ -s) koos (x \ gt 0), seega peab meil olema (x = 1) ja seega (P). Juhtumi (sigma \ lt 1) korral on meil (neg P). Seega (B) tähendab välistatud keskmise seadust.

Kuid piiskopi reaalarvude konstruktiivses teoorias, mis põhineb eelnevalt määratud konvergentsimääraga Cauchy jadadel, võime tõestada järgmist konstruktiivset vähima ülaosaga põhimõtet:

Olgu (S) (bR) mittevajalik alamhulk, mis on ülalpool piiratud. Siis on (S) minimaalselt ülaosaga siis ja ainult siis, kui see asub ülemise järjekorrani, selles mõttes, et kõigi reaalarvude (alfa, \ beeta) korral koos (alfa \ lt \ beeta), kas (beeta) on (S) ülemine piir või on olemas veel (x \ S \ -s) koos (x \ gt \ alpha) (Bishop & Bridges [1985], lk. 37, ettepanek (4.3)).

Möödudes mainime (bR) konstruktiivse teooria alternatiivset arengut, mis põhineb intervalli aritmeetikal; vt sildade ja Vîță [2006] 2. peatükki.

Kõik väited (C) ja (D), mis on klassikaliselt samaväärsed, on vaheväärtuse teoreemi versioon. Nendes avaldustes on (f) järjepidevuse mooduliks positiivsete reaalarvude järjestatud paaride ((varepsilon, \ delta)) komplekt (Omega), millel on kaks omadust:

• iga (varepsilon \ gt 0) jaoks on olemas (delta \ gt 0) nii, et ((varepsilon, \ delta) in \ Omega)
• iga ((varepsilon, \ delta) sisse \ Omega) ja kõigi (x, y [0,1]) korral (abs {x - y} lt \ delta), meil on (abs {f (x) - f (y)} lt \ varepsilon).

Avaldis (C) hõlmab veel ühte põhimõtteliselt mittekonstruktiivset põhimõtet, kõige vähem piiratud üldteadmise põhimõtet (LLPO):

Iga binaarse jada ((a_1, a_2, \ ldots)) kohta, mille maksimaalne termin on 1, kas (a_n = 0) kõigi paarisarvute (n) või (a_n = 0) kõigi paaritu (n) jaoks.

Lause (D), nõrga vormi (C), saab konstruktiivselt tõestada, kasutades standardset tüüpi intervalli vähendamise argumenti. Järgmine tugevam konstruktiivne vaheväärtuse teoreem, millest piisab enamikul praktilistel eesmärkidel, on tõestatud, kasutades ligikaudset intervalli vähendamise argumenti:

Olgu (f) pidev reaalväärtusega kaardistamine suletud intervalli ([0,1]) korral nii, et (f (0) cdot f (1) lt 0). Oletame ka, et (f) on lokaalselt nullist selles mõttes, et iga (x \ in [0,1]) ja iga (r \ gt 0) jaoks on olemas (y) selline, et (abs {x - y} lt r) ja (f (y) ne 0). Siis eksisteerib (x) selline, et (0 \ lt x \ lt 1) ja (f (x) = 0).

Vaheväärtuse teoreemi olukord on tüüpiline paljudele konstruktiivses analüüsis, kus leiame ühe klassikalise teoreemi, millel on mitu konstruktiivset versiooni, millest osa või kõik võivad klassikalise loogika alusel olla samaväärsed.

On üks kõiketeadlikkuse põhimõte, mille konstruktiivne staatus on vähem selge kui LPO-l ja LLPO-l - nimelt Markovi põhimõte (MP):

Iga binaarse jada ((a_n)) korral on vastuoluline, et kõik mõisted (a_n) võrduvad 0-ga, siis on olemas termin, mis on võrdne 1-ga.

See põhimõte on samaväärne mitmete lihtsate klassikaliste väidetega, sealhulgas järgmiste:

• Iga reaalarvu (x) korral, kui on vastuoluline, et (x) on võrdne 0, siis (x \ ne 0) (tähenduses, mida me varem mainisime).
• Iga reaalarvu (x) korral, kui on vaieldav, et (x) võrdub 0-ga, on olemas (y \ in \ bR) selline, et (xy = 1).
• Iga üks-ühe pideva kaardistamise jaoks (f: [0,1] paremnool \ bR), kui (x \ ne y), siis (f (x) ne f (y)).

Markovi põhimõte kujutab piiramatut otsingut: kui teil on tõendit selle kohta, et kõik terminid (a_n) on 0, tekitavad vastuolu, siis, testides termineid (a_1, a_2, a_3, \ ldots) omakorda, olete garanteeritud, et leiame tähtajaga 1; kuid see garantii ei laiene kinnitusele, et leiate soovitud termini enne universumi lõppu. Enamik konstruktiivse matemaatika praktikuid suhtub Markovi põhimõttesse vähemalt kahtlusega, kui mitte lausa uskumatuseni. Selliseid seisukohti toetab tähelepanek, et on olemas Kripke mudel, mis näitab, et MP pole konstruktiivselt tuletatav (Bridges & Richman [1987], 137–138.)

3. Konstruktiivse matemaatika sordid

Soov säilitada arvutusliku tõlgenduse võimalus on üks motivatsioon ülaltoodud loogiliste ühenduste ja kvantifikaatorite konstruktiivsete tõlgenduste kasutamiseks; kuid see pole just matemaatika konstruktivismi pioneeride motivatsioon. Selles osas vaatleme mõnda erinevat lähenemist matemaatika konstruktivismile viimase 130 aasta jooksul.

3.1 Intuitionistlik matemaatika

XIX sajandi lõpus olid mõned isikud - eriti Kronecker ja Poincaré - avaldanud kahtlust mõne nende kaasaegse kasutatud idealistlike ja mittekonstruktiivsete meetodite osas või isegi taunimises nende vastu; kuid LEJ Brouweri (1881–1966) poleemilistes kirjutistes, alustades Amsterdami doktoriväitekirjaga Brouwer [1907] ja jätkates järgmise neljakümne seitsme aasta jooksul, on konstruktiivse matemaatika täpse, süstemaatilise lähenemisviisi alused pandi. Brouweri filosoofias, mida tuntakse intuitionismina, on matemaatika inimmõistuse vaba looming ja objekt eksisteerib siis ja ainult siis, kui seda saab (vaimselt) üles ehitada. Kui võtta see filosoofiline seisukoht, siis juhitakse paratamatult eelnimetatud loogiliste ühenduste ja kvantifikaatorite konstruktiivset tõlgendust:kuidas saaks tõend teatava objekti olematuse kohta (x) kirjeldada (x) vaimset konstruktsiooni?

Brouwer ei olnud oma ideede kõige selgem väljapanija, nagu näitab järgmine tsitaat:

Matemaatika tekib siis, kui aja möödudes tekkiv kahest küljest tulenev teema on ära võetud kõigist erilistest sündmustest. Kõigi nende kahe sisuga ühise sisu järelejäänud tühi vorm) (n) seos (n + 1)] muutub matemaatika algseks intuitsiooniks ja seda korrata saab piiramatult uusi matemaatilisi aineid. (tsiteeritud Kline'is [1972], 1199–2000)

Brouweri vaate kaasaegse versiooni andis Errett Bishop (Bishop [1967], lk 2):

Matemaatika peamine mure on arv ja see tähendab positiivseid täisarvu. Me tunneme numbri järgi seda, kuidas Kant tundis kosmose suhtes. Positiivseid täisarvu ja nende aritmeetikat eeldab meie intelligentsuse olemus ja, kui meil on kiusatus uskuda, intelligentsuse olemus üldiselt. Positiivsete täisarvude väljatöötamine ühiku primitiivkontseptsioonist, ühikuga külgneva kontseptsiooni ja matemaatilise induktsiooni protsess on täielik veendumus. Kroneckeri sõnul lõid positiivsed täisarvud Jumal.

Vaatamata sellele, et Brouweri kirjutised võivad olla varjatud, oli üks asi alati selge: tema jaoks oli matemaatika loogika suhtes ülimuslik. Võib öelda, nagu tegi Hermann Weyl järgmises lõigus, et Brouwer pidas klassikalist matemaatikat vigaseks just klassikalise loogika kasutamisel, viitamata aluseks olevale matemaatikale:

[Brouweri] arvamuse ja ajaloo lugemise järgi võeti klassikaline loogika lõplike komplektide ja nende alamhulkade matemaatikast. … Unustades selle piiratud päritolu, viis see pärast seda loogikat millegi ees ja enne kogu matemaatikat valesti ja viis selle lõpuks ilma põhjenduseta lõpmatute komplektide matemaatikasse. See on määratud teooria langenud ja algupärane patt, mille eest seda karistavad õiglaselt antinoomiad. Üllatav pole mitte see, et sellised vastuolud ilmnesid, vaid see, et nad ilmnesid mängu nii hilises etapis. (Weyl [1946])

Eelkõige viis selline loogika väärkasutamine olemasolu mittekonstrueerivate eksistentsitõenditeni, mis Weyli sõnul “teatavad maailmale, et aare eksisteerib, ilma selle asukohta avaldamata”.

Intuitsionistist matemaatiku kasutatud loogika kirjeldamiseks oli esmalt vaja analüüsida mõistuse matemaatilisi protsesse, mille põhjal saaks loogika ekstraheerida. 1930. aastal avaldas Brouweri kuulsaim õpilane Arend Heyting formaalsete aksioomide komplekti, mis iseloomustavad intuitiivisti kasutatud loogikat nii selgelt, et neist on üldtuntud kui intuitionistliku loogika aksioomid (Heyting [1930]). Need aksioomid hõivasid ühenduste ja kvantifikaatorite mitteametliku tõlgenduse, mille me varem andsime.

Intuitionistlik matemaatika erineb mõiste „jada” teistsugusest konstruktiivsest matemaatikast. Tavaliselt antakse jada konstruktiivses matemaatikas reegli abil, mis määrab eelnevalt kindlaks, kuidas kõiki selle termineid konstrueerida; selline järjestus võib olla seadusega sarnane või ettemääratud. Brouwer üldistas seda järjestuse mõistet, et hõlmata võimalust konstrueerida termineid ükshaaval, iga termini valimisel võib kasutada vabalt või ainult teatud eelnevalt määratletud piiranguid. Enamik jadadega manipuleerimist ei nõua, et need oleksid eelnevalt kindlaks määratud, ja neid saab teha nende üldisemate vaba valikuga jadade korral.

Seega, intuitsioonisti jaoks ei pea reaalarv (bx = (x_1, x_2, \ ldots)) - põhimõtteliselt Cauchy ratsionaalsete numbrite jada andma - reegliga: selle terminid (x_1, x_2, \ ldots) on lihtsalt ratsionaalsed numbrid, mis on järjestikku konstrueeritud ja mille suhtes kehtivad ainult mingid Cauchy piirangud, näiteks järgmine, mida kasutas piiskop [1967]:

) foll m \ forall n \ left) abs {x_m - x_n} le \ left (frac {1} {m} + \ frac {1} {n} right) right])

Kui vabade valikute seeriad on matemaatikasse sisse lastud, on need ehk mõneti üllatuseks mõned tugeva valiku põhimõtted. Olgu (P) alamhulk numbrist (bN ^ { bN} korda \ bN) (kus (bN) tähistab naturaalarvude komplekti ja komplektide (A) ja (B, B ^ A) tähistab kaardistamise komplekti (A) -st (B)) ja oletagem, et iga (ba \ in \ bN ^ { bN}) jaoks on olemas (n \ sisse \ bN) selliselt, et ((ba, n) sisse P). Konstruktiivsest küljest tähendab see, et meil on protseduur, mis on rakendatav jadade jaoks ja mis arvutab (n) mis tahes antud (ba) jaoks. Brouweri sõnul on elemendi (bN ^ { bN}) konstrueerimine igavesti puudulik: geneeriline jada (ba) on puhtalt laiend selles mõttes, et me ei saa antud hetkel midagi teada umbes (ba), välja arvatud selle tingimuste piiratud kogum. Sellest järeldub, et meie protseduur peab olema võimeline arvutama (ba) tingimuste mingist lõplikust algjärjestusest ((a_0, \ ldots, a_N)) naturaalarvu (n) nii, et (P (ba, n)). Kui (bb \ in \ bN ^ { bN}) on selline jada, et (b_ {k} = a_ {k}) jaoks (0 \ le k \ le N), siis meie protseduur peab tagastama sama ((n) jaoks (bb) nagu (ba). See tähendab, et (n) on (ba) pidev funktsioon mõõdiku antud (bN ^ { bN}) topoloogia suhtesSee tähendab, et (n) on (ba) pidev funktsioon mõõdiku antud (bN ^ { bN}) topoloogia suhtesSee tähendab, et (n) on (ba) pidev funktsioon mõõdiku antud (bN ^ { bN}) topoloogia suhtes

) varrho: (ba, \ bb) rightsquigarrow \ inf {2 ^ {- n}: a_k = b_k \ text {jaoks} 0 \ le k \ le n }.)

Seetõttu juhitakse meid järgmise pideva valiku põhimõtte juurde, mis jaguneme järjepidevuse osaks ja valiku osaks.

CC1: Kõik funktsioonid vahemikust (bN ^ { bN}) kuni (bN) on pidevad.

CC2: Kui (P \ subseteq \ bN ^ { bN} korda \ bN) ja iga (ba \ in \ bN ^ { bN}) jaoks on olemas (n \ in \ bN) selliselt, et ((ba, n) in P), siis on olemas funktsioon (f: \ bN ^ { bN} parempoolne nool \ bN), mis ((ba, f (ba)) in P) kõigi (ba \ in \ bN ^ { bN}) jaoks.

Kui (P) ja (f) on nagu CC2, siis ütleme, et (f) on valiku (P) funktsioon.

Kõikvõimalikkuse põhimõtted LPO ja LLPO on hüpoteesi CC1–2 kohaselt ilmselgelt valed; kuid MP on sellega kooskõlas. CC1–2 tähelepanuväärsete tagajärgede hulgas on järgmised.

• Mis tahes funktsioon alates (bN ^ { bN}) või (2 ^ { bN}) meetermõõdustikuni on punkti suunas pidev.
• Iga kaardistamine mittevajalikust täielikult eraldatavast mõõdiku ruumist meetrilise ruumi juurde on punkti suunas pidev.
• Iga kaart reaalsest joonest (bR) kuni selleni on pidevas suunas.
• Olgu (X) täielik eraldatav normeeritud ruum, (Y) normeeritud tühik ja ((u_n)) lineaarsete seoste jada vahemikust (X) kuni (Y) selliselt, et iga ühiku vektor (x) väärtusest (X),) phi (x) = \ sup { Vert u_n (x) rVert: n \ in \ bN }) eksisteerib. Siis on olemas selline (c \ gt 0), et (lVert u_n (x) rVert \ le c) kõigi (n \ in \ bN) ja kõigi ühikvektorite (x) jaoks (X) (ühtse piiratuse põhimõte).

Kõik need väited näivad olevat vastuolus tuntud klassikaliste teooriatega. Võrdlemist klassikalise matemaatikaga ei tohiks siiski teha pealiskaudselt: selleks, et aru saada, et siin pole tõelist vastuolu, peame hindama, et selliste mõistete nagu „funktsioon” ja isegi „reaalarv” tähendus intuitiivses matemaatikas on üsna erinev sellest klassikalises keskkonnas. (Praktikas ei saa intuitionistlikku matemaatikat hõlpsalt ja otse võrrelda klassikalise matemaatikaga.)

Brouweri enesevaatlus funktsioonide olemuse ja pidevuse üle viis ta teise põhimõtte juurde, mis erinevalt pideva valiku põhimõttest on klassikaliselt kehtiv. Selle põhimõtte selgitamiseks on vaja pisut rohkem tausta.

Mis tahes hulga (S) jaoks tähistame tähega (S ^ *) elemendi (S) kõigi lõplike jadade komplekti, sealhulgas tühja jada (()). Kui (alpha = (a_1, \ ldots, a_n)) asub asukohas (S ^ *), nimetatakse (n) pikkuseks (alpha) ja tähistatakse tähega (abs { alpha}). Kui (m \ in \ bN) ja (alpha) on piiratud või lõpmatu jada vähemalt (S) pikkusega (m), siis tähistame tähega (riba { alfa} (m)) lõplik jada, mis koosneb (alfa) esimestest (m) terminitest. Pange tähele, et (riba { alpha} (0) = ()) ja (abs { bar { alpha} (0)}) = 0. Kui (alpha \ in S ^ *) ja (beeta = \ riba { alpha} (m)) mõne (m) jaoks, siis ütleme, et (alpha) on laiend (beeta) ja see (beeta) on (alfa) piirang.

Väidetavalt on (S) alamhulk (sigma) eemaldatav ((S)), kui

) jätkub x \ S-vormingus (x \ in \ sigma \ vee x \ not \ in \ sigma).)

(BN ^ *) eemaldatavat alamhulka (sigma) nimetatakse ventilaatoriks, kui

• see on piirangutega suletud: iga (alpha \ in \ bN ^ *) ja iga (n) korral, kui (bar { alpha} (n) S), siis (riba { alpha} (k) sisse S) alati (0 \ le k \ le n); ja
• iga (alpha \ in \ sigma) korral) { alpha ^ * n \ in S: n \ in \ bN }) on piiratud või tühi, kus (alpha ^ * n) tähistab lõplikku jada, mis saadakse naturaalarvu (n) liitumisel tingimustega (alpha).

Tee ventilaatoris (sigma) on jada (alpha), piiratud või lõpmatu, nii et (riba { alpha} (n) sisse \ sigma) iga kohaldatava (n). Me ütleme, et alamhulk (B) blokeerib tee (alfa), kui üksus (alfa) piirab asukohta (B); kui rakenduses (B) pole piiranguid (alpha), siis öeldakse, et (alpha) jätab kasutamata (B). Ventilaatori (sigma) alamhulka (B) nimetatakse (sigma) ribaks, kui (B) blokeerib (sigma) iga lõpmatu tee; riba (B) jaoks (sigma) on ühtlane, kui on olemas (n \ in \ bN), nii et (B) blokeerib iga pikkuse (n) tee.

Lõpuks võime öelda Brouweri järgmise intuitsiooni põhimõtte, eemaldatavate ribade fänniteoreemi (FT (_ D)):

Ventilaatori iga eemaldatav riba on ühtlane.

Klassikalises kontrapositiivses vormis on FT (_ D) tuntud kui Königi Lemma: kui iga (n) jaoks on olemas pikkuse ((n)) tee, mis jätab vahele (B), on olemas lõpmatu tee, mis jääb vahele (B) (vt Dummett 1977 [2000], 49–53). (Muidugi, klassikaliselt on eraldatavuse tingimus üleliigne.) Brouweri vastanäite konstrueerimine Königi Lemma juurde on lihtne.

Brouwer poseeris fänniteoreemil ilma riba riba eemaldatavust piiramata. Püüab tõestada, et fänni üldisem teoreem tugineb konstruktiivselt analüüsile, kuidas saime teada, et alamhulk on tulp, ja viis Brouwerini tulpade esilekutsumise mõiste juurde; seda on käsitletud matemaatikafilosoofia intuitsiooni käsitleva sissekande jaotises 3.6; veel üks hea viide riba esilekutsumiseks on van Atten (2004). Naaseme 4. osas fänniteooriate juurde.

Brouweri põhimõtete paljudest rakendustest on kõige kuulsam tema ühtne järjepidevuse teoreem (mis tuleneb CC1-2 punktilisest järjepidevuse tagajärjest koos fänniteoreemi üldisema vormiga kui FT (_ D)):

Iga kaardistamine kompaktsest (see tähendab täielikust, täielikult piiritletud) meetrilisest ruumist mõõdiku ruumi on ühtlaselt pidev.

Lugejat hoiatatakse veel kord, et ta peaks seda Brouweri intuitsioonistlikus raamistikus hoolikalt tõlgendama ja mitte hüppama eksliku järelduse juurde, et intuitionism on vastuolus klassikalise matemaatikaga. Mõistlikum on pidada kahte matemaatika tüüpi võrreldamatuks. Edasiseks aruteluks lugege intuitionistliku loogika sissekannet.

Kahjuks - ja võib-olla paratamatult - silmitsi seisuga matemaatikute, näiteks Hilbert, vastuseisuga, sattus Brouweri intuitsionistlik matemaatika- ja filosoofiakool üha enam sellesse, mis vähemalt klassikalistele matemaatikutele tundus olevat loodusest peaaegu müstiline spekulatsioon. konstruktiivse mõttega, konstruktiivse matemaatika enda praktika kahjuks. See ebaõnnestunud polariseerumine brouwerlaste ja hilbertlaste vahel kulmineerus 1920. aastate kurikuulsas Grundlagenstreitis, mille üksikasju võib leida van Daleni [1999, 2005] ja van Stigti [1990] Brouweri elulugudes.

3.2 Rekursiivne konstruktiivne matemaatika

1940. aastate lõpus alustas vene matemaatik AA Markov konstruktiivse matemaatika (RUSS) alternatiivse vormi väljatöötamist, mis on sisuliselt intuitiivse loogikaga rekursiivne funktsiooniteooria (Markov [1954], Kushner [1985]). Selles sordis määratletakse objektid Gödeli nummerdamise abil ja protseduurid on kõik rekursiivsed; peamine erinevus RUSS-i ja pärast Turingi, Kiriku jt 1936. aastal välja töötatud klassikalise rekursiivse analüüsi vahel, mis täpsustas arvutatavate protsesside olemust, on see, et VENES kasutatav loogika on intuitiivne.

Üks takistus, millega matemaatik üritab RUSS-iga hakkama saada, on see, et kui seda väljendatakse rekursiooniteooria keeles, pole see kergesti loetav; Kushneri suurepäraste loengute [1985] lehe avamisel võib tõepoolest andeks anda, kui mõelda, kas see on analüüs või loogika. (See märkus peaks olema kahendatud, viidates kahele suhteliselt loetavale Aberthi klassikalise rekursiivse analüüsi raamatule [1980, 2001].) Õnneks võib Richmani [1983] tõttu aksiomaatilise lähenemise abil pääseda VENE südamesse (vt ka Bridges & Richmani 3. peatükk [1987]).

Esiteks määratleme hulga (S), mis loendataks juhul, kui (bN) eraldatavast alamhulgast on olemas kaardistus (S). Intuitsionistliku loogika abil ei saa me tõestada, et (bN) iga alamhulk on eemaldatav (lugejat kutsutakse üles näitama Brouwerian näidet). Richmani aksiomaatilises lähenemisviisis loetavad (bN) alamhulgad on RUSS-i normaalses arengus rekursiivselt loendatavate komplektide vastandid.

Osafunktsiooni abil saidil (bN) peame silmas kaardistamist, mille domeen on (bN) alamhulk; kui domeen on (bN) ise, siis kutsume funktsiooni täielikuks osaliseks funktsiooniks saidil (bN). Richmani lähenemine VEN-ile põhineb intuitsioonilisel loogikal ja arvutatavate osaliste funktsioonide (CPF) ühel aksioomil:

Kõigi osaliste funktsioonide hulgast vahemikus (bN) kuni (bN) on loendatud (phi_0, \ phi_1, \ ldots) loendatavate domeenidega.

On tähelepanuväärne, mida saab selle põhimõtte abil puhtalt ja kiiresti järeldada. Näiteks võime tõestada järgmist tulemust, mis näitab peaaegu kohe, et LLPO ja seega ka LPO on rekursiivses seadistuses valed.

On olemas täielik osaline funktsioon (f: \ bN \ korda \ bN \ paremnool {0,1 }), nii et

• iga (m) kohta on maksimaalselt üks (n), nii et (f (m, n) = 1); ja
• iga osalise funktsiooni (f: \ bN \ paremnool {0,1 }) jaoks on (m, k) (bN) olemas nii, et (f (m, 2k + f (m)) = 1).

Suuremat huvi pakuvad aga järgmised tulemused RUSSis.

• Speckeri teoreem (Specker [1949]): on olemas rangelt kasvav ratsionaalsete arvude jada ((r_1, r_2, \ ldots)) suletud intervallis ([0,1]) nii, et iga (x \ in \ bR) on olemas (N \ in \ bN) ja (delta \ gt 0) nii, et (abs {x - r_n} ge \ delta) kõigi (n \ ge N).
• Iga (varepsilon \ gt 0) jaoks on olemas jada ((I_1, I_2, \ ldots)), mille piiratud intervall on piiratud vahemikus (bR) selliselt, et) algab {joondama} silt {i} bR & \ subseteq \ bigcup_ {n = 1} ^ { infty} I_n, \ text {ja} \ \ tag {ii} sum_ {n = 1} ^ N \ abs {I_n} & \ lt \ varepsilon \ text {iga} N. \ end {joonda}) jaoks (sellist intervallijada nimetatakse (varepsilon) - (bR) ainsuse katteks.)
• On olemas pidev punktfunktsioon (f: [0,1] paremnool \ bR), mis pole ühtlaselt pidev.
• On olemas positiivselt hinnatud ühtlaselt pidev funktsioon (f: [0,1] paremnool \ bR), mille alammäär on 0.

Klassikalisest vaatevinklist sobivad need tulemused paika, kui mõistab, et selliseid sõnu nagu “funktsioon” ja “reaalarv” tuleks tõlgendada vastavalt kui “rekursiivset funktsiooni” ja “rekursiivset reaalarvu”. Pange tähele, et ülaltoodud neljast rekursiivsest teoreemist teine on tugev rekursiivne vastunäide (rekursiivse) rearea avatud katte kompaktsuse omadusele; ja neljas on klassikalise teoreemi rekursiivne vastanäide, et kompaktse komplekti iga ühtlaselt pidev kaardistamine (bR) saavutab oma madalaima.

3.3 Piiskopi konstruktiivne matemaatika

Kõigis konstruktiivse matemaatika variantides oli järgmise pooleteise kümnendi jooksul areng suhteliselt aeglane. Matemaatikas oli konstruktivismi profiili tõstmiseks vaja kõrgel kohal asuvat klassikalist matemaatikut, kes näitas, et süvaanalüüsi põhjalik konstruktiivne arendamine on võimalik ilma Brouweri mitteklassikaliste põhimõtete või rekursiivsete funktsioonide teooria pühendumiseta. See vajadus täitus 1967. aastal, kui ilmus Errett Bishopi monograafia „Constructive Analysis Foundations of 1968“, mis on hämmastava paariaastane toode, kus Bishop pakkus konstruktiivse arengu, töötades mitteametlikus, kuid ranges stiilis, mida tavapärased analüütikud kasutasid. suure osa kahekümnenda sajandi analüüsist, sealhulgas Stone-Weierstrassi teoreem, Hahn-Banachi ja eraldamise teoreemid,isemagnevate operaatorite spektriteoreem Hilberti ruumis, Lebesgue'i abstraktsete integraalide konvergentsiteoreemid, Haari mõõt ja abstraktsed Fourier-teisendused, ergodilised teoreemid ning Banachi algebra teooria elemendid. (Vt ka Bishop & Bridges [1985].) Nii andis ta löögi ajal vale üldlevinud arvamusele, mida Hilbert nii jõuliselt väljendas:

Matemaatikust väljajäetud keskpunkti põhimõtte võtmine oleks sama, kui öelda, et keelata teleskoobil astronoomile või poksijale kasutada tema rusikad. (Hilbert [1928])

Piiskopi matemaatika BISH-l polnud mitte ainult loetavuse eelis - kui avate Bishopi raamatu mis tahes lehel, on see, mida näete, selgelt analüüsina äratuntav, isegi kui aeg-ajalt võivad tema käigud tõendusmaterjali käigus tunduda kummalised üks koolitatud tõrjutud keskosa seaduse kasutamisest - kuid erinevalt intuitionistlikust või rekursiivsest matemaatikast tunnistab see paljusid erinevaid tõlgendusi. Intuitionistlik matemaatika, rekursiivne konstruktiivne matemaatika ja isegi klassikaline matemaatika pakuvad kõik BISH-i mudeleid. Tegelikult saab BISH-i tulemusi ja tõestusi tõlgendada, äärmisel juhul väiksemate muudatustega, ükskõik millises arvutatava matemaatika mõistlikus mudelis, näiteks Weihrauchi 2. tüüpi efektiivsusteoorias (Weihrauch [2000]; Bauer [2005]).

Kuidas see mitmekordne tõlgendatavus saavutatakse? Vähemalt osaliselt piiskopi keeldumise tõttu täpsustada oma primitiivset mõistet “algoritm” või tema sõnul “piiratud rutiin”. See keeldumine on viinud kriitikani, et tema lähenemisviisis puudub täpsus, mida loogik tavaliselt loodaks põhisüsteemilt. Sellest kriitikast saab siiski üle, kui uurida lähemalt, mida BISHi praktikud teoreemide tõestamisel tegelikult teevad: praktikas teevad nad intuitsioonilise loogikaga matemaatikat. Kogemused näitavad, et intuitsioonilise loogika juurde sundimine sunnib matemaatikuid alati töötama viisil, mida saab vähemalt mitteametlikult kirjeldada kui algoritmilist; nii et algoritmiline matemaatika näib olevat samaväärne matemaatikaga, mis kasutab ainult intuitionistlikku loogikat. Kui see nii on,siis saame praktiseerida konstruktiivset matemaatikat, kasutades intuitiivset loogikat mis tahes mõistlikult määratletud matemaatilistel objektidel, mitte ainult mingil „konstruktiivsete objektide” klassil.

Tundub, et selle arvamuse esitas enam-vähem Richman [1990, 1996]. Võttes loogikat konstruktiivse matemaatika peamise tunnusjoonena, ei kajasta see matemaatika ülimuslikkust loogika ees, mis oli osa Brouweri, Heytingi, Markovi, piiskopi ja teiste konstruktivismi pioneeride veendumustest. Teisest küljest kajastab see konstruktiivse matemaatika olemust praktikas.

Nii võib eristada Brouweri ontoloogilist konstruktivismi teistest, kes on juhitud konstruktiivse matemaatikani veendumuse kaudu, et matemaatilised objektid on mentaalne looming, ning Richmani epistemoloogilisest konstruktivismist nende vahel, kes näevad konstruktiivset matemaatikat, mida iseloomustab selle metoodika, põhinedes kasutamisel intuitsioonilisest loogikast. Muidugi viib endine lähenemine konstruktivismile paratamatult viimase juurde; ja viimane pole kindlasti vastuolus Brouweri ontoloogiaga.

Matemaatika tegemiseks vajame enamat kui ainult intutionistlikku loogikat. Bishopi jaoks olid matemaatika alustalad positiivsed täisarvud (vt Bishop'i tsitaati [1967] jaotises 3.1). BISH-i varasemate ametlike süsteemide hulgas olid Myhilli [1975] aksiomaatiline alus, mis põhines arvu, komplekti ja funktsiooni primitiivsetel ideedel; Fefermani [1975] selgesõnalise matemaatika süsteem; ja Friedmani [1977] intuitiivne ZF-i teooria. Kaks BISHi eelistatuimat ametlikku alust selles etapis on CZF-i teooria Aczel ja Rathjen [2000] ning Martin-Löfi intuitsioonistlik teooria [1975, 1984].

3.4 Martin-Löfi konstruktiivse tüübi teooria

Enne meie moodsa konstruktiivse matemaatika sortide ringkäigu lõpetamist külastame neljandat varianti, mis põhineb Per Martin-Löfi intuitsioonistlikul teoorial (ML). Martin-Löf avaldas oma märkused konstruktiivse matemaatika kohta [1968], tuginedes aastatel 1966–68 Euroopas peetud loengutele; nii et tema seotus konstruktivismiga matemaatikas ulatub tagasi vähemalt selle ajani, mil Bishop kirjutas konstruktiivse analüüsi alused. Martin-Löfi raamat on pigem VENE, mitte BISHi vaimus; tõepoolest, selle autoril ei olnud piiskopi raamatule juurdepääsu enne, kui tema enda käsikiri oli valmis. Hiljem pööras Martin-Löf tähelepanu Bishop-stiilis konstruktiivse matemaatika alusele oma tüüptõdedele.

Siin on tema enda sõnul ML-i aluseks olnud ideede mitteametlik selgitus:

Me mõtleme matemaatilistele objektidele või konstruktsioonidele. Iga matemaatiline objekt on teatud tüüpi või tüüpi [… ja] antakse alati koos selle tüübiga. … Tüüpi määratletakse kirjeldades, mida peame tegema seda tüüpi objekti konstrueerimiseks. … teisiti öeldes, tüüp on hästi määratletud, kui mõistame … mida tähendab olla seda tüüpi objekt. Nii on näiteks (bN \ parempoolne nool \ bN) [funktsioonid vahemikust (bN) kuni (bN)] tüüp, mitte sellepärast, et me teaksime teatud arvu teoreetilisi funktsioone, näiteks primitiivseid rekursiivseid, vaid sest arvame, et mõistame numbriteoreetilise funktsiooni mõistet üldiselt. (Martin-Löf [975])

Täpsemalt, selles süsteemis saab iga väidet esitada tüübina: nimelt väite tõendite tüüpi. Iga tüüp määrab vastupidi väite: nimelt väite, et kõnealune tüüp on asustatud. Nii et kui mõelda teatud tüüpi (T) kui väidet, tõlgendame seda valemit

[x \ T-s]

kuna “(x) on väite (T) tõend”.

Martin-Löf konstrueerib uut tüüpi tooteid, näiteks Cartesiuse tooteid ja lahtiühendatud ametiühinguid. Näiteks Cartesiuse toode

[(Pi x \ in A) B (x))

on funktsioonide tüüp, mis viivad tüübi (A) suvalise objekti (x) tüüpi objekti ((B (x))). Pakkumiste tõendusmaterjalide tõlgenduses, kus (B (x)) tähistab väidet, vastab ülaltoodud Desarteesi toode universaalsele väitele

[(Forall x \ A-s) B (x).)

Martin-Löf eristab hoolikalt tõestusi ja tuletisi: tõestusobjekt on tunnistajaks asjaolule, et mõni väide on tõestatud; arvestades, et tuletis on tõestatud objekti ehituse register. Samuti kasutab ta otsustusvõime kahte põhivormi (üks ei julge siin öelda "tüüpe"). Esimene on seos tõendusobjektide ja väidete vahel, teine on mõne väite omadus. Esimesel juhul on kohtuotsus selline, et tõendusobjekt (a) on ütluse tunnistaja (A), või teine, kui kaks tõendusobjekti (a) ja (b) on võrdsed ja mõlemad tunnistavad, et (A) on tõestatud. Teise kohtuotsuse vormi esimene juhtum väidab, et väide (A) on hästi vormistatud, ja teises on kirjas, et kaks väidet (A) ja (B) on võrdsed.

ML vormistamiseks on vaja hoolikat ja väga detailset reeglistikku. Me ei hakka siin käsitlema, vaid suuname lugeja teistesse allikatesse, näiteks Sambin & Smith [1998].

Tüüpteoorias konstruktiivset matemaatikat tehes tuleb sageli varustada täielikult esitatud komplektid (tüübid) ekvivalentsussidemega, kombinatsiooni tuntakse setoidina. Kaardistused on siis funktsioonid, mis austavad neid ekvivalentsussuhteid. See on tihedas kooskõlas sellega, kuidas piiskop esitas oma mitteametliku teooriate komplekti. Martin-Löfi sõltuvad tüübid on kasulikud alamhulkade konstrueerimiseks. Näiteks saab reaalarvude konstrueerimiseks kasutada (Sigma) tüüpi (vaata Martin-Löf [1984]):

[(Sigma x \ sisse \ bN _ + \ paremnool \ bQ) (Pi m \ sisse \ bN _ +) (Pi n \ sisse \ bN _ +) vasakule) abs {x_ {m} - x_ {n }} le \ vasak (frac {1} {m} + \ frac {1} {n} right) right],)

Seda tüüpi (B) element on seega paar, mis koosneb konvergentsest jadadest ((bx)) ratsionaalidest ja tõestusest ((p)), et see on ühtlustunud. Sobiva ekvivalentsuse seose ({ sim}) abil (R) määratletakse nii, et ((x, p) sim (y, q)) tähendaks

) jätkub m \ in \ bN_ + \ vasakul (abs {x_ {m} - y_ {m}} le \ frac {2} {m} paremal).)

Saadud reaalarvude setoid on (bR = (R, { sim})). Saame seda hõlpsalt tõestada

) kõik x \ sisse \ bR \, \ olemas n \ Z-s (n \ lt x \ lt n + 2))

ja seejärel, kasutades valitud tüübiteoreetilist aksioomi (vt allpool 4. osa), leidke funktsioon (f: \ bR \ parempoolne nool \ bZ) nii, et (f (x) lt x \ lt f (x) +2). Siiski pole põhjust arvata, et funktsioon (f) austab ekvivalentsussuhteid, see tähendab, et (f (x) = f (y)) kehtib juhul, kui (x \ sim y).

Iga konstruktiivne tõestus sisaldab algoritmi, mida põhimõtteliselt saab kaevandada ja arvutiprogrammina uuesti sõnastada; pealegi on konstruktiivne tõend iseenesest algoritmi õigsuse kontroll - st vastab spetsifikatsioonile. Martin-Löfi ametliku lähenemise konstruktiivsele matemaatikale eeliseks on see, et see hõlbustab oluliselt programmide väljavõtmist tõenditest. See on viinud tõsise tööni konstruktiivse matemaatika rakendamiseks erinevates kohtades (vt Martin-Löf [1980], Constable [1986], Hayashi & Nakano [1988], Schwichtenberg [2009]). Tõendite ekstraheerimiseks on tüübiteooria mõned hiljutised rakendused Coq ja Agda (vt linke jaotises Muud Interneti-ressursid).

4. Valiku aksioom

Valitud täieliku aksioomi saab öelda järgmiselt:

Kui (A, B) on asustatud komplektid ja (S) (A \ korda B) alamhulk, nii et

) kõik x \ A-s, \ eksisteerib y \ B-s ((x, y) S-s),)

siis on olemas valikufunktsioon (f: A \ paremnool B) nii, et

) forall x \ in A ((x, f (x)) S)).)

Kui see peaks toimuma konstruktiivse tõlgenduse all, siis antud (x \ tähes A) sõltub valikfunktsiooni väärtus (f (x)) mitte ainult (x), vaid ka andmete kohta, mis tõendavad, et (x) kuulub (A.). Üldiselt ei saa me eeldada, et see moodustab seda tüüpi valikufunktsiooni. BHK aksioomi hüpoteeside tõlgendus seisneb aga selles, et eksisteerib algoritm (matemaatiline {A}), mis rakendatakse mis tahes kindlale (x \ in A) ja tekitab elemendi (y \ in B) selline, et ((x, y) S-is). Kui (A) on täielikult esitatud komplekt, mille korral ei pea komplekti iga elemendi ehitamisest kaugemale jõudma, et tõestada, et element tõepoolest kuulub (A), siis võime algselt oodata algoritmi (matemaatiline {A}) olema valikfunktsioon. Martin-Löfi tüüpi teoorias on iga komplekt täielikult esitatud javastavalt BHK tõlgendusele on valitud aksioom tuletatav.

Teisest küljest on piiskopi stiilis matemaatikas täiesti esitatud ––– või tema terminoloogias põhi- ––– komplektid haruldased, üks näide on (bN); seega võime arvata, et valitud aksioom ei ole tuletatav. Tegelikult, nagu näitasid Diaconescu [1975] ja Goodman & Myhill [1978] ning mille Bishop oli ise kujundanud piiskopi 1967 ülesande 2 probleemil 2, tähendab valitud aksioom välistatud keskosa seadust. Diaconescu-Goodman-Myhilli teoreem kehtib ilmselgelt ainult eeldusel, et mitte kõik komplektid pole täielikult esitatud.

Konstruktiivsed matemaatikud, kes ei tööta ML-s, lükkavad tavaliselt tagasi kogu valitud aksioomi, kuid hõlmavad loendatava valiku aksioomi, kus valitud valdkond on (bN) ja sõltuv valik. Kuid mõned eelistavad töötada ilma loendamatute valikuteta põhjusel, et lõpmatutest valikutest rääkimine ilma reeglit andmata kujutab endast sama suurt raskust, olenemata sellest, kas lõpmatus on loetav või mitte. Huvitav on see, et Lebesgue juhtis just seda punkti Borelile saadetud kirjas (vt Moore [2013], lk 316):

Olen täiesti nõus Hadamardiga, kui ta väidab, et valikute lõpmatusest rääkimine ilma reeglit andmata kujutab endast sama suurt raskust, olenemata sellest, kas lõpmatus on loetav või mitte.

Isegi loendatavast valikust loobumisel on välistatud paljud teoreemid, mille praegune tõestus põhineb järjestikustel, valikupõhistel argumentidel. Kuid need, kes pooldavad valiku vältimist, väidavad, et valiku vältimine sunnib teid asju paremini sõnastama.

Eriline huvipakkuv juhtum on Algebra põhiteoreem: igal keerulisel polünoomil on komplekstasandil vähemalt üks juur. Richman [2000] on näidanud, et ilma loendatava valikuta, ehkki võime konstrueerida ainult isoleeritud (võib-olla mitu) juurt, võime juurte mitmele osale meelevaldselt lähedased lähenemised luua. Selline lähenemisviis keskendub polünoomi ligikaudse lineaarse faktoriseerimise leidmisele, selle asemel, et leida igale juurile eraldi lähendid.

Valitud aksioomi täiendavaks analüüsiks komplektiteoorias ja tüübiteoorias leiate Martin-Löfist [2006] ja kategooriateooria, tüübiteooria ja intuitionistliku tüüptiteooria SEP-kirjetest.

5. Konstruktiivne vastupidine matemaatika

1970ndatel algatas Harvey Friedman pöördtemaatika uurimisprogrammi, mille eesmärk oli klassifitseerida matemaatilisi teoreeme vastavalt nende ekvivalentsusele väheste hulga setteoreetiliste põhimõtetega (Friedman 1975). See klassifikatsioon näitab huvitavaid, mõnikord tähelepanuväärseid erinevusi tõestusteoreetilise keerukuse osas. Näiteks, kuigi Ascoli-Arzelà teoreemi kasutatakse Peano olemasolu teoreemi standardses tõestuses tavaliste diferentsiaalvõrrandite lahenduste jaoks (Hurewicz [1958], lk 10), näitab pöördtemaatikaanalüüs, et esimene on võrdne rangelt tugevamaga. set-teoreetiline printsiip kui see, mis on samaväärne Peano teoreemiga (Simpson [1984], teoreemid 3.9 ja 4.2). Klassikalise pöördtemaatika standard traktaat on (Simpson [1999/2009]).

Selle sajandi vahetuse paiku algatasid Veldman (vt Muud Interneti-ressursid) Hollandis ja Ishihara [2005, 2006] Jaapanis iseseisvalt konstruktiivse pöördmatemaatika (CRM) programmi, mis põhineb pigem intuitionistlikul kui klassikalisel, loogika. (Pange siiski tähele, et esimene avaldatud teos CRM-i tänapäevasel ajastul on tõenäoliselt Julian ja Richman (1984), kes oli oma ajast kakskümmend aastat ees.) Kirjeldame artikli selles osas vähem formaalset lähenemist CRM-ile BISHi stiilis ja raamistikus. Selle CRM-programmi eesmärk on klassifitseerida teoreemid kolme standardmudeli - CLASS, INT ja RUSS - järgi, mille põhimõtteid me peame ja peame ainult BISH-i lisama, et neid tõestada.

Rõhutame, et piirdume mitteametliku CRM-iga, milles peame iseenesestmõistetavaks funktsiooni ja komplekti ülesehituse põhimõtteid, mida on kirjeldatud Bishopi [1967] või Bishop & Bridges'i [1985] esimestes peatükkides, ning töötame mitteametliku, ehkki range praktiseerija analüütiku, algebraisti, topoloogi … stiil.

Praktikas jaguneb CRM loomulikult kaheks osaks. Neist esimeses kaalume INT või RUSS teoreemi (T) ja proovime leida mõnda põhimõtet, mis kehtiks selles mudelis ja mis pole (T) ise, mille lisamine BISH-i on vajalik ja piisav konstruktiivne tõend (T) kohta. CRM-i teises osas käsitleme CLASS-i teoreemi (T), mille kohta arvame, et see pole konstruktiivne, ja proovime tõestada, et (T) on BISH-i tähenduses samaväärne ühega paljudest teadaolevatest sisuliselt- mittekonstruktiivsed põhimõtted, näiteks MP, LLPO, LPO või LEM. CRM selle osa näitena mainime meie varasemat tõestust, et klassikaline madalaima ülaosa põhimõte tähendab ja on sellega samaväärne LEM-iga.

Muuseas, on olemas kindel argument, miks Brouwer [1921] on esimene, kes tegeleb vastupidiste matemaatiliste ideedega: tema Brouweri vastanäited (vt eespool punktis 1 Goldbachi oletust kasutavat näidet) asuvad CRM-i teises osas otse. Isegi kui Brouwer ei nimetanud neid näiteid loogiliste ekvivalentidena, vaid tüübi implikatsioonidena

[P \ parempoolne nool \ tekst {mõni mittekonstruktiivne põhimõte},)

on raske uskuda, et ta ei teadnud, et parempoolne tähendab sellistel juhtudel vasakut.

5.1 Fänniteoreemid CRM-is

CRM-i esimese osa illustreerimiseks keskendume nüüd tüübi teoreemidele

) text {BISH} vdash \ text {FT} _? \ Vasakpoolne nool T,)

kus FT (_?) on Brouweri fänniteoreemi vorm ja (T) on INT teoreem. Selleks peame eristama teatud tüüpi riba täieliku binaarse ventilaatori (2 ^ *) jaoks (kõigi lõplike jadade komplekt jaotises ({0,1 })).

Olgu (alpha \ equiv (alpha_1, \ alpha_2, \ ldots)) piiratud või lõpmatu binaarne jada. (Alpha) liitmine teise stringi (beeta)ga on

) alpha ^ { frown} beeta \ equiv (alpha_1, \ alpha_2, \ ldots, \ alpha_n, \ beta_1, \ ldots, \ beta_m).)

(B) jaoks ({0,1 }) kirjutame (alpha ^ { frown} b), mitte (alpha ^ { frown} (b)). (Mathsf {c}) - (2 ^ *) alamhulga all peame silmas (2 ^ *) alamhulki (B) nii, et

) silt {1} B = {u \ in 2 ^ *: \ forall v \ in 2 ^ * (u ^ { frown} v \ in D) })

mõne eemaldatava alamhulga (D) jaoks (2 ^ *). (2 ^ *) iga eraldatav alamhulk on (mathsf {c}) - alamhulk. Teisest küljest tähendame (Pi ^ {0} _1) - alamhulgaga (2 ^ *) allkomplekti (B) (2 ^ *), millel on järgmine omadus: on olemas eraldatav alamhulk (S) (2 ^ * \ korda \ bN) selliselt, et

) jätkub u \ 2 ^ * \, \ forall n \ in \ bN \, ((u, n) S \ Rightarrow'is (u ^ { frown} 0, n) S \ kiilus (u ^ { pahasti} 1, n) S-s)

ja

[B = {u \ in 2 ^ *: \ forall n \ in \ bN ((u, n) in S) }.)

Iga (mathsf {c}) - (2 ^ *) alamhulk (B) on (Pi ^ {0} _1) - alamhulk: võtke lihtsalt (S = D \ korda \ bN), kus (D) on (2 ^ *) eraldatav alamhulk, nii et (1) mahub.

Kui (?) Tähistab (2 ^ *) alamhulkade omadust, siis Brouweri fänniteoreem väärtuseks (?) - ribad ütleb meile, et iga omadusega (?) Riba on ühtlane riba. Eriti huvitab meid eemaldatavate vardade ventilaatori teoreem (seda on juba käsitletud jaotises 3.1):

FT (_ D): binaarse ventilaatori iga eemaldatav riba on ühtlane;

(mathsf {c}) - ribade (st ribade, mis on (mathsf {c}) - alamhulgad) fänniteoreem:

FT (_ { mathsf {c}}): täieliku binaarse ventilaatori iga c-riba on ühtlane;

ventilaatori teoreem (Pi ^ {0} _1) - ribadele (st ribadele, mis on (Pi ^ {0} _1) - alamhulgad):

FT (_ { Pi ^ {0} _1}): iga (Pi ^ {0} _1) - kogu binaarse ventilaatori riba on ühtlane;

ja täielik fänni teoreem:

FT: täieliku binaarse ventilaatori iga riba on ühtlane.

Pange tähele, et BISH-i suhtes

FT (Rightarrow) FT (_ { Pi ^ {0} _1} Rightarrow) FT (_ c \ Rightarrow) FT (_ D).

Lubarsky ja Diener [2014] on näidanud, et need mõjud on ranged.

Tavaliselt tahame tõestada, et FT (_?) Võrdub BISH-iga eeldusega, et iga sobivat sorti komplekti (S) jaoks on vormi teatav punktine omadus

) tag {2} forall x \ in S \ eksisteerib t \ TP (s, t))

hoiab vormis ühtlaselt

) tag {3} eksisteerib t \ T \ foorides s \ SP-s (s, t).)

Meie strateegia selle probleemi ründamiseks on kahetine. Esiteks, arvestades sobivat sorti komplekti (S), konstrueerime (2 ^ *) a-subseti (N) selliselt, et

• kui (2) on käes, siis (B) on tulp ja
• kui (B) on ühtlane riba, siis (3) kehtib.

See on siiski vaid pool lahendusest. Tõestamaks, et implikatsioon punktidest 3 kuni 2 tähendab FT (_?), Kaalume (2 ^ *) a-alamkomplekti (B) ja konstrueerime vastava hulga (S) selline, et

• kui (B) on riba, siis (2) hoiab ja
• kui (3) on käes, on (B) ühtlane riba.

Selliste tulemuste kanooniline näide on Julian ja Richman [1984], kus (S) on antud ühtlaselt pideva kaardistamise väärtuste kogum (f: [0,1] parempoolne nool \ bR, T) on positiivsete reaalarvude kogum ja

[P (s, t) ekvivalent (s \ ge t).)

Otsene omadus, mida me peame, on

) jätkub x \ jaotises [0,1] eksisteerib t \ gt 0 (f (x) ge t),)

selle ühtne versioon on

) eksisteerib 0 = f x kõik x \ kujul [0,1] (f (x) ge t).)

Julian-Richmani tulemused on järgmised.

Teoreem 1: Olgu (f: [0,1] paremnool \ bR) ühtlaselt pidev. Siis on olemas eraldatav alamhulk (B) (2 ^ *) selliselt, et

• kui (f (x) gt 0) iga (x \ väärtuses [0,1]), siis (B) on tulp ja
• kui (B) on ühtne riba, siis (inf f \ gt 0).

Teoreem 2: Olgu (B) (2 ^ *) eraldatav alamhulk. Siis eksisteerib ühtlaselt pidev (f: [0,1] paremnool \ bR) nii, et

• kui (B) on riba, siis (f (x) gt 0) iga (x [0,1]) -is ja
• kui inf (f \ gt 0), siis (B) on ühtne riba.

Nende kahe teoreemi tõestused on peened ja keerulised; vt Julian & Richman [1984].

Kaks Julian-Richmani teoreemi koos näitavad, et BISH-i suhtes on fänni teoreem FT (_ D) samaväärne positiivsuse põhimõttega POS:

Igal positiivse väärtusega, ühtlaselt pideval funktsioonil väärtusel ([0,1]) on positiivne miinimum.

Sellest järeldub, et POS on tuletatav INT-is, milles täielik fänniteoreem, mitte ainult FT (_ D), on standardpõhimõte. Venemaal on olukord vaikne, vastupidine, kus on olemas nii eemaldatav (2 ^ *) riba, mis pole ühtlane, kui ka positiivse väärtusega, ühtlaselt pidev funktsioon funktsioonil ([0,1]), millel on minimaalne võrdne 0-ga; vaata Bridges & Richmani [1987] 5. ja 6. peatükki.

Berger ja Ishihara [2005] on POS-i ja FT-i (_ c) ekvivalentsuse määramiseks võtnud erineva kaudse tee. Need loovad samaväärsuse ahela POS, FT (_ c) ja nelja tüüpi põhimõtte vahel: „kui on maksimaalselt üks omadusega objekt (P), siis on üks selline objekt”. Neli ainulaadse eksisteerimise põhimõtet on järgmised:

CIN!: Kompaktsse ja kõige rohkem ühe ühise punktiga mõõdiku ruumi asustatud suletud alamkomplektide igas kahanevas järjestuses on asustatud ristmikud (Cantori ristumisteoreem koos ainulaadsusega.) Pange tähele, et meetrilise ruumi alamhulk (S) ((X, \ rho)) asub juhul, kui (X) iga (x) jaoks on minimaalne kaugus vahemikust (x) kuni (S).

MINA!: Igal ühtlaselt pideval, reaalväärtusega funktsioonil kompaktses mõõdus ruumis, kus on vähemalt üks miinimumpunkt, on minimaalne punkt.

WKL! Igal lõpmatul puul, millel on maksimaalselt üks lõpmatu haru, on lõpmatu haru (nõrk Königi lemma, millel on ainulaadsus).

FIX!: Igal ühtlaselt pideval funktsioonil kompaktsest mõõdiku ruumist endas, millel on maksimaalselt üks fikseeritud punkt ja ligikaudsete fikseeritud punktidega fikseeritud punkt.

Näiteks viimases neist ütleme, et kaart (f) mõõdiku ruumi ((X, \ varrho)) enda sisse

• on maksimaalselt üks fikseeritud punkt, kui (varrho (f (x), x) + \ varrho (f (y), y) gt 0) alati (varrho (x, y) gt 0);
• on ligikaudsed fikseeritud punktid, kui iga (varepsilon \ gt 0) jaoks on olemas (x \ X-is), nii et (varrho (f (x), x) lt \ varepsilon).

CRM-i suureks avatud probleemiks on ventilaatori teoreemi sellise vormi leidmine, mis on BISH-i alusel samaväärne ([0,1]) ühetaolise järjepidevuse teoreemiga, UCT (_ {[0,1]}): iga ([0,1]) punktine pidev kaardistamine (bR) on ühtlaselt pidev, väide, mille jaoks Brouwer töötas algselt välja oma tõendi fänniteoreemi kohta. (Pange tähele, et UCT (_ {[0,1]}) võrdub BISH-iga meetriliste ruumide üldise ühtlase järjepidevuse teoreemiga: Tervikliku, täielikult piiritletud mõõdiku ruumi iga punktpidine pidev kaardistamine mõõdikute ruumis on ühtlaselt pidev. Vt näiteks Loeb [2005].)

Bergeri [2006] tulemustest järeldub, et

BISH (vdash) UCT (_ {[0,1]} paremnool) FT (_ c).

Ka Diener ja Loeb (2008) on seda tõestanud

BISH (vdash) FT (_ { Pi ^ {0} _1} Parempoolne) UCT (_ {[0,1]}).

Kuid me ei tea, kas kumbagi neist implikatsioonidest saab asendada bi-implikatsiooniga. Võib-olla on UCT (_ {[0,1]}) ja sellest tulenevalt kompaktsete meetriliste ruumide täielik ühtne pidevuse teoreem BISH-i suhtes samaväärne mõne fänni teoreemi loomuliku, kuid seni tuvastamata versiooniga.

Lisateavet ventilaatori teoreemi kohta konstruktiivses pöördmatemaatikas leiate näiteks Berger & Bridges [2007]; Diener [2008, 2012]; Diener & Loeb [2009]; ja Diener & Lubarsky [2014]. Dentis [2013] on olemas selge, kuigi keeruline skeem, mis illustreerib fänniteoreemide, järjepidevuse ja kõiketeadlikkuse põhimõtete omavahelisi seoseid (vt Muud Interneti-ressursid).

Huvitatud lugejad võivad konstruktiivse vastupidise matemaatika teemat käsitleda üksikasjalikumalt järgmises lisadokumendis:

Ishihara põhimõte (BDN) ja spektervastane omadus

6. Konstruktiivne algebra ja topoloogia

Konstruktiivsed matemaatikud on kaldunud koondama oma jõupingutused analüüsi valdkonnale, saavutades märkimisväärset edu Bishopis [1967] välja töötatud funktsionaalse analüüsi rikkuse osas. See ei tähenda, et näiteks algebra oleks konstruktiivsest ettevõttest kõrvale jäetud: Mines'i jt [1986] monograafias sisalduvat materjali võib pidada oluliseks algebraliseks vasteks Bishop'i tehtud konstruktiivsele analüüsile. Hilisemal ajal on Lombardi ja Quitté [2011] avaldanud konstruktiivse algebrani kohta kavandatud kaheköitelise töö esimese suurema osa. Kuna me ei ole algebrani asjatundjad ja oleme teadlikud ohtust, et see artikkel võib olla liiga pikk lugeja tähelepanu hoidmiseks, otsustame konstruktiivse analüüsi või algebrani mitte mingisuguse detaili arutada; pigem järgmises lisadokumendispöördume konstruktiivse topoloogia poole, kirjeldades mõnda üsna erinevat lähenemisviisi antud teemal:

Lähenemisviisid konstruktiivsele topoloogiale

7. Konstruktiivne matemaatiline majandus ja rahandus

Konstruktiivse matemaatikaökonoomika uuringud pärinevad eelistuste, kasulikkuse ja nõudluse dokumentide seeriast alates 1982. aastast; vt Bridges [1999]. Hendtlass [2013] nõrgendas oma doktoritöös oluliselt nõudmisfunktsiooni olemasolu tingimusi; ta andis ka hulga tulemusi fikseeritud punkti teoorias ja selle rakendustes, eriti majandusliku tasakaalu olemasolu kahe klassikalise tõendi konstruktivisatsioonides.

2015. aastal alustasid Berger ja Svindland Münchenis Ludwig-Maximilians-Universitätis konstruktiivse matemaatilise rahanduse uurimisprojekti. Nad näitasid kõigepealt, et varade hinnakujunduse põhiteoreem, eraldav hüpertasanditeoreem ja Markovi põhimõte on konstruktiivselt ekvivalentsed (Berger & Svindland [2016]). Nende hilisemas töös on keskendutud sellele, kuidas klassikalise äärmusliku väärtuse teoreemi mittekonstruktiivsusest mööda hiilida, et tõestada funktsioonide äärmuslike punktide olemasolu isegi suhteliselt nõrkade kumerusomaduste korral (Berger & Svindland [2016a]). Nende projekt viitab sellele, et matemaatiline rahandus, nagu ka matemaatiline ökonoomika, võib olla rikas elegantsete, praktiliste konstruktiivsete teoreemide allikas.

8. Lõppmärkused

Matemaatikute konstruktiivset sisu analüüsida soovivate matemaatikute traditsiooniline suund on klassikalist loogikat järgiv; vältimaks otsuseid, näiteks seda, kas reaalarv on 0 või mitte, mida päris arvuti ei saa teha, peab matemaatik hoidma rangetes algoritmilistes piirides, nagu need, mis on moodustatud rekursiivse funktsiooni teooria abil. Konstruktiivse matemaatiku valitud marsruut järgib seevastu intuitiivset loogikat, mis hoolitseb automaatselt arvutuslikult vastuvõetamatu otsuse eest. Sellest loogikast (koos sobiva komplekti või tüübiteoreetilise raamistikuga) piisab, et hoida matemaatika konstruktiivsetes piirides. Seega on matemaatikul vabadus töötada analüütiku, algebraisti (nt Mines jt [1988]), geomeetri, topoloogi (nt Bridges & Natural) loomulikus stiilis. Vîță [2011], Sambini tulekul) või mõni muu tavaline matemaatik, ainsateks piiranguteks on intuitiivse loogikaga seatud piirangud. Nagu piiskop ja teised on näidanud, on Hilberti välja kuulutatud ja tänapäevalgi laialt levinud traditsiooniline usk, et intuitsiooniline loogika seab sellised piirangud, mis muudavad tõsise matemaatika arendamise võimatuks, ilmselgelt vale: suur osa kaasaegsest sügavast matemaatikast võib olla ja on on toodetud puhtalt konstruktiivsete meetoditega. Lisaks on konstruktiivse matemaatika ja programmeerimise vahelise seose jaoks abstraktse matemaatika edaspidiseks rakendamiseks ja arendamiseks arvutis suur lubadus. Hilberti välja kuulutatud ja tänapäevalgi laialt levinud traditsiooniline uskumus, et intuitsiooniline loogika seab sellised piirangud, mis muudavad tõsise matemaatika arengu võimatuks, on ilmselgelt vale: suur osa modernsest sügavast matemaatikast võib olla ja on toodetud puhtalt konstruktiivsete meetoditega. Lisaks on konstruktiivse matemaatika ja programmeerimise vahelise seose jaoks abstraktse matemaatika edaspidiseks rakendamiseks ja arendamiseks arvutis suur lubadus. Hilberti välja kuulutatud ja tänapäevalgi laialt levinud traditsiooniline uskumus, et intuitsiooniline loogika seab sellised piirangud, mis muudavad tõsise matemaatika arengu võimatuks, on ilmselgelt vale: suur osa modernsest sügavast matemaatikast võib olla ja on toodetud puhtalt konstruktiivsete meetoditega. Lisaks on konstruktiivse matemaatika ja programmeerimise vahelise seose jaoks abstraktse matemaatika edaspidiseks rakendamiseks ja arendamiseks arvutis suur lubadus.seos konstruktiivse matemaatika ja programmeerimise vahel on abstraktse matemaatika edaspidiseks rakendamiseks ja arendamiseks arvutis suur lubadus.seos konstruktiivse matemaatika ja programmeerimise vahel on abstraktse matemaatika edaspidiseks rakendamiseks ja arendamiseks arvutis suur lubadus.

Bibliograafia

Viited

• Aberth, O., 1980, arvutatav analüüs, New York: McGraw-Hill.
• –––, 2001, arvutatav arvutus, New York: Academic Press.
• Aczel, P. ja Rathjen, M., 2001, Märkused konstruktiivse komplekti teooria kohta (aruanne nr 40), Stockholm: Institut Mittag-Leffler, Rootsi Kuninglik Teaduste Akadeemia.
• Bauer, A., 2005, “Teostatavus kui seos arvutatava ja konstruktiivse matemaatika vahel”, loengu märkused juhendaja jaoks CCA2005 satelliidiseminaril, Kyoto, Jaapan [saadaval veebis].
• Beeson, M., 1985, Konstruktiivse matemaatika alused, Heidelberg: Springer Verlag.
• Berger, J., 2006, “Ühtse järjepidevuse teoreemi loogiline tugevus”, loogilistes lähenemisviisides arvutuslikele tõketele, A. Beckmann, U. Berger, B. Löwe ja JV Tucker (toim), Heidelberg: Springer Verlag.
• Berger, J. ja Bridges, DS, 2007, “Speckeri teoreemi antiteesi fänniteoreetiline ekvivalent”, Madalmaade Kuningliku Matemaatika Seltsi Toimetised (Indagationes Mathematicae) (Indag. Math. NS), 18 (2): 195 –202.
• –––, 2009, „Ventilaatori teoreem ja positiivse väärtusega ühtlaselt pidevad funktsioonid kompaktse intervalliga”, New Zealand Journal of Mathematics, 38: 129–135.
• Berger, J. ja Ishihara, H., 2005, “Brouweri fänniteoreem ja ainulaadne eksisteerimine konstruktiivses analüüsis”, Matemaatiline loogika kvartal, 51 (4): 360–364.
• Berger, J. ja Schuster, PM, 2006, “Dini teoreemi klassifitseerimine”, Notre Dame Journal of Formal Logic, 47: 253–262.
• Berger, J. ja Svindland, G., 2016, “Eraldav hüpertasandiline teoreem, varade hinnakujunduse põhiteoreem ja Markovi põhimõte”, Annals of Pure and Applied Logic, 167, 1161–1170.
• –––, 2016a, “Kumerus ja konstruktiivne infima”, Matemaatilise loogika arhiiv, 55: 873–881
• Bishop, E., 1967, Konstruktiivse analüüsi alused, New York: McGraw-Hill.
• –––, 1973, skisofreenia kaasaegses matemaatikas (Ameerika matemaatika seltsi kollokviumi loengud), Missoula: Montana ülikool; kordustrükk Errett Bishopis: Refleksioonid temast ja tema uurimistööst, Ameerika Matemaatika Seltsi memuaarid 39.
• Bishop, E. ja Bridges, D., 1985, Konstruktiivne analüüs (Grundlehren der mateischen Wissenschaften, 279), Heidelberg: Springer Verlag.
• Bourbaki, N., 1984, Éléments d'histoire des mathématiques, Pariis: Masson; Ingliskeelne väljaanne, Matemaatika ajaloo elemendid, J. Meldrum (tõlge), 2006, Berliin: Springer Verlag.
• Bridges, DS, 1999, “Konstruktiivsed meetodid matemaatilises majanduses”, Zeitschrift für Nationalökonomie (täiendus), 8: 1–21.
• Bridges, DS ja Diener, H., 2007, “[0, 1] pseudokompaktilisus on võrdne pideva järjepidevuse teoreemiga”, Journal of Symbolic Logic, 72 (4): 1379–1383.
• Bridges, DS, ja Richman, F., 1987, Konstruktiivse matemaatika variatsioonid, Londoni matemaatikaühingu loengumärkused 97, Cambridge: Cambridge University Press.
• Bridges, DS ja Vîță, LS, 2006, Konstruktiivse analüüsi tehnikad, Heidelberg: Springer Verlag.
• –––, 2011, Apartents ja ühtsus - konstruktiivne areng, Heidelberg: Springer Verlag
• Brouwer, LEJ, 1907, Over de Grondslagen der Wiskunde, doktoritöö, Amsterdami ülikool; koos lisamaterjaliga uuesti trükitud, D. van Dalen (toim), autor Matematisch Centrum, Amsterdam, 1981.
• –––, 1908, “De onbetrouwbaarheid der logische principes”, Tijdschrift voor Wijsbegeerte, 2: 152–158.
• –––, 1921, “Besitzt jede reelle Zahl eine Dezimalbruchentwicklung?”, Mathematische Annalen, 83: 201–210.
• –––, 1924, “Beweis, dass jede volle Funktion gleichmässig stetig ist”, Proceedings of Royal Holland Mathematical Society, 27: 189–193.
• –––, 1924A, “Bemerkung zum Beweise der Gleichmässigen Stetigkeit voller Funktionen”, Proceedings of Royal Holland Mathematical Society, 27: 644–646.
• Cederquist, J. ja Negri, S., 1996, “Heine-Boreli konstruktiivne tõend, mis katab formaalsete reaalainete teoreemi” tõendite ja programmide tüüpides (Lecture Notes in Computer Science, köide 1158), 62–75, Berliin: Springer Verlag.
• Constable, R., et al., 1986, Matemaatika rakendamine Nuprl-tõestussüsteemiga, Englewood Cliffs, NJ: Prentice-Hall.
• Coquand, T., 1992, “Tychonoffi teoreemi intuitiivne tõestus”, Journal of Symbolic Logic, 57: 28–32.
• –––, 2009, „Väärtuste ruum”, Annals of Pure and Applied Logic, 157: 97–109.
• –––, 2016, “Tüüpide teooria”, Stanfordi filosoofia entsüklopeedia (2016. aasta talve väljaanne), Edward N. Zalta (toim.), URL (= \ lt) https://plato.stanford.edu/entries/ tüübiteooria / (gt)
• Coquand, T. ja Spitters, B., 2009, “Integrals and Valuations”, Journal of Logic and Analysis, 1 (3): 1–22.
• Coquand, T., Sambin, G., Smith, J. ja Valentini, S., 2003, “Induktiivselt genereeritud formaalsed topoloogiad”, Annals of Pure and Applied Logic, 124: 71–106.
• Curi, G., 2010, “Stone-Čechi tihendamise olemasolust”, Journal of Symbolic Logic, 75: 1137–1146.
• Dent, JE, 2013, Specker-vastased omadused konstruktiivses pöördtemaatikas, Ph. D. lõputöö, Canterbury ülikool, Christchurch, Uus-Meremaa.
• Diaconescu, R., 1975, “Valitud ja täiendav aksioom”, Proceedings of the American Mathematical Society, 51: 176–178
• Diener, H., 2008, Kompaktsus konstruktiivse kontrolli all, Ph. D. lõputöö, Christchurch, Uus-Meremaa: Canterbury ülikool.
• –––, 2008a, “Üldistav kompaktsus”, matemaatiline loogika kvartal, 51 (1): 49–57.
• –––, 2012, “Spekeri teoreemi antiteesi ümberklassifitseerimine”, Matemaatilise loogika arhiiv, 51: 687–693.
• Diener, H. ja Loeb, I., 2009, “Reaalsete funktsioonide jadad [0, 1] konstruktiivses pöördtemaatikas”, Annals of Pure and Applied Logic, 157 (1): 50–61.
• Diener, H. ja Lubarsky, R., 2013, “Fänniteoreemi ja selle nõrkade külgede eraldamine”, arvutiteaduse loogilistes alustes (Lecture Notes in Computer Science, 7734), S. Artemov ja A. Nerode (toim)., Berliin: Springer Verlag.
• Dummett, Michael, 1977 [2000], Intuitsionismi elemendid (Oxford Logic Guides, 39), Oxford: Clarendon Press, 1977; 2. väljaanne, 2000. [Lehekülje viited on 2. väljaandele.]
• Ewald, W., 1996, Kantist Hilbertini: Allikaraamat matemaatika alustes (2. köide), Oxford: Clarendon Press.
• Feferman, S, 1975, “Keel ja eksisteeriva matemaatika aksioomid”, Algebra ja Logit, JN Crossley (toim), Heidelberg: Springer Verlag, lk 87–139.
• –––, 1979, „Funktsioonide ja klasside konstruktiivsed teooriad”, loogikakollokviumis '78, M. Boffa, D. van Dalen ja K. McAloon (toim.), Amsterdam: Põhja-Holland, lk 159–224.
• Friedman, H., 1975, “Mõned teise astme aritmeetika süsteemid ja nende kasutamine”, 17. rahvusvahelise matemaatikute kongressi toimetus, Vancouver, BC, 1974.
• –––, 1977, “Konstruktiivse analüüsi teoreetiliste aluste seadmine”, Annals of Mathematics, 105 (1): 1–28.
• Goodman, ND, ja Myhill, J., 1978, “Valik tähendab välistatud keskosa”, Zeitschrift für Logik ja Grundlagen der Mathematik, 24: 461.
• Hayashi, S. ja Nakano, H., 1988, PX: Computational Logic, Cambridge, MA: MIT Press.
• Hendtlass, M., 2013, Fikseeritud punktide ja majandusliku tasakaalu ehitamine, Ph. D. lõputöö, Leedsi ülikool.
• Heyting, A., 1930, “Die formalen Regeln der intuitionistischen Logik”, Sitzungsberichte der Preussische Akadademie der Wissenschaften. Berliin, 42–56.
• –––, 1971, Intuitsionism - sissejuhatus, 3. trükk, Amsterdam: Põhja-Holland.
• Hilbert, D., 1925, “Über das Unendliche”, Mathematische Annalen, 95: 161–190; tõlge “On lõpmatu”, autorid E. Putnam ja G. Massey, matemaatikafilosoofias: valitud lugemised, P. Benacerraf ja H. Putnam (toim.), Englewood Cliffs, NJ: Prentice Hall, 1964, 134–151.
• Hurewicz, W., 1958, Loengud tavalistest diferentsiaalvõrranditest, Cambridge, MA: MIT Press.
• Ishihara, H., 1992, “Järjepidevuse omadused konstruktiivses matemaatikas”, Journal of Symbolic Logic, 57 (2): 557–565.
• –––, 1994, “Banachi pöördvõrdelise kaardistamise teoreemi konstruktiivne versioon”, New Zealand Journal of Mathematics, 23: 71–75.
• –––, 2005, „Konstruktiivne vastupidine matemaatika: kompaktsusomadused“, komplektidest ja tüüpidest analüüsi ja topoloogiani: konstruktiivse matemaatika praktiliste aluste poole: L. Crosilla ja P. Schuster (toim), Oxford: The Clarendon Press.
• –––, 2006, “Pöördmatemaatika Bishopi konstruktiivses matemaatikas”, Philosophia Scientiae (Cahier Special), 6: 43–59.
• ––– 2013, „Piiskopi funktsiooniruumide seostamine naabrusruumidega“, Annals of Pure and Applied Logic, 164: 482–490.
• Johnstone, PT, 1982, Stone Spaces, Cambridge: Cambridge University Press.
• ––– 2003, „Mõttetu topoloogia mõte“, Ameerika Matemaatika Seltsi bülletään, 8: 41–53.
• Joyal, A. ja Tierney, M., 1984, “Grothendiecki Galoisi teooria laiendus”, Ameerika Matemaatika Seltsi memuaarid, 309: 85 lk.
• Julian, WH ja Richman, F., 1984, „Ühtlaselt pidev funktsioon funktsioonil [0, 1], mis erineb kõikjal oma alammäärast”, Pacific Journal of Mathematics, 111: 333–340.
• Kushner, B., 1985, Konstruktiivse matemaatilise analüüsi loengud, Providence, RI: American Mathematical Society
• Lietz, P., 2004, alates konstruktiivsest matemaatikast kuni arvutatava analüüsini realiseeritavuse tõlgendamise kaudu, dr rer. nat. väitekiri, Universität Darmstadt, Saksamaa.
• Lietz, P. ja Streicher, T., „Realiseeritavusmudelid, mis lükkavad ümber Ishihara piiritlemise põhimõtte“, Annals of Pure and Applied Logic, 163 (12): 1803–1807.
• Loeb, I., 2005, “(Nõrga) fänniteoreemi ekvivalendid”, Annals of Puhas ja rakendatud loogika, 132: 51–66.
• Lombardi, H., Quitté, C., 2011, Algèbre Commutative. Metoodikad konstruktiivsed, Nanterre, Prantsusmaa: Calvage et Mounet.
• Lorenzen, P., 1955, Einführung in die operative Logik und Mathematik (Grundlehren der mateischen Wissenschaften, 78. köide), 2. trükk, 1969, Heidelberg: Springer.
• Lubarsky, R. ja Diener, H., 2014, “Fänni teoreemi eraldamine ja selle nõrgenemised”, Journal of Symbolic Logic, 79 (3): 792–813.
• Markov, AA, 1954, algoritmide teooria, Trudy Mat. Istituta imeni VA Steklova, 42, Moskva: Izdatel'stvo Akademii Nauk SSSR.
• Marquis, J.-P., “Kategooria teooria”, Stanfordi filosoofia entsüklopeedia (2015. aasta talve väljaanne), Edward N. Zalta (toim.), URL (= \ lt) https://plato.stanford.edu / arhiivid / win2015 / kirjed / kategooriateooria / (gt).
• Martin-Löf, P., 1968, Märkused konstruktiivse analüüsi kohta, Stockholm: Almquist ja Wiksell.
• –––, 1975, „Tüüpide intuitiivne teooria: predikatiivne osa”, Logic Colloquium 1973, HE Rose ja JC Shepherdson (toim), Amsterdam: Põhja-Holland.
• –––, 1980, “Konstruktiivne matemaatika ja arvutiprogrammeerimine”, Proc. 6. Int. Loogika, metodoloogia ja teadusfilosoofia kongress, L. Jonathan Cohen (toim), Amsterdam: Põhja-Holland.
• –––, 1984, intuitsioonistüübi teooria, Giovanni Sambini märkused Padovas, juunis 1980, Napolis peetud loengusarjast: Bibliopolis.
• ––– 2006, „100 aastat valitud Zermelo aksioomist: milles sellega probleeme oli?”, Computer Journal, 49 (3): 345–350.
• Menger, K., 1940, “Punktideta topoloogia”, Rice Institute Pamphlet, 27 (1): 80–107 [saadaval veebis].
• Mines, R., Richman, F., ja Ruitenburg, W., 1988, Konstruktiivse algebra kursus, Universitext, Heidelberg: Springer Verlag.
• Moerdijk, I., 1984, “Heine-Borel ei tähenda fänniteoreemi”, Journal of Symbolic Logic, 49 (2): 514–519.
• Moore, GH, 2013, Zermelo valiku aksioom: selle päritolu, areng ja mõju, New York: Dover.
• Myhill, J., 1973, “Intuitionistliku Zermelo-Fraenkeli komplekti teooria mõned omadused”, Cambridge'i matemaatikaloogika suvekoolis, A. Mathias ja H. Rogers (toim), Matemaatika loengumärkused, 337, Heidelberg: Springer Verlag, 206-231.
• –––, 1975, “Konstruktiivne komplektiteooria”, Journal of Symbolic Logic, 40 (3): 347–382.
• Naimpally, S., 2009, Läheduslähenemine topoloogia ja analüüsi probleemidele, München: Oldenbourg Verlag.
• Naimpally, S. ja Warrack, BD, 1970, lähedusruumid (Cambridge Tracts in Math. And Math. Phys., Köide 59), Cambridge: Cambridge University Press.
• Nordström, B., Peterson, K. ja Smith, JM, 1990, “Programmeerimine Martin-Löfi tüüpi teoorias”, Oxford: Oxford University Press.
• Palmgren, E., 2007, “Kohati kompaktsete meetriliste ruumide konstruktiivne ja funktsionaalne manustamine lokaalideks”, Topoloogia ja selle rakendused, 154: 1854–1880.
• –––, 2008, „Ühtse alumise piiri lahendamine konstruktiivses analüüsis“, Matemaatiline loogika kvartal, 54: 65–69.
• –––, 2009, „Intuvistilisest formaalse topoloogiani: mõned märkused homotoopia teooria aluste kohta”, ajakirjas: Logicism, intuitionism ja formalism - mis neist on saanud?, S. Lindström, E. Palmgren, K. Segerberg ja V. Stoltenberg-Hansen (toim.), 237–253, Berliin: Springer Verlag.
• Petrakis, I., 2016, “Konstruktiivne funktsiooniteoreetiline lähenemine topoloogilisele kompaktsusele”, loogikameetodites arvutiteaduses 2016, IEEE Computer Society Publications: 605–614.
• –––, 2016a, „Urysohni laiendusteoreem piiskopiruumidele“, S. Artemov ja A. Nerode (toim), Arvutiteaduse loogiliste aluste sümpoosion 2016 (arvutiteaduse loengumärkused 9537), Berliin: Springer Verlag, 299–316.
• Picado, J. ja Pultr, A., 2011, Raamid ja kohad: punktideta topoloogia, Basel: Birkhäuser Verlag.
• Richman, F., 1983, “Kiriku väitekiri ilma pisarateta”, Journal of Symbolic Logic, 48: 797–803.
• –––, 1990, “Intuitsionism kui üldistus”, Philosophia Mathematica, 5: 124–128.
• –––, 1996, “Intervjuu konstruktiivse matemaatikuga”, Modern Logic, 6: 247–271.
• ––– 2000, “Algebra põhiteoreem: konstruktiivne käsitlus ilma valikuta”, Pacific Journal of Mathematics, 196: 213–230.
• Riesz, F., 1908, “Stetigkeitsbegriff und abstrakte Mengenlehre”, Atti IV Congresso Internationale Matematica Roma II, 18–24.
• Sambin, G., 1987, “Intuitionistlikud formaalsed ruumid - esimene suhtlus”, ajakirjas Mathematical Logic and selle Applications, D. Skordev (toim.), 187–204, New York: Plenum Press.
• –––, tulemas, Põhipilt: konstruktiivse topoloogia struktuurid, Oxford: Oxford University Press.
• Sambin, G. ja Smith, J. (toim.), 1998, Kakskümmend viis aastat konstruktiivse tüübi teooriat, Oxford: Clarendon Press.
• Schuster, PM, 2005, “Mis on konstruktiivne järjepidevus?”, Ajakiri Universal Computer Science, 11: 2076–2085
• –––, 2006, “Formaalne Zariski topoloogia: positiivsus ja punktid”, Annals of Pure and Applied Logic, 137: 317–359.
• Schwichtenberg, H., 2009, “Programmide ekstraheerimine konstruktiivses analüüsis”, logismis, intuitsioonis ja formalismis - mis neist on saanud?, S. Lindström, E. Palmgren, K. Segerberg ja V. Stoltenberg-Hansen (toim), Berliin: Springer Verlag, 255–275.
• Simpson, SG, 1984, “Milliseid eksisteerimise aksioome on vaja tavaliste diferentsiaalvõrrandite Cauchy / Peano teoreemi tõestamiseks”, Journal of Symbolic Logic, 49 (3): 783–802.
• –––, 2009, teise järgu aritmeetika alamsüsteemid, teine trükk, Cambridge: Cambridge University Press.
• Specker, E., 1949, “Nicht konstruktiv beweisbare Sätze der Analysis”, Journal of Symbolic Logic, 14: 145–158.
• Steinke, TA, 2011, Konstruktiivsed arusaamad eraldusruumide kompaktsusest, M. Sc. Lõputöö, Canterbury ülikool, Christchurch, Uus-Meremaa.
• Troelstra, AS, 1978, “Konstruktiivse matemaatika aspektid”, Matemaatilise loogika käsiraamat, J. Barwise (toim), Amsterdam: Põhja-Holland.
• Troelstra, AS, ja van Dalen, D., 1988, konstruktivism matemaatikas: sissejuhatus (kaks köidet), Amsterdam: Põhja-Holland.
• van Atten, M., 2004, Brouwer, Belmont: Wadsworth / Thomson Learning.
• van Dalen, D., 1981, Brouweri Cambridge'i loengud intuitsiooni kohta, Cambridge: Cambridge University Press.
• –––, 1999, müstik, geomeeter ja intuitsioonikunstnik: LEJ Brouweri elu (1. köide), Oxford: Clarendon Press.
• –––, 2005, müstik, geomeeter ja intuitsioonikunstnik: LEJ Brouweri elu (2. köide), Oxford: Clarendon Press.
• van Stigt, WP, 1990, Brouweri intuitsioon, Amsterdam: Põhja-Holland.
• Vickers, S., 2005, “Üldistatud meetriliste ruumide lokaalne valmimine I”, kategooriate teooria ja rakendused, 14 (15): 328–356.
• Waaldijk, F., 2005, Konstruktiivse matemaatika alustest, Science Sciences, 10 (3): 249–324.
• Wallman, H., 1938, “Topoloogiliste ruumide võred”, Annals of Mathematics, 39: 112–126.
• Weihrauch, K., 2000, arvutatav analüüs (EATCSi tekstid arvutiteoreetilises teoorias), Heidelberg: Springer Verlag.
• Weyl, H., 1946, “Matemaatika ja loogika”, American Mathematical Monthly, 53 (1): 2–13.
• Whitehead, AN, 1919, uurimus looduslike teadmiste põhimõtete kohta, Cambridge: Cambridge University Press, teine trükk, 1925.

Seotud kirjandus

• Heijenoort, Jean van, 1967, Fregest Gödelini: matemaatikaloogika lähteteos 1879–1931, Cambridge, MA: Harvard University Press.
• Hilbert, David, 1928, “Die Grundlagen der Mathematik”, Hamburger Mathematische Einzelschriften 5, Teubner, Leipzig. Ingliskeelse tõlke kordustrükk van Heijenoortis 1967.

Akadeemilised tööriistad

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

Muud Interneti-ressursid

• Agda Wiki, tipitud funktsionaalne programmeerimiskeel ja tõestusassistent, Göteborgi ülikool ja Chalmersi tehnikaülikool.
• Agda, kanne Vikipeediasse.
• Coq Proof Assistant, Inria, 1984-2017.
• Coq, kanne Vikipeediasse.
• James Denti skeem.
• Aczel, P. ja Rathjen, M., 2018, konstruktiivse komplekti teooria, veebipõhine PDF.
• Bauer, A., 2005, “Realiseeritavus kui seos arvutatava ja konstruktiivse matemaatika vahel”.
• Veldman, W., 2014, “Brouweri fänniteoreem kui aksioom ja kontrastiks Kleene'i alternatiivile”, arxiv: 1106.2738https://arxiv.org/abs/1106.2738.