11.5: Інтуїціоністична логіка

Last updated
Save as PDF

Page ID: 52810

$ \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $ $ \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} $$\newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\kernel}{\mathrm{null}\,}$ $ \newcommand{\range}{\mathrm{range}\,}$ $ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$ $ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$ $ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$ $ \newcommand{\Span}{\mathrm{span}}$ $\newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\kernel}{\mathrm{null}\,}$ $ \newcommand{\range}{\mathrm{range}\,}$ $ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$ $ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$ $ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$ $ \newcommand{\Span}{\mathrm{span}}$

Template:MathJaxZach

На відміну від логіки другого і вищого порядку, інтуїціоністична логіка першого порядку являє собою обмеження класичної версії, призначеної для моделювання більш «конструктивного» виду міркувань. Наступні приклади можуть служити для ілюстрації деяких основних мотивацій.

Припустимо, хтось підійшов до вас одного дня і оголосив, що вони визначили натуральне число$x$, з властивістю, що якщо$x$ просте, гіпотеза Рімана є істинною, а якщо$x$ є складовою, гіпотеза Рімана є помилковою. Чудова новина! Чи вірна гіпотеза Рімана чи ні, є одним із великих відкритих питань математики, і тут вони, здається, звели проблему до обчислення, тобто до визначення того, чи є конкретне число простим чи ні.

У чому полягає магічна цінність$x$? Вони описують його наступним чином:$x$ це натуральне число, яке дорівнює,$7$ якщо гіпотеза Рімана істинна, і$9$ інакше.

Сердито, ви вимагаєте назад свої гроші. З класичної точки зору, опис вище насправді визначає унікальне значення$x$; але те, що ви дійсно хочете, це значення$x$, що дається явно.

Щоб взяти інший, можливо, менш надуманий приклад, розглянемо наступне питання. Ми знаємо, що можна підняти ірраціональне число до раціональної влади, і отримати раціональний результат. Наприклад,$\sqrt{2}^2 = 2$. Менш зрозуміло, чи можна підняти ірраціональне число до ірраціональної влади, і отримати раціональний результат. Наступна теорема відповідає на це ствердно:

Теорема$\PageIndex{1}$

Є ірраціональні числа$a$ і$b$ такі, які$a^b$ є раціональними.

Доказ. Розглянемо$\sqrt{2}^{\sqrt{2}}$. Якщо це раціонально, ми зробили: можемо дозволити$a = b = \sqrt{2}$. В іншому випадку це нераціонально. Тоді ми маємо,\[(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2} \cdot \sqrt{2}} = \sqrt{2}^2 = 2,\nonumber\] що, безумовно, раціонально. Отже, в даному випадку нехай$a$ буде$\sqrt{2}^{\sqrt{2}}$, і нехай$b$ буде$\sqrt 2$. ◻

Чи є це дійсним доказом? Більшість математиків вважають, що це так. Але знову ж таки, тут є щось трохи незадовільне: ми довели існування пари дійсних чисел з певною властивістю, не маючи можливості сказати, яка пара чисел це. Можна довести той же результат, але таким чином, що пара$a$,$b$ наводиться в доказ: взяти$a = \sqrt{3}$ і$b = \log_3 4$. Тоді\[a^b = \sqrt{3}^{\log_3 4} = 3^{1/2 \cdot \log_3 4} = (3^{\log_3 4})^{1/2} = 4^{1/2}= 2,\nonumber\] з тих пір$3^{\log_3 x} = x$.

Інтуїціоністична логіка призначена для моделювання свого роду міркувань, де не допускаються рухи, подібні до того, що в першому доказі. Доведення існування$x$ задовольняє$A(x)$ означає, що ви повинні дати конкретне$x$, і доказ того, що він задовольняє$A$, як у другому доказі. Доведення того, що$A$ або$B$ тримає вимагає, що ви можете довести те чи інше.

