Інтуїціоністська логіка, Поняття та категорії
ІНТУІЦІОНІСТСЬКА ЛОГІКА – спочатку логіка інтуїціоністської математики, що згодом отримала ширше застосування. Неформально розвивалася Л.Брауером з 1907 р., першу інтерпретацію, незалежну від інтуїціоністської ідеології, дав А.М.Колмогоров, перші формалізації побудували В.Глівенко та А.Гейтінг.
Мова інтуїційної логіки збігається з мовою класичної логіки. Зберігаються й правила природного висновку всім зв'язок, крім заперечення. Для заперечення правило зняття подвійного заперечення послаблюється до правила «З неправди слід усе, що завгодно». У результаті послаблюються можливості опосередкованого висновку – опосередковано можна спростовувати (за правилом reductio ad absurdum), але, взагалі кажучи, не можна доводити позитивні судження від протилежного.
В інтуїціоністській логіці усі зв'язки незалежні. Більше того, для доказу затвердження А достатньо користуватися лише формулами, які не містять зв'язок, відсутніх в А. В інтуїціоністській логіці немає стандартних (нормальних) форм, аналогічних класичним. Як правило, перетворення, пов'язані із законами формулювання заперечень та приведення до попередньої форми, діють лише в один бік. Так, напр., вірно Α∨Β⇒ (Α&Β), а (А&В) ⇒Α∨Β виконано не завжди. Сильний виключений третій закон (tertium non datur) відкидається, але його слабка форма «А та його заперечення не можуть бути одночасно помилковими» (Α∨Α), зберігається. Тому неправильно трактувати інтуїціоністську логіку як таку, що вводить додаткові істиннісні значення, вона швидше відкидає саму концепцію логічних значень.
Інтуїціоністська логіка має низку видатних властивостей у класі некласичних логік. Для неї виконано теорему Крейга про інтерполяцію: «Якщо виводиться А⇒С, то можна побудувати формулуВ, що містить лише терміни, що входять і в А, і С, таку, що виводяться А⇒В, В ⇒С» і теорема Бета про визначальність: «Якщо в сигнатурі σ виділена підсишатура σ0, і термін Τ не належить σ0, але зберігає те саме значення всім моделей теорії Th, у яких збігаються значення термінів з σ0, то визначимо через σ0 теоретично Th.»
Ці дві теореми зберігаються лише малого числа некласичних логік. Найбільш поширеною властивістю є нормалізованість висновків, що дозволяє в принципі усунути леми з доказів. Воно також виконане для інтуїціоністської логіки.
Виконано для неї та властивість коректності щодо ∨ та ∃: якщо доведено А∨В, то доведено або А, або В; якщо доведено ∃хА(х), то деякого t доведено А(t). Цією властивістю класична логіка не має. Інтуїціоністська логіка - єдина логіка серед континууму логік з тією ж мовою, що і класична, для якої виконані всі ці властивості.
Таким чином, вона може бути основою змістовних математичних теорій, оскільки в ній інтуїтивна означність збігається з формальною. Хоча безлічі теорем та доказів інтуїціоністської логіки за обсягом уже відповідних множин класичної, остання вкладається в інтуїціоністську. Першим таке занурення здійснив Глівенко. Таким чином, виразні можливості інтуїціоністської логіки сильніші за класичну. У свою чергу К.Гедель показав, що інтуїціоністська логіка вкладається в модальну логіку S4. При цьому зануренні зв'язки &, ∨, ∃ залишаються без зміни, а на елементарні формули та на результати застосування інших зв'язок навішується модальність.
Інтуїціоністська логіка не може бути описана жодною кінцевою системою логічних значень, і, більше того, для неї неприродноопис з допомогою таблиць істинності (хоча рахункозначні таблиці істинності нею існують). Але вона має кілька математичних інтерпретацій. Історично першою була інтерпретація А.Тарського. У ній значеннями істинності для предикатів є відкриті підмножини топологічного простору. Значення &, ∨, ∃ визначаються булевим чином. Значення А є начинка доповнення значення А. Це викликано тим, що доповнення відкритої множини часто не є відкритим. Аналогічно визначаються значення А ⇒В і ∀xA(х). Напр., несправедливість A∨A можна продемонструвати так: об'єднання відкритого одиничного кола і начинки його доповнення дає не всю площину, а площину без одиничного кола.
Наступною інтерпретацією була модель алгебри – алгебри Лінденбаума-Тарського для інтуїціоністських теорій. Їх називають псевдобулевими алгебрами. Ці алгебри вперше були створені для цієї мети, але виявилися поширеною та широко застосовною структурою.
Паралельно з цим розвивалася лінія, яка веде початок від брауеровського змістовного змісту інтуїціоністської логіки. Формули тлумачилися як завдання, логічні зв'язки – як перетворення завдань, аксіоми – як завдання, котрим рішення вважаються відомими, а правила виведення – як перетворення рішень задач. Ці ідеї систематизував А.Н. Колмогори. Кожній формулі А зіставляється безліч її реалізацій. Кожна реалізація вважається вирішенням задачі, що відповідає А. Реалізації елементарних формул задаються за визначенням. ®(А&В) = ®А × ®В, де ®(А&В) це пара реалізацій ; ®(А∨В) = ®А ®В, де ®(А∨В) – реалізація А або В із зазначенням, яке із підзавдань вирішено; ®A = 0̊⇔®А = ∅, де ®А – стандартний елемент, наприклад, за умови, що завдання А нерозв'язне;®∃хА(х) = а∈U®A(α), де ®∃хА(х) – це пара зі значення х0 та рішення A(x0). Реалізаціями А ⇒ є ефективні функціонали з ®А в ®В. Реалізаціями ∀х(х) є ефективні функціонали, що переробляють кожне α ∈ U на реалізацію Α(α).
У цьому вся визначенні залишається не уточненим поняття ефективного функціоналу. Воно може уточнюватися по-різному, зокрема, якщо взяти як ефективні функціонали всі класичні функції, то логіка перетворюється на класичну. Кліні побудував перший точний варіант реалізованості, взявши в якості ефективних операторів алгоритми і кодуючи програми алгоритмів натуральними числами, обходячи таким чином складності з операторами вищих типів (клініївська реалізованість). Він показав, що з доказу в інтуїціоністській арифметиці витягується клінієвська реалізація доведеної теореми, і, таким чином, якщо ми довели ∃хА(х), є таке п, що доведено А(п). Це достеменно обгрунтувало тезу Брауера у тому, що інтуїціоністські докази дають, на відміну класичних, побудови.
Ще одна семантика інтуїціоністської логіки бере початок від Бета та розвинена Крипке. Це – один із видів моделей Крипке. Безліч світів – частково-упорядкована множина (достатньо розглядати дерево), істинність елементарних формул зберігається при підйомі, універсуми не зменшуються при підйомі, значення &, ∨, ∃визначаються локально, w⊧A⊃B⇔∀v≥w (v⊧ ⇒v⊧B), w ⊧A⇔∀v≥w (v ⊧ A), w ⊧∀x A(x) ⇔∀v ≥ w (∀a∈Uv ν ⊧A(a)), де v і w – це «змінні світами». Дані пункти практично повторюють на семантичному рівні геделево занурення інтуїціоністської логіки в S4. Моделі Крипке ізоморфні алгебраїчним та топологічним моделям (порядок визначає псевдобулеву алгебру верхніх відрізків множини світів та топологію, в якійоколицями служать верхні відрізки).
Унікальною для некласичних логік є наявність у інтуїціоністської логіки двох різнорідних класів семантик, що не зводяться один до одного: реалізацій і моделей Крипке. Аналогію між доказами в інтуїціоністській логіці та побудовами посилено Н.В.Каррі в його «Комбінаторній логіці» (Combinatory Logic, 1968). Замкнуті типізовані вирази у комбішаторній логіці ізоморфні висновкам у гільбертівському формулюванні імплікативного фрагменту інтуїціоністської логіки. Замкнуті типізовані λ-терми ізоморфні висновків в імплікативному фрагменті природного виведення. Ізоморфізм між висновками та λ-термами намагалися розширити на всю інтуїціоністську логіку, узагальнюючи λ-числення. Але на цьому шляху стоїть перешкода, вказана ще Брауер і явно виділена Н. А. Шаніним. Висновки в інтуїціоністській логіці поєднують побудови та їх обґрунтування. Зокрема, побудови, виконані під час виведення А, не можна обчислювати, оскільки вони призведуть до помилки. Але подібною ж дією можуть володіти й інші імплікації, зокрема, закон транзитивності ∀xyz (А(х, у) α А(у, z) ⇒ А(х, z) Тут може призвести до небажаних наслідків обчислення у. Такі об'єкти , які не можна чи не потрібно обчислювати в програмі, але потрібно розглядати для її обґрунтування, ввів Г.С.Цейтін і назвав «привидами» Н.А.Шанін розглянув алгоритм конструктивного розшифрування, що розбиває формулу на завдання та обґрунтування рішення, причому друга частина могла доводитися класично, його рішення має місце для рекурсивної реалізованості в теорії, поповненій принципом Маркова: ∀х (А(х) ∨A(х)) ∃xA(x) ⇒∃хА(х).
Змістовний зміст даного принципу розкривається вислівом «Шукайте і знайдете»: якщо відомі критерії перевірки правильності рішення та доведено йогоіснування, його може знайти машина повним перебором. Н.Н.Непейвода дав алгоритм класифікації об'єктів усередині довільного виведення в інтуїціоністській логіці, що відокремлює діючі об'єкти та формули від бездіяльних, що породжують лише обґрунтування та привиди.
Інтуїціоністську логіку намагалися варіювати багатьма способами. Першою варіацією була мінімальна логіка Йогансона, що виходить відкиданням falso sequitur quodlibet. Як виявилося, у прикладних теоріях інтуїціоністське заперечення проте моделюється (напр., у будь-якій теорії, що містить натуральні числа, як А ⇒0 = 1). Але мінімальна логіка, як і інтерпретація Колмогорова, висвітлила аномальний статус заперечення інтуїціоністської логіки. Це – єдина зв'язка, яка не вимагає жодної побудови.
У зв'язку з цим Гріс запропонував симетричну інтуїціоністську логіку, в якій істина та брехня визначаються одночасно і рівноправно. У симетричній інтуїціоністській логіці зберігаються звичайні правила формулювання заперечень класичної логіки, і в її натуральному варіанті вони навіть постулюються як правила виведення. Заперечення у ній зазвичай позначається
А й називається "сильним запереченням", або "конструктивним спростуванням". Воно інтерпретується як завдання на побудову контрприкладу до А. Симетрична інтуїціоністська логіка детально досліджена в монографії І. Д. Заславського.
Ю.М.Медведєв запропонував розглядати логіку фінітних завдань і зауважив, що, якщо функціонали скрізь визначені, то формула (А ⇒ В ∨C) ⇒ ((A ⇒ Β)∨( Α ⇒ C)) реалізована (реалізація А стандартна, і її можна підставити у функціонал, щоб виявити єдиного кандидата на рішення серед, C). Після цього почали розглядатися численні суперінтуїціоністські логіки, що виходять розширеннямінтуїціоністської логіки деякими схемами аксіом. Майже всі вони або тягнуть закон виключеного третього в прикладних теоріях, або не задовольняють теорему Крейга про інтерполяцію та теорему Бета. Отже, інтуїціоністська логіка займає унікальне місце в класі некласичних логік, не тільки як найстаріша з них, а й як концептуально цілісна система.
Нова філософська енциклопедія. У чотирьох томах. / Ін-т філософії РАН. Науково-ред. порада: В.С. Степін, А.А. Гусейнов, Г.Ю. Семигін. М., Думка, 2010, т. II, Е - М, с. 138-140.