W dniu piątek, 27 marca 2015 12:24:48 UTC+1 użytkownik M.M. napisał:
> On Friday, March 27, 2015 at 10:57:26 AM UTC+1, g...@g...com wrote:
> > Oczywiście pewien problem natury epistemicznej wiąże się ze sformułowaniem
> > odpowiedniej listy aksjomatów, które miałyby odzwierciedlać rozważany
> > przez nas problem
> Właśnie o tym pisałem. Poprawność dowodu, to też jego poprawność w
> odzwierciedlaniu oryginalnego zadania.

W takim razie zgoda -- tego rodzaju "poprawność" jest niemożliwa do uzyskania.
Należy jednak mieć na uwadze, że z formalnego punktu widzenia poprzez
"poprawność" dowodu rozumie się to, czy każdy krok jest zgodny z regułami,
natomiast w tym przypadku raczej należałoby użyć słowa "adekwatność"
(na przykład teza Churcha-Turinga postuluje adekwatność maszyny Turinga
jako modelu ujmującego intuicyjne rozumienie obliczalności)

Jednak z drugiej strony jeśli mamy na przykład dowód indukcyjny twierdzenia,
że funkcja "append" zdefiniowana (dajmy na to w czymś haskelopodobnym) jako

append [] y = y
append (h:t) y = h:(append t y)

jest operatorem łącznym, tzn dla dowolnych skończonych list a, b, c
append (append a b) c === append a (append b c)

to tak naprawdę trudno jest to kwestionować i podważać, tzn. albo uznajemy
regułę indukcji, i wtedy musimy uznać dowód za poprawny, albo jej nie uznajemy,
i obawiamy się, że "mogą istnieć takie listy, dla których append wcale
nie będzie się zachowywał jako operator łączny" -- choć byłoby czymś
szokującym, gdyby ktoś był w stanie podać pozbawione błędów rozumowanie,
które pozwalałoby taki obiekt skonstruować. Tym bardziej trudno byłoby
tutaj sformułować zarzut nieadekwatności, bo nie za bardzo można wskazać
jakąś zewnętrzną dziedzinę problemową, do której mielibyśmy odnosić
dowód

(a przy okazji jak kogoś ciekawi, to znajdzie ten dowód w notatkach
http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jr
h-1996/all.pdf
na stronie 86)