Konstruktivna Matematika

Kazalo:

Konstruktivna Matematika
Konstruktivna Matematika

Video: Konstruktivna Matematika

Video: Konstruktivna Matematika
Video: А. Марков. О логике конструктивной математики 2024, Marec
Anonim

Vstopna navigacija

  • Vsebina vpisa
  • Bibliografija
  • Akademska orodja
  • Prijatelji PDF predogled
  • Informacije o avtorju in citiranju
  • Nazaj na vrh

Konstruktivna matematika

Prvič objavljeno, 18. novembra 1997; vsebinska revizija sreda, 30. maja 2018

Konstruktivno matematiko od tradicionalnega kolega, klasične matematike, razlikuje po strogi razlagi besedne zveze "obstaja" kot "lahko konstruiramo". Da bi konstruktivno delovali, moramo ponovno interpretirati ne le eksistencialni kvantifikator, ampak tudi vse logične vezi in kvantifikatorje kot navodila, kako sestaviti dokaz trditve, ki vključuje te logične izraze.

V tem članku predstavljamo sodobno konstruktivno matematiko, ki temelji na BHK-interpretaciji logičnih konektiv in kvantifikatorjev. Govorimo o štirih glavnih sortah konstruktivne matematike, s posebnim poudarkom na dveh sortah, povezanih z Errettom Bishopom in Per Martinom-Löfom, ki jih je mogoče šteti za minimalne konstruktivne sisteme. Nato smo orisali napredek v (neformalni) konstruktivni obratni matematiki, raziskovalnem programu, ki si prizadeva določiti načela, kot je Brouwerjev izrek o oboževalcih, ki poleg minimalnih konstruktivnih sort olajšajo dokazovanje pomembnih analitičnih izrek. Po kratki razpravi o konstruktivni algebri, ekonomiji in financah se vnos zaključi z dvema prilogama: ena o določenih logičnih načelih klasične, intuicijistične in rekurzivne matematike in ki jih je dodal Bishop 's konstruktivno matematiko, olajšati dokazovanje nekaterih uporabnih teoremov analize; in eden razpravlja o pristopih k konstruktivnemu razvoju splošne topologije.

  • 1. Uvod
  • 2. Konstruktivna interpretacija logike
  • 3. Sorte konstruktivne matematike

    • 3.1 Intuitionistična matematika
    • 3.2 Rekurzivna konstruktivna matematika
    • 3.3 Škofova konstruktivna matematika
    • 3.4 Martino-Löfova konstruktivna teorija tipa
  • 4. Aksiom izbire
  • 5. Konstruktivna obratna matematika

    5.1 Teoreme ventilatorjev v CRM

  • 6. Konstruktivna topologija
  • 7. Konstruktivna matematična ekonomija in finance
  • 8. Zaključne pripombe
  • Bibliografija

    • Reference
    • Sorodna literatura
  • Akademska orodja
  • Drugi internetni viri
  • Povezani vnosi

1. Uvod

Preden matematiki uveljavijo nekaj (razen aksioma), naj bi to dokazali. Kaj torej pomenijo matematiki, ko uveljavijo ločitev (P / vee Q), kjer sta (P) in (Q) skladenjsko pravilni stavki v nekem (formalnem ali neformalnem) matematičnem jeziku? Naravna - čeprav, kot bomo videli, ni edinstvena - razlaga te ločitve je, da ne velja le (vsaj) ena od navedb (P, Q), ampak se lahko tudi odločimo, katera drži. Tako kot bodo matematiki zatrdili (P) šele, ko se bodo odločili, da (P) drži z dokazovanjem, lahko uveljavijo (P / vee Q) le, če lahko predložijo dokaz o (P) ali ustvarite enega od (Q).

S to razlago pa naletimo na resno težavo v posebnem primeru, ko je (Q) negacija (neg P) (P). Trditi (neg P) pomeni pokazati, da (P) pomeni nasprotovanje (na primer (0 = 1)). A pogosto se zgodi, da matematiki nimajo niti dokaza o (P) niti enega od (neg P). Da bi to videli, moramo razmisliti samo o naslednji Goldbachovi domnevi (GC):

Vsako celo število (gt 2) lahko zapišemo kot vsoto dveh praštevilk, ki kljub najboljšim prizadevanjem številnih vodilnih matematikov ni niti dokazano niti ovrženo, saj je bilo prvič zapisano v pismu Goldbachu Eulerju leta 1742. Prisiljeni smo sklepati, da je po zelo naravni razlagi P (vee Q) samo trmast optimist lahko ohrani prepričanje v zakon izključene sredine (LEM):

Za vsak stavek (P) drži (P) ali (neg P).

Klasična logika to zaokroži s širjenjem interpretacije ločitve: interpretira (P / vee Q) kot (neg (neg P / wedge / neg Q)) ali z drugimi besedami, "nasprotuje si tako (P) kot (Q) sta napačni “. To posledično vodi k idealistični razlagi obstoja, v kateri (obstaja xP (x)) pomeni (neg / forall x / neg P (x)) ("nasprotuje, da (P (x)) biti napačno za vsak (x)”). Na teh interpretacijah ločitve in obstoja so matematiki zgradili veliko in na videz nepredstavljivo zgradbo klasične matematike, ki je temelj za fizične, družbene in (vse bolj) biološke vede. Vendar pa širše razlage prinašajo drago: na primer, ko preidemo od naše prvotne, naravne interpretacije (P / vee Q) do neomejene uporabe idealistične,(neg (neg P / klin / neg Q)) nastale matematike ni mogoče na splošno razlagati v računskih modelih, kot je teorija rekurzivne funkcije.

To točko ponazarja dobro obrabljen primer:

Obstajajo iracionalna števila (a, b) taka, da je (a ^ b) racionalen.

Gladek klasičen dokaz je naslednji. Bodisi je (sqrt {2} ^ { sqrt {2}}) racionalen, v tem primeru vzamemo (a = b = / sqrt {2}); ali pa je (sqrt {2} ^ { sqrt {2}}) iracionalen; v tem primeru vzamemo (a = / sqrt {2} ^ { sqrt {2}}) in (b = / sqrt {2}) (glej Dummett 1977 [2000], 6). A kot kaže, nam ta dokaz ne omogoča natančnega določanja, katera od dveh izbir para ((a, b)) ima zahtevano lastnost. Da bi ugotovili pravilno izbiro ((a, b)), bi se morali odločiti, ali je (sqrt {2} ^ { sqrt {2}}) racionalen ali iracionalen, kar je ravno za uporabite prvotno razlago ločitve z (P) stavek "(sqrt {2} ^ { sqrt {2}}) je racionalen".

Tu je še ena ilustracija razlike med interpretacijami. Razmislite o naslednjem preprostem stavku o množici (bR) realnih števil:

(oznaka {*} forall x / v / bR (x = 0 / vee x / ne 0),)

