Konstruktywizm (filozofia matematyki)

Ten artykuł dotyczy poglądu w filozofii matematyki. Aby zapoznać się z innymi zastosowaniami tego terminu, zobacz Konstruktywizm .

W filozofii matematyki konstruktywizm twierdzi , że konieczne jest znalezienie (lub „skonstruowanie”) konkretnego przykładu obiektu matematycznego, aby udowodnić, że przykład istnieje. Z drugiej strony, w matematyce klasycznej można udowodnić istnienie obiektu matematycznego bez wyraźnego „znajdowania” tego obiektu, zakładając jego nieistnienie, a następnie wyprowadzając z tego założenia sprzeczność . Taki dowód przez sprzeczność można by nazwać niekonstruktywnym, a konstruktywista mógłby go odrzucić. Konstruktywny punkt widzenia obejmuje weryfikacyjną interpretację kwantyfikatora egzystencjalnego , co jest sprzeczne z jego klasyczną interpretacją.

Istnieje wiele form konstruktywizmu. Należą do nich program intuicjonizmu założony przez Brouwera , finityzm Hilberta i Bernaysa , konstruktywna matematyka rekurencyjna Shanina i Markowa oraz program konstruktywnej analizy Bishopa . Konstruktywizm obejmuje również badanie konstruktywnych teorii mnogości, takich jak CZF , oraz badanie teorii toposu .

Konstruktywizm jest często utożsamiany z intuicjonizmem, chociaż intuicjonizm jest tylko jednym z programów konstruktywistycznych. Intuicjonizm utrzymuje, że podstawy matematyki leżą w intuicji indywidualnego matematyka, czyniąc w ten sposób matematykę czynnością wewnętrznie subiektywną. Inne formy konstruktywizmu nie opierają się na tym intuicyjnym punkcie widzenia i są zgodne z obiektywnym punktem widzenia na matematykę.

Matematyka konstruktywna

Wiele konstruktywnej matematyki wykorzystuje logikę intuicjonistyczną , która jest zasadniczo logiką klasyczną bez prawa wyłączonego środka . Prawo to stwierdza, że ​​dla każdego zdania albo to zdanie jest prawdziwe, albo jego zaprzeczenie. Nie oznacza to, że całkowicie odrzuca się prawo wyłączonego środka; szczególne przypadki prawa będą możliwe do udowodnienia. Po prostu ogólne prawo nie jest przyjmowane jako aksjomat . Prawo niesprzeczności (które stwierdza, że ​​zdania sprzeczne nie mogą być jednocześnie prawdziwe) nadal obowiązuje.

Na przykład w arytmetyce Heytinga można udowodnić, że dla dowolnego zdania p , które nie zawiera kwantyfikatorów , ${\ Displaystyle \ forall x, y, z, \ ldots \ in \mathbb {N} :p\vee \neg p}$ jest twierdzeniem (gdzie x , y , z ... są wolnymi zmiennymi w zdaniu p ). W tym sensie zdania ograniczone do skończoności są nadal uważane za prawdziwe lub fałszywe, tak jak ma to miejsce w matematyce klasycznej, ale ta biwalencja nie rozciąga się na zdania odnoszące się do nieskończonych zbiorów.

W rzeczywistości LEJ Brouwer , założyciel szkoły intuicjonistycznej, postrzegał prawo wyłączonego środka jako wyabstrahowane ze skończonego doświadczenia, a następnie bez uzasadnienia stosowane do nieskończoności . Na przykład hipoteza Goldbacha polega na twierdzeniu, że każda liczba parzysta (większa niż 2) jest sumą dwóch liczb pierwszych . Możliwe jest przetestowanie dowolnej liczby parzystej, czy jest ona sumą dwóch liczb pierwszych (na przykład poprzez wyczerpujące wyszukiwanie), więc każda z nich jest albo sumą dwóch liczb pierwszych, albo nie. I jak dotąd każdy testowany w ten sposób był w rzeczywistości sumą dwóch liczb pierwszych.

