Теорема Леба

В математической логике теорема Леба утверждает, что в арифметике Пеано (PA) (или любой формальной системе, включая PA), для любой формулы P , если в PA доказуемо, что «если P доказуемо в PA, то P истинно», тогда P доказуемо в PA. Если Prov( P ) означает, что формула P доказуема, мы можем выразить это более формально как

Если

{\mathit {PA}}\vdash {\mathrm {Prov} (P)\rightarrow P}

затем

{\mathit {PA}}\vdash P

.

Непосредственным следствием ( контрапозитивом ) теоремы Лёба является то, что если P недоказуемо в PA, то «если P доказуемо в PA, то P истинно» недоказуемо в PA. Например: «Если $1+1=3$ доказуемо в PA, то $1+1=3$ "не доказуемо в ПА. ^{[ 1 ]}

Теорема Леба названа в честь Мартина Хьюго Леба , сформулировавшего ее в 1955 году. ^{[ 2 ]} Это связано с парадоксом Карри . ^{[ 3 ]}

Теорема Леба в логике доказуемости

Логика доказуемости абстрагируется от деталей кодирования, используемых в теоремах Гёделя о неполноте, выражая доказуемость $\phi$ в данной системе на языке модальной логики , посредством модальности $\Box \phi$ . То есть, когда $\phi$ является логической формулой, другую формулу можно составить, поставив квадрат перед $\phi$ , и предназначено для того, чтобы означать, что $\phi$ доказуемо.

Тогда мы можем формализовать теорему Лёба аксиомой

\Box (\Box P\rightarrow P)\rightarrow \Box P,

известная как аксиома GL, для Гёделя – Лёба. Иногда это формализуется с помощью правила вывода:

Если

\vdash \Box P\rightarrow P

затем

\vdash P

.

Логика доказуемости GL, возникающая в результате взятия модальной логики K4 (или K , поскольку схема аксиом 4 , $\Box A\rightarrow \Box \Box A$ , то становится излишним) и добавление вышеуказанной аксиомы GL является наиболее интенсивно исследуемой системой в логике доказуемости.

Модальное доказательство теоремы Лёба

Теорему Лёба можно доказать в рамках модальной логики, используя только некоторые основные правила, касающиеся оператора доказуемости (системы K4), а также существования модальных неподвижных точек .

Модальные формулы

Мы примем следующую грамматику для формул:

Если $X$ является пропозициональной переменной , то $X$ это формула.
Если $K$ является пропозициональной константой, то $K$ это формула.
Если $A$ это формула, то $\Box A$ это формула.
Если $A$ и $B$ являются формулами, то и $\neg A$ , $A\rightarrow B$ , $A\wedge B$ , $A\vee B$ , и $A\leftrightarrow B$

Модальное предложение — это формула в этом синтаксисе, которая не содержит пропозициональных переменных. Обозначения $\vdash A$ используется для обозначения того, что $A$ это теорема.

Модальные фиксированные точки

Если $F(X)$ это модальная формула только с одной пропозициональной переменной $X$ , то модальная фиксированная точка $F(X)$ это предложение $\Psi$ такой, что

\vdash \Psi \leftrightarrow F(\Box \Psi )

Существование таких неподвижных точек будем предполагать для каждой модальной формулы с одной свободной переменной. Это, конечно, неочевидная вещь, но если мы интерпретируем $\Box$ как доказуемость в арифметике Пеано, то существование модальных неподвижных точек следует из диагональной леммы .

Модальные правила вывода

Помимо существования модальных неподвижных точек, мы предполагаем следующие правила вывода для оператора доказуемости $\Box$ , известные как условия доказуемости Гильберта – Бернейса :

(необходимость) От $\vdash A$ заключать $\vdash \Box A$ : Неформально это говорит о том, что если А — теорема, то она доказуема.
(внутренняя необходимость) $\vdash \Box A\rightarrow \Box \Box A$ : Если А доказуемо, то доказуемо, что оно доказуемо.
(коробочная дистрибутивность) $\vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)$ : Это правило позволяет вам выполнять modus ponens внутри оператора доказуемости. Если доказуемо, что A влечет за собой B, и A доказуемо, то B доказуемо.

