Úvodem

Vítejte na stránkách učebnice Coqbook, která slouží k interaktivnímu studiu logiky! Logika je (v obrovské zkratce) nauka o procesu vyvozování závěrů z předpokladů. Je to základní (fundamentální) disciplína, která má důležité uplatnění v řadě oborů, včetně matematiky, informatiky, filosofie a lingvistiky.

V této učebnici se seznámíte s některými základními principy a technikami matematické logiky. Zaměříme se na výrokovou logiku a pojem důkazu v přirozené dedukci. Pojmy a konstrukce, které zavedeme, budete mít možnost použít na řadě problémů a cvičení, což vám pomůže rozvíjet vaše schopnosti kritického myšlení a logického uvažování.

Interaktivní část učebnice spočívá ve cvičeních (logických důkazech), která budete řešit ve speciálním programovacím jazyce Coq, který je velmi vhodný k logické práci. Tento přístup má několik výhod. Zaprvé si procvičíte zcela formální dokazování, v němž se (stejně jako v programování) neodpouští žádná nepřesnost. Zadruhé budete mít možnost okamžité zpětné vazby, zda je vaše řešení korektní; to provede Coq za vás. A zatřetí, Coq vám může s dokazováním pomoci v režimu interaktivního dokazování, u kterého vám ukazuje, kam už jste v důkazu postoupili a co vám ještě chybí.

Ať už jste student, profesionál, nebo zkrátka kdokoli, kdo chce zlepšit své schopnosti uvažování, tato učebnice je navržena tak, aby vám poskytla pevné základy logiky a pomohla vám aplikovat tyto principy v reálných situacích. Tak se do toho pusťte!