Лемма Линденбаума и аксиома выбора

[Ираклий]

Лемма Линденбаума говорит, что любое непротиворечивое множество формул логики предикатов можно расширить до максимального по включению непротиворечивого множества формул.
http://en.wikipedia.org/wiki/Lindenbaum's_lemma

С одной стороны, конечно, из AC (аксиома выбора) следует это утверждение: оно легко получается из леммы Цорна (утверждения, эквивалентного АС). С другой стороны, утверждается, что для доказательства ЛЛ достаточна слабая версия АС $-$ принцип зависимого выбора. В связи с этим приводится следующее доказательство:

Пусть $\Gamma -$ наше непротиворечивое множество формул. Пронумеруем эффективно вообще все формулы: $Fm = \{A_0, A_1, ...\}$
Рассмотрим последовательность $\Gamma_n$, определяемую следующим образом:
$\Gamma_0 = \Gamma$,
$\Gamma_{n+1}=\begin{cases} \Gamma_n\cup \{A_n\},&\text{если $\Gamma_n\cup \{A_n\}$ непротиворечива;}\\ \Gamma_n\cup \{\neg A_n\},&\text{в противном случае.} \end{cases}$
Далее можно показать, что $\bigcup\limits_n\Gamma_n$ есть нужное расширение.

Так вот, утверждается, что в построении последовательности $\Gamma_n$ используется AC (а точнее, ее слабая версия). Я в упор не вижу, где она там используется. Построение последовательности $\Gamma_n$ мне кажется совершенно конструктивным. В том смысле, что эту последовательность можно описать внешней формулой. После чего существование этой последовательности следует из аксиомы выделения. В чем я не прав?

[Nik_Nikols]

Теорема (ZF). Существует множество U максимальных по включению непротиворечивых расширений непротиворечивого множества высказываний $\Gamma $.

Откуда следует непустота множества U?

[Ираклий]

Nik_Nikols в сообщении #263485 писал(а):

Откуда следует непустота множества U?

Она следует из того, что один конкретный элемент с этим свойством предъявлен $-$$\bigcup\limits_n\Gamma_n$.

[Nik_Nikols]

Судя по вашим определениям, язык у вас не более, чем счетный.
Вы рассматриваете его вместе с фиксированной нумерацией нелогических символов?

[Ираклий]

Ираклий в сообщении #263595 писал(а):

Вы рассматриваете его вместе с фиксированной нумерацией нелогических символов?

Да. Нелогических символов конечное число. Формулы суть слова в фиксированном конечном алфавите. Фиксирована некоторая эффективная нумерация всех формул (например, по длине, а при одинаковой длине по алфавиту). Так что эта нумерация выражается некоторой внешней формулой. Учитывая всё это, я считаю построение последовательности $\Gamma_n$ совершенно конструктивным и доказательство существования этой последовательности, на мой взгляд, не использует АС.

[Nik_Nikols]

Цитата:

Да. Нелогических символов конечное число.

Ну, этого вам вряд ли хватит Мне сложно представить содержательную задачу, в которой вам понадобилось бы непротиворечивое, но не свидетельское замыкание множества формул CPC.
Впрочем, эта трудность, конечно, обходится.

[Ираклий]

Вот я и перестал Вас понимать. Что значит "не свидетельское"? Не хватит для чего?
Я имею в виду классическую формулировку леммы Линденбаума, например, эта сойдет:
http://en.wikipedia.org/wiki/Lindenbaum's_lemma
Сам я с ней познакомился на спецкурсе по модальной логике, лектор рассматривал модальную логику с n боксами. А вообще важно лишь то, что множество Fm можно эффективно (т.е. алгоритмически, а значит, и внешней формулой) пронумеровать. Это верно для широкого класса языков.

[Nik_Nikols]

Цитата:

Вот я и перестал Вас понимать. Что значит "не свидетельское"? Не хватит для чего?

Ну, непротиворечивые пополнения множества формул CPC (или аналоги в предикатных модальных языках) часто возникают на некотором этапе построения моделей; поэтому появляются расширения языков множеством констант ("свидетелей"), и конечными языками для большинства естественных задач не обойтись.

Впрочем, как вы справедливо отметили,...

Цитата:

...важно лишь то, что множество Fm можно эффективно (т.е. алгоритмически, а значит, и внешней формулой) пронумеровать. Это верно для широкого класса языков.

В-общем, кажется, разобрались

[Someone]

Ираклий в сообщении #263409 писал(а):

$\Gamma_{n+1}=\begin{cases} \Gamma_n\cup \{A_n\},&\text{если $\Gamma_n\cup \{A_n\}$ непротиворечива;}\\ \Gamma_n\cup \{\neg A_n\},&\text{в противном случае.} \end{cases}$

А можно ли конструктивно определить, что $\Gamma_n\cup \{A_n\}$ непротиворечива?

[Ираклий]

Да, можно. Если Х - множество формул, то оно непротиворечиво, если не существует вывода из Х противоречия. Это условие можно записать внешней формулой с параметром Х (и, быть может, другими параметрами, характеризующими язык).

[Someone]

Записать-то, может быть, и можно, а конструктивно проверить? С помощью алгоритма, то есть.

[Ираклий]

Алгоритма может и не быть. Но это вовсе не означает, что нужна АС. АС нужна, когда объект нельзя описать формулой.

[AGu]

Ираклий в сообщении #263409 писал(а):

Я в упор не вижу, где она там используется.

Я тоже не вижу. А где утверждается, что она там используется?

[Ираклий]

AGu в сообщении #264106 писал(а):

А где утверждается, что она там используется?

Это сказал уважаемый мною лектор на спецкурсе по модальным логикам. Он куда-то торопился и мне не удалось у него подробно выведать, что же он имел в виду.

[AGu]

Аксиома зависимого выбора пригодилась бы, если бы на $n$-м шаге приходилось выбирать $A_n$. Но у нас $A_n$ уже «выбраны» нумерацией языка. Кстати, если я не глючу, то тут даже эффективность нумерации не нужна, достаточно счетности языка. А если трансфинитно обобщить приведенную Вами конструкцию, то получится доказательство леммы Линденбаума без какой-либо версии аксиомы выбора при условии, что язык вполне упорядочен. (Кажется, я даже где-то встречал это утверждение.)