Доказательство теоремы Лёба

Большая часть доказательства не использует предположение $\Box P\to P$ , поэтому для простоты понимания приведенное ниже доказательство разделено на части, зависящие от $\Box P\to P$ до конца.

Позволять $P$ быть любым модальным предложением.

Примените существование модальных неподвижных точек к формуле $F(X)=X\rightarrow P$ . Отсюда следует, что существует предложение $\Psi$ такой, что
$\vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)$ .
$\vdash \Psi \rightarrow (\Box \Psi \rightarrow P)$ , с 1.
$\vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))$ , из 2 по правилу необходимости.
$\vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)$ , из 3 и правила распределительности ящика.
$\vdash \Box (\Box \Psi \rightarrow P)\rightarrow (\Box \Box \Psi \rightarrow \Box P)$ , применяя правило коробочной дистрибуции с $A=\Box \Psi$ и $B=P$ .
$\vdash \Box \Psi \rightarrow (\Box \Box \Psi \rightarrow \Box P)$ , с 4 и 5.
$\vdash \Box \Psi \rightarrow \Box \Box \Psi$ , из 6 по правилу внутренней необходимости.
$\vdash \Box \Psi \rightarrow \Box P$ , с 6 и 7.

Теперь переходим к той части доказательства, где используется гипотеза.
Предположим, что $\vdash \Box P\rightarrow P$ . Грубо говоря, это теорема, что если $P$ доказуемо, то оно действительно истинно. Это претензия на обоснованность .
$\vdash \Box \Psi \rightarrow P$ , с 8 и 9.
$\vdash (\Box \Psi \rightarrow P)\rightarrow \Psi$ , с 1.
$\vdash \Psi$ , с 10 и 11.
$\vdash \Box \Psi$ , из 12 по правилу необходимости.
$\vdash P$ , с 13 и 10.

Более неформально мы можем набросать доказательство следующим образом.

С ${\mathit {PA}}\vdash {\mathrm {Prov} _{PA}(P)\rightarrow P}$ по предположению, мы также имеем ${\mathit {PA}}\vdash {\neg P\rightarrow \neg \mathrm {Prov} _{PA}(P)}$ , что подразумевает $\{{\mathit {PA}},\neg P\}\vdash {\neg \mathrm {Prov} _{PA}(P)}$ .
Итак, гибридная теория $\{{\mathit {PA}},\neg P\}$ $\{{\mathit {PA}},\neg P\}$ может рассуждать следующим образом:
1. Предполагать $\{{\mathit {PA}},\neg P\}$ противоречиво, то PA доказывает $\neg P\to \bot {}$ , что то же самое, что $P$ .
2. Однако, $\{{\mathit {PA}},\neg P\}$ уже знает это $\neg \mathrm {Prov} _{PA}(P)$ , противоречие.
3. Поэтому, $\{{\mathit {PA}},\neg P\}$ является последовательным.
По второй теореме Гёделя о неполноте из этого следует $\{{\mathit {PA}},\neg P\}$ является противоречивым.
Таким образом, ПА доказывает $\neg P\to \bot {}$ , что то же самое, что $P$ .

Примеры

Непосредственным следствием теоремы Лёба является то, что если P недоказуемо в PA, то «если P доказуемо в PA, то P истинно» недоказуемо в PA. Учитывая, что мы знаем, что PA непротиворечив (но PA не знает, что PA непротиворечив), вот несколько простых примеров:

"Если $1+1=3$ доказуемо в PA, то $1+1=3$ "не доказуемо в PA, так как $1+1=3$ недоказуемо в PA (поскольку оно неверно).
"Если $1+1=2$ доказуемо в PA, то $1+1=2$ " доказуемо в PA, как и любое утверждение вида "Если X, то $1+1=2$ ".
«Если усиленная конечная теорема Рамсея доказуема в PA, то усиленная конечная теорема Рэмси истинна» недоказуема в PA, поскольку «Усиленная конечная теорема Рэмси истинна» недоказуема в PA (несмотря на то, что она верна).

