Вопросы о теореме Трахтенброта

[Tcirkubakin]

Здравствуйте. Возникли сложности с пониманием теоремы Трахтенброта (https://archive.org/details/a-concise-i ... 5/mode/1up). Попробую разбить вопросы на пункты(не по порядку):
1. В доказательстве применяется упражнение 1 пятого параграфа третьей главы (https://archive.org/details/a-concise-i ... 1/mode/1up). Нужно доказать, что получившееся расширение будет разрешимым. Алгоритм построить достаточно легко, при условии известности всех новых формул теории: чтобы узнать, принадлежит ли любая формула получившейся теории $T'$, сначала нужно понять, принадлежит ли она $T$(это возможно, так как $T$ разрешима). Если формула принадлежит $T$, то она будет принадлежать и $T'$(алгоритм останавливается). Если же нет, то достаточно её "сверить" с конечным множеством $T'/T$ на предмет принадлежности. Как я уже говорил, такой алгоритм можно построить при условии, что мы можем определить(алгоритмически) множество $T'/T$. А можно ли это сделать(каким алгоритмом найти это множество(также понять, что к этому множеству больше не присоединить конечное количество неких формул)), если по условию лишь известно, что расширение теории $T$ конечно?

2. Также используется упражнение 2 шестого параграфа третьей главы (https://archive.org/details/a-concise-i ... 6/mode/1up). Не смог понять, какое решение предлагает автор в пункте a) (https://page.mi.fu-berlin.de/raut/logic3/hint.pdf) (страница 9, 3.6). Как пишет автор, на шаге $n$ нужно записать лишь те формулы(с индексом меньшим или равным $n$), которые не будут удовлетворять энной модели $A$. Не может ли произойти случая, когда, например, формуле $\varphi_{10}$ не будет удовлетворять лишь конечная модель $A_{2}$(остальные будут)?(т.к. согласно построению автора , как я понял, для $\varphi_{10}$ на предмет удовлетворимости моделям можно будет лишь проверить модели с порядковым номером "больше или равно 10" (на предмет удовлетворимости модели $A_{2}$ можно лишь проверить формулы с индексом $i\le 2$))

3. Автор указывает, что если теория $\mathrm{Tautfin}_{\mathcal{L}}$(также $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}$) аксиоматизируема, то она разрешима(из-за свойства конечных моделей), согласно упражнению 2. Но для применения упражнения 2 эти теории должны удовлетворять ещё одному условию: все конечные модели этих теорий должны быть эффективно перечислимы, а как для них это доказать?

4. Упражнением 1 доказывается, что если бы $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}$ была разрешима, то это бы влекло разрешимость теории FSG(теории конечных полугрупп), так как она конечно расширяется (добавляется формула ассоциативности). Как в данном случае показать, что теория $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}+\alpha$ (где $\alpha$ - закон ассоциативности) будет конечным расширением? (под конечным расширением теории(могу неправильно переводить) я понимаю теорию, которая, при добавлении конечного множества формул, увеличится на конечное множество элементов).

[mihaild]

Tcirkubakin в сообщении #1587573 писал(а):

Как я уже говорил, такой алгоритм можно построить при условии, что мы можем определить(алгоритмически) множество $T'/T$. А можно ли это сделать(каким алгоритмом найти это множество(также понять, что к этому множеству больше не присоединить конечное количество неких формул)), если по условию лишь известно, что расширение теории $T$ конечно?

Так любое конечное множество разрешимо. От Вас не требуется как-то "угадать", что это за множество. Вам приносят множество, и просят алгоритм.

Tcirkubakin в сообщении #1587573 писал(а):

Как пишет автор, на шаге $n$ нужно записать лишь те формулы(с индексом меньшим или равным $n$), которые не будут удовлетворять энной модели $A$.

Да, мне тоже непонятно, как это должно работать. Но правится легко: на шаге $n$ выписываете $n$-ю формулу, если она не удовлетворяет одной из первых $n$ моделей, а также формулы с номерами, меньшими $n$, если они удовлетворяют первым $n-1$ моделям, но не $n$-й.

Tcirkubakin в сообщении #1587573 писал(а):

Как в данном случае показать, что теория $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}+\alpha$ (где $\alpha$ - закон ассоциативности) будет конечным расширением? (под конечным расширением теории(могу неправильно переводить) я понимаю теорию, которая, при добавлении конечного множества формул, увеличится на конечное множество элементов).

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

[Tcirkubakin]

С первыми двумя вопросами разобрался. Пока не понял ответ на два последних: 1. Можно ли как-то эффективно перечислить конечные модели теории $\mathrm{Tautfin}_{\mathcal{L}}$(также $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}$)? 2. И как убедиться, что расширение теории $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}+\alpha$ будет конечным?

[mihaild]

Tcirkubakin в сообщении #1587870 писал(а):

