Лидия Арбенина · лист, вложенный в переплёт Кодекса
Утверждение о каждом деле доказывается по тому, как дело собрано. Не по тому, как оно выглядит снаружи: так легко пропустить случай или упереться в стену. А по тому, каким правилом машина приняла его последним. Сколько правил, столько случаев. Для каждой посылки над чертой утверждение у тебя уже есть.
Под этими строками на листе два правила с чертой и короткое доказательство. Тимофей Ильич уверен, что лист вырван из рабочего блокнота: края неровные, в углу номер страницы, 41. Где остальные сорок страниц, никто не знает.
Сомова читает лист дважды: «Это главный инструмент её Кодекса. Если мы хотим проверить обещание на первой странице, нам придётся доказывать так же». В уроке 29 ты доказывал утверждения о термах по их устройству. Арбенина предлагает доказывать утверждения о выводах по их устройству. Это индукция по выводу, и на ней держатся главные теоремы TAPL.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.