Ale nie ma znanego dowodu na to, że wszystkie z nich tak są, ani żadnego znanego dowodu na to, że nie wszystkie z nich są takie; nie wiadomo nawet, czy dowód lub obalenie hipotezy Goldbacha (hipoteza może być nierozstrzygalna w tradycyjnej teorii mnogości ZF) . Tak więc dla Brouwera nie mamy prawa twierdzić, że „albo przypuszczenie Goldbacha jest prawdziwe, albo nie”. I chociaż hipoteza może kiedyś zostać rozwiązana, argument dotyczy podobnych nierozwiązanych problemów; dla Brouwera prawo wyłączonego środka było równoznaczne z założeniem, że każdy problem matematyczny ma rozwiązanie.

Z pominięciem prawa wyłączonego środka jako aksjomatu, pozostały system logiczny ma właściwość istnienia , której logika klasyczna nie ma: ilekroć $x)}$${\ Displaystyle \ istnieje _ {x \ w X}$$jest udowodnione konstruktywnie dla$$często$ konstruktywnie, to w rzeczywistości przynajmniej) jednego konkretnego świadkiem . . Zatem dowód istnienia obiektu matematycznego jest powiązany z możliwością jego konstrukcji.

Przykład z prawdziwej analizy

W klasycznej analizie rzeczywistej jednym ze sposobów definiowania liczby rzeczywistej jest klasa równoważności ciągów Cauchy'ego liczb wymiernych .

W matematyce konstruktywnej jednym ze sposobów konstruowania liczby rzeczywistej jest funkcja ƒ , która przyjmuje dodatnią liczbę $i$ wyprowadza liczbę wymierną ƒ ( n ), razem z funkcją g , która przyjmuje dodatnią liczbę całkowitą n i wyprowadza a dodatnia liczba całkowita g ( n ) taka, że

${\ Displaystyle \ forall n \ \ forall i, j \ geq g (n) \ quad | f (i) -f (j) | \ równoważnik {1 \ nad n}}$

tak, że wraz ze wzrostem n wartości ƒ ( n ) zbliżają się do siebie. Możemy użyć ƒ i g razem, aby obliczyć jak najbardziej racjonalne przybliżenie liczby rzeczywistej, którą reprezentują.

Zgodnie z tą definicją prostą reprezentacją liczby rzeczywistej e jest:

${\ Displaystyle f (n) = \ suma _ {i = 0} ^ {n} {1 \ nad ja!}, \ quad g (n) = n.}$

Ta definicja odpowiada klasycznej definicji wykorzystującej ciągi Cauchy'ego, z wyjątkiem konstruktywnego zwrotu: w przypadku klasycznego ciągu Cauchy'ego wymagane jest, aby dla dowolnej odległości istniał (w klasycznym sensie ) element ciągu, po którym wszystkie elementy są bliżej siebie niż ta odległość. W wersji konstruktywnej wymagane jest, aby dla dowolnej danej odległości możliwe było faktyczne określenie punktu w sekwencji, w którym to nastąpi (ta wymagana specyfikacja jest często nazywana modułem zbieżności ) . W rzeczywistości standardowa konstruktywna interpretacja matematycznego stwierdzenia

${\ Displaystyle \ forall n: \ istnieje m: \ forall i, j \ geq m: | f (i) -f (j) | \ równoważnik {1 \ nad n}}$

jest właśnie istnienie funkcji obliczającej moduł zbieżności. Tak więc różnicę między dwiema definicjami liczb rzeczywistych można traktować jako różnicę w interpretacji stwierdzenia „dla wszystkich… istnieje…”

To następnie otwiera pytanie, jaki rodzaj funkcji ze zbioru przeliczalnego do zbioru przeliczalnego, takiego jak f i g powyżej, może faktycznie zostać skonstruowany. Różne wersje konstruktywizmu różnią się w tej kwestii. Konstrukcje można zdefiniować tak szeroko, jak sekwencje wolnego wyboru , co jest poglądem intuicjonistycznym, lub tak wąsko, jak algorytmy (lub bardziej technicznie, funkcje obliczeniowe ), a nawet pozostawić nieokreślone. Jeśli, na przykład, przyjmiemy podejście algorytmiczne, to konstruowane tutaj liczby rzeczywiste są zasadniczo tym, co klasycznie nazwalibyśmy liczbami obliczalnymi .

