Treść książki

Przejdź do opcji czytnikaPrzejdź do nawigacjiPrzejdź do informacjiPrzejdź do stopki
Wstęp
Logikawspółczesnadostarczaformalnychnarzędziumożliwiającychprecy-
zyjnąanalizępoprawnościrozumowań.Najważniejszymsposobemuzasad-
nianiagłoszonychtwierdzeńjestbezwątpieniadowód.Nagruncielogiki
wypracowanowieletypówsystemówdowodzeniatakichjaksystemyaksjo-
matyczne,systemyrezolucji,systemysekwentoweczysystemydedukcjina-
turalnej.Teostatniezostałyzaproponowanejakonajbardziejzbliżonedo
faktycznejpraktykidowodzeniastosowanejprzedewszystkimprzezmate-
matyków.Wprezentowanymopracowaniuskupimysięnaopisiestruktury
izastosowańostatniegozwymienionychsposobówkodyfikacjidowodzenia.
Wrozdzialepierwszymzaprezentujemyjednozjegomożliwychrealizacji
wodniesieniudologikiklasycznej.Dowodyidedukcjebędątutajprezento-
wanewczystoformalnysposób.Prezentacjędedukcjinaturalnejpoprzedzi-
mykrótkimomówieniemaksjomatycznejformalizacjiklasycznegorachunku
zdań.Wdrugimrozdzialezaprezentowanezostanądwieteorieaksjomatycz-
ne:arytmetykaliczbnaturalnychwujęciuPeanoiobszernyfragmentteorii
mnogościwujęciuZermeloiFraenkela.Dowodytwierdzeńwtychteoriach
zostanąprzedstawioneskrótowo,wsposóbniesformalizowanyalenatyledo-
kładny,żemożnajenprzepisać”jakowpełniformalnedowodywsystemie
dedukcjinaturalnejzczęścipierwszej,wzbogaconymoaksjomatyrozważa-
nychteorii.Takierozwiązaniepokazujenamwnaturalnysposóbzwiązek
dedukcjinaturalnejzfaktycznieprezentowanymiszkicamidowodówwlite-
raturzematematycznejaponadtojestekonomiczne,gdyżformalnedowody
ważnychtwierdzeńzwyklebardzodługie.
Zanimprzejdziemydocharakterystykidedukcjinaturalnejwypadapo-
święcićniecouwagihistoriizagadnienia.Dowody,częstocałkiemzadowa-
lającezpunktuwidzeniastosowanychobecniekryteriów,konstruowalijuż
matematycygreccyzkręguszkołypitagorejskiejdziałającywVI–Vw.p.n.e.
Wypracowalioniwieleregułitechnik,którenależądowypróbowanegore-
pertuaruśrodkówdowodzeniastosowanegowspółcześnie.Należądonichnp.
9