Теорема Лёба

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

${\ displaystyle \ mathrm {if} \ PA \ vdash ({\ rm {Prov}} (P) \ rightarrow P) \ mathrm {, затем} \ PA \ vdash P,}$

или же

${\ displaystyle {\ dfrac {PA \ vdash {\ rm {Prov}} (P) \ rightarrow P} {PA \ vdash P}}.}$

Непосредственным следствием ( противоположным ) теоремы Лёба является то, что если P не доказуемо в PA, то «если P доказуемо в PA, то P истинно» не доказуемо в PA. Например, «Если доказуемо в PA, то » не доказуемо в PA. ${\ displaystyle 1 + 1 = 3}$${\ displaystyle 1 + 1 = 3}$

Теорема Лёба названа в честь Мартина Хуго Лёба, сформулировавшего её в 1955 году.

• 1 Теорема Лёба в логике доказуемости
• 2 Модальное доказательство теоремы Лёба
  • 2.1 Модальные формулы
  • 2.2 Модальные фиксированные точки
  • 2.3 Модальные правила вывода
  • 2.4 Доказательство теоремы Лёба
• 3 Примеры
• 4 Обратное: из теоремы Лёба следует существование модальных неподвижных точек
• 5 Примечания
• 6 цитат
• 7 ссылки
• 8 Внешние ссылки

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

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

${\ Displaystyle \ Box (\ Box P \ rightarrow P) \ rightarrow \ Box P,}$

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

${\ displaystyle P}$

из

${\ displaystyle \ Box P \ rightarrow P.}$

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

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

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

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

1. Если - пропозициональная переменная, то - формула. ${\ displaystyle X}$ ${\ displaystyle X}$
2. Если - пропозициональная константа, то - формула. ${\ displaystyle K}$${\ displaystyle K}$
3. Если это формула, то это формула. ${\ displaystyle A}$${\ displaystyle \ Box A}$
4. Если и есть формулы, то и,,,, и ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle \ neg A}$${\ displaystyle A \ rightarrow B}$${\ Displaystyle A \ клин B}$${\ displaystyle A \ vee B}$${\ displaystyle A \ leftrightarrow B}$

Модальное предложение - это модальная формула, не содержащая пропозициональных переменных. Мы имеем в виду теорему. ${\ displaystyle \ vdash A}$${\ displaystyle A}$

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

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

${\ Displaystyle \ vdash \ Psi \ leftrightarrow F (\ Box \ Psi)}$

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

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

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

1. (необходимость) Из заключения: Неформально это означает, что если A - теорема, то она доказуема. ${\ displaystyle \ vdash A}$${\ displaystyle \ vdash \ Box A}$
2. (внутренняя необходимость) : Если A доказуемо, то доказуемо. ${\ displaystyle \ vdash \ Box A \ rightarrow \ Box \ Box A}$
3. (распределительная коробка) : это правило позволяет вам выполнять modus ponens внутри оператора доказуемости. Если доказуемо, что A влечет B и A доказуемо, то B доказуемо. ${\ Displaystyle \ vdash \ Box (A \ rightarrow B) \ rightarrow (\ Box A \ rightarrow \ Box B)}$

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

1. Предположим, что существует модальное предложение такое, что. Грубо говоря, это теорема, что если и доказуема, то на самом деле истинна. Это заявление о разумности. ${\ displaystyle P}$${\ displaystyle \ vdash \ Box P \ rightarrow P}$ ${\ displaystyle P}$
2. Из существования модальных неподвижных точек для каждой формулы (в частности, формулы) следует, что существует такое предложение, что. ${\ Displaystyle X \ rightarrow P}$${\ Displaystyle \ Psi}$${\ Displaystyle \ vdash \ Psi \ leftrightarrow (\ Box \ Psi \ rightarrow P)}$
3. Из 2 следует, что. ${\ Displaystyle \ vdash \ Psi \ rightarrow (\ Box \ Psi \ rightarrow P)}$
4. Из правила необходимости следует, что. ${\ Displaystyle \ vdash \ Box (\ Psi \ rightarrow (\ Box \ Psi \ rightarrow P))}$
5. Из 4 и правила распределенности ящика следует, что. ${\ Displaystyle \ vdash \ Box \ Psi \ rightarrow \ Box (\ Box \ Psi \ rightarrow P)}$
6. Применение правила распределенности коробки с и дает нам. ${\ Displaystyle A = \ Box \ Psi}$${\ Displaystyle B = P}$${\ Displaystyle \ vdash \ Box (\ Box \ Psi \ rightarrow P) \ rightarrow (\ Box \ Box \ Psi \ rightarrow \ Box P)}$
7. Из 5 и 6 следует, что. ${\ Displaystyle \ vdash \ Box \ Psi \ rightarrow (\ Box \ Box \ Psi \ rightarrow \ Box P)}$
8. Это следует из правила внутренней необходимости. ${\ Displaystyle \ vdash \ Box \ Psi \ rightarrow \ Box \ Box \ Psi}$
9. Из 7 и 8 следует, что. ${\ Displaystyle \ vdash \ Box \ Psi \ rightarrow \ Box P}$
10. Из 1 и 9 следует, что. ${\ Displaystyle \ vdash \ Box \ Psi \ rightarrow P}$
11. Из 2 следует, что. ${\ Displaystyle \ vdash (\ Box \ Psi \ rightarrow P) \ rightarrow \ Psi}$
12. Из 10 и 11 следует, что ${\ displaystyle \ vdash \ Psi}$
13. Из 12 и правила необходимости следует, что. ${\ Displaystyle \ vdash \ Box \ Psi}$
14. Из 13 и 10 следует, что. ${\ displaystyle \ vdash P}$

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

• «Если доказуемо в PA, то » не доказуемо в PA, как и не доказуемо в PA (поскольку оно ложно). ${\ displaystyle 1 + 1 = 3}$${\ displaystyle 1 + 1 = 3}$${\ displaystyle 1 + 1 = 3}$
• «Если доказуемо в PA, то » доказуемо в PA, как и любое утверждение формы «Если X, то ». ${\ displaystyle 1 + 1 = 2}$${\ displaystyle 1 + 1 = 2}$${\ displaystyle 1 + 1 = 2}$
• «Если усиленная конечная теорема Рамсея доказуема в PA, то усиленная конечная теорема Рамсея верна» не доказуема в PA, поскольку «усиленная конечная теорема Рамсея верна» не доказуема в PA (несмотря на то, что она истинна).

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

Вторая теорема Гёделя о неполноте следует из теоремы LoB путем подстановки ложных показаний для P. ${\ displaystyle \ bot}$

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

• Булос, Джордж С. (1995). Логика доказуемости. Издательство Кембриджского университета. ISBN   978-0-521-48325-4.
• Лёб, Мартин (1955), «Решение проблемы Леона Хенкина», Journal of Symbolic Logic, 20 (2): 115–118, JSTOR   2266895
• Хинман, П. (2005). Основы математической логики. А.К. Петерс. ISBN   978-1-56881-262-5.
• Вербрюгге, Ринеке (LC) (1 января 2016 г.). «Логика доказуемости». Стэнфордская энциклопедия философии. Проверено 6 апреля +2016.

• Теорема Лёба в PlanetMath
• Руководство по Cartoon теореме LOB в по Юдковски