Математическая логика на Python 25

Объявления

• Дэдлайн по 1 домашнему заданию - 31.01.25.
• Добавили гугл-класс https://classroom.google.com/c/NzI1NTIzNTE3MjA0?cjc=frttno2
• Добавлено ДЗ №2. Дэдлайн - 07.02.25
• Добавлено ДЗ №3. Дэдлайн - 14.02.25
• Теперь все сдаем через github
• Добавлено ДЗ №4. Дэдлайн - 28.02.25
• Добавлено ДЗ №5 Дэдлайн - 14.03.25

Введение

Этот курс -- попытка представить математическую логику через призму программирования на Python. Такой подход, позваляет студентам использовать интуицию и опыт программированя для изучения логики и, будем надеятся, сделает логику более доступной и наглядной. Практическая работа с кодом позволяет глубже понять концепции математической логики и увидеть работу этих концепций в реальных программах.

Описание курса

Курс включает пропозициональную логику и логику первого порядка. При этом планируется логику планируется изложить на уровне полноценного курса по математической логики со всеми важными теоремами и доказательствами. В качестве литературы можно использовать Н. К. Верещагин, А. Шень. Часть 2. Языки и исчисления. 5-е изд., М.: МЦНМО, 2017.

С другой стороны будет уделено много внимание тому как реализовать все формальные конструкции на языке Python и тут мы будем в основном следовать материалам на сайте https://www.logicthrupython.org/ Вместо решения обычных задач на семинарах мы будем писать программы, которые реализуют используемые в курсе конструкции. Имеются шаблоны программ, в которых недописаны некоторые куски кода, которые студенты должны дописать, чтобы в результате получилась работающая программа. В шаблонах имеются тесты, которые позволяют проверить работоспособность.

Формула оценки

В формуле участвуют: ДЗ -- доля пройденных тестов в заданиях на Python умноженная на 10. Колл -- оценка за коллоквиум, который пройдет после 3 модуля во время сессии (по 10 бальной шкале). Экз -- оценка за экзамен (по 10 бальной шкале)

Автомат будет выставлятся при условии, что MIN(ДЗ, Колл) >= 8. В этом случае итоговая оценка будет равна (2*ДЗ+Колл)/3, с округлением к ближайшему целому числу.

Итоговая оценка = 0.5 ДЗ + 0.25 Колл + 0.25 Экз

Домашние задания

Домашнее задание №1 (дэдлайн 31.01.25)

В этом задании вам надо будет внести изменения в файл propositions/syntax.py

Загрузить можно в гугл классе: https://classroom.google.com/c/NzI1NTIzNTE3MjA0?cjc=frttno2

Задание 1.1 (Task 1.1) В файле мето отмечено следующим комментарием: # Task 1.1

Реализуйте недостающий код для метода __repr__() класса Formula, который возвращает строку, представляющую формулу (в синтаксисе, определённом в Определении 1.1).

Обратите внимание, что в Python строка, возвращаемая методом formula.__repr__(), также возвращается вызовом str(formula). Таким образом, решив эту задачу, вы также реализуете функциональность метода str() для данного класса.

Задание 1.2 (Task 1.2) Реализуйте недостающий код для метода variables() класса Formula, который возвращает множество (set) имен переменных, присутствующие в формуле. Напомним, что имя переменной — это лист дерева, метка которого является буквой от «p» до «z», за которой следуют цифры.

Задание 1.3 (Task 1.3)

Реализуйте недостающий код для метода operators() класса Formula, который возвращает все операторы, присутствующие в формуле. Операторами в этом задании являются не только все унарные и бинарные операторы, но и константы T и F.

Задание 1.4 (Task 1.4)

Реализуйте недостающий код для статического метода _parse_prefix(string) класса Formula, который принимает строку, и возвращает формулу (объект типа Formula), созданное из префикса строки, а также строку, содержащую непроанализированный остаток строки (которая может быть пустой, если вся строка образует формулу). Обратите внимание, что формула это очень строгое формальное понятие, обратите внимание на скобки.

Задание 1.5 (Task 1.5)

Реализуйте недостающий код для статичного метода is_formula(string) класса Formula, который проверяет, представляет ли заданная строка корректную формулу.

Подсказка: используйте метод _parse_prefix().

Задание 1.6 (Task 1.6)

Реализуйте недостающий код для статичного метода parse(string) класса Formula, который разбирает строковое представление формулы. (Можно предположить, что входная строка корректна, то есть удовлетворяет предусловию Formula.is_formula(string), в коде уже есть соответствующий assert)