В доксастической логике теорема Лёба показывает, что любая система, классифицируемая как рефлексивный мыслитель « типа 4 », также должна быть « скромной »: такой мыслитель никогда не сможет поверить, что «моя вера в P будет означать, что P истинно», не веря при этом, что P это правда. ^{[ 4 ]}

Вторая теорема Гёделя о неполноте следует из теоремы Лёба заменой ложного утверждения $\bot$ для П.

Обратное: из теоремы Лёба следует существование модальных неподвижных точек.

Из существования модальных неподвижных точек не только следует теорема Лёба, но и обратное тоже справедливо. Когда теорема Лёба задана в виде аксиомы (схемы), существование неподвижной точки (с точностью до доказуемой эквивалентности) $p\leftrightarrow A(p)$ для любой формулы A ( p ), модализованной в p, можно получить. ^{[ 5 ]} Таким образом, в нормальной модальной логике аксиома Лёба эквивалентна конъюнкции схемы аксиом 4 : $(\Box A\rightarrow \Box \Box A)$ и существование модальных неподвижных точек.

Примечания

^ Если только PA не является непоследовательным (в этом случае каждое утверждение доказуемо, включая $1+1=3$ ).
^ Лёб 1955 .
^ Нил, Кришнасвами. «Теорема Лёба — это (почти) Y-комбинатор» . Семантическая область . Проверено 9 апреля 2024 г.
^ Смуллян 1986 .
^ Линдстрем 2006 .

Ссылки

Булос, Джордж С. (1995). Логика доказуемости . Издательство Кембриджского университета . ISBN 978-0-521-48325-4 .
Хинман, П. (2005). Основы математической логики . АК Петерс. ISBN 978-1-56881-262-5 .
Джапаридзе, Георгий; Де Йонг, Дик (1998). «Глава VII. Логика доказуемости». В Бассе, Сэмюэл Р. (ред.). Справочник по теории доказательств . Исследования по логике и основам математики. Том. 137. Эльзевир . стр. 475–546. дои : 10.1016/S0049-237X(98)80022-0 .
Линдстрем, Пер (июнь 2006 г.). «Заметка о некоторых конструкциях с фиксированной точкой в логике доказуемости». Журнал философской логики . 35 (3): 225–230. дои : 10.1007/s10992-005-9013-8 . S2CID 11038803 .
Лёб, Мартин (1955). «Решение проблемы Леона Хенкина». Журнал символической логики . 20 (2): 115–118. дои : 10.2307/2266895 . JSTOR 2266895 . S2CID 250348262 .
Смуллян, Раймонд М. (1986). «Логики, рассуждающие о себе» . Материалы конференции 1986 года по теоретическим аспектам рассуждений о знании, Монтерей (Калифорния) . Сан-Франциско (Калифорния): Morgan Kaufmann Publishers Inc., стр. 341–352. дои : 10.1016/B978-0-934613-04-0.50028-4 . ISBN 9780934613040 .

Внешние ссылки

«Теорема Леба» . 22 марта 2013. ПланетаМатематика . Проверено 14 декабря 2023 г.
«Логика доказуемости» Запись Ринеке (LC) Вербрюгге в Стэнфордской энциклопедии философии , 2017 г.

[1] Если только PA не является непоследовательным (в этом случае каждое утверждение доказуемо, включая $1+1=3$ ).

[FOOTNOTELöb1955-2] Лёб 1955 .

[3] Нил, Кришнасвами. «Теорема Лёба — это (почти) Y-комбинатор» . Семантическая область . Проверено 9 апреля 2024 г.

[FOOTNOTESmullyan1986-4] Смуллян 1986 .

[FOOTNOTELindström2006-5] Линдстрем 2006 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]