Це переклад першої статті від Филип Уайшчак (Filip Łajszczak) - https://filip.lajszczak.dev/lean-4-with-a-math-textbook—part-1—defining-sets-and-membership.html про формалізацію класичної теорії множин від Хелени Расьової у Lean4

Ми починаємо наше дослідження книги Хелени Расьової «Introduction to Modern Mathematics» шляхом формалізації в Lean 4. Ми опрацюємо Розділ I, Параграф 1 - «Поняття множини», перекладаючи класичні математичні визначення в типо-теоретичні засади. Дивіться вступ для контексту та мотивації.

Визначення з підручника у порівнянні із предикатним кодування Lean

Расьова починає перший розділ словами:

Поняття множини є одним із фундаментальних понять математики. Як приклади множин можна навести: множину всіх книг у певній бібліотеці; множину всіх літер грецького алфавіту; множину всіх цілих чисел; множину всіх сторін даного многокутника; множину всіх кіл на даній площині.

Далі вона встановлює своє визначення членства:

Об’єкти, які належать до даної множини, називаються її елементами. Твердження про те, що елемент a належить множині $A$ (або: що a є елементом множини $A$), записується так:

\[a \in A \tag{1}\]

Коли множини вперше вводяться в підручнику, вони подаються просто як сукупності об’єктів, але, попри таке представлення, Расьова явно пов’язує множини з властивостями. Щоб чітко встановити зв’язок із представленням множин у Lean, нам потрібно зробити короткий крок уперед - до Розділу 5:

Коли розглядаються підмножини деякого універсуму 𝑋, поняття підмножини часто ототожнюється з властивістю, яка є атрибутом кожного елемента цієї підмножини й не є атрибутом жодного іншого елемента цього універсуму. Тоді, якщо $A \subseteq X$, запис $x \in A$ замінюють на $A(x)$ і читають як «$x$ має властивість $A$».

Це, здається, створює важливий місток до нашого програмного подання в Lean. Расьова показує, що множини та властивості - це два способи вираження одного й того самого математичного змісту. Визначення на основі властивостей - саме те, що ми будемо використовувати для формалізації множин у Lean.

Щоб закодувати це в Lean, нам спочатку потрібно виконати деякі налаштування

Спочатку ми імпортуємо класичну логіку для розміркувань про заперечення та суперечності:

open Classical

Директива open Classical надає доступ до класичних логічних принципів, таких як закон виключеного третього (кожне твердження є або істинним, або хибним) та доведення від супротивного. Хоча для наших базових визначень це не є необхідним, ці принципи стануть важливими під час доведення властивостей, що містять заперечення та відношення «не є підмножиною».

Це піднімає цікаве питання щодо засад. Теорія залежних типів (як уже згадувалося у вступі) зазвичай пов’язується з конструктивною логікою, де існування доводиться шляхом побудови, а не від супротивного. Проте тут ми використовуємо класичні міркування для формалізації класичної теорії множин Расьової. Підхід Lean виглядає прагматичним: його логіка за замовчуванням є конструктивною, але класичні принципи доступні як аксіоми, коли вони потрібні. Оскільки міркування Расьової за своєю природою є класичними (вона застосовує доведення від супротивного та виходить із закону виключеного третього), ми дотримуємося її математичного стилю, а не намагаємося здійснити конструктивне переосмислення. Такий вибір віддає перевагу точному відтворенню її математичних міркувань над засадничою «чистотою».

Ці основні питання стають особливо актуальними, коли ми звертаємось до пізніших розділів Расьової, присвячених аксіомам теорії множин (Розділ 6), ширшому розгляду аксіоматики множин (Розділ 9) та її обговоренню аксіоматичних підходів, включно з парадоксом Рассела (Розділ 10). Якщо ми згодом пройдемо ці розділи, то зіткнемося з глибшими питаннями про те, як різні фундаментальні системи - класична теорія множин, конструктивна теорія типів та різні аксіоматичні підходи - співвідносяться між собою.

Далі нам потрібно оголосити рівень універсуму:

universe u

