Теорема Льоба

Теорема Леба — теорема в математичній логіці про взаємозв'язок між доказовими твердження і самим твердженням. Доведена математиком Мартіном Лебом в 1955 році.

Теорема Леба стверджує, що у всякій теорії, що включає аксіоматику Пеано, для будь-якого висловлювання ${\displaystyle P}$ доведеність висловлювання «доведеність ${\displaystyle P}$ тягне ${\displaystyle P}$» можлива тільки у разі доведеності самого висловлювання ${\displaystyle P}$. Символічно ця теорема може бути записана наступним чином:

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

Наслідком теореми Леба є те, що тільки в суперечливій теорії висловлювання «доведеність ${\displaystyle P}$ тягне ${\displaystyle P}$» доказове для всіх тверджень ${\displaystyle P}$.

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