Kardynalność

Przyjęcie powyższej interpretacji algorytmicznej wydaje się sprzeczne z klasycznymi koncepcjami liczności . Wyliczając algorytmy, możemy klasycznie pokazać, że liczby obliczalne są policzalne. A jednak diagonalny argument Cantora pokazuje, że liczby rzeczywiste mają większą liczność. Co więcej, argument diagonalny wydaje się całkowicie konstruktywny. Utożsamianie liczb rzeczywistych z liczbami obliczalnymi byłoby zatem sprzecznością.

I faktycznie, diagonalny argument Cantora jest konstruktywny w tym sensie, że biorąc pod uwagę bijekcję między liczbami rzeczywistymi a liczbami naturalnymi, konstruujemy liczbę rzeczywistą, która nie pasuje, a tym samym dowodzimy sprzeczności. Możemy rzeczywiście wyliczyć algorytmy, aby skonstruować funkcję T , co do której początkowo zakładamy, że jest to funkcja od liczb naturalnych do liczb rzeczywistych. Ale każdemu algorytmowi może odpowiadać liczba rzeczywista lub nie, ponieważ algorytm może nie spełniać ograniczeń lub nawet nie kończyć się ( T jest funkcją częściową ), więc nie daje to wymaganej bijekcji. Krótko mówiąc, ten, kto uważa, że ​​liczby rzeczywiste są (indywidualnie) efektywnie obliczalne, interpretuje wynik Cantora jako pokazujący, że liczby rzeczywiste (zbiorowo) nie są rekurencyjnie przeliczalne .

Mimo to można by się spodziewać, że skoro T jest funkcją częściową od liczb naturalnych do liczb rzeczywistych, to liczby rzeczywiste są jedynie policzalne . A ponieważ każdą liczbę naturalną można trywialnie przedstawić jako liczbę rzeczywistą, dlatego liczby rzeczywiste są nie mniej niż policzalne. Są więc dokładnie policzalne. Jednak to rozumowanie nie jest konstruktywne, ponieważ nadal nie konstruuje wymaganej bijekcji. Klasyczne twierdzenie dowodzące istnienia bijekcji w takich okolicznościach, a mianowicie twierdzenie Cantora-Bernsteina-Schroedera , jest niekonstruktywne. Niedawno wykazano, że twierdzenie Cantora-Bernsteina-Schroedera implikuje prawo wyłączonego środka , stąd nie może być konstruktywnego dowodu twierdzenia.

Aksjomat wyboru

Status aksjomatu wyboru w matematyce konstruktywistycznej komplikują różne podejścia różnych programów konstruktywistycznych. Jedno trywialne znaczenie słowa „konstruktywny”, używane nieformalnie przez matematyków, jest „możliwe do udowodnienia w teorii mnogości ZF bez aksjomatu wyboru”. Jednak zwolennicy bardziej ograniczonych form konstruktywnej matematyki twierdzą, że sam ZF nie jest systemem konstruktywnym.

W intuicjonistycznych teoriach teorii typów (zwłaszcza arytmetyki wyższego typu) dozwolonych jest wiele form aksjomatu wyboru. Na przykład aksjomat AC ₁₁ można sparafrazować tak, że dla dowolnej relacji R w zbiorze liczb rzeczywistych, jeśli udowodniono, że dla każdej liczby rzeczywistej x istnieje taka liczba rzeczywista y , że zachodzi R ( x , y ), wtedy faktycznie istnieje funkcja F taka, że ​​R ( x , F ( x )) zachodzi dla wszystkich liczb rzeczywistych. Podobne zasady wyboru są akceptowane dla wszystkich typów skończonych. Motywacją do przyjęcia tych pozornie niekonstruktywnych zasad jest intuicjonistyczne rozumienie dowodu, że "dla każdej liczby rzeczywistej x istnieje taka liczba rzeczywista y , że zachodzi R ( x , y )". Zgodnie z interpretacją BHK sam dowód jest zasadniczo pożądaną funkcją F. Zasady wyboru, które akceptują intuicjoniści, nie implikują prawa wyłączonego środka .

