Niepodlegający badaniu dowód

W filozofii matematyki dowód , którego nie można zweryfikować, jest dowodem matematycznym , który jest uważany za niewykonalny dla ludzkiego matematyka do zweryfikowania , a zatem ma kontrowersyjną ważność . Termin został ukuty przez Thomasa Tymoczko w 1979 roku w krytyce wspomaganego komputerowo dowodu twierdzenia o czterech kolorach Kennetha Appela i Wolfganga Hakena i od tego czasu był stosowany do innych argumentów, głównie tych z nadmiernym dzieleniem przypadków i/lub z porcjami wysyłanymi przez trudny do zweryfikowania program komputerowy. Możliwość geodezji pozostaje ważnym zagadnieniem w matematyce obliczeniowej .

Argument Tymoczki

Tymoczko argumentował, że trzy kryteria określają, czy argument jest dowodem matematycznym:

Przekonywalność , która odnosi się do zdolności dowodu do przekonania racjonalnego dowodzącego o jego konkluzji;
Surveyability , która odnosi się do dostępności dowodu do weryfikacji przez członków ludzkiej społeczności matematycznej; I
Formalizowalność , która odnosi się do odwoływania się dowodu tylko do logicznych relacji między pojęciami w celu uzasadnienia jego argumentu.

- Hakena nie spełnił kryterium sprawdzalności, argumentując, zastępując dedukcję eksperymentem :

…jeśli zaakceptujemy [Twierdzenie o Czterech Kolorach] jako twierdzenie, jesteśmy zobowiązani do zmiany sensu „twierdzenia” lub, bardziej do rzeczy, do zmiany sensu leżącego u podstaw pojęcia „dowód”. … [użycie] komputerów w matematyce, jak w [twierdzeniu o czterech kolorach], wprowadza do matematyki eksperymenty empiryczne. Niezależnie od tego, czy zdecydujemy się uznać [twierdzenie o czterech kolorach] za udowodnione, musimy przyznać, że obecny dowód nie jest tradycyjnym dowodem, nie jest a priori twierdzenia z przesłanek. Jest to tradycyjny dowód z luką, którą wypełniają wyniki dobrze przemyślanego eksperymentu.

- Thomas Tymoczko, „Problem czterech kolorów i jego znaczenie filozoficzne”

Bez sprawdzalności dowód może służyć swemu pierwszemu celowi, jakim jest przekonanie czytelnika do swojego wyniku, a jednak zawieść drugiemu celowi, jakim jest wyjaśnienie czytelnikowi, dlaczego ten wynik jest prawdziwy — może odgrywać raczej rolę obserwacji niż argumentu.

To rozróżnienie jest ważne, ponieważ oznacza, że dowody, których nie da się zbadać, narażają matematykę na znacznie większy potencjał błędu. Zwłaszcza w przypadku, gdy niemożność zbadania wynika z użycia programu komputerowego (który może zawierać błędy ), zwłaszcza gdy ten program nie jest opublikowany, w rezultacie może ucierpieć przekonanie. Jak pisał Tymoczko:

Załóżmy, że jakiś superkomputer został ustawiony do pracy nad spójnością arytmetyki Peano i podał dowód niespójności , dowód, który był tak długi i złożony, że żaden matematyk nie byłby w stanie go zrozumieć poza najbardziej ogólnymi terminami. Czy moglibyśmy mieć wystarczającą wiarę w komputery, aby zaakceptować ten wynik, czy też powiedzielibyśmy, że empiryczne dowody na ich niezawodność nie są wystarczające?

- Thomas Tymoczko, „Problem czterech kolorów i jego znaczenie matematyczne”

Kontrargumenty do twierdzeń Tymoczki o niepodleganiu badaniu

Pogląd Tymoczki jest jednak kwestionowany przez argumenty, że dowody trudne do zbadania niekoniecznie są tak samo nieważne jak dowody niemożliwe do zbadania.

Paul Teller twierdził, że sprawdzalność jest kwestią stopnia i zależną od czytelnika, a nie czymś, co dowód ma lub nie ma. Jak argumentuje Teller, nie odrzuca się dowodów, gdy uczniowie mają problem z ich zrozumieniem, tak samo nie należy ich odrzucać (chociaż można je krytykować) tylko dlatego, że zawodowi matematycy mają trudności z nadążeniem za argumentem. (Teller nie zgodził się z oceną Tymoczki, że „[Twierdzenie o czterech kolorach] nie zostało sprawdzone przez matematyków krok po kroku, tak jak wszystkie inne dowody zostały sprawdzone. Rzeczywiście, nie można tego sprawdzić w ten sposób”).

Argumentem podobnym do tego jest to, że podział przypadków jest akceptowaną metodą dowodową, a dowód Appela-Hakena jest tylko skrajnym przykładem podziału przypadków.

Środki zaradcze przeciwko niemożności zbadania

Z drugiej strony, generalnie nie kwestionuje się stanowiska Tymoczki, że dowody muszą być przynajmniej możliwe do zbadania i że błędy w dowodach trudnych do zbadania są mniej prawdopodobne; zamiast tego zaproponowano metody poprawy możliwości badania, zwłaszcza dowodów wspomaganych komputerowo. Wśród wczesnych sugestii była równoległość: zadanie weryfikacji można podzielić na wielu czytelników, z których każdy mógłby przejrzeć część dowodu. Ale współczesna praktyka, rozsławiona przez Flyspeck , polega na renderowaniu wątpliwych części dowodu w ograniczonym formalizmie, a następnie weryfikowaniu ich za pomocą kontrolera dowodu który jest dostępny do badania. Rzeczywiście, dowód Appela-Hakena został w ten sposób zweryfikowany.

Niemniej jednak automatyczna weryfikacja nie spotkała się jeszcze z powszechnym przyjęciem.