Чтобы проверить верно ли вы сделали все задание надо в корне папки запустить файл test_chapter01.py

Домашнее задание №2 (дэдлайн 07.02.25)

В этом задании вам надо будет внести изменения в файл propositions/semantics.py

Загрузить можно в гугл классе: https://classroom.google.com/c/NzI1NTIzNTE3MjA0?cjc=frttno2

Задание 2.1 (Task 2.1)

Реализуйте недостающий код для функции evaluate(formula, model), которая возвращает истинностное значение данной формулы (formula) в данной модели (model).

Задание 2.2 (Task 2.2)

Реализуйте недостающий код для функции all_models(variables), которая возвращает список всех возможных моделей над заданными именами переменных. Обратите внимание, что модели должны выводиться в лексикографическом порядка, считая, что F меньше T.

Задание 2.3 (Task 2.3)

Реализуйте недостающий код для функции truth_values(formula, models), которая возвращает список истинностных значений данной формулы (formula) в данных моделях (models).

Задание 2.4 (Task 2.4)

Реализуйте недостающий код для функции print_truth_table(formula), которая выводит таблицу истинности данной формулы (переменные должны быть отсортированы лексикографически, и строки в таблице тоже должны идти в лексикографическом порядке).

Задание 2.5 (Task 2.5a, Task 2.5b, Task 2.5c)

Реализуйте недостающий код для функций is_tautology(formula), is_contradiction(formula) и is_satisfiable(formula), которые соответственно определяют, является ли данная формула тавтологией, тождественно ложной или выполнимой.

Задание 2.6 (Task 2.6)

Реализуйте недостающий код для функции _synthesize_for_model(model), которая возвращает формулу высказываний в виде элементарной конъюнкции, принимающую значение True на данной модели и False на всех остальных моделях с теми же именами переменных.

Задание 2.7 (Task 2.7)

(Программное доказательство теоремы о ДНФ) Реализуйте недостающий код для функции synthesize(variables, values), которая строит формулу высказываний в дизъюнктивной нормальной форме (ДНФ) по заданному описанию её таблицы истинности.

Чтобы проверить верно ли вы сделали все задание надо в корне папки запустить файл test_chapter02.py

Домашнее задание №3 (дэдлайн 14.02.25)

В этом задании вам надо будет внести изменения в файлы: propositions/semantics.py , propositions/syntax.py и propositions/operators.py

Загрузить можно в гугл классе.

Задание 1 (Task 3.1)

Расширьте класс Formula из главы 1, добавив поддержку четырех новых бинарных операторов: +, <->, -&, -|.

• Измените функцию is_binary() в файле propositions/syntax.py. (По сути надо закоментить старый функционал и раскоментить строчку с новым функционалом)
• Внесите необходимые изменения в метод _parse_prefix() класса Formula.
• Проверьте, что все методы (как экземпляра, так и статические), реализованные в этом классе в главе 1, теперь работают корректно для всех семи бинарных операторов (старых и новых). (Для этого достаточно запустить тест для 3 главы и если будут ошибки - исправить их)
• Если код написан правильно, дополнительных изменений, кроме указанных выше, не потребуется.

Задание 2 (Task 3.2)

Расширьте функцию evaluate() из главы 2, добавив поддержку четырех новых операторов.

Проверьте, что функции truth_values(), print_truth_table(), is_tautology(), is_contradiction() и is_satisfiable() автоматически приобретают поддержку этих операторов благодаря изменениям в evaluate().

Задание 3 (Task 3.3)

Реализуйте недостающий код для метода substitute_variables(substitution_map) класса Formula.

Метод принимает на вход словарь, сопоставляющий некоторые переменные с формулами, и возвращает новую формулу, полученную путем замены переменных на их значения (формулы) из словаря.

Задание 4 (Task 3.4)

Реализуйте недостающий код для метода substitute_operators(substitution_map) класса Formula.

• Метод принимает словарь, где ключи — операторы, а значения — формулы, использующие только переменные p и q.
• Переменная p служит заместителем первого операнда (если оператор унарный или бинарный), q — второго (если оператор бинарный).
• Метод возвращает новую формулу, в которой каждый оператор из словаря заменен соответствующей формулой, при этом p и q подставляются вместо исходных операндов.
• Если оператор — константа (T или F), то он просто заменяется на соответствующую формулу без подстановки переменных.

Задание 5 (Task 3.5)

Реализуйте недостающий код для функции to_not_and_or(formula), которая возвращает формулу, эквивалентную данной (то есть имеющую ту же таблицу истинности), но использующую только операторы not, and и or.

