Суждения и правила: черта в блокноте Арбениной

Тимофей Ильич · архивариус

Нашёл, когда разбирал полку с описями. Коробка без номера, внутри четыре тетради в клеёнке, на каждой «Л. А.». Почерк аккуратный, но слов почти нет: строчка, под ней черта, под чертой ещё строчка. На первой странице одна фраза: «Так машина решает, что можно». Что можно, что нельзя, не написано. Разберётесь?

Это блокноты Лидии Арбениной, инженера, которая построила Арбитра. Сомова листает первую тетрадь и на первой же странице узнаёт старых знакомых: 0, s, слово even и два правила с чертой. Те самые, что были на листе 41 из урока 30. «Значит, лист вырван отсюда», говорит она. «Тогда мы пользовались этими чертами на ходу. Если машина решает по ним, читай их как статьи закона: каждую букву, каждое место над чертой и под ней. Иначе мы никогда не узнаем, что она сделала с делом склада».

Правила с чертой ты уже встречал дважды. В уроке 28 ими задавали множество термов, в уроке 30 чётные числа. Там хватало грубого прочтения: над чертой посылки, под чертой заключение. Черта это главный значок в книге Пирса и на странице Кодекса, поэтому теперь разберём саму запись. Что такое суждение вообще, а не только n even. Что значат буквы в правиле и как их заменять. Почему аксиома тоже бывает шаблоном. И как прочитать вывод вслух, сверху вниз и снизу вверх.