Рівні універсумів у теорії типів розв’язують парадокс Рассела. Ми не можемо мати «тип усіх типів», адже це призводить до суперечностей. Натомість Lean створює ієрархію: Type 0, Type 1, Type 2 тощо. Оголошення universe u вводить змінну рівня універсуму, яка може відповідати будь-якому рівню в цій ієрархії.

Далі нам потрібно оголосити змінну типу:

variable {α : Type u}

Змінні типів, такі як α : Type u, дозволяють нам писати узагальнені визначення, що працюють для будь-якого типу елементів. Замість того щоб створювати окремі визначення для NatSet, StringSet, BoolSet тощо, ми пишемо одне визначення RasiowaSet α, яке підходить для будь-якого типу α. Фігурні дужки {α : Type u} роблять α неявним параметром - Lean визначає його з контексту, тож нам не потрібно щоразу вказувати його явно.

І нарешті, ми можемо визначити наш тип RasiowaSet:

def RasiowaSet (α : Type u) : Type u := α → Prop

У Lean Prop - це тип висловлювань, тобто тверджень, які можуть бути істинними або хибними. Приклади: 2 + 2 = 4 (істинне), 1 = 0 (хибне) або x > 5 (залежить від значення x). На відміну від обчислень, що повертають значення, висловлювання потребують доказів, аби встановити їхню істинність.

Отже, α → Prop означає «функцію, яка приймає елемент типу α та повертає висловлювання». Це добре відображає ідею властивості: дай мені елемент, і я сформулюю твердження про те, чи задовольняє цей елемент дану властивість.

Звісно, у Lean вже є вбудований тип множин для цього, але ми оголошуємо власний RasiowaSet, щоб у майбутньому мати змогу розвивати його далі.

Підручникові множини та предикатні функції в Lean, здається, представляють одне й те саме математичне поняття, але на різних засадах:

  • Підручник: множини - це сукупності; належність є первинним поняттям; властивості випливають із підмножин.
  • Lean: властивості є первинними; множини - це предикати; належність зводиться до застосування функції.

Переклад належності:

def mem (a : α) (A : RasiowaSet α) : Prop := A a

Оскільки ми оголосили змінну {α : Type u} на початку, Lean автоматично визначає параметр типу в усіх наших означеннях.

Отже, належність визначається як функція, що приймає елемент a типу α та предикат A типу RasiowaSet α, а потім застосовує предикат A до елемента a.

Але ми хочемо використовувати математичне позначення ∈ замість mem:

infixr:50 " ∈ " => mem

Цим ми оголошуємо ∈ як інфіксний оператор із правою асоціативністю та пріоритетом 50. Частина infixr:50 відповідає за розбір (як Lean читає символи), а => mem надає йому обчислювальне значення (яку функцію насправді викликати). Коли ми пишемо a ∈ A, Lean за лаштунками перекладає це у mem a A.

У Lean вираз a ∈ A розгортається у A a - твердження про те, що «a має властивість A». Оскільки A : RasiowaSet α визначено як α → Prop, це означає, що A є функцією, яка приймає елемент типу α та повертає висловлювання (Prop). Застосувавши A до елемента a, ми отримуємо A a : Prop - твердження, яке або доводиться (істинне), або не доводиться (хибне). Якщо A a доводиться, ми кажемо «a задовольняє властивість A» або «a має властивість A». Якщо ж A a не доводиться, тоді «a не має властивості A».

Наприклад, якщо A позначає властивість «бути парним числом», то A 4 є твердженням «4 є парним» (довідне), а A 3 - твердженням «3 є парним» (недовідне). Отже, 4 ∈ A істинне, а 3 ∈ A - хибне. Це безпосередньо пов’язується з ідеєю Расьової: множини та властивості - це одне й те саме, тільки розглянуте під різними кутами.

Належність-заперечення: Формула (2)

Расьова визначає неналежність у формулі (2):

Твердження про те, що $a$ не належить множині $A$ (тобто $a$ не є елементом множини $A$), записується так:

\[a \notin A \quad \text{or} \quad \sim(a \in A) \tag{2}\]

Символ ∼ завжди означатиме «не» або «не є так, що».

У Lean ми визначаємо це як заперечення належності:

def not_mem (a : α) (A : RasiowaSet α) : Prop := ¬(a ∈ A)
infixr:50 " ∉ " => not_mem