Задание 6 (Task 3.6a, Task 3.6b, Task 3.6c, Task 3.6d)

Реализуйте недостающий код для следующих четырех функций:

• to_not_and(formula)
• to_nand(formula)
• to_implies_not(formula)
• to_implies_false(formula)

Каждая из них должна возвращать формулу, эквивалентную данной, но использующую только операторы, указанные в названии функции.

Домашнее задание №4 (дэдлайн 28.02.25)

В этот раз мы настроим систему загрузки решения в classroom.github.com Подробная инструкция появится чуть позже.

Задание 1 (Task 4.1) Файл: proofs.py

Реализуйте недостающий код для метода variables() класса InferenceRule, который возвращает множество имен переменных, встречающихся в предположениях и/или в заключении правила.

---

Задание 2 (Task 4.2) Файл: semantics.py

Реализуйте недостающий код для функции evaluate_inference(rule, model), которая возвращает True, если данное правило вывода выполняется в заданной модели, и False в противном случае.

Правило считается выполненным, если не существует модели, в которой все предположения истинны, а заключение ложно.

---

Задание 3 (Task 4.3) Файл: semantics.py

Реализуйте недостающий код для функции is_sound_inference(rule), которая проверяет, является ли данное правило вывода корректным, то есть сохраняет ли оно истинность формул в любой модели.

---

Задание 4 (Task 4.4) Файл: proofs.py

Реализуйте недостающий код для метода specialize(specialization_map) класса InferenceRule, который возвращает частный случай данного правила вывода согласно заданной подстановке.

Подсказка: Используйте метод substitute_variables() класса Formula, реализованный в ДЗ 3.

---

Задание 5 (Task 4.5) Файл: proofs.py

В этой задаче требуется определить, является ли одно правило вывода частным случаем другого, и, если это так, найти соответствующую карту специализации.

a. Реализуйте недостающий код статичного метода _merge_specialization_maps(map1, map2) класса InferenceRule. Метод должен проверить совместимость двух карт специализации (т.е. проверить, чтобы одно и то же имя переменной не отображалось в разные формулы) и, если карты совместимы, вернуть их объединение, иначе None.

b. Реализуйте недостающий код статичного метода _formula_specialization_map(general, specialization) класса InferenceRule. Метод должен вернуть словарь подходящей замены, если вторая формула является частным случаем первой, иначе None.

Подсказка: Используйте метод _merge_specialization_maps().

c. Реализуйте недостающий код метода specialization_map(specialization) класса InferenceRule, который возвращает словать замены, если правило-аргумент является частным случаем текущего (self), иначе None.

Важно: Порядок посылок должен сохраняться.

---

Задание 6 (Task 4.6) Файл: proofs.py

Проверьте корректность данного доказательства, т.е. убедитесь, что каждая строка является либо допущением, либо корректным выводом из предыдущих строк согласно допустимым правилам вывода.

a. Реализуйте недостающий код метода rule_for_line(line_number) класса Proof, который возвращает правило вывода для указанной строки.

Пояснение: Например, если в строке стоит формула A, и в списке формул посылок (порядок важен!) указаны формулы B1, ..., Bn, то вернуть нужно правило с посылками B1, ..., Bn и заключением A.

b. Реализуйте недостающий код метода is_line_valid(line_number) класса Proof, который проверяет корректность указанной строки.

Подсказка: Используйте метод rule_for_line().

c. Реализуйте недостающий код метода is_valid() класса Proof, который возвращает True, если доказательство корректно, иначе False.

---

Правило вывода Г/A называется допустимым, если A логически следует из Г.

Задание 7 (Task 4.7) Файл: some_proofs.py

Докажите допустимость правила вывода с посылкой (p&q) и заключением (q&p) с помощью следующих правил:

• Правило 1: Предположения: x, y; Заключение: (x&y)
• Правило 2: Предположение: (x&y); Заключение: y
• Правило 3: Предположение: (x&y); Заключение: x

Вывод, доказывающий допустимость, должен быть возвращен функцией prove_and_commutativity().

---

Задание 8 (Task 4.8) Файл: some_proofs.py

Правила упомянутые в этом задании правила вывода есть в файле axiomatic_systems.py. Их можно оттуда импортировать.

Докажите допустимость правила вывода с заключением (p->p) без посылок, используя правила MP, I1 и D.

Вывод, доказывающий допустимость, должен быть возвращен функцией prove_I0().

---

Задание 9 (Task 4.9) Файл: soundness.py