Jednak w niektórych systemach aksjomatów konstruktywnej teorii mnogości aksjomat wyboru implikuje prawo wyłączonego środka (w obecności innych aksjomatów), jak pokazuje twierdzenie Diaconescu-Goodmana- Myhilla . Niektóre konstruktywne teorie mnogości obejmują słabsze formy aksjomatu wyboru, takie jak aksjomat zależnego wyboru w teorii mnogości Myhilla.

Teoria miary

Klasyczna teoria miary jest zasadniczo niekonstruktywna, ponieważ klasyczna definicja miary Lebesgue'a nie opisuje żadnego sposobu obliczania miary zbioru lub całki funkcji. W rzeczywistości, jeśli ktoś pomyśli o funkcji jako o regule, która „wprowadza liczbę rzeczywistą i wyprowadza liczbę rzeczywistą”, to nie może istnieć żaden algorytm do obliczania całki funkcji, ponieważ każdy algorytm byłby w stanie wywołać tylko skończenie wiele wartości funkcji na raz, a skończenie wiele wartości nie wystarcza do obliczenia całki z jakąkolwiek nietrywialną dokładnością. Rozwiązanie tej zagadki, przeprowadzone po raz pierwszy w Bishop (1967) , polega na uwzględnieniu tylko funkcji zapisanych jako punktowa granica funkcji ciągłych (o znanym module ciągłości), z informacją o szybkości zbieżności. Zaletą konstruktywizującej teorii miary jest to, że jeśli można udowodnić, że zbiór jest konstruktywnie pełnej miary, to istnieje algorytm znajdowania punktu w tym zbiorze (ponownie patrz Bishop (1967) ). Na przykład, to podejście może być użyte do skonstruowania liczby rzeczywistej, która jest normalna do każdej podstawy.

Miejsce konstruktywizmu w matematyce

Tradycyjnie niektórzy matematycy byli podejrzliwi, jeśli nie wrogo nastawieni do konstruktywizmu matematycznego, głównie z powodu ograniczeń, jakie ich zdaniem stwarzał on dla konstruktywnej analizy. Poglądy te zostały z mocą wyrażone przez Davida Hilberta w 1928 roku, kiedy napisał w Grundlagen der Mathematik : „Przyjęcie zasady wyłączonego środka od matematyka byłoby tym samym, powiedzmy, zakazaniem teleskopu astronomowi lub bokserowi używania jego pięści".

Errett Bishop w swojej pracy z 1967 roku Foundations of Constructive Analysis starał się rozwiać te obawy, rozwijając wiele tradycyjnych analiz w konstruktywnych ramach.

Chociaż większość matematyków nie akceptuje tezy konstruktywistów, że tylko matematyka oparta na metodach konstruktywnych jest słuszna, metody konstruktywistyczne cieszą się coraz większym zainteresowaniem ze względów pozaideologicznych. Na przykład konstruktywne dowody w analizie mogą zapewnić ekstrakcję świadków w taki sposób, że praca w ramach ograniczeń metod konstruktywnych może ułatwić znalezienie świadków teorii niż przy użyciu metod klasycznych. Zastosowania matematyki konstruktywnej znaleziono również w typowanych rachunkach lambda , teorii toposu i logice kategorycznej , które są ważnymi przedmiotami w matematyce podstawowej i informatyce . W algebrze, dla takich bytów jak toposy i algebra Hopfa , struktura wspiera wewnętrzny język , który jest konstruktywną teorią; praca w ramach ograniczeń tego języka jest często bardziej intuicyjna i elastyczna niż praca z zewnątrz za pomocą takich środków, jak wnioskowanie o zbiorze możliwych algebr konkretnych i ich homomorfizmach .

Fizyk Lee Smolin pisze w Three Roads to Quantum Gravity , że teoria toposu jest „właściwą formą logiki dla kosmologii” (strona 30) i „W swoich pierwszych formach nazywano ją„ logiką intuicjonistyczną ”” (strona 31). „W tego rodzaju logice twierdzenia, które obserwator może wypowiedzieć na temat wszechświata, dzielą się na co najmniej trzy grupy: te, które możemy uznać za prawdziwe, te, które możemy uznać za fałszywe, oraz te, o których prawdziwości nie możemy zdecydować teraźniejszość” (strona 28).

