Пить или не пить?
Программисты привыкли мыслить в рамках булевой логики. Я хочу немножко поломать классические программистские представления о том, что такое логично.
В классической математической логике есть такое понятие: пропозиция. Она же утверждение, суждение и т.д. Утверждение может быть верным, верным может быть и его отрицание. Пока вроде всё нормально:
int p=1;
if (p) {
printf ("OK!\n");
}
int p=0;
if (!p) {
printf ("OK!\n");
}
Но это — булева логика. В более общем описании понятие утверждения можно сформулировать так:
Суждение верно, когда имеет хотя бы одно доказательство.
Есть суждения, которые верны (доказаны) по определению. Если помните школьную математику, их там называли аксиомами или гипотезами. А теперь ловкость рук.
Вот список аксиом в некой вселенной:
- Когда у Петровича зарплата, он пьян.
- Когда у Петровича зарплата, он трезв.
Может ли существовать такая вселенная, есть ли тут логическое противоречие, из которого следует абсурдность самого её существования?
Нет, со вселенной всё хорошо. Потому что ни из чего не следует, что Петровичу выдали зарплату, а следовательно во вселенной нет повода для противоречий. Чтобы возникло противоречие и вселенная разрушилась, необходимо ввести ещё одну аксиому:
- У Петровича зарплата.
И да, и нет?
На самом деле, дилемма Петровича сводится к закону противоречия, на котором построена математика и чуть ли не все точные науки:
\begin{equation} P \land \neg P \implies \bot \end{equation}
«Утверждение \(P\) одновременно с утверждением \(\text{not } P\) — абсурдно, не имеет доказательств». Но прежде надо нашей вселенной оказаться в такой позе, чтобы вот это «не имеет доказательств» из закона противоречия выстрелило. Поэтому зарплаты Петровичу не видать.
Для начала, формализуем Петровича, который счастлив, потому что пьёт:
(* Определим список необходимых переменных, которые имеют тип «пропозиция» (утверждение) *)
Variables PetrovichHasSalary PetrovichDrinks PetrovichIsHappy : Prop.
(* Аксиома a1 : когда верно утверждение что у Петровича зарплата, верно и утверждение, что он пьёт *)
Axiom a1 : PetrovichHasSalary -> PetrovichDrinks.
(* Аксиома a2 : когда верно утверждение что Петрович пьёт, верно и утверждение о его счастливой жизни *)
Axiom a2 : PetrovichDrinks -> PetrovichIsHappy.
(* Аксиома a3 : безусловно доказывает, что зарплата у Петровича есть *)
Axiom a3 : PetrovichHasSalary.
(* Теорема 'he_is_happy' к доказательству: Петрович счастлив *)
Theorem he_is_happy : PetrovichIsHappy.
(* Нам надо доказать верность утверждения PetrovichIsHappy. Из аксиомы a2 известно, что он счастлив,
когда он пьёт. Применим это утверждение. *)
apply a2.
(* После применения a2 надо доказать, что Петрович пьёт. Верность этого утверждение может следовать из
аксиомы a1. Попробуем её применить *)
apply a1.
(* Теперь осталось доказать, что у Петровича есть зарплата. Это легко, ведь именно это утверждает
аксиома a3. Мы можем её применить, а можем подставить в качестве доказуемого. Варианты
применения тактик:
- apply a3.
- exact a3.
Для разнообразия, применим тактику exact *)
exact a3.
(* Подзадач не осталось. Теорема доказана *)
Qed.
Теперь можем использовать теорему he_is_happy в качестве тезиса всякий раз когда надо показать, что Петрович счастлив.
Аргументированные утверждения (но не совсем)
А что если пить предстоит Петровичу, а зарплата у жены Марьи? Как нам это обозначить? На помощь приходят предикаты, или утверждения с аргументами. Для начала, перепишем доказательство выше с помощью предикатов:
(* Утверждение "человек" *)
Variable Human : Prop.
(* Петрович и Марья - люди *)
Variables Petrovich Maria : Human.
(* Утверждение "оно пьёт" требует указания личности *)
Variable IsDrinking : Human -> Prop.
(* Аналогично с утверждениями "оно хранит зарплату" и "оно счастливо" *)
Variable HoldingSalary : Human -> Prop.
Variable IsHappy : Human -> Prop.
(* Аксиома a1 : когда верно утверждение что у Петровича зарплата, верно и утверждение что он пьёт *)
Axiom a1 : HoldingSalary Petrovich -> IsDrinking Petrovich.
(* Аксиома a2 : пьющий Петрович — счастливый Петрович *)
Axiom a2 : IsDrinking Petrovich -> IsHappy Petrovich.
(* Аксиома a3 : эта аксиома доказывает, что зарплата у Петровича всё же есть *)
Axiom a3 : HoldingSalary Petrovich.
(* Теорема 'petrovich_is_happy' к доказательству: Петрович счастлив *)
Theorem petrovich_is_happy : IsHappy Petrovich.
apply a2.
apply a1.
exact a3.
Qed.
Теперь можно попробовать доказать, что Петрович несчастлив, когда Марья успела отобрать зарплату. Для этого нам необходимо ввести несколько уточняющих импликаций (связей):
- Петрович несчастлив, когда не пьёт
- Петрович не пьёт, когда нет денег
- Зарплата может быть только у одного из них
Variable Human : Prop.
Variables Petrovich Maria : Human.
Variable IsDrinking : Human -> Prop.
Variable HoldingSalary : Human -> Prop.
Variable IsHappy : Human -> Prop.
Axiom a1 : HoldingSalary Petrovich -> IsDrinking Petrovich.
Axiom a2 : IsDrinking Petrovich -> IsHappy Petrovich.
(* Зарплата в этот раз у Марьи *)
Axiom a3 : HoldingSalary Maria.
(* Без водки счастья нет *)
Axiom a4 : ~ IsDrinking Petrovich -> ~ IsHappy Petrovich.
(* Без зарплаты нет водки *)
Axiom a5 : ~ HoldingSalary Petrovich -> ~ IsDrinking Petrovich.
(* Когда зарплата у Марьи - у Петровича её нет *)
Axiom a6 : HoldingSalary Maria -> ~ HoldingSalary Petrovich.
(* Теорема 'petrovich_is_unhappy' к доказательству: счастья у Петровича нет *)
Theorem petrovich_is_unhappy : ~ IsHappy Petrovich.
(* Без водки счастья нет *)
apply a4.
(* Нет водки, поскольку нет зарплаты *)
apply a5.
(* Надо доказать, что зарплаты у Петровича нет. Применим аксиому a6, которая доказывает, что
у Петровича действительно нет зарплаты, когда она у Марьи *)
apply a6.
(* ... А зарплата действительно у Марьи, ведь это утверждает аксиома a3 *)
apply a3.
Qed.
Кстати, можно посмотреть доказательство теоремы с помощью команды
Print petrovich_is_unhappy.:
petrovich_is_unhappy = a4 (a5 (a6 a3))
: ~ IsHappy Petrovich
Абсурд и бездоказательность
В Coq есть два утверждения, названия для которых, по мнению многих, выбраны не совсем удачно:
True, она же \(\top\). Это утверждение, которое всегда доказано.False, или \(\bot\). Утверждение, не имеющее доказательств.
На самом деле, отрицание утверждения (\(\neg P\)) равносильно импликации вида:
\begin{equation} P \implies \bot \end{equation}
То есть, буквально, «Из \(P\) следует, что доказательства не существуют». А раз доказано, что нет доказательств \(P\), то доказано отрицание \(P\).
Бездоказательность можно доказать, и иногда это очень удобно. Докажем, что когда одновременно верно «быть» и «не быть», то конструкция слишком шатка, чтобы быть верной:
(* Объявляем секцию. Поскольку ниже мы захотим видоизменять гипотезы (они же переменные),
необходимо локализовать их в секции *)
Section ToBeAndNotToBe.
Variable Be : Prop.
(* Гипотеза доказывает утверждение «быть» *)
Variable to_be : Be.
(* Гипотеза доказывает утверждение «не быть» *)
Variable not_to_be : ~ Be.
(* Необходимо доказать, что это не имеет доказательств *)
Theorem this_is_absurdity : False.
(* Гипотезу «не быть» заменим на утверждение «быть → не имеет доказательств» *)
unfold not in not_to_be.
(* Поскольку нам надо доказать False («не имеет доказательств»), мы можем смело
применить нашу видоизмененную not_to_be *)
apply not_to_be.
(* Теперь нам осталось доказать «быть». Это легко т.к. именно это утверждает гипотеза to_be *)
apply to_be.
Qed.
(* Всё, после доказательства to_be доказывать больше нечего.
Теорема об отсутствии доказательств доказана *)
End ToBeAndNotToBe.
Горе Петровича
Теперь, имея представление о том, как доказать бездоказательность, мы вынуждены огорчить Петровича фактом, что счастливая жизнь с зарплатой у Марьи невозможна.
Section PetrovichInTrouble.
Variable Human : Prop.
Variables Petrovich Maria : Human.
Variable IsDrinking : Human -> Prop.
Variable HoldingSalary : Human -> Prop.
Variable IsHappy : Human -> Prop.
Axiom a1 : HoldingSalary Petrovich -> IsDrinking Petrovich.
Axiom a2 : IsDrinking Petrovich -> IsHappy Petrovich.
Axiom a3 : HoldingSalary Maria.
Axiom a4 : ~ IsDrinking Petrovich -> ~ IsHappy Petrovich.
Axiom a5 : ~ HoldingSalary Petrovich -> ~ IsDrinking Petrovich.
Axiom a6 : HoldingSalary Maria -> ~ HoldingSalary Petrovich.
(* Предположим, что ни смотря ни на что Петрович всё ещё счастлив *)
Axiom a7 : IsHappy Petrovich.
(* Задача доказать невозможность такой комбинации аксиом *)
Theorem sorry_petrovich : False.
(* Чтобы доказать абсурдность, воспользуемся законом противоречия, который утверждает False, когда
пропозиция одновременно и верна, и не верна. Докажем, что у нас одновременно верно утверждение,
что Петрович счастлив и верно обратно утверждение. Знакомьтесь, тактика absurd *)
absurd (IsHappy Petrovich).
(* Строчка выше доказала False, но теперь предлагает доказать верность двух новых утверждений.
Сначала докажем, что утверждение о счастье Петровича неверно: *)
apply a4.
apply a5.
apply a6.
apply a3.
(* Теперь докажем, что утверждение о счастье Петровича верно: *)
apply a7.
Qed.
(* Больше доказывать нечего, абсурдность доказана *)
End PetrovichInTrouble.