Формально кажучи, інтуїціоністична логіка першого порядку - це те, що ви отримаєте, якщо опустити обмежити систему доказів для логіки першого порядку певним чином. Аналогічно існують інтуїціоністичні версії логіки другого або вищого порядку. З математичної точки зору це всього лише формальні дедуктивні системи, але, як уже зазначалося, вони призначені для моделювання свого роду математичних міркувань. Можна вважати це видом міркування, яке виправдано на певному філософському погляді на математику (наприклад, інтуїціонізм Брауера); можна вважати це свого роду математичним міркуванням, яке є більш «конкретним» і задовольняючим (за лініями конструктивізму єпископа); і можна сперечатися про незалежно від того, чи фіксує формальний опис неформальної мотивації. Але які б філософські позиції ми не займали, ми можемо вивчати інтуїціоністичну логіку як формально представлену логіку; і з яких-небудь причин багатьом математичним логікам цікаво це зробити.

Існує неформальна конструктивна інтерпретація інтуїціоністських зв'язків, зазвичай відома як тлумачення БХК (названа на честь Брауера, Хейтінга, Колмогорова). Він працює наступним чином: доказ$A \land B$ складається з доказу$A$ парного з доказом$B$; доказ$A \lor B$ складається або з доказу$A$, або з доказу того$B$, де ми маємо явне інформація про те, яка справа; доказ$A \lif B$ складається з процедури, яка перетворює доказ на$A$ доказ$B$; доказ$\lforall{x}{A(x)}$ складається з процедури, яка повертає доказ$A(x)$ для будь-якого значення$x$; і доказ$\lexists{x}{A(x)}$ складається з значення$x$, разом з доказом того, що це значення задовольняє$A$. Можна описати інтерпретацію обчислювальними термінами, відомими як «ізоморфізм Керрі-Говарда» або «парадигма формули як типи»: думати про формулу як визначення певного типу даних, і докази як обчислювальні об'єкти цих типів даних, які дозволяють нам побачити, що відповідна формула є істинною .

Інтуїціоністична логіка часто розглядається як класична логіка «мінус» закон виключеної середини. Ця наступна теорема робить це більш точним.

Теорема$\PageIndex{2}$

Інтуїціоністично такі схеми аксіом еквівалентні:

$(A \lif \lfalse) \lif \lnot A$.
$A \lor \lnot A$
$\lnot \lnot A \lif A$

Отримання екземплярів однієї схеми від будь-якої з інших - хороша вправа в інтуїціоністичній логіці.

Перші дедуктивні системи для інтуїціоністичної пропозіціонной логіки, висунуті як формалізації інтуїціонізму Брауера, зобов'язані самостійно Колмогорову, Глівенко, Хейтінгу. Перша формалізація інтуїціоністичної логіки першого порядку (і частин інтуїціоністської математики) обумовлена Хейтінгом. Хоча ряд класично дійсних схем не є інтуїціоністично дійсними, багато хто з них.

Переклад подвійного заперечення описує важливу взаємозв'язок між класичною та інтуїціоністською логікою. Він визначається індуктивно наступним чином (розглядати$A^N$ як «інтуїціоністський» переклад класичної формули$A$):\[\begin{aligned} A^N & \ident \lnot\lnot A \quad \text{for atomic formulas $A$} \\ (A \land B)^N & \ident (A^N \land B^N) \\ (A \lor B)^N & \ident \lnot\lnot (A^N \lor B^N) \\ (A \lif B)^N & \ident (A^N \lif B^N) \\ (\lforall{x}{A})^N & \ident \lforall{x}{A^N} \\ (\lexists{x}{A})^N & \ident \lnot\lnot\lexists{x}{A^N}\end{aligned}\] Колмогоров і Глівенко мали версії цього перекладу для логіки пропозиції; для логіки присудків це пов'язано з Геделем і Гентценом, самостійно. У нас є

Теорема$\PageIndex{3}$

