| Prethodna tema :: Sljedeća tema |
| Autor/ica |
Poruka |
Melkor
Forumaš(ica)
Pridružen/a: 07. 10. 2004. (18:48:00)
Postovi: (291)16
Spol: 
Lokacija: Void
|
 Postano: 13:54 pet, 13. 9. 2013 Naslov: Five Stages of Accepting Constructive Mathematics |
    |
|
|
U moje vrijeme je, ako se dobro sjećam, na jednom od prvih predavanja Elementarne matematike 1 prezentiran tzv. [b]princip[/b] ili [b]zakon isključenja trećega[/b]:
[i]Za svaku propoziciju [tex]P[/tex] vrijedi [tex]P\vee \lnot P[/tex].[/i]
Sva daljnja matematika na studiju izgrađena je uz pretpostavku tog zakona. Npr. svaki dokaz kontradikcijom implicitno koristi zakon isključenja trećega: "Pretpostavimo da propozicija P nije istinita. Tada ..., što je kontradikcija. Dakle, P je istinita."
No, što ako odbacimo zakon isključenja trećega? Mnogi rezultati koje smo naučili na studiju prestaju vrijediti. Neki od takvih rezultata su:
[list]
[*]Svaki podskup konačnog skupa je konačan.
[*]Svaki vektorski prostor ima bazu.
[*]Ne postoji injekcija iz [tex]\mathbb{R}[/tex] u [tex]\mathbb{N}[/tex].
[/list:u]
Ima li matematika bez zakona isključenja trećega ipak smisla? [b]Andrej Bauer[/b] vas u svom predavanju [b]Five Stages of Accepting Constructive Mathematics[/b] vodi kroz pet emocionalnih stanja kroz koja ćete, kao matematičari s klasičnim obrazovanjem, proći suočeni svijetom bez tog zakona: poricanje, bijes, cjenkanje, depresija i prihvaćanje.
[url]http://video.ias.edu/members/1213/0318-AndrejBauer[/url]
U moje vrijeme je, ako se dobro sjećam, na jednom od prvih predavanja Elementarne matematike 1 prezentiran tzv. princip ili zakon isključenja trećega:
Za svaku propoziciju [tex]P[/tex] vrijedi [tex]P\vee \lnot P[/tex].
Sva daljnja matematika na studiju izgrađena je uz pretpostavku tog zakona. Npr. svaki dokaz kontradikcijom implicitno koristi zakon isključenja trećega: "Pretpostavimo da propozicija P nije istinita. Tada ..., što je kontradikcija. Dakle, P je istinita."
No, što ako odbacimo zakon isključenja trećega? Mnogi rezultati koje smo naučili na studiju prestaju vrijediti. Neki od takvih rezultata su:
- Svaki podskup konačnog skupa je konačan.
- Svaki vektorski prostor ima bazu.
- Ne postoji injekcija iz [tex]\mathbb{R}[/tex] u [tex]\mathbb{N}[/tex].
Ima li matematika bez zakona isključenja trećega ipak smisla? Andrej Bauer vas u svom predavanju Five Stages of Accepting Constructive Mathematics vodi kroz pet emocionalnih stanja kroz koja ćete, kao matematičari s klasičnim obrazovanjem, proći suočeni svijetom bez tog zakona: poricanje, bijes, cjenkanje, depresija i prihvaćanje.
http://video.ias.edu/members/1213/0318-AndrejBauer
_________________
I don't know half of you half as well as I should like; and I like less than half of you half as well as you deserve.
|
|
| [Vrh] |
|
krcko
Forumaš nagrađen za životno djelo
Pridružen/a: 07. 10. 2002. (15:57:59)
Postovi: (18B3)16
|
|
| [Vrh] |
|
Melkor
Forumaš(ica)
Pridružen/a: 07. 10. 2004. (18:48:00)
Postovi: (291)16
Spol:
Lokacija: Void
|
| Postano: 13:15 sub, 14. 9. 2013 Naslov: Re: Five Stages of Accepting Constructive Mathematics |
|
|
|
[quote="krcko"][quote="Melkor"]Mnogi rezultati koje smo naučili na studiju prestaju vrijediti.[/quote]
Ako dokaz na koji smo navikli nije konstruktivan, ili ako se uopće ne može dokazati konstruktivno, to ne znači da je rezultat prestao vrijediti. Znači samo da ga ne znamo dokazati.[/quote]
Naravno, postoje teoremi dokazani nekonstruktivno za koje postoje konstruktivni dokazi. No, situacija s tvrdnjama o kojima govorim je drukčija. Situacija je analogna onoj s ne-euklidskim geometrijama. Ako odbacimo Euklidov peti aksiom, onda nije samo da više ne znamo dokazati da je zbroj kutova u trokutu 180°, već postoje modeli geometrije (npr. sferna ili hiperbolička geometrija) u kojima zbroj kutova u trokutu može biti različit od 180°. Tako je i s tvrdnjama koje sam naveo. Ako odbacimo zakon isključenja trećega, onda uz klasičnu matematiku (koja odgovara euklidskoj geometriji) dobijemo i druge matematike (koje odgovaraju ne-euklidskim geometrijama) u kojima konačan skup može imati beskonačan podskup, vektorski prostor ne mora imati bazu, sve funkcije mogu biti neprekidne (čak i glatke), sve funkcije mogu biti izračunljive itd.
| krcko (napisa): | | Melkor (napisa): | | Mnogi rezultati koje smo naučili na studiju prestaju vrijediti. |
Ako dokaz na koji smo navikli nije konstruktivan, ili ako se uopće ne može dokazati konstruktivno, to ne znači da je rezultat prestao vrijediti. Znači samo da ga ne znamo dokazati. |
Naravno, postoje teoremi dokazani nekonstruktivno za koje postoje konstruktivni dokazi. No, situacija s tvrdnjama o kojima govorim je drukčija. Situacija je analogna onoj s ne-euklidskim geometrijama. Ako odbacimo Euklidov peti aksiom, onda nije samo da više ne znamo dokazati da je zbroj kutova u trokutu 180°, već postoje modeli geometrije (npr. sferna ili hiperbolička geometrija) u kojima zbroj kutova u trokutu može biti različit od 180°. Tako je i s tvrdnjama koje sam naveo. Ako odbacimo zakon isključenja trećega, onda uz klasičnu matematiku (koja odgovara euklidskoj geometriji) dobijemo i druge matematike (koje odgovaraju ne-euklidskim geometrijama) u kojima konačan skup može imati beskonačan podskup, vektorski prostor ne mora imati bazu, sve funkcije mogu biti neprekidne (čak i glatke), sve funkcije mogu biti izračunljive itd.
_________________
I don't know half of you half as well as I should like; and I like less than half of you half as well as you deserve.
|
|
| [Vrh] |
|
krcko
Forumaš nagrađen za životno djelo
Pridružen/a: 07. 10. 2002. (15:57:59)
Postovi: (18B3)16
|
|
| [Vrh] |
|
Melkor
Forumaš(ica)
Pridružen/a: 07. 10. 2004. (18:48:00)
Postovi: (291)16
Spol:
Lokacija: Void
|
| Postano: 14:29 čet, 26. 9. 2013 Naslov: |
|
|
|
Bio sam neoprezan kad sam rekao [b]beskonačan[/b] podskup. Trebao sam reći podskup koji [b]nije konačan[/b].
Kad se odbaci zakon isključenja trećega, mnogi pojmovi koji su klasično ekvivalentni postaju različiti. Tako je potreban oprez pri definiciji konačnog i beskonačnog skupa. Koliko sam uspio shvatiti surfajući, definicija konačnog skupa koja se dobro ponaša i klasično i konstruktivno je definicija Kuratowski-konačnog skupa: Skup S je konačan ako postoji surjekcija s [tex][n]=\{k\in\mathbb{N}\mid k<n\}[/tex] na S. S druge strane, skup S je beskonačan ako postoji injekcija iz [tex]\mathbb{N}[/tex] u S. Uz takve definicije više nije jasno je li ekvivalentno biti beskonačan i ne biti konačan.
Uglavnom, teorem koji sam spomenuo u prvom postu, a više se ne može dokazati konstruktivno je sljedeći: Svaki podskup konačnog skupa je konačan. Nazovimo tu tvrdnju [i]konačnost podskupova[/i]. Ako tražiš model u kojem konačnost podskupova ne vrijedi, ključan pojam je [b]efektivni topos[/b]. Nažalost, ne znam dovoljno teorije kategorija i teorije toposa da samo tako raspišem o čemu se radi.
Ono što mogu pokazati je da konačnost podskupova povlači zakon isključenja trećega. Naime, pretpostavimo konačnost podskupova i neka je [tex]P[/tex] proizvoljna propozicija. Definiramo [tex]S=\{k\in [1]\mid P\}[/tex]. Kao podskup konačnog skupa, [tex]S[/tex] je konačan. Prema tome, postoji [tex]n\in\mathbb{N}[/tex] i surjekcija [tex]f\colon [n]\to S[/tex]. Ako je [tex]n=0[/tex], [tex]S[/tex] je prazan, kao slika praznog skupa. No, tada vrijedi [tex]\lnot P[/tex]. Ako je pak [tex]n\neq 0[/tex], [tex]S[/tex] sadrži [tex]f(0)[/tex]. U tom slučaju vrijedi [tex]P[/tex].
Budući da je konačnost podskupova teorem u klasičnoj matematici, dakle implicirana je zakonom isključenja trećega, vidimo da su te dvije tvrdnje ekvivalentne.
Bio sam neoprezan kad sam rekao beskonačan podskup. Trebao sam reći podskup koji nije konačan.
Kad se odbaci zakon isključenja trećega, mnogi pojmovi koji su klasično ekvivalentni postaju različiti. Tako je potreban oprez pri definiciji konačnog i beskonačnog skupa. Koliko sam uspio shvatiti surfajući, definicija konačnog skupa koja se dobro ponaša i klasično i konstruktivno je definicija Kuratowski-konačnog skupa: Skup S je konačan ako postoji surjekcija s [tex][n]=\{k\in\mathbb{N}\mid k<n\}[/tex] na S. S druge strane, skup S je beskonačan ako postoji injekcija iz [tex]\mathbb{N}[/tex] u S. Uz takve definicije više nije jasno je li ekvivalentno biti beskonačan i ne biti konačan.
Uglavnom, teorem koji sam spomenuo u prvom postu, a više se ne može dokazati konstruktivno je sljedeći: Svaki podskup konačnog skupa je konačan. Nazovimo tu tvrdnju konačnost podskupova. Ako tražiš model u kojem konačnost podskupova ne vrijedi, ključan pojam je efektivni topos. Nažalost, ne znam dovoljno teorije kategorija i teorije toposa da samo tako raspišem o čemu se radi.
Ono što mogu pokazati je da konačnost podskupova povlači zakon isključenja trećega. Naime, pretpostavimo konačnost podskupova i neka je [tex]P[/tex] proizvoljna propozicija. Definiramo [tex]S=\{k\in [1]\mid P\}[/tex]. Kao podskup konačnog skupa, [tex]S[/tex] je konačan. Prema tome, postoji [tex]n\in\mathbb{N}[/tex] i surjekcija [tex]f\colon [n]\to S[/tex]. Ako je [tex]n=0[/tex], [tex]S[/tex] je prazan, kao slika praznog skupa. No, tada vrijedi [tex]\lnot P[/tex]. Ako je pak [tex]n\neq 0[/tex], [tex]S[/tex] sadrži [tex]f(0)[/tex]. U tom slučaju vrijedi [tex]P[/tex].
Budući da je konačnost podskupova teorem u klasičnoj matematici, dakle implicirana je zakonom isključenja trećega, vidimo da su te dvije tvrdnje ekvivalentne.
_________________
I don't know half of you half as well as I should like; and I like less than half of you half as well as you deserve.
|
|
| [Vrh] |
|
Melkor
Forumaš(ica)
Pridružen/a: 07. 10. 2004. (18:48:00)
Postovi: (291)16
Spol:
Lokacija: Void
|
| Postano: 10:18 uto, 11. 10. 2016 Naslov: |
|
|
|
Sada postoji i Andrejev članak Five stages of accepting constructive mathematics, objavljen u Bulletin of the AMS. Članak je besplatno dostupan svima.
[url]http://dx.doi.org/10.1090/bull/1556[/url]
Između ostalog, u članku je dodatno osvijetljena i tvrdnja o konačnosti podskupova konačnoga skupa. Konkretno, dan je model matematike u kojem ta tvrdnja ne vrijedi — model [i]ostvarljivosti[/i] (engl. [i]realizability[/i]). U tom modelu tvrdnja je istinita ako za nju postoji program koji je ostvaruje. Tvrdnja oblika [tex]\forall x\in A.\,P(x)[/tex] ostvarena je programom koji kao ulaz prima [tex]a\in A[/tex], a kao izlaz daje ostvaritelja tvrdnje [tex]P(a)[/tex].
Pokažimo da u ovom modelu ne samo da ne vrijedi konačnost podskupova, nego ne vrijedi ni specijalnija tvrdnja: Svaki prebrojiv podskup skupa [tex]\{0,1\}[/tex] je konačan.
Prebrojiv skup [tex]S[/tex] u ovom modelu reprezentiran je programom koji ostvaruje surjekciju [tex]f\colon\mathbb{N}\to S[/tex]. Taj program možemo jednostavno shvatiti kao prebrojivo beskonačnu listu elemenata iz [tex]S[/tex] s dozvoljenim ponavljanjem. Slično tome, konačan skup [tex]S[/tex] reprezentiran je programom koji ostvaruje surjekciju [tex]f\colon [n]\to S[/tex] za neki [tex]n\in\mathbb{N}[/tex], što je ništa drugo nego konačna lista elemenata iz [tex]S[/tex] s dozvoljenim ponavljanjem.
Specijalna tvrdnja koju želimo ostvariti je oblika [tex]\forall x\in A.\,P(x)[/tex] pa tražimo program koji preslikava prebrojiv podskup od [tex]\{0,1\}[/tex] u konačan podskup s istim elementima. Drugim riječima, tražimo program koji će uzeti prebrojivo beskonačnu listu elemenata iz [tex]\{0,1\}[/tex] i pretvoriti je u konačnu listu s istim elementima.
Problem se javlja kad uzmemo listu [tex]0,0,0,0,\ldots[/tex] Koji god konačan prefiks program uzme, ne može znati da se kasnije neće pojaviti [tex]1[/tex]. Analogno je s listom [tex]1,1,1,1,\ldots[/tex].
Dokaz da ne postoji ostvaritelj specijalne tvrdnje ide redukcijom s Halting problema: pretpostavimo da postoji program [tex]q[/tex] koji ostvaruje specijalnu tvrdnju i konstruiramo program koji rješava Halting problem. Neka je [tex]T[/tex] Turingov stroj i [tex]n[/tex] ulaz za [tex]T[/tex]. Definiramo program [tex]p\colon\mathbb{N}\to\{0,1\}[/tex] na sljedeći način:
[tex]\displaystyle p(k)=
\begin{cases}
1\quad T(n)\text{ staje u najviše }k\text{ koraka} \\
0\quad \text{inače}
\end{cases}
[/tex]
Program [tex]p[/tex] predstavlja prebrojiv podskup od [tex]\{0,1\}[/tex] i ulaz je za [tex]q[/tex]. Izlaz [tex]q(p)[/tex] je konačna lista elemenata iz [tex]\{0,1\}[/tex]. Ako lista sadrži [tex]1[/tex], [tex]T(n)[/tex] staje, inače ne staje.
U članku se spominju i drugi teoremi koji vrijede u klasičnoj matematici, a ne vrijede u konstruktivnoj: teorem o srednjoj vrijednosti i teorem Tychonoffa o produktu kompaktnih prostora. No pokazuje se da je u prvom slučaju dovoljno iskazati teorem u drugom (klasično ekvivalentnom) obliku, a u drugom slučaju redefinirati pojam topološkog prostora, da bi rezultati vrijedili i konstruktivno.
Uglavnom, vrlo zanimljivo. Preporučujem!
Sada postoji i Andrejev članak Five stages of accepting constructive mathematics, objavljen u Bulletin of the AMS. Članak je besplatno dostupan svima.
http://dx.doi.org/10.1090/bull/1556
Između ostalog, u članku je dodatno osvijetljena i tvrdnja o konačnosti podskupova konačnoga skupa. Konkretno, dan je model matematike u kojem ta tvrdnja ne vrijedi — model ostvarljivosti (engl. realizability). U tom modelu tvrdnja je istinita ako za nju postoji program koji je ostvaruje. Tvrdnja oblika [tex]\forall x\in A.\,P(x)[/tex] ostvarena je programom koji kao ulaz prima [tex]a\in A[/tex], a kao izlaz daje ostvaritelja tvrdnje [tex]P(a)[/tex].
Pokažimo da u ovom modelu ne samo da ne vrijedi konačnost podskupova, nego ne vrijedi ni specijalnija tvrdnja: Svaki prebrojiv podskup skupa [tex]\{0,1\}[/tex] je konačan.
Prebrojiv skup [tex]S[/tex] u ovom modelu reprezentiran je programom koji ostvaruje surjekciju [tex]f\colon\mathbb{N}\to S[/tex]. Taj program možemo jednostavno shvatiti kao prebrojivo beskonačnu listu elemenata iz [tex]S[/tex] s dozvoljenim ponavljanjem. Slično tome, konačan skup [tex]S[/tex] reprezentiran je programom koji ostvaruje surjekciju [tex]f\colon [n]\to S[/tex] za neki [tex]n\in\mathbb{N}[/tex], što je ništa drugo nego konačna lista elemenata iz [tex]S[/tex] s dozvoljenim ponavljanjem.
Specijalna tvrdnja koju želimo ostvariti je oblika [tex]\forall x\in A.\,P(x)[/tex] pa tražimo program koji preslikava prebrojiv podskup od [tex]\{0,1\}[/tex] u konačan podskup s istim elementima. Drugim riječima, tražimo program koji će uzeti prebrojivo beskonačnu listu elemenata iz [tex]\{0,1\}[/tex] i pretvoriti je u konačnu listu s istim elementima.
Problem se javlja kad uzmemo listu [tex]0,0,0,0,\ldots[/tex] Koji god konačan prefiks program uzme, ne može znati da se kasnije neće pojaviti [tex]1[/tex]. Analogno je s listom [tex]1,1,1,1,\ldots[/tex].
Dokaz da ne postoji ostvaritelj specijalne tvrdnje ide redukcijom s Halting problema: pretpostavimo da postoji program [tex]q[/tex] koji ostvaruje specijalnu tvrdnju i konstruiramo program koji rješava Halting problem. Neka je [tex]T[/tex] Turingov stroj i [tex]n[/tex] ulaz za [tex]T[/tex]. Definiramo program [tex]p\colon\mathbb{N}\to\{0,1\}[/tex] na sljedeći način:
[tex]\displaystyle p(k)=
\begin{cases}
1\quad T(n)\text{ staje u najviše }k\text{ koraka} \\
0\quad \text{inače}
\end{cases}
[/tex]
Program [tex]p[/tex] predstavlja prebrojiv podskup od [tex]\{0,1\}[/tex] i ulaz je za [tex]q[/tex]. Izlaz [tex]q(p)[/tex] je konačna lista elemenata iz [tex]\{0,1\}[/tex]. Ako lista sadrži [tex]1[/tex], [tex]T(n)[/tex] staje, inače ne staje.
U članku se spominju i drugi teoremi koji vrijede u klasičnoj matematici, a ne vrijede u konstruktivnoj: teorem o srednjoj vrijednosti i teorem Tychonoffa o produktu kompaktnih prostora. No pokazuje se da je u prvom slučaju dovoljno iskazati teorem u drugom (klasično ekvivalentnom) obliku, a u drugom slučaju redefinirati pojam topološkog prostora, da bi rezultati vrijedili i konstruktivno.
Uglavnom, vrlo zanimljivo. Preporučujem!
_________________
I don't know half of you half as well as I should like; and I like less than half of you half as well as you deserve.
|
|
| [Vrh] |
|
|
