Формальна система як орієнтований граф
Формальна аксіоматична система визначає орієнтований граф:
- Вершини: усі правильно сформовані формули, що можуть бути побудовані з символів системи
- Ребра: етапи висновування — одна формула слідує з інших за правилом висновування
- Аксіоми: відзначені вихідні вершини без вхідних ребер
- Теореми: усі вершини, досяжні з набору аксіом
Доказ теореми T: орієнтований шлях від набору аксіом до T. Доказ — це послідовність вершин A₁, A₂, ..., Aₙ = T де кожен крок слідує за правилом висновування.
Два фундаментальні властивості формальної системи, виражені геометрично:
Несуперечливість: жодна формула F і її заперечення ¬F не досяжні одночасно з аксіом. Геометрично: вершина теореми F і вершина теореми ¬F не досяжні обидві одночасно. Немає 'вибухового' шляху.
Повнота: кожна формула F або ¬F є теоремою (досяжна). Геометрично: граф сильно зв'язний у тому сенсі, що для кожної вершини F принаймні одна з F або ¬F має шлях від аксіом.
Неповнота Геделя як геометрична властивість
Курт Гедель довів у 1931 році, що будь-яка несуперечлива формальна система, достатньо потужна для виразу основної арифметики, є неповною: існують формули G такі, що ні G ні ¬G не доказуються.
Геометрично: у будь-якій досить багатій несуперечливій формальній системі є вершини у графі формул, які не досяжні з аксіом — ні вершина G ні вершина ¬G не мають шляху від набору аксіом.
Конструкція Геделя: він закодував формулу G, яка, по суті, каже: 'Я не доказуюся.' Якби G було доказуємим, система була б суперечливою (справжнє твердження каже, що воно не доказується). Якби ¬G було доказуємим, система була б суперечливою (G була б хибною, але система це доказує). Отже, ні G ні ¬G не доказуються — G є недосяжною вершиною в несуперечливій системі.
Неповнота — це не недолік обраних аксіом: Гедель показав, що це структурна властивість будь-якої несуперечливої системи, достатньо виразної для роботи з арифметикою. Недосяжні вершини не можна видалити, додавши більше аксіом, без створення нових.
Математичні об'єкти як точки в просторі
Платонів погляд на математику можна формалізувати геометрично: математичні об'єкти населяють абстрактний простір, чиї точки є самі об'єкти, а структура якого задана відносинами між ними.
Розглянемо натуральні числа ℕ = {0, 1, 2, 3, ...}. Відношення подільності визначає частковий порядок: m ділить n тоді й тільки тоді, коли m | n. Цей частковий порядок визначає геометрію — діаграму Хассе решітки подільності.
Кожне просте число сидить на мінімальній позиції над 1. Кожне складене число сидить над його простими множниками. Структура цього простору кодує всю теорію чисел.
Що робить це платонівським: структура існує незалежно від того, чи вивчає її якийсь розум. Той факт, що 7 є простим числом — що 7 не має дільників між 1 і 7 — це факт про позицію 7 в решітці подільності, незалежний від позначень, культури чи цивілізації.
Будь-яка цивілізація, яка досліджує лічення та подільність, виявить ту саму структуру. Геометрія системи чисел універсальна.
Навігація в решітці подільності
У решітці подільності найменше спільне кратне (НСК) двох чисел відповідає їхньому об'єднанню (найменша верхня межа) і найбільший спільний дільник (НСД) відповідає їхньому зустрічу (найбільша нижня межа).
НСД можна обчислити за допомогою алгоритму Евкліда: НСД(a, b) = НСД(b, a mod b), завершуючись коли b = 0.
Що абстракція прибирає
Геометрична абстракція: проектування високовимірного об'єкту на нижчовимірний підпростір. Проекція втрачає інформацію (координати не у підпросторі), але досконало зберігає структуру підпростору.
Математична абстракція працює так само. Група — це набір з однією бінарною операцією, що задовольняє чотирьом аксіомам. Абстрагування до структури групи прибирає: конкретні елементи, обчислювальне правило операції, будь-яку додаткову структуру (порядок, метрику, топологію). Що залишається: каркас чотирьох аксіом.
Винагорода: кожна теорема про групи застосовується до УСІХ груп — цілих чисел при додаванні, обертань при композиції, перестановок при композиції, симетрій молекули, груп Галуа поліноміальних рівнянь — одночасно. Абстрактна теорема доказується один раз; її екземпляри вільні.
Ось чому чисті математики опираються додаванню припущень, специфічних для домену: кожне додане припущення обмежує застосовуваність теореми. Теорема про поля (додаючи мультиплікативний обернений елемент) застосовується до менших структур, ніж теорема про кільця (мультиплікативний обернений елемент не потрібен).
Компроміс точності та універсальності
Є компроміс: більш абстрактні теореми застосовуються ширше, але говорять менше про конкретні екземпляри. Теорема про векторні простори над полем говорить менше про ℝ^n, ніж теорема саме про ℝ^n (де визначені відстань і кут).
Імплікований Геммінгом закон: абстрагуйте настільки далеко, наскільки це можливо, збереігаючи властивості, які вам потрібні. Абстрагуйте занадто далеко, і ваші теореми стають порожньо загальними ('будь-яка множина з будь-якою операцією задовольняє...'). Абстрагуйте занадто мало, і ваші теореми не передаються новим застосуванням.