13 Logika – formalizace

Matematická tvrzení je výhodné zapisovat ve zkrácené formě pomocí symboliky predikátové logiky. Podrobněji bude tato oblast matematiky probrána v předmětu  BI-DML.2139. Díky využití tohoto přístupu vynikne logická struktura tvrzení, která by jinak mohla čtenáři zůstat skryta za větami přirozeného (v našem případě českého) jazyka. Na tomto místě pouze stručně shrneme základy, které jsou čtenáři již jistě známy.

Poznámka 13.1

Ihned učiňme jednu motivační a vysvětlující poznámku. Řada studentů má k formálním zápisům jistý odpor. Ten je nutné překonat. Uvědomte si, že přesná formulace matematických tvrzení pouze přirozeným českým jazykem je velice „křehká“ a náchylná na dezinterpretaci. Obranou proti tomu je velmi podrobný slovní popis, čímž ovšem text ztrácí na čitelnosti. Tento přístup se používal ve středověku, od té doby jsme se již posunuli. Formální zápis odstraňuje neurčitost, řada problémů tím následně odpadá.

Je také vhodné si uvědomit, že libovolný programovací jazyk je ve své podstatě vysoce formalizovaný zápis jistých instrukcí. Budoucím programátorům by formálně přesné vyjadřování mělo být blízké. Překladač vás vytrestá za sebemenší chybičku, matematika je v tomto směru přeci jen malinko shovívavější!

13.1 Výrok a formule

13.2 Pravdivost výroků

13.3 Negace výroků

13.4 Nutná a postačující podmínka