Реализуйте функцию rule_nonsoundness_from_specialization_nonsoundness(general, specialization, model), которая для заданного правила вывода, его частного случая и модели, являющейся контрпримером для частному случаю, возвращает модель, являющуюся контрпримером для исходного правила.

---

Задание 10 (Task 4.10) Файл: soundness.py

Реализуйте функцию nonsound_rule_of_nonsound_proof(proof, model), которая для корректного вывода и модели, являющейся контрпримером для заключения доказательства, возвращает некорректное правило вывода, использованное в доказательстве, а также модель-контрпример для этого правила.

---

Каждое задание проверяйте на корректность с помощью тестов в файле test_chapter04.py.

Домашнее задание №5 (дэдлайн 14.03.25)

Задание 5.1 (Task 5.1) file:propositions/proofs.py

Реализуйте недостающий код для функции prove_specialization(proof, specialization), которая принимает корректное доказательство некоторого правила вывода и возвращает дедуктивное доказательство (вывод) частного случая этого правила, используя то же множество правил вывода.

Подсказка: Используйте метод specialization_map() класса InferenceRule для получения карты замены, которое надо сделать в правиле, доказываемое в proof, чтобы получить правило specialization.

Задание 5.2 (Task 5.2) file:propositions/proofs.py

Реализуйте недостающий код для функции inline_proof(main_proof, lemma_proof), которая принимает доказательство (вывод) main_proof некоторого правила вывода с использованием множества правил R и дедуктивное доказательство lemma_proof одного из правил λ из R (леммы) с использованием множества правил R' (где λ не лежит в R') и возвращает доказательство правила вывода, доказанного в main_proof, но с использованием множества правил R \ {λ} ∪ R'.

а. Сначала реализуйте функцию _inline_proof_once(main_proof, line_number, lemma_proof), которая заменяет один экземпляр использования данной леммы в доказательстве.

б. Затем реализуйте inline_proof(main_proof, lemma_proof), вызывая _inline_proof_once() до тех пор, пока все вхождения данной леммы не будут удалены.

Задание 5.3 (Task 5.3) file:propositions/deduction.py

а. Реализуйте недостающий код для функции prove_corollary(antecedent_proof, consequent, conditional), которая принимает доказательство некоторой формулы φ (посылки) из некоторых предположений, желаемое заключение ψ и правило вывода conditional, для которого ‘(φ → ψ)’ является частным случаем, и возвращает доказательство ψ из тех же предположений, используя те же правила вывода, а также MP и conditional.

б. Реализуйте более сложный вариант функции combine_proofs(antecedent1_proof, antecedent2_proof, consequent, double_conditional), которая принимает два доказательства формул φ1 и φ2 (посылок), выведенных из одних и тех же предположений с использованием одних и тех же правил вывода, а также желаемое заключение ψ и правило вывода double_conditional, для которого ‘(φ1 → (φ2 → ψ))’ является с

Задание 5.4 (Task 5.4) file:propositions/deduction.py

Реализуйте недостающий код для функции remove_assumption(proof), которая принимает доказательство (вывод) некоторого заключения ψ из непустого списка посылок с использованием правил вывода, которые, кроме MP, не имеют посылок, и возвращает доказательство ‘(φ → ψ)’, где φ — последняя посылка правила (тут важно, что посылки - это не множество, а упорядоченный список и последняя посылка - это формула, стоящая в конце этого списка), которое доказывает proof, из тех же посылок, за исключением φ, с использованием того же множества правил, а также MP, I0, I1 и D.

Задание 5.5 (Task 5.5) file:propositions/some_proofs.py

Докажите следующее правило вывода:

• Посылки: ‘(p → q)’, ‘(q → r)’
• Заключение: ‘(p → r)’
• Множество правил: MP, I0, I1, D

Доказательство должно быть реализовано в функции prove_hypothetical_syllogism() в файле propositions/some_proofs.py.

Подсказка: Используйте теорему о дедукции, реализованную в Task 5.4.

Задание 5.6 (Task 5.6) file:propositions/deduction.py

Реализуйте недостающий код для функции proof_from_opposites(proof_of_affirmation, proof_of_negation, conclusion), которая принимает доказательство формулы φ и доказательство её отрицания ‘~φ’, оба с использованием одних и тех же правил вывода и из одних и тех же посылок, а также произвольное заключение (формулу) conclusion. Функция должна вернуть доказательство формулы conclusion из тех же посылок, используя те же правила вывода, что в доказательствах, а также MP и I2.

Подсказка: Функция combine_proofs(), реализованная в Task 5.3, может упростить применение аксиомы I2.

Задание 5.7 (Task 5.7) file:propositions/deduction.py

