Coq: Азы классической логики для алкоголиков

Пить или не пить?

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

В клас­си­чес­кой ма­те­ма­ти­чес­кой ло­ги­ке есть та­кое по­ня­тие: про­по­зи­ция. Она же утверж­де­ние, суж­де­ние и т.д. Утверж­де­ние мо­жет быть вер­ным, вер­ным мо­жет быть и его от­ри­ца­ние. Пока вро­де всё нор­маль­но:

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.

Бес­цен­ные ссыл­ки