kjer zaradi razlogov, ki jih razkrijemo v kratkem, (x / ne 0) pomeni, da lahko najdemo racionalno število (r) z (0 / lt r / lt / abs {x}). Naravna računska razlaga (*) je, da imamo postopek, ki na katero koli realno število (x) bodisi pove, da (x = 0) bodisi nam pove, da (x / ne 0). (Na primer, tak postopek lahko ustvari 0, če (x = 0), in 1, če (x / ne 0). Vendar, ker lahko računalnik z dejanskimi približki ravna z realnimi številkami, imajo težavo s prelivanjem, pri katerem lahko dovolj majhno pozitivno število napačno preberete kot 0; zato ne more biti postopka odločanja, ki bi utemeljil trditev (*). Z drugimi besedami, ne moremo pričakovati, da bo (*) v skladu z našo naravno računsko razlago kvantifikatorja (forall) in vezivnega sistema (vee).

Preučimo to z drugega zornega kota. Naj ((G (n)) deluje kot okrajšava za stavek "(2n + 2) je vsota dveh praštevil", kjer se (n) giblje nad pozitivnimi celimi številkami in določa neskončno binarno zaporedje (ba = (a_1, a_2, / ldots)):

[a_n = / začeti {primeri} 0 & / besedilo {če} G (n) besedilo {drži za vse} k / le n \\ 1 & / besedilo {če} nega G (n) besedilo {drži za nekatere} k / le n \\ / konec {primeri})

Ni dvoma, da je (ba) računsko dobro definirano zaporedje, v smislu, da imamo algoritem za računanje (a_n) za vsako (n): preverite parne številke (4, 6,8, / ldots, 2n + 2) za določitev, ali je vsak od njih vsota dveh praštevil; v tem primeru nastavite (a_n = 0) in v nasprotnem primeru nastavite (a_n = 1). Zdaj upoštevati realne številke, katerih (n) th binarni znak je (a_n):

(začeti {poravnati *} x & = (0 / cdot a_1 a_2 / cdots) _ {2} & = 2 ^ {- 1} a_1 + 2 ^ {- 2} a_2 + / cdots \& = / sum_ {n = 1} ^ { infty} 2 ^ {- n} a_n. / konec {poravnati *})

Če (*) velja za našo računalniško razlago, se lahko odločimo med naslednjima dvema možnostoma:

  • (2 ^ {- 1} a_1 + 2 ^ {- 2} a_2 + / cdots = 0), kar pomeni, da je (a_n = 0) za vsak (n);
  • lahko najdemo pozitivno celo število (N) takšno, da (2 ^ {- 1} a_1 + 2 ^ {- 2} a_2 + / cdots / gt 2 ^ {- N}).

V slednjem primeru lahko s testiranjem (a_1, / ldots, a_N) ugotovimo (n / le N) takšno, da je (a_n = 1). Tako nam računalniška razlaga (*) omogoča, da se odločimo, ali obstaja (n) taka, da je (a_n = 1); z drugimi besedami, omogoča nam, da se odločimo o statusu Konstitucije Goldbach. Primer te vrste, ki kaže, da bi nam konstruktivni dokaz nekega klasičnega rezultata (P) omogočil reševanje Goldbachove domneve (in s podobnimi trditvami se imenujejo številni drugi doslej odprti problemi, kot je Riemannova hipoteza). primer Brouwerian-a ali celo Brouwerian-ov kontrakseks za stavek (P) (čeprav v običajnem pomenu te besede ni kontra-vzorec).

Uporaba Goldbachove zasnove je tukaj povsem dramatična. Argument iz prejšnjega odstavka je mogoče spremeniti tako, da pokaže, da v skladu z našo računalniško razlago (*) pomeni omejeno načelo vsevednosti (LPO):

Za vsako binarno zaporedje ((a_1, a_2, / ldots)) bodisi (a_n = 0) za vse (n) bodisi obstaja (n) tak, da (a_n = 1), kar se na splošno šteje za v bistvu nekonstruktivno načelo iz več razlogov. Prvič, njegova rekurzivna razlaga, Obstaja rekurzivni algoritem, ki na katero koli rekurzivno določeno binarno zaporedje ((a_1, a_2, / ldots)) izstopa 0, če (a_n = 0) za vse (n), in izpiše 1, če (a_n = 1) za nekatere (n), očitno je napačen znotraj teorije rekurzivne funkcije, tudi s klasično logiko (glej Bridges & Richman [1987], poglavje 3); Torej, če želimo omogočiti rekurzivno razlago vse naše matematike, potem ne moremo uporabiti LPO. Drugič, obstaja teorija mode (Kripkejevi modeli), v kateri je mogoče pokazati, da LPO konstruktivno ni mogoče izpeljati (Bridges & Richman [1987], poglavje 7).

2. Konstruktivna interpretacija logike

Do zdaj bi moralo biti jasno, da polnokrvni računski razvoj matematike onemogoča idealistične interpretacije ločitve in obstoja, od katerih je odvisna večina klasične matematike. Če želimo delovati konstruktivno, se moramo vrniti od klasičnih interpretacij k naravnim konstruktivnim:

(vee) (ali): da dokažemo (P / vee Q) moramo bodisi imeti dokaz (P) bodisi imeti dokaz (Q).
(klin) (in): da dokažemo (P / klin Q), moramo imeti tako dokaz (P) kot tudi dokaz (Q).
(Rightarrow) (pomeni): dokaz (P / rightarrow Q) je algoritem, ki pretvori vsak dokaz (P) v dokaz (Q).
(neg) (ne): da dokažemo (neg P) moramo pokazati, da (P) pomeni (0 = 1).
(obstaja) (obstaja): da bi dokazali (obstaja xP (x)), moramo zgraditi predmet (x) in dokazati, da drži (P (x)).
(forall) (za vsakega / vse): dokaz (forall x / v SP (x)) je algoritem, ki se uporablja za kateri koli predmet (x) in za podatke, ki dokazujejo, da (x / v S) dokazuje, da (P (x)) drži.

Te BHK-interpretacije (ime odraža njihov izvor v delu Brouwerja, Heytinga in Kolmogorova) je mogoče natančneje določiti s Kleenovim pojmom uresničljivosti; glej (Dummett [1977/2000], 222–234; Beeson [1985], poglavje VII).

Kakšne stvari iščemo, če resno razmišljamo o razvoju matematike tako, da ko izrek izkaže obstoj predmeta (x) s lastnostjo (P), potem dokaz teorema uteleša algoritmi za gradnjo (x) in za dokazovanje, kolikor so potrebni izračuni, da ima lastnost (x) lastnost (P). Tu je nekaj primerov izrek, ki jim sledi neuraden opis zahtev po njegovem konstruktivnem dokazu.

  1. Za vsako realno število (x) bodisi (x = 0) bodisi (x / ne 0). Zahteva za dokaz: algoritem, ki se uporabi za dano realno število (x), odloči, ali bo (x = 0) ali (x / ne 0). Upoštevajte, da lahko algoritem za to odločitev uporablja ne le podatke, ki opisujejo (x), ampak tudi podatke, ki kažejo, da je (x) dejansko število.
  2. Vsaka nepopolna podskupina (S) (bR), ki je omejena zgoraj, ima najmanj zgornjo mejo.

    Zahteva za dokaz: algoritem, ki se uporabi za niz (S) realnih števil, član (s) (S) in zgornjo mejo za (S),

    1. izračuna predmet (b) in pokaže, da je (b) resnično število;
    2. kaže, da je (x / le b) za vsakega (x / v S); in
    3. glede na resnično število (b '\ lt b) izračuna element (x) iz (S), tako da (x / gt b').
  3. Če je (f) neprekinjeno preslikavo v realni vrednosti v zaprtem intervalu ([0,1]), tako da (f (0) cdot f (1) lt 0), potem obstaja (x) tako, da (0 / lt x / lt 1) in (f (x) = 0).

    Zahteva za dokaz: algoritem, ki se uporablja za funkcijo (f), modul kontinuitete za (f) in vrednosti (f (0)) in (f (1)),

    1. izračuna predmet (x) in pokaže, da je (x) resnično število med 0 in 1; in
    2. kaže, da je (f (x) = 0).
  4. Če je (f) neprekinjeno preslikavo v realni vrednosti v zaprtem intervalu ([0,1]), tako da (f (0) cdot f (1) lt 0), potem za vsako (varepsilon / gt 0) obstaja (x) tako, da (0 / lt x / lt 1) in (abs {f (x)} lt / varepsilon).

    Zahteva za dokaz: algoritem, ki se uporablja za funkcijo (f), modul kontinuitete za (f), vrednosti (f (0)) in (f (1)) ter a pozitivna številka (varepsilon),

    1. izračuna predmet (x) in pokaže, da je (x) resnično število med 0 in 1; in
    2. kaže, da je (abs {f (x)} lt / varepsilon).

Razloge za dvom, da ima (A) konstruktiven dokaz, že imamo. Če je mogoče izpolniti zahteve po dokazu za (B), potem lahko glede na kateri koli matematični stavek (P) uporabimo naš dokaz (B) za izračun racionalnega približanja (z) za supremum (sigma) niza

[S = {0 } skodelica {{ v / bR: P / klin x = 1 })

z napako (lt / bfrac {1} {4}). Nato lahko ugotovimo, ali je (z / gt / bfrac {1} {4}), v tem primeru (sigma / gt 0) ali (z / lt / bfrac {3} {4}), ko (sigma / lt 1). V prvem primeru obstaja (x / v S) z (x / gt 0), zato moramo imeti (x = 1) in zato (P). V primeru (sigma / lt 1) imamo (neg P). Tako (B) implicira zakon izključene sredine.

Vendar lahko v Bishopovi konstruktivni teoriji resničnih števil, ki temelji na Cauchyjevih zaporedjih z vnaprej določeno stopnjo konvergence, lahko dokažemo naslednje konstruktivno načelo najmanj zgornje meje:

Naj bo (S) nepopolna podskupina (bR), ki je zgoraj omejena. Potem ima (S) najmanj zgornjo mejo, če in le, če je nameščen v zgornjem vrstnem redu, v smislu, da je za vsa realna števila (alfa, / beta) z (alfa / lt / beta), bodisi (beta) je zgornja meja za (S) bodisi obstaja (x / v S) z (x / gt / alfa) (Bishop & Bridges [1985], str. 37, predlog (4.3)).

Mimogrede omenimo še alternativni razvoj konstruktivne teorije (bR), ki temelji na intervalni aritmetiki; glej poglavje 2 Bridges & Vîță [2006].

Vsaka od stavkov (C) in (D), ki sta klasično enakovredna, je različica teoreme o vmesni vrednosti. V teh stavkih je modul zveznosti za (f) niz (Omega) urejenih parov ((varepsilon, / delta)) pozitivnih realnih števil z naslednjima dvema lastnostima:

  • za vsak (varepsilon / gt 0) obstaja (delta / gt 0) tak, da ((varepsilon, / delta) v / Omega)
  • za vsak ((varepsilon, / delta) v / Omega) in za vse (x, y / v [0,1]) z (abs {x - y} lt / delta), imamo (abs {f (x) - f (y)} lt / varepsilon).

Izjava (C) vključuje drugo v bistvu nekonstruktivno načelo, manj omejeno načelo vseznanosti (LLPO):

Za vsako binarno zaporedje ((a_1, a_2, / ldots)) z največ enim pojmom enakim 1, bodisi (a_n = 0) za vse celo (n) ali drugače (a_n = 0) za vse lihe (n).

Izjava (D), šibka oblika (C), je mogoče konstruktivno dokazati z uporabo intervala, ki se prepolovi, standardne vrste. Naslednji močnejši konstruktivni teorem o vmesni vrednosti, ki zadostuje za večino praktičnih namenov, je dokazan z argumentom približno prepolovljenega intervala:

Naj bo (f) neprekinjeno preslikavo realnih vrednosti v zaprtem intervalu ([0,1]), tako da je (f (0) cdot f (1) lt 0). Predpostavimo tudi, da je (f) lokalno nič, v smislu, da za vsak (x / v [0,1]) in za vsak (r / gt 0) obstaja (y) tak, da (abs {x - y} lt r) in (f (y) ne 0). Potem obstaja (x) tak, da (0 / lt x / lt 1) in (f (x) = 0).

Položaj izrek z vmesno vrednostjo je značilen za mnoge v konstruktivni analizi, kjer najdemo en klasični izrek z več konstruktivnimi različicami, od katerih so nekatere ali vse enake v klasični logiki.

Obstaja eno načelo vsemogočnosti, katerega konstruktivni status je manj jasen kot LPO in LLPO-istoimenski, Markov princip (MP):

Če je za vsako binarno zaporedje ((a_n)) nasprotujoče, da so vsi izrazi (a_n) enaki 0, potem obstaja izraz enak 1.

To načelo je enakovredno številnim preprostim klasičnim predlogom, vključno z naslednjim:

  • Če je za vsako resnično število (x) nasprotujoče, da je (x) enako 0, potem (x / ne 0) (v pomenu, ki smo ga omenili prej).
  • Če je za vsako resnično število (x) nasprotujoče, da je (x) enako 0, potem obstaja (y / in / bR) tak, da je (xy = 1).
  • Za vsako neprekinjeno preslikavo (f: [0,1] rightarrow / bR), če (x / ne y), potem (f (x) ne f (y)).

Markovo načelo predstavlja neomejeno iskanje: če imate dokaz, da vsi izrazi (a_n) 0 vodijo v protislovje, potem s preizkušanjem izrazov (a_1, a_2, a_3, / ldots) posledično ste zajamčeno, da naleti na termin, ki je enak 1; vendar ta garancija ne velja za zagotovilo, da boste želeni izraz našli pred koncem vesolja. Večina praktikov konstruktivne matematike gleda na Markov princip vsaj sumljivo, če že ne povsem neverno. Takšna stališča so podkrepljena z ugotovitvijo, da obstaja Kripkejev model, ki kaže, da MP ni konstruktivno izvedljiv (Bridges & Richman [1987], 137–138.)

3. Sorte konstruktivne matematike

Želja obdržati možnost računalniške interpretacije je ena motivacija za uporabo konstruktivnih reinterpretacij logičnih konektiv in kvantifikatorjev, ki smo jih podali zgoraj; ni pa ravno motivacija pionirjev konstruktivizma v matematiki. V tem razdelku si ogledamo nekaj različnih pristopov konstruktivizma v matematiki v zadnjih 130 letih.

3.1 Intuitionistična matematika

V poznem devetnajstem stoletju so nekateri posamezniki - predvsem Kronecker in Poincaré - izrazili dvom ali celo neodobravanje idealističnih, nekonstruktivnih metod, ki so jih uporabljali nekateri njihovi sodobniki; toda temelj natančnega, sistematičnega pristopa k konstruktivni matematiki je v polemičnih spisih LEJ Brouwerja (1881–1966), začenši z amsterdamsko doktorsko disertacijo Brouwer [1907] in nadaljevati v naslednjih sedemindvajsetih letih. so bili položeni. V Brouwerjevi filozofiji, znani kot intuicionizem, je matematika svobodna stvaritev človeškega uma in predmet obstaja, če in samo, če ga je mogoče (mentalno) zgraditi. Če zavzamemo to filozofsko stališče, potem se neizprosno vleče k prej konstruktivni razlagi logičnih veziv in kvantifikatorjev:kajti kako bi lahko dokaz o nemožnosti neobstoja določenega predmeta (x) opisal miselno konstrukcijo (x)?

Brouwer ni bil najbolj jasen razlagalec njegovih idej, kar kaže naslednji citat:

Matematika nastane, ko je predmet dvotirnosti, ki izhaja iz časa časa, abstrahiran od vseh posebnih dogodkov. Preostala prazna oblika [odnos (n) do (n + 1)] skupne vsebine vseh teh dveh nosilcev postane izvirna intuicija matematike in ponavljajoče se neomejeno ustvarja nove matematične predmete. (citirano v Kline [1972], 1199–2000)

Errett Bishop (Škof [1967], str. 2) je dal sodobno različico Brouwerjevega stališča:

Glavni problem matematike je število, kar pomeni pozitivna cela števila. Število menimo, kot se je počutil Kant glede vesolja. Pozitivna cela števila in njihova aritmetika predpostavljajo samo naravo naše inteligence in verjamemo v naravo inteligence. Razvoj pozitivnih celih števil iz primitivnega koncepta enote, koncepta sosednje enote in procesa matematične indukcije ima popolno prepričanje. Po besedah Kroneckerja je pozitivne celote ustvaril Bog.

Kljub temu, da bi lahko bili Brouwerjevi zapisi nekritični, je bila ena stvar vedno jasna: zanj je matematika imela prednost pred logiko. Lahko bi rekli, kot je to storil Hermann Weyl v naslednjem odlomku, da je Brouwer videl klasično matematiko kot napačno ravno v njeni uporabi klasične logike brez sklicevanja na osnovno matematiko:

Po [Brouwerjevem] pogledu in branju zgodovine je bila klasična logika abstrahirana iz matematike končnih množic in njihovih podmnožic. … Pozabljeni na to omejeno poreklo, je nekoč napačno uporabil to logiko za nekaj nad in pred vso matematiko in jo na koncu brez utemeljitve uporabil pri matematiki neskončnih množic. To je padec in izvirni greh teorije množic, za katero jo pravično kaznujejo antinomije. Ne kaže, da so se pokazala takšna nasprotja, kar je presenetljivo, ampak da so se pokazala v tako pozni fazi igre. (Weyl [1946])

Zlasti taka zloraba logike je povzročila nekonstruktivne dokaze o obstoju, ki po Weylovih besedah "svetu sporočajo, da zaklad obstaja, ne da bi razkrili njegovo lokacijo".

Da bi opisali logiko, ki jo uporablja intuicijski matematik, je bilo treba najprej analizirati matematične procese uma, iz katerih bi lahko analizo izvlekli. Leta 1930 je Brouwerjev najslavnejši učenec Arend Heyting objavil nabor formalnih aksiomov, ki tako jasno označujejo logiko, ki jo uporablja intuicij, da so postali splošno znani kot aksiomi intuicijske logike (Heyting [1930]). Ti aksiomi so zajeli neformalno BHK-interpretacijo veziv in kvantifikatorjev, ki smo jih dali prej.

Intuitionistična matematika se v razlagi izraza „zaporedje“razlikuje od drugih vrst konstruktivne matematike. Običajno je zaporedje v konstruktivni matematiki določeno s pravilom, ki vnaprej določa, kako sestaviti vsak njegov izraz; za takšno zaporedje lahko rečemo, da je zakonito ali vnaprej določeno. Brouwer je pojem zaporedja posplošil tako, da je vključeval možnost konstrukcije pojmov, enega izmed drugega, pri čemer je bil lahko vsak poizveden prosto ali pod določenimi vnaprej določenimi omejitvami. Za večino manipulacij zaporedij ni treba, da so vnaprej določene, in se lahko izvajajo na teh splošnejših zaporedjih proste izbire.

Tako za intuicionista resnično število (bx = (x_1, x_2, / ldots)) - v bistvu Cauchijevo zaporedje racionalnih števil, ne sme biti določeno s pravilom: njegovi izrazi (x_1, x_2, / ldots) so preprosto racionalna števila, zaporedno izdelana, podvržena le nekakšni Cauchyjevi omejitvi, kot je naslednja, ki jo je uporabljal škof [1967]:

(forall m / forall n / left (abs {x_m - x_n} le / left (frac {1} {m} + / frac {1} {n} desno) desno])

Ko so zaporedja proste izbire sprejeta v matematiko, so torej, morda na prvo presenečenje, nekatera močna načela izbire. Naj bo (P) podmnožica (bN ^ { bN} krat / bN) (kjer (bN) označuje množico naravnih števil in za množice (A) in (B, B ^ A) označuje nabor preslikav iz (A) v (B)) in predpostavimo, da za vsako (ba / in / bN ^ { bN}) obstaja (n / v / bN) tako, da ((ba, n) v P). S konstruktivnega vidika to pomeni, da imamo postopek, ki se uporablja za zaporedja, ki izračuna (n) za kateri koli dan (ba). Po Brouwerjevem mnenju je konstrukcija elementa (bN ^ { bN}) za vedno nepopolna: generično zaporedje (ba) je čisto ekstenzivno, v smislu, da v danem trenutku ne moremo vedeti ničesar o (ba) razen končnega niza njegovih pogojev. Iz tega sledi, da mora biti naš postopek sposoben izračunati iz nekega končnega začetnega zaporedja ((a_0, / ldots, a_N)) izrazov (ba), naravno število (n), tako da (P (ba, n)). Če je (bb / in / bN ^ { bN}) katerokoli zaporedje, ki je (b_ {k} = a_ {k}) za (0 / le k / le N), potem je naš postopek mora vrniti isto (n) za (bb) kot za (ba). To pomeni, da je (n) neprekinjena funkcija (ba) glede na topologijo na (bN ^ { bN}), podana z metrikoTo pomeni, da je (n) neprekinjena funkcija (ba) glede na topologijo na (bN ^ { bN}), podana z metrikoTo pomeni, da je (n) neprekinjena funkcija (ba) glede na topologijo na (bN ^ { bN}), podana z metriko

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

Zato nas vodi naslednje načelo neprekinjene izbire, ki ga delimo na del kontinuitete in na izbiro.

CC1: Vsaka funkcija od (bN ^ { bN}) do (bN) je neprekinjena.

CC2: Če (P / podseteq / bN ^ { bN} krat / bN) in za vsako (ba / in / bN ^ { bN}) obstaja (n / in / bN) taka, da je ((ba, n) v P), potem obstaja funkcija (f: / bN ^ { bN} desnica / bN) taka, da ((ba, f (ba)) v P) za vse (ba / in / bN ^ { bN}).

Če sta (P) in (f) kot v CC2, potem rečemo, da je (f) izbirna funkcija za (P).

Načela ozaveščenosti LPO in LLPO sta v hipotezah CC1–2 očitno napačna; vendar je MP v skladu s tem. Med izjemnimi posledicami CC1-2 so naslednje.

  • Vsaka funkcija od (bN ^ { bN}) ali (2 ^ { bN}) do metričnega prostora je točkovno neprekinjena.
  • Vsako preslikavo iz praznega popolnega ločljivega metričnega prostora v metrični prostor je točno neprekinjeno.
  • Vsak zemljevid od prave črte (bR) do samega sebe je točkovno neprekinjen.
  • Naj bo (X) celoten ločen normiran prostor, (Y) normiran prostor in ((u_n)) zaporedje linearnih preslikav od (X) do (Y), tako da za vsak enota vektor (x) od (X), (phi (x) = / sup { Vert u_n (x) rVert: n / in / bN }) obstaja. Potem obstaja (c / gt 0) tak, da je (lVert u_n (x) rVert / le c) za vse (n / v / bN) in vse vektorje enot (x) od (X) (načelo enotne omejitve).

Zdi se, da je vsaka od teh trditev v nasprotju z znanimi klasičnimi teoremi. Vendar pa primerjave s klasično matematiko ne bi smeli narediti površno: da bi razumeli, da tukaj ni resničnega protislovja, moramo razumeti, da je pomen pojmov "funkcija" in celo "resnično število" v intuicijistični matematiki povsem drugačen od tistega v klasičnem okolju. (V praksi intuicijske matematike ni mogoče takoj in neposredno primerjati s klasično matematiko.)

Brouwerjeva samospektiva nad naravo funkcij in kontinuumom ga je pripeljala do drugega načela, ki je za razliko od neprekinjene izbire klasično veljavno. To načelo zahteva nekoliko več ozadja za njegovo razlago.

Za kateri koli niz (S) označimo z (S ^ *) nabor vseh končnih zaporedij elementov (S), vključno s praznim zaporedjem (()). Če je (alfa = (a_1, / ldots, a_n)) v (S ^ *), potem se (n) imenuje dolžina (alfa) in jo označuje z (abs { alfa}). Če je (m / v / bN) in (alfa) končno ali neskončno zaporedje v (S) dolžini vsaj (m), potem označujemo z (bar { alfa} (m)) končno zaporedje, sestavljeno iz prvih (m) izrazov (alfa). Upoštevajte, da sta (bar { alfa} (0) = ()) in (abs { bar { alfa} (0)}) = 0. Če (alfa / v S ^ *) in (beta = / bar { alfa} (m)) za nekatere (m), rečemo, da je (alfa) podaljšek (beta) in da je (beta) omejitev (alfa).

Podnabor (sigma) (S) naj bi bil snemljiv (od (S)), če

(forall x / v S (x / in / sigma / vee x / not / in / sigma).)

Snemljiva podmnožica (sigma) (bN ^ *) se imenuje ventilator, če

  • je zaprt pod omejitvijo: za vsakega (alfa / v / bN ^ *) in vsakega (n), če (bar { alfa} (n) v S), potem (vrstica { alfa} (k) v S) kadarkoli (0 / le k / le n); in
  • za vsak (alfa / v / sigma) niz ({ alfa ^ * n / v S: n / in / bN }) je končno ali prazno, kjer (alfa ^ * n) označuje končno zaporedje, ki ga dobimo s priključitvijo naravnega števila (n) na izraze (alfa).

Pot v ventilatorju (sigma) je zaporedje (alfa), končno ali neskončno, tako da je (bar { alfa} (n) v / sigma) za vsako veljavno (n). Pravimo, da pot (alfa) blokira podmnožica (B), če je neka omejitev (alfa) v (B); če v (B) ni omejitve (alfa), rečemo, da (alfa) manjka (B). Podmnožica (B) ventilatorja (sigma) se imenuje vrstica za (sigma), če je vsaka neskončna pot (sigma) blokirana s (B); črt (B) za (sigma) je enak, če obstaja (n / v / bN), tako da je vsaka dolžina poti (n) blokirana s (B).

Končno lahko navedemo Brouwerjevo naslednje načelo intuicijma, izrek ventilatorja za snemljive palice (FT (_ D)):

Vsak snemljiv drog ventilatorja je enoten.

FT (_ D) je v svoji klasični kontrapozitivni obliki znana kot Königova lema: če za vsako (n) obstaja pot dolžine (n), ki manjka (B), potem obstaja neskončno pot, ki pogreša (B) (glej Dummett 1977 [2000], 49–53). (Seveda je stanje snemljivosti klasično odveč.) Enostavno je konstruirati Brouwerjev kontra-primer na Königovo lemo.

Brouwer je dejansko postavil teorem ventilatorja brez omejitve snemljivosti palice. Poskusi dokazati, da se splošnejši izrek oboževalcev konstruktivno opira na analizo, kako bi lahko vedeli, da je podmnožica bar, in je Brouwerja pripeljal do pojma indukcije palice; o tem razpravlja razdelek 3.6 vnosa o intuicijstvu v filozofiji matematike; še ena dobra referenca za indukcijo palice je van Atten (2004). Na teoreme ventilatorjev se bomo vrnili v razdelku 4.

Med številnimi aplikacijami Brouwerjevih načel je najbolj znan njegov enotni teorem o kontinuiteti (ki izhaja iz natančnih posledic kontinuitete CC1-2 skupaj s splošno obliko teorema ventilatorja kot FT (_ D)):

Vsako preslikavo iz kompaktnega (torej popolnega, popolnoma omejenega) metričnega prostora v metrični prostor je enakomerno kontinuirano.

Bralca še enkrat opozorimo, naj to previdno razloži znotraj Brouwerjevega intuicijističnega okvira in naj ne skoči do zmotnega sklepa, da je intuicij v nasprotju s klasično matematiko. Obe vrsti matematike je bolj smiselno obravnavati kot neprimerljivi. Za nadaljnjo razpravo glejte vnos o intuicijski logiki.

Na žalost - in morda neizogibno ob nasprotovanju matematikov takšnega stasa, kot je Hilbert - je Brouwerjeva intuicijska šola matematike in filozofije postajala vse bolj vpletena v to, kar se je vsaj klasičnim matematikom zdelo kvazi mistično špekuliranje o naravi konstruktivne misli, na škodo same prakse konstruktivne matematike. Ta nesrečna polarizacija med Brouweričani in Hilbertijci je dosegla vrhunec v zloglasnem Grundlagenstreitu iz dvajsetih let 20. stoletja, katerega podrobnosti lahko najdemo v Brouwerjevih življenjepisih van Dalena [1999, 2005] in van Stigta [1990].

3.2 Rekurzivna konstruktivna matematika

V poznih 40. letih je ruski matematik AA Markov začel razvijati alternativno obliko konstruktivne matematike (RUSS), ki je v bistvu rekurzivna teorija funkcij z intuicijsko logiko (Markov [1954], Kushner [1985]). V tej raznolikosti so predmeti definirani z Gödel-številkami, postopki pa so rekurzivni; glavna razlika med RUSS in klasično rekurzivno analizo, razvite po delu Turinga, Churcha in drugih, je leta 1936 pojasnila naravo računskih procesov, da je logika, uporabljena v RUSS, intuicijska.

Ena ovira, s katero se matematik srečuje pri poskusu spopadanja z RUSS, je, da je izražen z jezikom teorije rekurzije, ki ga ni težko razbrati; res se bo ob odpiranju strani izvrstnih predavanj Kushnerja [1985] mogoče oprostiti, če se sprašujemo, ali gre za analizo ali logiko. (To opombo je treba omiliti glede na dve relativno berljivi knjigi o klasični rekurzivni analizi Abertha [1980, 2001].) Na srečo lahko nekdo pride do osrčja RUSS z aksiomatičnim pristopom zaradi Richmana [1983] (glej tudi Poglavje 3 Bridges & Richman [1987]).

Najprej določimo niz (S), ki ga je mogoče šteti, če obstaja preslikava iz snemljive podmnožice (bN) na (S). Z intuicijsko logiko ne moremo dokazati, da je vsaka podmnožica (bN) snemljiva (bralca povabimo, da poda brouwerjanski primer, da to dokaže). Števljive podvrste (bN) v aksiomatičnem pristopu Richmana so protipostavke rekurzivno naštetih nizov v normalnem razvoju RUSS.

Z delno funkcijo na (bN) mislimo na preslikavo, katere domena je podmnožica (bN); če je domena (bN), potem imenujemo funkcijo skupna delna funkcija na (bN). Richmanov pristop k RUSS temelji na intuicijski logiki in enem samem aksiomu računskih delnih funkcij (CPF):

Obstaja naštevanje (phi_0, / phi_1, / ldots) nabora vseh delnih funkcij od (bN) do (bN) s števljivimi domenami.

Izjemno je, kaj lahko na podlagi tega načela sklepamo čisto in hitro. Na primer, lahko dokažemo naslednji rezultat, ki skoraj takoj pokaže, da sta LLPO in s tem LPO v rekurzivni nastavitvi napačna.

Obstaja celotna delna funkcija (f: / bN / krat / bN / rightarrow {0,1 }) taka, da

  • za vsak (m) obstaja največ en (n) tak, da je (f (m, n) = 1); in
  • za vsako skupno delno funkcijo (f: / bN / desna puščica {0,1 }) obstaja (m, k) v (bN) taka, da (f (m, 2k + f (m)) = 1).

Bolj zanimivi pa so rezultati, kot so naslednji znotraj RUSS.

  • Speckerjev teorem (Specker [1949]): Obstaja strogo naraščajoče zaporedje ((r_1, r_2, / ldots)) racionalnih števil v zaprtem intervalu ([0,1]) tako, da je za vsako (x / v / bR) obstajata (N / v / bN) in (delta / gt 0) taka, da je (abs {x - r_n} ge / delta) za vse (n / ge N).
  • Za vsak (varepsilon / gt 0) obstaja zaporedje ((I_1, I_2, / ldots)) omejenih odprtih intervalov v (bR), tako da (začne {poravnati} oznaka {i} bR & / subseteq / bigcup_ {n = 1} ^ { infty} I_n, / text {in} / \ oznaka {ii} sum_ {n = 1} ^ N / abs {I_n} & / lt / varepsilon / text {za vsakega} N. / konec {poravnava}) (Takšno zaporedje intervalov se imenuje (varepsilon) - edninski pokrov (bR).)
  • Obstaja natančno neprekinjena funkcija (f: [0,1] rightarrow / bR), ki ni enakomerno neprekinjena.
  • Obstaja enakomerno neprekinjena funkcija s pozitivno vrednostjo (f: [0,1] rightarrow / bR), katere infimum je 0.

S klasičnega stališča se ti rezultati prilegajo mestu, ko se zaveda, da je treba besede, kot sta "funkcija" in "resnično število", razlagati kot "rekurzivna funkcija" in "rekurzivna realna številka". Upoštevajte, da je drugi od zgornjih štirih rekurzivnih teorem močan rekurzivni kontraekzor lastnosti kompaktnosti odprtega pokrova (rekurzivne) realne črte; četrti pa je rekurzivni kontraprimer klasičnega izrekanja, da vsako enakomerno neprekinjeno preslikavo kompaktne množice v (bR) doseže svoj infimum.

3.3 Škofova konstruktivna matematika

Napredek pri vseh sortah konstruktivne matematike je bil v naslednjem desetletju in pol razmeroma počasen. Kar je bilo potrebno za povečanje prepoznavnosti konstruktivizma v matematiki, je bil vrhunski klasični matematik, ki je pokazal, da je možen temeljit konstruktiven razvoj globoke analize brez zavezanosti Brouwerjevih neklasičnih načel ali strojev rekurzivne teorije funkcij. Ta potreba je bila izpolnjena leta 1967, z nastopom monografije Erretta Bishopa Temelji konstruktivne analize [1967], produkta osupljivega nekaj let, v katerem je Bishop, ki deluje v neformalnem, a strogem slogu, ki ga uporabljajo običajni analitiki, konstruktivno razvil velikega dela analize dvajsetega stoletja, vključno s teoremom Stone-Weierstrass, teoremi Hahn-Banach in ločitvijo,spektralni teorem za samo-sosednje operaterje na Hilbertovem prostoru, Lebesguejeva konvergenčna teorema za abstraktne integrale, Haarjeva mera in abstraktna Fourierova preobrazba, ergodične teoreme in elementi teorije Banachove algebre. (Glej tudi Bishop & Bridges [1985].) Tako je ob kapi dal laž splošnemu stališču, ki ga je Hilbert izrazil tako močno:

Če bi matematik vzel načelo izključene sredine, bi bilo enako, recimo, če bi teleskopu astronomu ali bokserju prepovedal uporabo pest. (Hilbert [1928])

Ne samo, da je škofova matematika BISH imela prednost berljivosti - če odprete Bishopovo knjigo na kateri koli strani, je to, kar vidite, jasno prepoznavno kot analiza, četudi se občasno njegove poteze med dokazom morda zdijo čudne eden se je šolal z uporabo zakona izključene srednje, vendar za razliko od intuicijske ali rekurzivne matematike dopušča veliko različnih interpretacij. Intuitionistična matematika, rekurzivna konstruktivna matematika in celo klasična matematika vse ponujajo modele BISH. Pravzaprav je mogoče rezultate in dokaze v BISH razlagati z vsaj manjšimi spremembami v katerem koli razumnem modelu računalniške matematike, kot je na primer Weihrauchova teorija učinkovitosti drugega tipa (Weihrauch [2000]; Bauer [2005]).

Kako je dosežena ta večkratna razlaga? Vsaj deloma zaradi Bishopove zavrnitve, da bi omejila svoj primitivni pojem "algoritem" ali, po njegovih besedah, "končne rutine". To zavrnitev je privedlo do kritike, da njegov pristop nima natančnosti, ki bi jo logik običajno pričakoval od temeljnega sistema. Vendar pa je to kritiko mogoče premagati, če natančneje pogledamo, kaj v resnici delajo BISH, ko dokazujejo teoreme: v praksi matematiko delajo z intuicijsko logiko. Izkušnje kažejo, da omejevanje na intuicijsko logiko matematike vedno prisili, da delujejo na način, ki ga lahko vsaj neuradno opišemo kot algoritem; zato se zdi, da je algoritmična matematika enakovredna matematiki, ki uporablja samo intuicijsko logiko. Če je tako,tedaj lahko konstruktivno matematiko izvajamo z intuicijsko logiko na katerem koli razumno opredeljenem matematičnem predmetu, ne le na neki razred "konstruktivnih predmetov".

Zdi se, da je bolj ali manj takšno stališče prvi predstavil Richman [1990, 1996]. Vzemi logiko kot glavno značilnost konstruktivne matematike in ne odraža primatosti matematike nad logiko, ki je bila del prepričanja Brouwerja, Heytinga, Markova, škofa in drugih pionirjev konstruktivizma. Po drugi strani pa dejansko zajame bistvo konstruktivne matematike v praksi.

Tako bi lahko ločili med ontološkim konstruktivizmom Brouwerja in drugimi, ki jih konstruktivna matematika vodi skozi prepričanje, da so matematični predmeti duševne stvaritve, in epistemološki konstruktivizem Richmana in tiste, ki vidijo konstruktivno matematiko, kot jo odlikuje njegova metodologija, ki temelji na uporabi intuicijske logike. Seveda prvi pristop k konstruktivizmu neizogibno vodi do drugega; in slednje gotovo ni v neskladju z Brouwerjanovo ontologijo.

Za dejansko matematiko potrebujemo več kot samo intuicijsko logiko. Za Bishopa so bili gradniki matematike pozitivna cela števila (glej citat Bishopa [1967] v zgornjem oddelku 3.1). Med zgodnjimi formalnimi sistemi za BISH so bili Myhillski [1975] aksiomatični temelji, ki temeljijo na primitivnih pojmih števila, sklopa in funkcije; Fefermannov [1975] sistem za eksplicitne matematike; in Friedmanova [1977] intuicijistična teorija množic ZF. Dve najpomembnejši formalni podpori BISH na tej stopnji sta teorija množic CZF Aczel in Rathjen [2000] in intuicijska teorija tipa Martin-Löf [1975, 1984].

3.4 Martino-Löfova konstruktivna teorija tipa

Preden zaključimo ogled različic sodobne konstruktivne matematike, obiščemo četrto sorto, ki temelji na intuicijski tipistični teoriji Per Martin-Löfa (ML). Martin-Löf je objavil svoje Beležke o konstruktivni matematiki [1968], ki temeljijo na predavanjih, ki jih je imel v Evropi v letih 1966–68; zato njegovo sodelovanje z konstruktivizmom v matematiki sega vsaj do obdobja škofovega pisanja Temelji konstruktivne analize. Knjiga Martina Löfa je v duhu RUSS in ne BISH; Dejansko njen avtor ni imel dostopa do Škofove knjige, dokler ni bil dokončan njegov rokopis. Martin-Löf je pozneje usmeril pozornost na svojo teorijo tipov kot temelj za škofovo konstruktivno matematiko.

Po njegovih besedah je neuradna razlaga idej, na katerih temelji ML:

Pomislili bomo na matematične predmete ali konstrukcije. Vsak matematični predmet je določene vrste ali vrste [… in] je vedno dan skupaj s svojo vrsto. … Tip je opredeljen tako, da opiše, kaj moramo narediti, da konstruiramo predmet tega tipa. … Povedano drugače, tip je dobro opredeljen, če razumemo… kaj pomeni biti predmet tega tipa. Tako je na primer (bN / rightarrow / bN) [funkcije od (bN) do (bN)] tip, ne zato, ker poznamo določene teoretične funkcije števila, kot so primitivne rekurzivne, ampak ker mislimo, da na splošno razumemo pojem teoretične funkcije števil. (Martin-Löf [975])

Zlasti v tem sistemu je lahko vsak predlog predstavljen kot vrsta: in sicer vrsta dokazov predloga. Nasprotno pa vsaka vrsta določa predlog: in sicer trditev, da je zadevna vrsta naseljena. Ko torej pomislimo na določen tip (T) kot predlog, razlagamo formulo

[x / v T)

kot je "(x) dokaz predloga (T)".

Martin-Löf nadaljuje z oblikovanjem novih vrst, kot so kartezijanski izdelki in ločeni sindikati, od starih. Na primer kartuzijanski izdelek

[(Pi x / v A) B (x))

je vrsta funkcij, ki poljuben predmet (x) tipa (A) prevzamejo v objekt tipa (B (x)). V razlagi propozicij kot dokazov, kjer (B (x)) predstavlja predlog, zgornji kartuzijanski izdelek ustreza univerzalnemu predlogu

[(forall x / v A) B (x).)

Martin-Löf skrbno loči med dokazi in izpeljavami: dokazni predmet je priča dejstva, da so bile nekatere trditve dokazane; ker je izpeljava zapis gradnje dokaznega predmeta. Prav tako izvaja dve osnovni obliki (tukaj ne smejo reči »vrste«) presoje. Prvo je razmerje med dokaznimi predmeti in propozicijami, drugo lastnost nekaterih propozicij. V prvem primeru je presoja bodisi, da je dokazni predmet (a) priča predloga (A), bodisi tak, da sta dva dokazna predmeta (a) in (b) enaka in oba pričata, da je (A) dokazano. Prvi primer druge oblike presoje določa, da je predlog (A) dobro oblikovan, drugi pa, da sta dve predlogi (A) in (B) enaki.

Obstaja previden in zelo podroben sklop pravil za formalizacijo ML. Ne bomo se spuščali v te, ampak bralca napotili na druge vire, kot sta Sambin & Smith [1998].

Kadar dejansko delamo konstruktivno matematiko v teoriji vrst, je treba pogosto opremiti popolnoma predstavljene sklope (tipe) z enakovrednim razmerjem, pri čemer je kombinacija znana kot setoid. Preslikave so nato funkcije, ki spoštujejo ta razmerja enakovrednosti. To se zelo ujema z načinom, kako je škof predstavil svojo neformalno teorijo sklopov. Odvisne vrste Martin-Löf so uporabne za oblikovanje podmnožic. Na primer, dejanske številke je mogoče zgraditi s tipom (Sigma) (glej Martin-Löf [1984]):

[(Sigma x / in / bN _ + / rightarrow / bQ) (Pi m / in / bN _ +) (Pi n / in / bN _ +) levo (abs {x_ {m} - x_ {n }} le / levo (frac {1} {m} + / frac {1} {n} desno) desno],)

Element te vrste (B) je torej par, sestavljen iz konvergentnega zaporedja (bx) racional in dokazov (p), da je konvergenčen. Primerno razmerje enakovrednosti ({ sim}) na (R) je določeno tako, da ((x, p) sim (y, q)) pomeni

(forall m / in / bN_ + / levo (abs {x_ {m} - y_ {m}} le / frac {2} {m} desno).)

Nastali setoid realnih števil je (bR = (R, { sim})). To lahko hitro dokažemo

(forall x / in / bR \, / obstaja n / v Z (n / lt x / lt n + 2))

nato pa z uporabo izbranega teoretičnega aksioma (glej oddelek 4 spodaj) poišči funkcijo (f: / bR / rightarrow / bZ) tako, da (f (x) lt x / lt f (x) +2). Vendar ni razloga za domnevo, da funkcija (f) spoštuje enakovredna razmerja - to pomeni, da ima (f (x) = f (y)), če (x / sim y).

Vsak konstruktiven dokaz uteleša algoritem, ki ga je načeloma mogoče izvleči in prenoviti kot računalniški program; poleg tega je konstruktivni dokaz sam po sebi preverjanje, da je algoritem pravilen - torej da ustreza njegovim specifikacijam. Ena večjih prednosti Martinovega Löfovega formalnega pristopa k konstruktivni matematiki je, da močno olajša pridobivanje programov iz dokazov. To je privedlo do resnega dela pri izvajanju konstruktivne matematike na različnih lokacijah (glej Martin-Löf [1980], Constable [1986], Hayashi & Nakano [1988], Schwichtenberg [2009]). Nekatere novejše izvedbe teorije vrst za pridobivanje dokazov sta Coq in Agda (glejte povezave v Drugih internetnih virov).

4. Aksiom izbire

Celoten izbirni aksiom lahko navedemo na naslednji način:

Če so (A, B) naseljeni sklopi in (S) podmnožica (A / krat B), tako da

(forall x / v A \, / obstaja y / v B ((x, y) v S),)

potem obstaja funkcija izbire (f: A / pravica B) taka, da

(forall x / v A ((x, f (x)) v S).)

Zdaj, če gre za konstruktivno razlago, bo za določeno (x / v A) vrednost (f (x)) izbirne funkcije odvisna ne le od (x), ampak tudi na podatkih, ki dokazujejo, da (x) spada v (A.) Na splošno ne moremo pričakovati, da bo ustvaril takšno izbiro. Vendar je BHK interpretacija hipotez v aksiomi, da obstaja algoritem (mathcal {A}), ki na katero koli dano (x / v A) ustvari element (y / v B) taka, da je ((x, y) v S). Če je (A) popolnoma predstavljen niz, za katerega ni potrebno delo, ki presega konstrukcijo vsakega elementa v množici, da bi dokazal, da element res spada v (A), potem lahko upravičeno pričakujemo algoritem (mathcal {A}) funkcija izbire. V teoriji tipa Martin-Löf je vsak sklop v celoti predstavljen inAksiom izbire je v skladu z razlago BHK izpeljan.

Po drugi strani pa je matematika v škofovskem slogu popolnoma predstavljena ––– ali v njegovi terminologiji osnovne ––– množice so redke, en primer je (bN); zato lahko pričakujemo, da aksiom izbire ne bi bil izvedljiv. V resnici, kot sta pokazala Diaconescu [1975] in Goodman & Myhill [1978], ki jo je sam prepisal v težavi 2 na strani 58 škofa 1967, aksiom izbire pomeni zakon izključene sredine. Jasno je, da izrek Diaconescu-Goodman-Myhill velja le pod predpostavko, da ni vsak sklop v celoti predstavljen.

Konstruktivni matematiki, ki ne delujejo v ML, običajno zavrnejo polni aksiom izbire, vendar sprejmejo aksiom izbire, ki jo je mogoče šteti, v kateri je domena izbire (bN) in odvisna izbira. Toda nekateri raje delajo brez celoštevilne izbire, ker lahko govorimo o neskončnosti izbire, ne da bi pri tem postavili pravilo, težave, ki so ravno tako velike, ali je neskončnost nešteta ali ne. Zanimivo je, da je Lebesgue natančno to poudaril v pismu Borelu (glej Moore [2013], stran 316):

Popolnoma se strinjam s Hadamardom, ko trdi, da govoriti o neskončnosti izbire, ne da bi določil pravilo, predstavlja težavo, ki je prav tako velika, ali je neskončnost nešteta ali ne.

Učinek opustitve celo štetja izbire je izključitev številnih teoremov, ki se dokazujejo z zaporednimi argumenti, ki temeljijo na izbiri. Toda tisti, ki zagovarjate izogibanje izbiri, trdijo, da vas izogibanje izbiri prisili, da stvari oblikujete bolje.

Poseben primer je temeljni teorem algebre: vsak kompleksni polinom ima vsaj eno korenino v kompleksni ravnini. Richman [2000] je pokazal, da brez štetja izbire, čeprav lahko konstruiramo samo izolirane (morda več) korenin, lahko zgradimo poljubno blizu približkov večnamenskim koreninam. Takšen pristop se osredotoča na iskanje približne linearne faktorizacije polinoma, namesto na iskanje ločenih približkov vsakega od njegovih korenin.

Za nadaljnjo analizo izbire aksioma v teoriji množic in teoriji tipov glej Martin-Löf [2006] in vnose SEP o teoriji kategorij, teoriji tipov in teoriji intuicijističnega tipa.

5. Konstruktivna obratna matematika

Harvey Friedman je v 70. letih prejšnjega stoletja sprožil raziskovalni program povratne matematike, katerega cilj je razvrstiti matematične teoreme glede na njihovo enakovrednost enemu od majhnega števila teoretičnih načel (Friedman 1975). Ta razvrstitev odkriva zanimive, včasih izjemne razlike v dokazno-teoretični zapletenosti. Čeprav se na primer izrek Ascoli-Arzelà uporablja v standardnem dokazu Peanovega teorema za rešitve navadnih diferencialnih enačb (Hurewicz [1958], stran 10), obratno-matematična analiza kaže, da je prva enakovredno strogo močnejši set-teoretično načelo kot enakovredno Peanovemu teoremu (Simpson [1984], Teoremi 3.9 in 4.2). Standardni traktat o klasični obratni matematiki je (Simpson [1999/2009]).

Na začetku tega stoletja sta Veldman (glej Druge internetne vire) na Nizozemskem in Ishihara [2005, 2006] na Japonskem samostojno sprožila program konstruktivne povratne matematike (CRM), ki temelji na intuicijističnem, ne pa na klasičnem oz. logika. (Kljub temu upoštevajte, da je prvo objavljeno delo v moderni dobi CRM verjetno Julian in Richman [1984], kar je bilo dvajset let pred svojim časom.) V tem delu članka opisujemo manj formalni pristop do CRM, v slogu in okvirju BISH. Cilj tega CRM programa je razvrstiti teoreme v tri standardne modele - CLASS, INT in RUSS - po katerih načelih moramo in jih potrebujemo le dodati BISH, da jih dokažemo.

Poudarjamo, da se tukaj omejimo na neformalni CRM, v katerem jemljemo za samoumevno načela funkcionalnosti in konstrukcije, opisana v prvih poglavjih Bishop [1967] ali Bishop & Bridges [1985], in delamo v neformalnih, čeprav strog, slog praktičnega analitika, algebraista, topologa,….

CRM se v praksi naravno razdeli na dva dela. V prvem od teh pomislimo na izrek (T) INT ali RUSS in skušamo najti neko načelo, ki bi veljalo v tem modelu in ki ni samo (T), katerega dodatek k BISH je nujen in zadosten za konstruktivni dokaz (T). V drugem delu CRM imamo opravka s teoremom (T) RAZREDA, za katerega sumimo, da je nekonstruktiven, in poskušamo dokazati, da je (T) ekvivalenten BISH enemu od številnih znanih v bistvu- nekonstruktivna načela, kot so MP, LLPO, LPO ali LEM. Za primer tega dela CRM omenimo naš prejšnji dokaz, da klasični princip najmanj zgornje meje pomeni in je zato enakovreden LEM.

Mimogrede, obstaja močan argument, da se je Brouwer [1921] prvi lotil obratno-matematičnih idej: njegovi vzorci Brouwerian (glej tistega, ki uporablja Goldbachovo domnevo, zgoraj v 1. poglavju) ležijo v drugem delu CRM. Tudi če Brouwer teh primerov ni navedel kot logične enakovrednosti, ampak kot implikacije tipa

[P / Righttarrow / text {neko nekonstruktivno načelo},)

težko je verjeti, da se ni zavedal, da desnica v takih primerih implicira levico.

5.1 Teoreme ventilatorjev v CRM

Za ponazoritev prvega dela CRM se zdaj osredotočamo na teoreme tipa

(besedilo {BISH} vdash / text {FT} _? / Leva stekla T,)

kjer je FT (_?) neka oblika Brouwerjevega teorema ventilatorjev in (T) izrek INT. Da bi to storili, moramo razlikovati med določenimi vrstami vrstice za celotni binarni ventilator (2 ^ *) (množica vseh končnih zaporedij v ({0,1 })).

Naj bo (alfa / equiv (alfa_1, / alfa_2, / ldots)) končno ali neskončno binarno zaporedje. Povezava (alfa) z drugim nizom (beta) je

(alfa ^ { frown} beta / equiv (alfa_1, / alfa_2, / ldots, / alpha_n, / beta_1, / ldots, / beta_m).)

Za (b) v ({0,1 }) pišemo (alfa ^ { frown} b) in ne (alfa ^ { frown} (b)). Z (mathsf {c}) - podnizom (2 ^ *) mislimo na podmnožico (B) z (2 ^ *), tako da

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

za nekatere snemljive podmnožice (D) (2 ^ *). Vsaka snemljiva podmnožica (2 ^ *) je (mathsf {c}) - podmnožica. Po drugi strani pod (Pi ^ {0} _1) - podvrsto (2 ^ *) mislimo na podmnožico (B) (2 ^ *) z naslednjo lastnostjo: obstaja snemljiva podmnožica (S) z (2 ^ * / krat / bN) taka, da

(forall u / in 2 ^ * \, / forall n / in / bN \, ((u, n) in S / Rightarrow (u ^ { frown} 0, n) in S / wedge (u ^ { frown} 1, n) v S))

in

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

Vsak (mathsf {c}) - podniz (B) od (2 ^ *) je (Pi ^ {0} _1) - podniz: preprosto vzemite (S = D / krat / bN), kjer je (D) snemljiva podmnožica (2 ^ *), tako da (1) drži.

Če (?) Označuje lastnost podmnožic (2 ^ *), potem Brouwerjev teorem ventilatorjev za (?) - palice pove, da je vsaka vrstica s lastnostjo (?) Enakomerna vrstica. Zanima nas zlasti teorem ventilatorja za snemljive palice (o čemer smo že govorili v oddelku 3.1):

FT (_ D): vsaka snemljiva palica celotnega binarnega ventilatorja je enotna;

teorem ventilatorja za (mathsf {c}) - palice (to je palice, ki so (mathsf {c}) - podmnožja):

FT (_ { mathsf {c}}): vsak c-trak celotnega binarnega ventilatorja je enakomeren;

teorem ventilatorja za (Pi ^ {0} _1) - palice (torej palice, ki so (Pi ^ {0} _1) - podmnožja):

FT (_ { Pi ^ {0} _1}): vsak (Pi ^ {0} _1) - bar celotnega binarnega ventilatorja je enakomeren;

in celotni izrek ventilatorja:

FT: Vsaka palica celotnega binarnega ventilatorja je enotna.

Upoštevajte, da v primerjavi z BISH, FT (Rightarrow) FT (_ { Pi ^ {0} _1} Rightarrow) FT (_ c / Rightarrow) FT (_ D).

Lubarsky in Diener [2014] sta pokazala, da so te posledice stroge.

Značilno je, da želimo dokazati, da je FT (_?) Nad BISH enakovreden predlogu, da je za vsak niz (S) ustrezne vrste nekakšna točkovna lastnost obrazca

(oznaka {2} forall x / v S / obstaja t / v TP (s, t))

dejansko drži enotno obliko

(oznaka {3} obstaja t / v T / forall s / v SP (s, t).)

Naša strategija za napad na to težavo je dvojna. Najprej s pomočjo niza (S) ustrezne vrste sestavimo? -Skupino (N) od (2 ^ *) takšno, da

  • če drži (2), je (B) vrstica in
  • če je (B) enakomerna vrstica, potem (3) drži.

To pa je le polovica rešitve. Da dokažemo, da implikacija iz (3) na (2) pomeni FT (_?), Smatramo? -Skupino (B) (2 ^ *) in sestavimo ustrezen niz (S) taka, da

  • če je (B) vrstica, potem (2) drži in
  • če drži (3), je (B) enakomerna vrstica.

Kanonični primer takšnih rezultatov je Julian in Richman [1984], v katerem je (S) množica vrednosti danega enakomerno neprekinjenega preslikavanja (f: [0,1] rightarrow / bR, T) je niz pozitivnih realnih števil in

[P (s, t) equiv (s / ge t).)

Točkovna lastnost, ki jo štejemo, je

(forall x / v [0,1] obstaja t / gt 0 (f (x) ge t),)

je njegova enotna različica

(obstaja t / gt 0 / forall x / v [0,1] (f (x) ge t).)

Rezultati Juliana-Richmana so naslednji.

Izrek 1: Naj bo (f: [0,1] pravica / bR) enakomerno neprekinjena. Potem obstaja snemljiva podmnožica (B) od (2 ^ *) taka, da

  • če je (f (x) gt 0) za vsako (x / v [0,1]), potem je (B) vrstica in
  • če je (B) enakomerna vrstica, potem (inf f / gt 0).

Izrek 2: Naj bo (B) snemljiva podmnožica (2 ^ *). Potem obstaja enakomerno neprekinjeno (f: [0,1] pravica / bR), tako da

  • če je (B) vrstica, potem (f (x) gt 0) za vsako (x / v [0,1]) in
  • če je inf (f / gt 0), potem je (B) enakomerna vrstica.

Dokazi teh dveh izrek so subtilni in zapleteni; glej Julian & Richman [1984].

Oba izrek Julian-Richman skupaj razkrivata, da je v primerjavi z BISH izrek ventilatorja FT (_ D) enakovreden principu pozitivnosti, POS:

Vsaka enakomerno neprekinjena funkcija na ([0,1]) s pozitivno vrednostjo ima pozitiven infimum.

Iz tega sledi, da je POS izpeljan v INT, v katerem je celotni teorem ventilatorja, ne le FT (_ D), standardno načelo. Stanje je mirno, nasprotno v RUSS, kjer obstaja snemljiv drog (2 ^ *), ki ni enakomeren, in enakomerno neprekinjena funkcija s pozitivno vrednostjo na ([0,1]), ki ima infimum enako 0; glej poglavji 5 in 6 Bridges & Richman [1987].

Berger in Ishihara [2005] sta ubrala drugačno, posredno pot do vzpostavitve enakovrednosti POS in FT (_ c). Vzpostavijo verigo enakovrednosti med POS, FT (_ c) in štirimi načeli tipa "če obstaja največ en predmet s lastnostjo (P), potem je en tak objekt". Štiri načela edinstvenega obstoja so:

CIN!: Vsako padajoče zaporedje naseljenih zaprtih ločenih podmnožic kompaktnega metričnega prostora z največ eno skupno točko ima naseljeno presečišče (Cantorjeva teorema o presečitvi z edinstvenostjo.) Upoštevajte, da je podmnožica (S) metričnega prostora ((X, / rho)) se nahaja, če obstaja za vsako (x) v (X) najmanjša razdalja od (x) do (S).

MIN!: Vsaka enakomerno neprekinjena funkcija z resnično vrednostjo na kompaktnem metričnem prostoru z največ eno minimalno točko ima minimalno točko.

WKL! Vsako neskončno drevo z največ eno neskončno vejo ima neskončno vejo (šibka Königova lema z edinstvenostjo).

POPRAVEK!: Vsaka enakomerno neprekinjena funkcija iz kompaktnega metričnega prostora v sebe z največ eno fiksno točko in s približno fiksnimi točkami ima fiksno točko.

Na primer, zadnji od teh, pravimo, da je zemljevid (f) metričnega prostora ((X, / varrho)) v sebi

  • ima največ eno fiksno točko, če (varrho (f (x), x) + / varrho (f (y), y) gt 0) kadar koli (varrho (x, y) gt 0);
  • ima približne fiksne točke, če za vsak (varepsilon / gt 0) obstaja (x / v X), tako da (varrho (f (x), x) lt / varepsilon).

Glavna odprta težava v CRM-u je iskanje oblike teoreme ventilatorja, ki je nad BISH enakovredna enotnemu izreku kontinuitete za ([0,1]), UCT (_ {[0,1]}): vsako točkovno neprekinjeno preslikavo ([0,1]) v (bR) je enakomerno neprekinjeno, predlog, za katerega je Brouwer prvotno razvil svoj dokaz o teoremih oboževalcev. (Upoštevajte, da je UCT (_ {[0,1]}) v primerjavi z BISH enakovredna splošni enotni izrek kontinuitete za metrične prostore: Vsako natančno neprekinjeno preslikavo celotnega, popolnoma omejenega metričnega prostora v metrični prostor je enakomerno neprekinjeno. Glej na primer Loeb [2005].)

Iz rezultatov Bergerja [2006] izhaja, da je

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

Tudi Diener in Loeb (2008) sta to dokazala

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

Vendar ne vemo, ali lahko katero koli od teh posledic nadomestimo z dvopomenko. Morda je UCT (_ {[0,1]}) in s tem polna enotna izrek o kontinuiteti za kompaktne metrične prostore enakovredna BISH-u nekakšni naravni, vendar še neidentificirani različici teorema ventilatorja.

Za dodatno gradivo o teorem ventilatorjev konstruktivne povratne matematike glej na primer Berger & Bridges [2007]; Diener [2008, 2012]; Diener & Loeb [2009]; in Diener & Lubarsky [2014]. V Dentu [2013] obstaja jasen, čeprav zapleten diagram, ki prikazuje povezave med teoremi ventilatorjev, kontinuiteto in načeli ozaveščenosti (glej Drugi internetni viri).

Zainteresirani bralci lahko podrobneje obravnavajo temo konstruktivne povratne matematike v naslednjem dopolnilnem dokumentu:

Ishiharino načelo (BDN) in lastnost proti Speckerju

6. Konstruktivna algebra in topologija

Konstruktivni matematiki si prizadevajo, da bi svoja prizadevanja osredotočili na analitično področje, z velikim uspehom pričajo o bogastvu funkcionalnih analiz, ki so jih razvili v Bishopu [1967]. To ne pomeni, da je bila na primer algebra umaknjena od konstruktivnega podjetja: gradivo v monografiji Mines et al. [1986] je mogoče obravnavati kot pomembno algebrsko sogovornico konstruktivni analizi, ki jo je opravil Bishop. Precej pred kratkim sta Lombardi in Quitté [2011] objavila prvi obsežni del predlaganega dvo zvezka o konstruktivni algebri. Ker pa ne poznamo algebre in se zavedamo nevarnosti, da bo ta članek predolg za pozornost bralca, se odločimo, da o konstruktivni analizi ali algebri ne bomo razpravljali podrobneje; v naslednjem dodatnem dokumentu:obrnemo se na konstruktivno topologijo, ki opisuje nekaj precej različnih pristopov k tej temi:

Pristopi k konstruktivni topologiji

7. Konstruktivna matematična ekonomija in finance

Raziskave konstruktivne matematične ekonomije segajo v vrsto prispevkov o preferencah, uporabnosti in povpraševanju od leta 1982 dalje; glej Mostovi [1999]. Hendtlass [2013] je v svoji doktorski nalogi bistveno oslabil pogoje za obstoj funkcije povpraševanja; ustvaril je tudi obilico rezultatov teorije fiksnih točk in njenih aplikacij, zlasti k konstruktivizaciji dveh klasičnih dokazov obstoja ekonomskega ravnovesja.

Leta 2015 sta Berger in Svindland na Ludwig-Maximilians-Universität v Münchnu začela raziskovalni projekt konstruktivnih matematičnih financ. Prvi sta pokazala, da so temeljni izrek o določanju cen premoženja, ločitveni teorem o ločitvi in Markov princip konstruktivno enakovreden (Berger & Svindland [2016]). Njihovo novejše delo se je osredotočilo na to, kako zaobiti nekonstruktivnost klasičnega izrekanja ekstremnih vrednosti, da bi dokazali obstoj ekstremnih točk za funkcije ob prisotnosti celo razmeroma šibkih lastnosti konveksnosti (Berger & Svindland [2016a]). Njihov projekt nakazuje, da so matematične finance, tako kot matematična ekonomija, lahko bogat vir elegantnih, praktičnih konstruktivnih izrek.

8. Zaključne pripombe

Tradicionalna pot matematikov, ki želijo analizirati konstruktivno vsebino matematike, je tista, ki sledi klasični logiki; Da bi se izognili odločitvam, na primer, ali je resnično število enako 0, ki ga resnični računalnik ne more sprejeti, se mora matematik držati znotraj strogih algoritmičnih meja, kot so tiste, ki jih tvori rekurzivna teorija funkcij. Nasprotno pa pot, ki jo je opravil konstruktivni matematik, sledi intuicijski logiki, ki samodejno poskrbi za računsko nedopustne odločitve. Ta logika (skupaj z ustreznim teoretičnim okvirom za vrsto ali tip) zadostuje, da matematiko ohranja znotraj konstruktivnih meja. Tako ima matematik prosto delo v naravnem slogu analitika, algebraista (npr. Mines et al., 1988), geometra, topologa (npr. Bridges &Vîță [2011], prihajajoči Sambin) ali drug običajni matematik, pri čemer so edine omejitve omejene z intuicijsko logiko. Kot so pokazali Bishop in drugi, je tradicionalno prepričanje, ki ga je objavil Hilbert in še danes velja, da intuicijska logika postavlja omejitve, zaradi katerih razvoj resne matematike ni mogoč, očitno napačno: veliki deli globoke moderne matematike so lahko in imajo so bile proizvedene po povsem konstruktivnih metodah. Poleg tega je povezava med konstruktivno matematiko in programiranjem velika obljuba za prihodnjo implementacijo in razvoj abstraktne matematike na računalniku.tradicionalno prepričanje, ki ga je izrekel Hilbert in je še danes zelo razširjeno, da intuicijska logika nalaga takšne omejitve, da onemogoča razvoj resne matematike, je očitno napačno: veliki deli globoke moderne matematike so lahko nastali po povsem konstruktivnih metodah. Poleg tega je povezava med konstruktivno matematiko in programiranjem velika obljuba za prihodnjo implementacijo in razvoj abstraktne matematike na računalniku.tradicionalno prepričanje, ki ga je izrekel Hilbert in je še danes zelo razširjeno, da intuicijska logika nalaga takšne omejitve, da onemogoča razvoj resne matematike, je očitno napačno: veliki deli globoke moderne matematike so lahko nastali po povsem konstruktivnih metodah. Poleg tega je povezava med konstruktivno matematiko in programiranjem velika obljuba za prihodnjo implementacijo in razvoj abstraktne matematike na računalniku.povezava med konstruktivno matematiko in programiranjem veliko obeta za prihodnjo implementacijo in razvoj abstraktne matematike na računalniku.povezava med konstruktivno matematiko in programiranjem veliko obeta za prihodnjo implementacijo in razvoj abstraktne matematike na računalniku.

Bibliografija

Reference

  • Aberth, O., 1980, Računalniška analiza, New York: McGraw-Hill.
  • –––, 2001, Computable Calculus, New York: Academic Press.
  • Aczel, P., in Rathjen, M., 2001, Opombe k teoriji konstruktivnih množic (Poročilo št. 40), Stockholm: Institut Mittag-Leffler, Kraljevska švedska akademija znanosti.
  • Bauer, A., 2005, »Uresničljivost kot povezava med računalniško in konstruktivno matematiko«, Opombe predavanj za vadnico na satelitskem seminarju CCA2005, Kjoto, Japonska [dostopno na spletu].
  • Beeson, M., 1985, Temelji konstruktivne matematike, Heidelberg: Springer Verlag.
  • Berger, J., 2006, "Logična moč enotnega izrek kontinuitete", v Logičnih pristopih k računskim oviram, A. Beckmann, U. Berger, B. Löwe in JV Tucker (ur.), Heidelberg: Springer Verlag.
  • Berger, J., in Bridges, DS, 2007, "Fantovsko-teoretični ekvivalent antiteze Speckerjevega teorema", Zbornik kraljevskega nizozemskega matematičnega društva (Indagationes Mathematicae) (Indag. Math. NS), 18 (2): 195 –202.
  • –––, 2009, „Teorema ventilatorjev in enakomerno neprekinjene funkcije v kompaktnih intervalih s pozitivno vrednostjo“, New Zealand Journal of Mathematics, 38: 129–135.
  • Berger, J. in Ishihara, H., 2005, "Brouwerjev teorem oboževalcev in edinstven obstoj v konstruktivni analizi", Mathematical Logic Quarterly, 51 (4): 360–364.
  • Berger, J., in Schuster, PM, 2006, "Razvrščanje Dinovega izrek", Notre Dame Journal of Formal Logic, 47: 253–262.
  • Berger, J., in Svindland, G., 2016, "Teorem o hiperplanih, ločen temeljni izrek cen sredstev in Markov princip", Annals of Pure and Applied Logic, 167, 1161–1170.
  • –––, 2016a, „Konveksnost in konstruktivna infima“, Arhiv za matematično logiko, 55: 873–881
  • Bishop, E., 1967, Temelji konstruktivne analize, New York: McGraw-Hill.
  • –––, 1973, Shizofrenija v sodobni matematiki (Ameriška predavanja za kolokvij Ameriškega matematičnega društva), Missoula: Univerza v Montani; ponatisnjeno v Errett Bishop: Razmišljanja o njem in njegovih raziskavah, Ameriško matematično društvo Memoari 39.
  • Bishop, E. in Bridges, D., 1985, Konstruktivna analiza, (Grundlehren der mathematischen Wissenschaften, 279), Heidelberg: Springer Verlag.
  • Bourbaki, N., 1984, Éléments d'histoire des mathématiques, Pariz: Masson; Angleška izdaja, Elements of the History of Mathematics, J. Meldrum (trans), 2006, Berlin: Springer Verlag.
  • Mostovi, DS, 1999, "Konstruktivne metode v matematični ekonomiji", v Zeitschrift für Nationalökonomie (Dodatek), 8: 1–21.
  • Bridges, DS, in Diener, H., 2007, „Psevdokompaktnost [0, 1] je enakovredna izrekam enotne kontinuitete“, Journal of Symbolic Logic, 72 (4): 1379–1383.
  • Bridges, DS, in Richman, F., 1987, Sorte konstruktivne matematike, London Mathematical Society Lecture Notes 97, Cambridge: Cambridge University Press.
  • Mostovi, DS in Vîță, LS, 2006, Tehnike konstruktivne analize, Heidelberg: Springer Verlag.
  • –––, 2011, Naključnost in enotnost-A konstruktivni razvoj, Heidelberg: Springer Verlag
  • Brouwer, LEJ, 1907, Over de Grondslagen der Wiskunde, doktorska disertacija, Univerza v Amsterdamu; ponatisnil z dodatnim gradivom, D. van Dalen (ur.), avtor 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“, Zbornik kraljevskega nizozemskega matematičnega društva, 27: 189–193.
  • –––, 1924A, „Bemerkung zum Beweise der gleichmässigen Stetigkeit voller Funktionen“, Zbornik kraljevskega nizozemskega matematičnega društva, 27: 644–646.
  • Cederquist, J. in Negri, S., 1996, "Konstruktiven dokaz Heine-Borelovega izrekanja, ki pokriva formalne razloge", v Vrste za dokaze in programe (Lekcije za računalništvo, letnik 1158), 62–75, Berlin: Springer Verlag.
  • Constable, R. in sod., 1986, Izvajanje matematike s sistemom za razvoj dokazov Nuprl, Englewood Cliffs, NJ: Prentice-Hall.
  • Coquand, T., 1992, "intuicijski dokaz Thonoffovega teorema", Journal of Symbolic Logic, 57: 28–32.
  • –––, 2009, „Prostor vrednotenj“, Anali čiste in uporabne logike, 157: 97–109.
  • –––, 2016, „Teorija tipov“, Stanfordska enciklopedija filozofije (izdaja zima 2016), Edward N. Zalta (ur.), URL (= / lt) https://plato.stanford.edu/entries/ teorija vrst / (gt)
  • Coquand, T. in Spitters, B., 2009, “Integrali in vrednotenja”, Journal of Logic and Analysis, 1 (3): 1–22.
  • Coquand, T., Sambin, G., Smith, J., in Valentini, S., 2003, "Induktivno ustvarjene formalne topologije", Anali čiste in uporabne logike, 124: 71–106.
  • Curi, G., 2010, "O obstoju kompakiranja Stone-Čecha", Časopis za simbolično logiko, 75: 1137–1146.
  • Dent, JE, 2013, Anti-Specker lastnosti v konstruktivni obratni matematiki, dr. diplomsko delo, Univerza v Canterburyju, Christchurch, Nova Zelandija.
  • Diaconescu, R., 1975, "Aksiom izbire in dopolnjevanja", Zbornik Ameriškega matematičnega društva, 51: 176–178
  • Diener, H., 2008, Kompaktnost pod konstruktivnim pregledom, dr. diplomsko delo, Christchurch, Nova Zelandija: Univerza v Canterburyju.
  • –––, 2008a, „Splošna kompaktnost“, Matematična logika četrtletje, 51 (1): 49–57.
  • –––, 2012, „Prerazvrstitev antiteze Speckerjevega izrekanja“, Arhiv za matematično logiko, 51: 687–693.
  • Diener, H., in Loeb, I., 2009, "Slednje resničnih funkcij na [0, 1] v konstruktivni obratni matematiki", Anali čiste in uporabne logike, 157 (1): 50–61.
  • Diener, H. in Lubarsky, R., 2013, "Ločevanje teorema ventilatorja in njegovih oslabitev", v Logičnih temeljih računalništva (Lectures Notes of Computer Science, 7734), S. Artemov in A. Nerode (ur.), Berlin: Springer Verlag.
  • Dummett, Michael, 1977 [2000], Elementi intuicijma (Oxford Logic Guides, 39), Oxford: Clarendon Press, 1977; 2. izdaja, 2000. [Stran se sklicuje na 2. izdajo.]
  • Ewald, W., 1996, Od Kanta do Hilberta: Izvorna knjiga v osnovah matematike (zvezek 2), Oxford: Clarendon Press.
  • Feferman, S, 1975, "Jezik in aksiomi za eksplicitne matematike", v Algebri in Logitu, JN Crossley (ur.), Heidelberg: Springer Verlag, str. 87–139.
  • –––, 1979, „Konstruktivne teorije funkcij in razredov“, v Logic Colloquium '78, M. Boffa, D. van Dalen in K. McAloon (ur.), Amsterdam: Severna Holandija, str. 159–224.
  • Friedman, H., 1975, "Nekateri sistemi aritmetike drugega reda in njihova uporaba", v Zborniku 17. mednarodnega kongresa matematikov, Vancouver, BC, 1974.
  • –––, 1977, „Postavite teoretične temelje za konstruktivno analizo“, Annals of Mathematics, 105 (1): 1–28.
  • Goodman, ND, in Myhill, J., 1978, „Izbirni implici izključujejo sredino“, Zeitschrift für Logik und Grundlagen der Mathematik, 24: 461.
  • Hayashi, S. in Nakano, H., 1988, PX: Računalniška logika, Cambridge MA: MIT Press.
  • Hendtlass, M., 2013, Izdelava fiksnih točk in ekonomskih ravnotežij, dr. diplomsko delo, Univerza v Leedsu.
  • Heyting, A., 1930, "Die formalen Regeln der intuitionistischen Logik", Sitzungsberichte der Preussische Akadademie der Wissenschaften. Berlin, 42–56.
  • –––, 1971, Intucionizem - uvod, 3. izdaja, Amsterdam: Severna Holandija.
  • Hilbert, D., 1925, „Über das Unendliche“, Mathematische Annalen, 95: 161–190; prevod, "In the Infinite", E. Putnam in G. Massey, iz filozofije matematike: izbrana branja, P. Benacerraf in H. Putnam (ur.), Englewood Cliffs, NJ: Prentice Hall, 1964, 134–151.
  • Hurewicz, W., 1958, Predavanja o navadnih diferencialnih enačbah, Cambridge, MA: MIT Press.
  • Ishihara, H., 1992, "lastnosti neprekinjenosti v konstruktivni matematiki", Journal of Symbolic Logic, 57 (2): 557–565.
  • –––, 1994, „Konstruktivna različica Banachovega teorema o obratnem preslikavi“, New Zealand Journal of Mathematics, 23: 71–75.
  • –––, 2005, „Konstruktivna obratna matematika: lastnosti kompaktnosti“, v Od sklopov in vrst do analiz in topologije: Do izvedljivih temeljev za konstruktivno matematiko, L. Crosilla in P. Schuster (ur.), Oxford: The Clarendon Press.
  • –––, 2006, „Povratna matematika v Bishopovi konstruktivni matematiki“, Philosophia Scientiae (Cahier Special), 6: 43–59.
  • –––, 2013, „Povezava škofovih funkcijskih prostorov s sosednjimi prostori“, Anali čiste in uporabne logike, 164: 482–490.
  • Johnstone, PT, 1982, Stone Spaces, Cambridge: Cambridge University Press.
  • –––, 2003, „Smisel nesmiselne topologije“, Bilten Ameriškega matematičnega društva, 8: 41–53.
  • Joyal, A. in Tierney, M., 1984, "Razširitev Galoisove teorije Grothendiecka", Memoirs of American Mathematical Society, 309: 85 str.
  • Julian, WH, in Richman, F., 1984, "Enakomerno neprekinjena funkcija na [0, 1], ki je povsod drugačna od njenega povprečja", Pacific Journal of Mathematics, 111: 333–340.
  • Kushner, B., 1985, Predavanja o konstruktivni matematični analizi, Providence, RI: American Mathematical Society
  • Lietz, P., 2004, od konstruktivne matematike do računalniške analize s pomočjo interpretacijske sposobnosti, dr. Rer. nat disertacija, Universität Darmstadt, Nemčija.
  • Lietz, P. in Streicher, T., „Modeli uresničljivosti, ki zavračajo načelo omejenosti Ishihara“, Anali čiste in uporabne logike, 163 (12): 1803–1807.
  • Loeb, I., 2005, "Ekvivalenti (šibkega) teorema oboževalcev", Anali čiste in uporabne logike, 132: 51–66.
  • Lombardi, H., Quitté, C., 2011, Algèbre Commutative. Konstrukcije Méthodes, Nanterre, Francija: Calvage et Mounet.
  • Lorenzen, P., 1955, Einführung in die operative Logik und Mathematik (Grundlehren der mathematischen Wissenschaften, letnik 78), 2. izdaja, 1969, Heidelberg: Springer.
  • Lubarsky, R., in Diener, H., 2014, “Ločevanje teorema ventilatorja in njegovih oslabitev”, Journal of Symbolic Logic, 79 (3): 792–813.
  • Markov, AA, 1954, Teorija algoritmov, Trudy Mat. Istituta imeni VA Steklova, 42 let, Moskva: Izdatel'stvo Akademii Nauk SSSR.
  • Marquis, J.-P., "Teorija kategorij", Stanfordska enciklopedija filozofije (izdaja zima 2015), Edward N. Zalta (ur.), URL (= / lt) https://plato.stanford.edu / arhivi / win2015 / vnosi / teorija kategorij / (gt).
  • Martin-Löf, P., 1968, Opombe o konstruktivni analizi, Stockholm: Almquist & Wiksell.
  • –––, 1975, „Intuitionistična teorija vrst: predikativni del“, v Logic Colloquium 1973, HE Rose in JC Shepherdson (ur.), Amsterdam: Severna Holandija.
  • –––, 1980, „Konstruktivna matematika in računalniško programiranje“, v Proc. 6. Int. Kongres za logiko, metodologijo in filozofijo znanosti, L. Jonathan Cohen (ur.), Amsterdam: Severna Holandija.
  • –––, 1984, intuicionistična teorija tipa, Opombe Giovannija Sambina o številnih predavanjih iz Padove, junij 1980, Neapelj: Bibliopolis.
  • –––, 2006, „100 let Aksioma izbire Zermelo: kaj je bilo s tem težavo?“, Computer Journal, 49 (3): 345–350.
  • Menger, K., 1940, „Topologija brez točk“, Rice Institute Pamphlet, 27 (1): 80–107 [dostopno na spletu].
  • Mines, R., Richman, F. in Ruitenburg, W., 1988, Tečaj konstruktivne algebre, Universitext, Heidelberg: Springer Verlag.
  • Moerdijk, I., 1984, "Heine-Borel ne pomeni teorema ventilatorjev", Journal of Symbolic Logic, 49 (2): 514–519.
  • Moore, GH, 2013, Aksiom izbire Zermelo: njeni izvori, razvoj in vpliv, New York: Dover.
  • Myhill, J., 1973, "Nekaj lastnosti intuicijske teorije zermelo-Fraenkel", v Cambridgeovi poletni šoli za matematično logiko, A. Mathias in H. Rogers (ur.), Opombe predavanj iz matematike, 337, Heidelberg: Springer Verlag, 206-231.
  • –––, 1975, „Teorija konstruktivne množice“, Časopis za simbolično logiko, 40 (3): 347–382.
  • Naimpally, S., 2009, Bližnji pristop k problemom topologije in analize, München: Oldenbourg Verlag.
  • Naimpally, S., in Warrack, BD, 1970, Proximity Spaces (Cambridge Tracts in Math. And Math. Phys., Letnik 59), Cambridge: Cambridge University Press.
  • Nordström, B., Peterson, K., in Smith, JM, 1990, »Programiranje v teoriji Martina-Löfa«, Oxford: Oxford University Press.
  • Palmgren, E., 2007, „Konstruktivno in funkcionalno vdelavo lokalno kompaktnih metričnih prostorov v kraje“, Topologija in njene aplikacije, 154: 1854–1880.
  • –––, 2008, „Reševanje enotnega problema spodnje meje v konstruktivni analizi“, četrtletje Matematična logika, 54: 65–69.
  • –––, 2009, „Od intuicijske do formalne topologije: nekatere opombe o temeljih teorije homotopije“, v: Logika, intuicij in formalizem - kaj se je od njih zgodilo?, S. Lindström, E. Palmgren, K. Segerberg in V. Stoltenberg-Hansen (ur.), 237–253, Berlin: Springer Verlag.
  • Petrakis, I., 2016, „Konstruktivni teoretsko-teoretični pristop k topološki kompaktnosti“, v Logičnih metodah v računalništvu 2016, IEEE Publikacije Computer Society: 605–614.
  • –––, 2016a, „Urysohnova podaljševalna teorema za škofovske prostore“, S. Artemov in A. Nerode (ur.), Simpozij o logičnih temeljih računalništva 2016 (Predavanja v računalništvu 9537), Berlin: Springer Verlag, 299–316.
  • Picado, J. in Pultr, A., 2011, Okviri in lokale: Topologija brez točk, Basel: Birkhäuser Verlag.
  • Richman, F., 1983, "Cerkvena teza brez solz", Journal of Symbolic Logic, 48: 797–803.
  • –––, 1990, „Intuicionizem kot posplošitev“, Philosophia Mathematica, 5: 124–128.
  • –––, 1996, „Intervju s konstruktivnim matematikom“, Moderna logika, 6: 247–271.
  • –––, 2000, „Temeljni teorem algebre: konstruktivno zdravljenje brez izbire“, Pacific Journal of Mathematics, 196: 213–230.
  • Riesz, F., 1908, "Stetigkeitsbegriff und abstrakte Mengenlehre", Atti IV Kongresni internacionali Matematica Roma II, 18–24.
  • Sambin, G., 1987, „Intuitionistični formalni prostori - prva komunikacija“, v Matematični logiki in njenih aplikacijah, D. Skordev (ur.), 187–204, New York: Plenum Press.
  • –––, prihajajoča, Osnovna slika: Strukture za konstruktivno topologijo, Oxford: Oxford University Press.
  • Sambin, G. in Smith, J. (ur.), 1998, Petindvajset let teorije konstruktivnega tipa, Oxford: Clarendon Press.
  • Schuster, PM, 2005, "Kaj je kontinuiteta konstruktivno?", Journal of Universal Computer Science, 11: 2076–2085
  • –––, 2006, „Formalna Zariska topologija: pozitivnost in točke“, Anali čiste in uporabne logike, 137: 317–359.
  • Schwichtenberg, H., 2009, "Programski izvleček v konstruktivni analizi", v logiki, intuicijstvu in formalizmu - kaj se je od njih zgodilo?, S. Lindström, E. Palmgren, K. Segerberg in V. Stoltenberg-Hansen (ur.), Berlin: Springer Verlag, 255–275.
  • Simpson, SG, 1984, "Kateri aksiomi obstoja so potrebni za dokazovanje teorema Cauchy / Peano za navadne diferencialne enačbe", Journal of Symbolic Logic, 49 (3): 783–802.
  • –––, 2009, Podsistem Aritmetika drugega reda, druga izdaja, Cambridge: Cambridge University Press.
  • Specker, E., 1949, "Nicht konstruktiv beweisbare Sätze der Analysis", Časopis za simbolično logiko, 14: 145–158.
  • Steinke, TA, 2011, Konstruktivne predstave o kompaktnosti v apartmajskih prostorih, mag. Diplomsko delo, Univerza v Canterburyju, Christchurch, Nova Zelandija.
  • Troelstra, AS, 1978, "Aspekti konstruktivne matematike", v priročniku matematične logike, J. Barwise (ur.), Amsterdam: North-Holland.
  • Troelstra, AS, in van Dalen, D., 1988, Konstruktivizem v matematiki: uvod (dva zvezka), Amsterdam: Severna Holandija.
  • van Atten, M., 2004, On Brouwer, Belmont: Wadsworth / Thomson Learning.
  • van Dalen, D., 1981, Brouwer's Cambridge Lectures on Intuitionism, Cambridge: Cambridge University Press.
  • –––, 1999, Mystic, Geometer and Intuitionist: The Life of LEJ Brouwer (zvezek 1), Oxford: Clarendon Press.
  • –––, 2005, Mystic, Geometer in Intuitionist: Življenje LEJ Brouwer (zvezek 2), Oxford: Clarendon Press.
  • van Stigt, WP, 1990, Brouwerjev intuicij, Amsterdam: Severna Holandija.
  • Vickers, S., 2005, "Lokalno dokončanje posplošenih metričnih prostorov I", Teorija in aplikacije kategorij, 14 (15): 328–356.
  • Waaldijk, F., 2005, Na temeljih konstruktivne matematike, Temelji znanosti, 10 (3): 249–324.
  • Wallman, H., 1938, „rešetke topoloških prostorov“, Annals of Mathematics, 39: 112–126.
  • Weihrauch, K., 2000, Računalniška analiza (EATCS Besedila v teoretični računalništvu), Heidelberg: Springer Verlag.
  • Weyl, H., 1946, "Matematika in logika", Ameriški matematični mesečnik, 53 (1): 2–13.
  • Whitehead, AN, 1919, Povpraševanje o načelih naravnega znanja, Cambridge: Cambridge University Press, druga izdaja, 1925.

Sorodna literatura

  • Heijenoort, Jean van, 1967, Od Fregea do Gödela: Izvorna knjiga v matematični logiki 1879–1931, Cambridge, MA: Harvard University Press.
  • Hilbert, David, 1928, "Die Grundlagen der Mathematik", Hamburger Mathematische Einzelschriften 5, Teubner, Leipzig. Ponatisnjeno v angleškem prevodu v van Heijenoort 1967.

Akademska orodja

sep man ikona
sep man ikona
Kako navajati ta vnos.
sep man ikona
sep man ikona
Predogled PDF različice tega vnosa pri Društvu prijateljev SEP.
ikona
ikona
Poiščite to temo vnosa pri projektu Internet Filozofija Ontologija (InPhO).
ikona papirjev phil
ikona papirjev phil
Izboljšana bibliografija za ta vnos pri PhilPapers s povezavami do njegove baze podatkov.

Drugi internetni viri

  • Agda Wiki, vtipkan funkcionalni programski jezik in docent, Univerza Göteborg in Tehnološka univerza Chalmers.
  • Agda, vpis v Wikipedijo.
  • Pomočnik za dokazovanje Coq, Inria, 1984–2017.
  • Coq, vpis v Wikipedijo.
  • Diagram Jamesa Denta.
  • Aczel, P. in Rathjen, M., 2018, Teorija konstruktivnih nizov, spletni PDF.
  • Bauer, A., 2005, „Uresničljivost kot povezava med računalniško in konstruktivno matematiko“.
  • Veldman, W., 2014, “Brouwerjeva teorema oboževalcev kot aksiom in kot kontrast Kleenovi alternativi”, arxiv: 1106.2738https://arxiv.org/abs/1106.2738.

Priporočena: