НОУ ІНТУІТ, Лекція,Контрприклад
Інтуїціоністська пропозиційна логіка
Виключимо з-поміж аксіом закон виключеного третього. Отримане літочислення називається інтуїціоністським літочисленням висловлювань. (Звичайне обчислення висловлювань називають класичним, щоб уникнути плутанини при його порівнянні з інтуїціоністським. Взагалі математичні міркування, що спираються на аксіому виключеного третього, називають "класичними", а ті, що уникають її - "інтуїціоністськими".)
Звичайно, відразу виникають природні питання. Чому саме ця аксіома викликає сумніви? Взагалі аксіом багато, і можна було б виключити будь-яку і дивитися, що вийде без неї — але ясно, що швидше за все вийде щось дивне. Як зрозуміти, які формули залишаться теоремами без закону виключеного третього? Раніше обчислення висловлювань мали "надзавдання" — вивести всі тавтології і тільки їх, а тепер?
Що ми маємо на увазі (або повинні мати на увазі), говорячи про те, що ми встановили, що "або"? Це означає, за Брауером, що ми встановили , або встановили . Коли ми встановлюємо, що "і", це означає, що ми встановили і , і . "Якщо, то" означає, що ми маємо якусь загальну міркування, яка дозволить нам встановити, як тільки хтось встановить нам. Заперечення означає, що ми маємо в своєму розпорядженні міркування, яке призводить до суперечності припущення, що встановлено. (Як з погляду інтуїціонізму, так і з класичної точки зору, у всіх сенсах еквівалентно, де — явно хибне твердження. Можна було б взагалі не використовувати заперечення, а мати константу — це не дуже звично, але технічно зручно.)
Інтуїціонізм відкидає ідею у тому, що це висловлювання діляться на істинні і хибні (нехай невідомим нам образом). З цього погляду законвиключеного третього абсолютно безпідставний: означає, що з довільного твердження ми можемо встановити чи , чи його заперечення (тобто пояснити, чому у принципі може бути встановлено) — чому, власне?
Зазвичай, говорячи про інтуїціонізм, наводять такий приклад міркування, неприйнятного з погляду інтуїціонізму. Доведемо, що є ірраціональні числа і , котрим раціонально. Справді, розглянемо два випадки. Якщо раціонально, можна покласти . Якщо ж ірраціонально, то покладемо і; легко перевірити, що . Інтуїціоніст скаже, що це міркування некоректно: довести існування чогось означає побудувати цей об'єкт, а ми так і не побудували чисел і, оскільки не встановили, який із двох випадків має місце. (Зауважимо у дужках, що фахівці з алгебраїчної теорії чисел знають, що ірраціонально і навіть трансцендентно. Крім того, не потрібно бути фахівцем, щоб помітити, що можна покласти і.) Цей приклад можна критикувати і з іншого погляду, кажучи, що саме поняття дійсного числа не є інтуїтивно зрозумілим і потребує обґрунтування.
Взагалі інтуїція — справа тонка: якщо довго міркувати, скажімо, про дійсні числа, то здається, що вони в якомусь сенсі існують незалежно від наших міркувань. Саме тому психологічно виправдане питання про те, скажімо, як справи з континуум-гіпотезою "насправді": чи існує безліч дійсних чисел, не рівносильне всім дійсним числам, чи не існує?
Ми не говоритимемо про філософські передумови інтуїціонізму докладно. Коротко спрощена історія питання така. Брауер намітив плани перебудови математики на інтуїціоністських принципах і відстоював їх настільки гаряче, що одного разу Гільберту роздратуванні зауважив: скасувати закон виключеного третього — це все одно, що відібрати в астрономів телескоп або заборонити боксерам користуватися кулаками. Але, продовжував він, ніхто не може вигнати математиків з раю, який створив Кантор.
У плани Брауера не входила формалізація інтуїціоністської логіки та математики, скоріше навпаки. Проте аналіз принципів інтуїціонізму пішов саме цим шляхом, коли Гейтинг став вивчати пропозиційну логіку без закону виключеного третього. Різні спірні інтуїціоністські принципи стали предметом вивчення з погляду формальної логіки; були побудовані інтуїціоністські варіанти формальної арифметики, теорії множин, логіки предикатів, а також генценівські варіанти інтуїціоністських систем. Було запропоновано різні інтерпретації інтуїціоністської логіки. Колмогоров запропонував трактувати її як "логіку завдань", Кліні запропонував поняття "реалізованості", що використовує теорію алгоритмів для тлумачення формул; були запропоновані топологічні моделі для інтуїціоністської логіки тощо. буд. У СРСР прапор Брауера підхопила школа Маркова, написавши у ньому, втім, " конструктивізм " замість ідеологічно сумнівного " інтуіціонізму " і послідовно обмежуючись кінцевими об'єктами. Крипке в 1960-і роки запропонував деяку семантику (визначення істинності), узгоджену з інтуїціоністським обчисленням висловлювань і природну (навіть дивно, що її не вигадали раніше); Чудовим виявилося, що вона в певному сенсі близька до методу форсингу, який приблизно в цей же час придумав Коен, щоб довести незалежність аксіоми вибору та континуум-гіпотези в теорії множин.
Повертаючись до інтуїціоністського обчислення висловлювань, наведемо кілька формул, що виводяться.