Początkowa część kursu omawia te zagadnienia, o których założyłem, że są znane słuchaczom seminarium. W szczególności notatka 02 oraz notatka 03 to wprowadzenie do systemu dedukcji naturalnej. Notatka 04 omawia paradygmat ,,dowody jako programy".
W pierwszej części prezentacji omówiłem rachunek sekwentów dla logiki intuicjonistycznej. Notatka 09 wprowadza ten system oraz pokazuje jak wyprowadzić z niego najstotniejsze własności logiki konstruktywnej (spójność, własność dyzjunkcyjna, niewywodliwość reguły wyłączonego środka). W notatce 10 omówiono regułę cięcia (cut) oraz równoważność systemów z cięciem oraz bez cięcia. Notatka 11 omawia wariant reguł, w których kontrakcja używana jest tak rzadko jak to możliwe. Dodatkowo scharakteryzowany jest zestaw reguł odwracalnych -- nie było to omówione podczas prezentacji, ale warto o tym poczytać, gdyż ta obserwacja pozwala mocno ograniczyć niedeterminizm podczas poszukiwania dowodów. Wreszcie w notatce 12 wyprowadzony jest bezkontrakcyjny rachunek sekwentów Roya Dyckhoffa. W porównaniu do oryginalnego artykułu Dyckhoffa w swoich notatkach Pfenning prezentuje wyprowadzenie krok po kroku.
W drugiej części rozmawialiśmy o logice klasycznej. W notatce 07 omówiono różne warianty aksjomatów, które można dodać do systemu dedukcji naturalnej aby uzyskać system poprawny i pełny względem rachunku zdań opartego o tabelki prawdziwościowe. Dodatkowo, pokazano dlaczego każda z propozycji jest nie do końca satysfakcjonująca i zaproponowano inne podejście, oparte o sądy A true i A false. W notatce 08 opisano jak można upraszczać dowody klasyczne i w jaki sposób jest to powiązane z operatorami sterowania. Podobne podejście jest opisane w podręczniku Practical Foundations for Programming Languages Boba Harpera w rozdziale 31. Różnica polega na tym, że u Harpera fałszywość (dokładniej: zaprzeczalność, obalalność) formuły jest opisana indukcyjnie, a nie poprzez bezpośrednie odwołanie do sądu opisującego prawdziwość (dokładniej: dowodliwość) formuły oraz do pojęcia sprzeczności. Ponadto system opisany u Harpera jest całkowicie symetryczny i np. wśród termów dowodowych mamy operatory call-with-current-proof i call-with-current-refutation. Warto także rzucić okiem na wstęp do rozdziału 30, aby lepiej poczuć różnicę między systemem intuicjonistycznym i klasycznym.
Wojciech Jedynak