avva | аналогии

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

В этот разъем, эту щель между "есть доказательство" и "можно доказать" укладывается вся тема формализации понятия "алгоритм", машина Тьюринга, теория вычисления и компьютеры. Сначала нужно было достаточно формализовать логику для того, чтобы фразу "есть доказательство", которая до того в основном означала "вот оно, доказательство", переинтерпретировать как абстрактное "есть такой объект, он является доказательством, которое мы ищем, и он существует". Только тогда стала заметной возможная щель между "этот объект существует" и "мы можем гарантированным образом найти и продемонстрировать этот объект за конечное время", и из первой теоремы неполноты Гёделя как раз и следует, что эта щель реальна, т.е. общего алгоритма для идентификации аналитических истин просто не существует.

(аналитические истины тут на самом деле ни при чем, просто я перечитываю "Две догмы эмпиризма" Куайна, и гоняюсь за растекающимися ассоциациями)