1. Можно ли как-то эффективно перечислить конечные модели теории $\mathrm{Tautfin}_{\mathcal{L}}$(также $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}$)?

А это разве не просто все возможные конечные интерпретации?

Tcirkubakin в сообщении #1587870 писал(а):

И как убедиться, что расширение теории $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}+\alpha$ будет конечным?

А как определяется конечность расширения? Просто обычно если добавили конечное множество аксиом - значит расширение конечное.

[Tcirkubakin]

mihaild в сообщении #1587880 писал(а):

А это разве не просто все возможные конечные интерпретации?

Да, множество таких интерпретаций - счётно. Но будет ли существовать алгоритм, пошагово перечисляющий эти модели(как быть в случае, если число моделей не является конечным). Здесь (первый абзац страницы: https://archive.org/details/a-concise-i ... 8/mode/1up) (может, снова неправильно понимаю) эффективно перечислимыми являются такие перечисления, которые имеют алгоритм, пошагово выводящий элементы.

mihaild в сообщении #1587880 писал(а):

А как определяется конечность расширения? Просто обычно если добавили конечное множество аксиом - значит расширение конечное.

Читал в учебнике, что любая теория обязательно должна быть дедуктивно-замкнутой, т.е., если из теории выводится некоторое утверждение, то оно должно ей (теории) принадлежать. В каком моменте рассуждения я ошибаюсь?
1. К теории (в данном случае это $\mathrm{Tautfin}_{\mathcal{L}}$(также $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}$)) можно присоединить некую аксиому.
2. Мы должны проверить, что множество утверждений $A$:=($\mathrm{Tautfin}_{\mathcal{L}}$ ($\mathrm{Tautfin}_{\mathcal{L}_{\circ }}$) с добавлением аксиомы) должно быть дедуктивно-замкнутым. Если это не так, то мы должны добавить предложения, выводимые из $A$, но не принадлежащие ей, и когда этот процесс будет завершён, мы получим дедуктивно-замкнутое множество, которое будет являться полноправной теорией. Как мы поймём, что при завершении этого процесса получится конечно-расширенная теория(или что к $A$ уже не надо ничего добавлять - может оно уже будет теорией(дедуктивно-замкнутой))? Благодарю.
P.S. Как я понял из учебника, что если, например $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}+\alpha$- теория, то это минимальное дедуктивно-замкнутое множество, содержащее $\mathrm{Tautfin}_{\mathcal{L}_{\circ }}$ и $\alpha$.

[mihaild]

Tcirkubakin в сообщении #1587896 писал(а):

Но будет ли существовать алгоритм, пошагово перечисляющий эти модели(как быть в случае, если число моделей не является конечным)

Ну так берете перечисляете все $n$-элементные (носителем пусть будут числа от $1$ до $n$) - для каждого предикатного символа перебираете все подмножества, для каждого функционального символа все функции и т.д., всегда всего будет конечно, потом перейдем к $n + 1$.

А Вы можете найти опредление "конечного расширения"? В подходе с "любая теория дедуктивно-замкнутая" было бы логично сказать, что $T'$ - конечное расширение $T$, если для некоторого конечного семейства формул $X$, $T'$ - минимальная теория, содержащая $T$ и $X$.

[Tcirkubakin]

mihaild в сообщении #1587899 писал(а):

А Вы можете найти опредление "конечного расширения"?

Да, подвела память, нашёл определение в учебнике:(последний абзац страницы: https://archive.org/details/a-concise-i ... 2/mode/1up). В таком случае надо переосмыслить в т.ч. и доказательство упражнения 1.
Определение теории, как дедуктивно-замкнутого множества формул дано на предыдущей странице.

[Tcirkubakin]

Нашёл простое доказательство упражнения 1 здесь, первый ответ после "Here are a few observations:": (https://math.stackexchange.com/question ... gical-deci).

mihaild в сообщении #1587899 писал(а):

Ну так берете перечисляете все $n$-элементные (носителем пусть будут числа от $1$ до $n$) - для каждого предикатного символа перебираете все подмножества, для каждого функционального символа все функции и т.д., всегда всего будет конечно, потом перейдем к $n + 1$.

Я правильно понял, что на области определения конечной модели будет, очевидно, конечное множество функций и отношений?(с точностью до изоморфизма)(т.к. множество функций (или отношений) (у функций арность - число, меньшее $n$, у отношений арность - не больше числа $n$) будет не мощнее множества(конечного) всех подмножеств области определения энной модели).

[mihaild]

Tcirkubakin в сообщении #1587963 писал(а):

Я правильно понял, что на области определения конечной модели будет, очевидно, конечное множество функций и отношений?

Да, так. На $n$-элементом множестве можно ввести максимум $2^{n^k}$ предикатов валентности $k$.

[Tcirkubakin]

Кажется, всё об этой теме уяснил, благодарю.