Matematycy, którzy wnieśli znaczący wkład w konstruktywizm

• Leopold Kronecker (stary konstruktywizm, półintuicjonizm)
• LEJ Brouwer (twórca intuicjonizmu)
• AA Markow (przodek rosyjskiej szkoły konstruktywizmu)
• Arend Heyting (sformalizowana logika intuicjonistyczna i teorie)
• Per Martin-Löf (twórca konstruktywnych teorii typów)
• Errett Bishop (promował wersję konstruktywizmu uważaną za zgodną z matematyką klasyczną)
• Paul Lorenzen (opracowana analiza konstruktywna)

Gałęzie

• Logika konstruktywna
• Konstruktywna teoria typów
• Konstruktywna analiza
• Konstruktywna analiza niestandardowa

Zobacz też

• Teoria obliczalności - Badanie funkcji obliczalnych i stopni Turinga
• Dowód konstruktywny - Metoda dowodu w matematyce
• Finityzm - Filozofia matematyki, która akceptuje istnienie tylko skończonych obiektów matematycznych
• Semantyka gier – podejście do semantyki formalnej Strony wyświetlające opisy wikidanych jako rozwiązanie awaryjne
• Zbiór zamieszkany - Rodzaj zbioru w matematyce konstruktywnej
• Intuicjonizm – Podejście w filozofii matematyki i logiki
• Intuicjonistyczna teoria typów – Alternatywne podstawy matematyki
• Finistyczna teoria mnogości

Notatki

•   Beeson, Michael J. (1985). Podstawy matematyki konstruktywnej: studia metamatematyczne . 9783540121732. ISBN 9783540121732 .

•   Biskup, Errett (1967). Podstawy konstruktywnej analizy . Nowy Jork: prasa akademicka. ISBN 4-87187-714-0 .

• Mosty, Douglas; Richman, Fred (1987). Odmiany konstruktywnej matematyki . Wydawnictwo Uniwersytetu Cambridge. doi : 10.1017/CBO9780511565663 .

•   Edwards, Harold Mortimer (2005). Eseje z matematyki konstruktywnej . Springer-Verlag. ISBN 0-387-21978-1 .

• Feferman, Salomon (1997). Relacje między konstruktywnymi, predykatywnymi i klasycznymi systemami analizy (PDF) .

• Pradić, Pierre; Brązowy, Czad E. (2019-04-19). „Cantor-Bernstein implikuje wykluczony środek”. arXiv : 1904.09193 [ matematyka.LO ].

• Troelstra, Anne Sjerp (1977a). „Aspekty konstruktywnej matematyki”. Podręcznik logiki matematycznej . 90 : 973–1052. doi : 10.1016/S0049-237X(08)71127-3 .

•   Troelstra, Anne Sjerp (1977b). Sekwencje wyboru: rozdział matematyki intuicjonistycznej . Oxford University Press. ISBN 0-19-853163-X .

•   Troelstra, Anne Sjerp ; Van Dalen, Dirk (1988a). Konstruktywizm w matematyce: wprowadzenie, tom 1 . Nauka Elseviera. ISBN 9780444702661 .

•   Troelstra, Anne Sjerp ; Van Dalen, Dirk (1988b). Konstruktywizm w matematyce: wprowadzenie, tom 2 . Nauka Elseviera. ISBN 9780444703583 .

• Troelstra, Anne Sjerp (1991). Historia konstruktywizmu w XX wieku (PDF) . University of Amsterdam, ITLI Prepublication Series ML-91-05. Zarchiwizowane od oryginału w dniu 2006-02-09 . Źródło 2019-07-09 . {{ cite book }} : CS1 maint: bot: stan oryginalnego adresu URL nieznany ( link )

Linki zewnętrzne

• „Matematyka konstruktywna” . Internetowa encyklopedia filozofii .
• Stanford Encyclopedia of Philosophy wpis