Програма інтуїціонізму, Гуманітарна енциклопедія
Програма інтуїціонізму, або інтуїціонізм - це один з трьох головних напрямів (поряд з логіцизмом і формалізмом), що традиційно виділяються в підставах математики та логіки (див. Логіка), в основі якого лежить принцип математичної побудови. Основна відмінність інтуїціонізму від інших напрямів у тому, що він ставить іншу мету математики: не доказ «істинних» теорем, а пошук «інтуїтивно переконливих» та «наглядно-змістовних» математичних («розумових», у термінології первісного інтуїціонізму) конструкцій, що органічно поєднують у собі побудова та її обгрунтування; при цьому побудова є єдиним засобом обґрунтування математики. Інтуїціонізм відкидає використання в математиці та логіці ідеї актуальної нескінченності та погляд на логіку як на науку, що «передує» математиці. Головним об'єктом інтуїціоністської критики став широко використовується в класичній математиці та логіці закон виключеного третього (див. Закон виключеного третього). Відповідно до інтуїціонізму, вся математика повинна спиратися на інтуїтивне уявлення низки натуральних чисел і принцип математичної індукції, тлумачений як вимога діяти послідовно, крок за кроком; допускаються лише конструктивні докази існування об'єкта, що розглядається, що вказують спосіб його побудови. Представники інтуїціонізму вважають, що чиста математика є розумової активністю, яка залежить від мови, її об'єкт — нелінгвістичні математичні конструкції. Мова служить лише повідомлення математичних ідей, математика не зводиться до мови і більше не може бути витлумачена як особлива мова. Предметом дослідження (математичної) логіки є математична мова, яка більш-менш адекватно передаєматематичні побудови. Логіка вторинна стосовно математики, остання може бути обгрунтована з допомогою логічних засобів.
Попередниками інтуїціонізму є німецький математик ХІХ століття Л. Кронекер, французькі ефективісти, А. Пуанкаре та Е. Борель. Вони з різних позицій наголошували на ознаках неблагополуччя в математиці, пов'язані з тим, що в класичній математиці докази багатьох теорем існування не дають побудов шуканих об'єктів, і намагалися дещо обмежити математичні конструкції для усунення цього недоліку. Ідеї інтуїціонізму в явному вигляді були сформульовані на початку XX століття голландським ученим Л. Е. Я. Брауером, який в 1907 році показав, що коріння багатьох небажаних властивостей класичної математики сягає класичної логіки і висунув програму радикальної перебудови математики, протиставивши її концепції знання до логіки (програма логіцизму - див. Логіцизм) та тлумачення математики виключно як мови математичних символів (програма формалізму - див. Формалізм). Ідеї Брауера були розвинені Г. Вейлем (Німеччина) та А. Гейтінгом (Нідерланди). До 1945 року інтуїціонізм розвивався переважно в Голландії, хоча деякі фундаментальні роботи були створені в Укаїні, Австрії та Польщі вченими, які не зараховували себе до цього напряму. Нині найсильнішою школою інтуїціонізму залишається голландська, але, крім неї, є, зокрема, американська та українська школи. Для загальної характеризації напрямів, що виросли з інтуїціонізму, часто користуються терміном конструктивізм (див. математичний Конструктивізм). Тому слід розрізняти інтуїціонізм у вузькому значенні (брауеровський), український конструктивізм та різні частково конструктивні напрямки, які часто також називають сучасним.інтуїціонізмом.
Підстави для висновків Брауера (з дещо модернізованої точки зору) є такими. Відповідно до теореми К. Геделя про неповноту, у досить багатої теорії є така формула G, що ні вона, ні її заперечення недоведені. За допомогою класичної логіки легко вивести: ∃x(G ⇒ x = 0) & (⌉G ⇒ x = l). Позначимо цю формулу ∃xA(x). Для жодного конкретного x0 не можна довести A(x0). Теоретично множин ситуація погіршується лише незначно. Аксіома вибору дає можливість побудувати таку доведену формулу ∃хВ(x), що не можна побудувати формулу C(x), для якої ∃l xC(x) та ∀x(C(x) ⇒ B(x)). Така сама ситуація виникає під час використання альтернативи до аксіоми вибору — аксіоми детермінованості.
Відповідно до аналізу А. А. Маркова, класична математика базується на трьох абстракціях: абстракції ототожнення, що не дозволяє використовувати властивості, що розрізняють рівні об'єкти; абстракції потенційної здійсненності, що дозволяє знехтувати фізичними обмеженнями на реалізованість дуже великих кінцевих об'єктів і процесів, і абстракції актуальної нескінченності, що дозволяє мислити нескінченні сукупності як завершені і використовувати нескінченні множини і нескінченні процеси для побудови інших математичних об'єктів. Брауер прийняв дві перші абстракції та відкинув третю. У цьому з ним солідарні майже всі нинішні продовжувачі конструктивних традицій математики. У деяких розділах сучасного інтуїціонізму це припущення послаблюється, а в деяких посилюється. Але в будь-якому випадку беруться до уваги принципові обмеження здійсненних побудов: необхідність зведення будь-якого нового завдання до вже вирішених, щоб представити нову побудову як композицію старих.
За такого підходу логіка неспроможна розглядатися якщось дане a priori, вона повинна підбиратися відповідно до класу об'єктів, що розглядаються, і з класом допустимих методів вирішення завдань. Так, класична логіка виявляється або логікою кінцевих об'єктів, або логікою всіх теоретико-множинних побудов з аксіомою вибору. Сама інтерпретація логічних формул змінюється докорінно. Значення істинності є щось другорядне проти конкретним побудовою, проведеним за підтвердження теореми. Тому формули інтерпретуються як завдання, логічні зв'язки - як перетворення завдань, методи доказу - як методи зведення нових завдань до вже вирішеним або прийнятим як вирішені. Брауер запропонував скористатися для перебудови математики логікою, подібною до класичної, за винятком законів виключеного третього та зняття подвійного заперечення (які в даному контексті еквівалентні) — інтуїціоністською логікою (див. Логіка інтуїціоністська). Він відмовився від багатьох об'єктів, створених у теоретико-множинні математики, і обмежився тими, які хоча б побічно зводяться до двох вихідних сутностей: до конструктивних об'єктів, що будуються як кінцеві конструкції з кінцевого числа вихідних ясно помітних об'єктів, і до послідовностей вибору, що представляють з методи послідовного конструювання потенційно нескінченного числа вихідних об'єктів. Прикладами послідовностей вибору є алгоритми, послідовності вимірів фізичних величин тощо. Спочатку Брауер намагався прямо перебудувати основні розділи математики, причому він, зокрема, раніше, ніж це було зроблено класичними засобами, встановив важливий результат (теорема про віяли або лема Кеніга): дерево з кінцевим розгалуженням і кінцевими шляхами звичайно. Перебудова математики,здійснювалася Брауером, відрізнялася максимальною обережністю за дотримання принципів конструктивності. Він прагнув урятувати все, що можна було врятувати. Приклади набагато жорсткіших підходів продемонстрували Р. Л. Гудстейн і Н. А. Шанін.
Найбільш цікавими є наступні результати Брауера. Оператори над послідовностями вибору повинні використовувати кінцеве число значень послідовності отримання кінцевої вихідної інформації. На основі цього він довів безперервність інтуїціоністських функцій дійсної змінної. Брауер показав, що у різних галузях математики використовувалися різні поняття функції дійсної змінної, зокрема, що вимірні функції не варто для конструктивних цілей трактувати як оператори над дійсними числами. Відразу після формалізації інтуїціоністської логіки багато математиків почали розвивати варіації інтуїціонізму, або ще сильніше обмежуючи логіку, або ще сильніше обмежуючи об'єкти. Йохансон запропонував використовувати як основу для інтуїціонізму мінімальну логіку, але виявилося, що в будь-якій теорії, що містить натуральні числа, визначне інтуїціоністське заперечення, і перехід до мінімальної логіки нічого нового не дає. Д. Гріс запропонував розглядати безнегативну математику, у якій заборонено порожні поняття типу квадратного кола. Просування в даному напрямку йде дуже повільно незвичайності та труднощі конструкцій, що виникають.
Новий імпульс дослідженням у галузі інтуїціоністських понять дали інтерпретація інтуїціоністської логіки А. Н. Колмогоровим та її (логіки) формалізація А. Гейтингом. На цій основі та на основі точного поняття алгоритму С. К. Кліні (1945) дав першу точну класичну модель некласичної математики: поняття реалізованості. Уінтерпретації Кліні стало можливим формально висловити тезу А. Чорча як схему аксіом.
А. А. Марков (1947) і радянська школа конструктивізму розвинули варіант математики, що послідовно проводить ідею про те, що немає нічого, крім конструктивних об'єктів, а алгоритми ототожнюються з їхніми програмами. Він запровадив «принцип Маркова», який явно розділив обгрунтування і побудови, різниця між якими від початку відчувалася в інтуїціонізмі. Змістовно принцип Маркова говорить, що з обгрунтування вже зроблених побудов можна скористатися класичної логікою (це показав М. А. Шанін, побудувавши алгоритм конструктивної розшифровки, що розбиває будь-яку формулу на явне побудова і класичне обгрунтування даного побудови). Польська школа пішла іншим шляхом, обмежуючись конструктивними об'єктами, але зберігаючи класичну логіку.
Реалізованість виявила, що інтуїціоністські теорії можуть розходитися з класичними. Наприклад, якщо A(x) — нерозв'язна властивість натуральних чисел, то конструктивно вірна формула — ∀x(A(x) ∨ ⌉A(x)). Зафіксувавши поняття послідовності, що обчислюється, ми зберігаємо свободу при визначенні операторів вищих типів. Першим це показав Кліні, побудувавши загальнорекурсивну реалізованість, при якій виконано схему: ∀x (⌉A(x) ⇒ ∃yВ (x, y)) ⇒ ∀x∃y(⌉A(x) ⇒ B(x, y)) , Виражає всюди визначеність всіх функцій. Можливість висловити формулами першого порядку ті висловлювання, котрим класичної логіці потрібні конструкції вищих порядків — ще одна перевага інтуїціонізму. Принцип Маркова несумісний з цією схемою у всіх змістовних інтуїціоністських теоріях, хоча обидва є класичними тавтологіями.
Е. Бішоп (1960), перевизначивши обчислювані функціонали, запропонував варіант інтуїціонізму, що характеризуєтьсяпринципом: «використовувати лише алгоритми, але цього не говорити». Цей варіант, надалі розвинений багатьма вченими, зокрема П. Мартін-Лефом, поєднав багато переваг брауеровського та марківського підходів.