$A \liff A^N$доведено класично
Якщо$A$ доведено класично, то$A^N$ це доведено інтуїціоністично.

Тепер ми можемо уявити наступний діалог. Класичний математик: «Я довів$A$!» Математик-інтуїціоніст: «Ваш доказ недійсний. Те, що ви дійсно довели, це»$A^N$. Класичний математик: «Добре мною!» Що стосується класичного математика, то інтуїціоніст просто розщеплює волоски, оскільки ці два рівнозначні. Але інтуїціоніст наполягає, що різниця є.

Зауважте, що вищевказаний переклад стосується лише чистої логіки; він не стосується питання про те, які нелогічні аксіоми є відповідними для класичної та інтуїціоністичної математики, або які відносини між ними. Але наступне невелике розширення теореми вище дає деяку корисну інформацію:

Теорема$\PageIndex{4}$

Якщо$\Gamma$ доводить$A$ класично,$\Gamma^N$ доводить$A^N$ інтуїціоністично.

Іншими словами, якщо$A$ доведено з деяких гіпотез класично, то$A^N$ це доведено з їх подвійного заперечення перекладів.

Щоб показати, що речення або пропозиційна формула є інтуїціоністично дійсними, все, що вам потрібно зробити, це надати доказ. Але як ви можете показати, що він не дійсний? Для цього нам потрібна семантика, яка є здоровою і бажано повною. А семантика завдяки Кріпке добре вписується в законопроект.

Ми можемо грати в ту саму гру, що і для класичної логіки: визначити семантику, довести обґрунтованість і повноту. Варто, однак, відзначити наступне розмежування. У випадку з класичною логікою семантика була «очевидною», в певному сенсі неявною в значенні зв'язків. Хоча можна забезпечити деяку інтуїтивну мотивацію для семантики Кріпке, остання не дає такого ж відчуття неминучості. Крім того, поняття класичної структури є природно-математичним, тому ми можемо або прийняти поняття структури як інструмент для вивчення класичної логіки першого порядку, або взяти класичну логіку першого порядку як інструмент для вивчення математичних структур. На відміну від цього, структури Кріпке можна розглядати лише як логічну конструкцію; вони, схоже, не мають самостійного математичного інтересу.

Структура Кріпке$\mModel M = \tuple{W, R, V}$ для пропозіційної мови складається з множини$W$, часткового порядку$R$ на$W$ з найменшим елементом та «монотонного» присвоєння пропозиційних змінних елементам$W$. Інтуїція полягає в тому, що елементи$W$ представляють «світи» або «стани знання»; елемент$v \geq u$ являє собою «можливий майбутній стан»$u$; а запропоновані змінні,$u$ призначені для - це пропозиції, які є як відомо, вірно в державі$u$. $\mSat[,w]{M}{A}$Потім примусове відношення розширює це відношення до довільних формул у мові; читати$\mSat[,w]{M}{A}$ як «$A$істинно в державі»$w$. Відносини визначаються індуктивно, наступним чином:

$\mSat[,w]{M}{\Obj p_i}$iff$\Obj p_i$ є однією з запропонованих змінних, присвоєних$w$.
$\mSatN[,w]{M}{\lfalse}$.
$\mSat[,w]{M}{(A \land B)}$іфф$\mSat[,w]{M}{A}$ і$\mSat[,w]{M}{B}$.
$\mSat[,w]{M}{(A \lor B)}$Вимкніть$\mSat[,w]{M}{A}$ або$\mSat[,w]{M}{B}$.
$\mSat[,w]{M}{(A \lif B)}$Якщо, коли$w' \geq w$ і$\mSat[,w']{M}{A}$, то$\mSat[,w']{M}{B}$.

Це хороша вправа, щоб спробувати показати, що$\lnot (p \land q) \lif (\lnot p \lor \lnot q)$ це не є інтуїціоністично дійсним, приготувавши структуру Кріпке, яка забезпечує контрприклад.