Реализуйте недостающий код для функции prove_by_way_of_contradiction(proof), которая принимает доказательство ‘~(p → p)’ из некоторых предположений, а также из отрицания ‘~φ’ некоторой формулы, и возвращает доказательство φ из этих предположений (без ‘~φ’) с использованием тех же правил вывода, а также MP, I0, I1, D и N.

Подсказка: Используйте теорему о дедукции (remove_assumption(proof)) и затем аксиому N.

Домашнее задание №6 (дэдлайн 28.03.25)

Задание 6.1 (Task 6.1) (file: propositions/tautology.py)

a. Реализуйте недостающий код для функции formulas_capturing_model(model), которая возвращает список формул (переменных или их отрицаний), описывающий данную модель (то, что на лекции обозначалось Г_М). Обратите внимание, что список должен быть упорядочен в лексикографическом порядке.

b. Реализуйте недостающий код для функции prove_in_model(formula, model), которая принимает пропозициональную формулу (содержащую только операторы '->' и '~') и модель, и возвращает либо вывод (proof) самой формулы (если она истинна в данной модели), либо вывод её отрицания (если формула ложна в данной модели) из множества Г_М в стандартной системе правил (AXIOMATIC_SYSTEM из axiomatic_systems.py).

Задание 6.2 (Task 6.2) (file: propositions/tautology.py)

Реализуйте недостающий код для функции reduce_assumption(proof_from_affirmation, proof_from_negation). Эта функция принимает два доказательства, оба доказывающих одно и то же заключение, используя одни и те же правила вывода, но из разных списков посылок. Списоки посылок должны быть почти одинаковые, за исключением последней формулы, т.е. последняя формула в списке посылок вывода proof_from_negation должна являться отрицанием последней формулы в списке посылок вывода proof_from_affirmation.

Функция должна вернуть вывод того же заключения, но уже из списка посылок, которые являются общими для обоих доказательств (то есть всех формул, кроме последних в списках посылок каждого вывода). Вывод должен использовать правила вывода, как в исходных выводах, а также также включать правила MP, I0, I1, D и R (их можно импортировать из модуля axiomatic_systems.py).

Подсказка: Используйте теорему о дедукции и аксиому R.

Задание 6.3 (Task 6.3) (file: propositions/tautology.py)

a. Реализуйте недостающий код для функции prove_tautology(tautology, model), которая возвращает доказательство данной тавтологии в рамках нашей стандартной аксиоматической системы, используя множество посылок, описывающее данную модель (Г_М). Если модель построена на пустом множестве посылок (по умолчанию), возвращаемое доказательство должно доказывать тавтологию без предположений.

Рекомендации:

Если модель содержит все переменные, входящие в тавтологию, просто постройте доказательство с помощью prove_in_model(tautology, model).

В противном случае рекурсивно вызовите prove_tautology() с моделями, в которых также задано значение для следующей неуказанной переменной, а затем используйте функцию reduce_assumption().

b. Реализуйте недостающий код для функции proof_or_counterexample(formula), которая либо возвращает доказательство данной формулы без посылок в рамках нашей аксиоматической системы (если эта формула является тавтологией), либо возвращает модель, в которой данная формула не выполняется (если формула не является тавтологией).

Задание 6.4 (Task 6.4) (file: propositions/tautology.py)

a. Реализуйте недостающий код для функции encode_as_formula(rule), которая возвращает формулу, "кодирующую" данное правило вывода (как кодировать было на лекции). Формула единственным образом задается по правилу, учитывая, что посылки в rule задаются упорядоченным списком [A1, A2, ..., An]. Для этого списка посылок и заключения B "кодирующая" формула выглядит так: (A1->(A2->(...(An->B)...)))

b. Реализуйте недостающий код для функции prove_sound_rule(rule), которая принимает корректное правило вывода и возвращает его доказательство в нашей стандартной аксиоматической системе.

Задание 6.5 (Task 6.5) (file: propositions/tautology.py)

Реализуйте недостающий код для функции model_or_inconsistency(formulas), которая возвращает либо модель, в которой выполняются данные формулы (если такая модель существует), либо доказательство ~(p → p) в нашей стандартной аксиоматической системе из данных формул в качестве посылок (если такая модель не существует).

Подсказка:

Если модели для данных формул не существует, то что можно сказать о правиле вывода, где посылками являются данные формулы, а заключением – ~(p -> p)?

Является ли оно корректным? Почему?

Как можно использовать решение задания 6.4 для завершения текущего задания?

Постарайтесь осознать, как код который вы пишите повторяет доказательства, которые были на лекциях.