Інтуїціоністська пропозиційна логіка
Завдання про пошук висновку та аналіз його структури, хоч і були у свій час модними у зв'язку з «штучним інтелектом», становлять великий інтерес, і про них є ціла наука, в якій обчислення генценівського типу відіграють центральну роль. Ми розглянули один із варіантів обчислення секвенцій для класичного обчислення висловлювань; бувають обчислення для інтуїціоністських і модальних логік, для обчислення предикатів і т. д. Вихідною мотивацією для розгляду таких обчислень було бажання довести несуперечність арифметики. Відповідно до знаменитої другої теореми Геделя про неповноту без додаткових аксіом цього не можна, але якщо прийняти схему аксіом для трансфінітної індукції по ординалу " 0 , це вдається зробити, як показав Генцен.
2.4. Інтуїціоністська пропозиційна логіка
Виключимо з-поміж аксіом закон виключеного третього A ¬A. Отримане обчислення називається інту-
іціоністським обчисленням висловлювань. (Звичайне літочислення висловлювань називають класичним, щоб уникнути плутанини при його порівнянні з інтуїціоністським. Взагалі математичні міркування, що спираються на аксіому виключеного третього, називають «класичними», а уникають її «інтуїціоністськими».)
Звичайно, відразу виникають природні питання. Чому саме ця аксіома викликає сумніви? Загалом аксіом багато, і можна було б виключити будь-яку і дивитися, що вийде без неї, але ясно, що швидше за все вийде щось дивне. Як зрозуміти, які формули залишаться теоремами без закону виключеного третього? Раніше обчислення висловлювань мали «надзавдання» вивести всі тавтології і тільки їх, а тепер?
Інтуїціоністська логіка виникла як спроба (зроблена Гейтингом) формалізувати (нехай частково) методи міркувань,практикувані в «інтуїціоністській
Що ми маємо на увазі (або повинні мати на увазі), говорячи про те, що ми встановили, що A або B? Це означає, що за Брауером, що або ми встановили A, або встановили B. Коли ми встановлюємо, що "A і B", це означає, що ми встановили і A, і B. "Якщо A, то B" означає, що ми маємо якусь загальну міркування, яка дозволить нам встановити B, як тільки хтось встановить нам A. Заперечення A означає, що ми маємо міркування, яке приводить до суперечності припущення, що A встановлено. (Як з погляду інтуїціонізму, так і з класичної точки зору, A у всіх сенсах еквівалентно A →, де
свідомо хибне твердження. Можна було б взагалі не використати заперечення, а мати константу це
не дуже звично, але технічно зручно.) Інтуїціонізм відкидає ідею про те, що всі висловлюють
зування діляться на істинні і хибні (нехай невідомим нам чином). З цього погляду закон виключеного третього абсолютно безпідставний: A ¬ A озна-
сподівається, що для довільного затвердження A ми можемо
Інтуїціоністська пропозиційна логіка
встановити або A, або його заперечення (тобто пояснити, чому A в принципі не може бути встановлено), а чому, власне?
Зазвичай, говорячи про інтуїціонізм, наводять такий приклад міркування, неприйнятного з погляду інтуїціонізму. Доведемо, що існують ірраціональ-
ні числа і , для яких раціонально. Справді, розглянемо два випадки. Якщо √ 2 2 раціонально, то
можна покласти = = √ 2. Якщо ж 2 ірраціонально, то покладемо = √ 2 2 і = √ 2; легко прове-
рити, що = 2. Інтуїціоніст скаже, що це міркування некоректно: довести існування чогось означає побудувати цейоб'єкт, а ми так і не побудували чисел і , оскільки не встановили, який із двох
випадків має місце. (Зауважимо у дужках, що фахівці з алгебраїчної теорії чисел знають, що √ 2 √2
ірраціонально і навіть трансцендентно. Крім того, не
потрібно бути фахівцем, щоб помітити, що можна покласти = 2 і = 2 log 2 3.) Цей приклад можна
критикувати і з іншого погляду, кажучи, що саме поняття дійсного числа не є інтуїтивно ясним і потребує обґрунтування.
Взагалі інтуїція справа тонка: якщо довго міркувати, скажімо, про справжні числа, то починає здаватися, що вони в якомусь сенсі існують незалежно від наших міркувань. Саме тому психологічно виправдане питання про те, скажімо, як справи з континуум-гіпотезою «насправді»: чи існує безліч дійсних чисел, не рівносильне всім дійсним числам, чи не існує?
Ми не говоритимемо про філософські передумови інтуїціонізму докладно. Коротко спрощена історія питання така. Брауер намітив плани перебудови математики на інтуїціоністських принципах і відстоював їх настільки гаряче, що одного разу Гільберт у роздратуванні зауважив: скасувати закон виключеного тре-