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