Агата Сомова · старший инспектор
Вот страница из середины тетради. Черта на черте, наверху пусто, внизу одна строчка. Похоже на родословную, только вверх ногами. Покажи мне, как из правил получается этот вывод, ступенька за ступенькой. И объясни, почему наверху ничего нет.
В прошлом уроке у правил чётности была одна посылка, и вывод выглядел как столбик: ноль чётен, значит, два чётно, значит, четыре чётно. На странице, которую принесла Сомова, у правил по две посылки. Над чертой стоят два суждения, и каждое нужно доказать отдельно. Столбик раздваивается, и получается дерево. Одно такое ветвление ты уже видел в уроке 28: у правила T-If для термов три посылки. Теперь разберём, как дерево устроено и как его строить.
Именно так устроены выводы в книге Пирса и на странице Кодекса. Каждый шаг Арбитра, как ты увидишь в конце урока, это такое дерево.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.