Порожня множина

Расьова вводить порожню множину:

Зручно ввести в математику поняття порожньої множини, тобто множини, яка не має жодного елемента. Наприклад, можна сказати, що множина всіх дійсних коренів рівняння $𝑥^2 + 1 = 0$ є порожньою, замість того щоб формулювати: «не існує жодного дійсного числа, яке є коренем рівняння $𝑥^2 + 1 = 0$».

Вона зазначає, що «порожня множина позначається символом ∅».

У предикатному кодуванні Lean:

def empty : RasiowaSet α := fun _ => False
notation "∅" => empty

Синтаксис fun _ => False створює функцію (лямбду), яка ігнорує свій аргумент (позначений _) і завжди повертає False. Це відображає ідею, що жоден елемент не задовольняє умову порожньої множини.

Порожня множина - це умова, яка ніколи не виконується. Для будь-якого елемента a:

  • a ∈ ∅ розгортається у empty a (за означенням ∈),
  • empty a розгортається у (fun _ => False) a (за означенням empty),
  • це β-скорочується до False (застосування лямбда-функції).

Скінченні множини та одноелементні множини: Формули (3) і (4)

Расьова вводить позначення для скінченних множин:

Множина, всі елементи якої - $a_1,…,a_n$, позначатиметься так:

\[\lbrace a_1, \dots, a_n \rbrace \tag{3}\]

Далі вона визначає одноелементні множини:

Множина може також складатися лише з одного елемента. Наприклад, множина всіх парних простих чисел має рівно один елемент - число 2. Множина, єдиним елементом якої є 𝑎, за аналогією з (3) позначатиметься так:

\[\lbrace a \rbrace \tag{4}\]

У Lean ми можемо визначити одноелементні множини так:

def singleton (a : α) : RasiowaSet α := fun x => x = a

Це визначає одноелементну множину, що містить лише елемент a, як предикат «x дорівнює a».

Розбір конкретного прикладу

Щоб побачити, як наше кодування працює на практиці, визначимо конкретну множину і доведемо, що певний елемент належить їй. Працюватимемо з множиною $\lbrace 1, 2 \rbrace$ і продемонструємо покроковий процес перевірки належності.

Ключове слово example створює анонімний доказ для демонстраційних цілей. На відміну від theorem, воно не дає доказові імені, за яким можна було б посилатися пізніше - воно просто перевіряє, що твердження є довідним.

Тактики - це команди, які допомагають будувати докази інтерактивно: вони перетворюють цілі доказу крок за кроком, поки не дістанемося до чогось, що можна довести. Тут ми використовуємо ключове слово by, щоб увійти в режим тактик для покрокової побудови доказу. Тактика right обирає праву частину диз’юнкції (∨) - у нашому прикладі вона вибирає доведення 2 = 2 замість 2 = 1. Тактика rfl доводить мету 2 = 2 за допомогою рефлексивності рівності.

-- Визначте множину, що містить 1 та 2
def exampleSet : RasiowaSet Nat := fun x => x = 1 ∨ x = 2

-- Перевірте, чи 2 належить до цієї множини
example : 2 ∈ exampleSet := by
  -- Крок 1: 2 ∈ exampleSet стає mem 2 exampleSet
  -- Крок 2: За визначенням mem: exampleSet 2 
  -- Крок 3: За визначенням exampleSet: (fun x => x = 1 ∨ x = 2) 2
  -- Крок 4: Бета-зменшення: 2 = 1 ∨ 2 = 2
  -- Крок 5: Це можна довести, використовуючи правий диз'юнкт: 2 = 2
  right
  rfl

Бета-редукція - це процес застосування лямбда-функції до її аргументу, тобто підстановки параметра фактичним значенням.

Тепер, коли ми визначили базове кодування множин як предикатів і побачили, як працює належність на практиці, ми можемо вийти за межі окремих елементів і дослідити відношення між цілими множинами. Наступним природним кроком у розвитку підходу Расьової є поняття підмножини - випадок, коли одна множина повністю міститься в іншій. Це познайомить нас із універсальною квантифікацією в Lean і покаже, як математичні твердження про «всі елементи» перетворюються на формальні докази.

Далі: Частина 2 - Підмножини