00:15Логика высшего порядка. Эпсилон-оператор Гильберта
02:49Доказательство леммы (код)
06:03Доказательство аксиомы выбора (код)
11:20Логика HOL. HOAS. Синтаксические декларации
16:40Примеры mixfix'ов (код)
18:15Базовые определения в HOL. Аксиомы HOL. Константы, типы и аксиомы по определению в HOL
23:48Использование именованных предположений с помощью шаблона assumes-shows. Правило impE
30:54Как работает логика HOL. Задание своей логики. iffI
35:38Вывод правила интродукции allI
40:44Вывод правила spec
42:56Вывод правила элиминации allE. Аналогичные выводы правил для FalseE, False_neq_True, notI, notE, False_not_True, exE , exI
44:24Вывод правила conjI
47:02Вывод правила conjE. Аналогичные выводы правил для дизъюнкции и для правил классической логики. Самостоятельная задача операторов и вывод правил для них
