Про определение модели в ZFC

[kp9r4d]

Примерно понятно, как в ZFC определить такие понятия как "формальная грамматика", "формальный язык" и "формальная теория". Но ведь я правильно понимаю, что в ZFC предикат вида $R(T,M) \leftrightarrow (\text{M - модель T})$ невыразим и можно только выразить предикат $R_T(M) \leftrightarrow (\text{M - модель T})$ для каждой конкретной $T$?

[arseniiv]

А из каких соображений?

(Оффтоп)

Если теория здесь — это множество формул (замкнутое относительно логического следствия), то, наверное, я чего-то не понимаю в вопросе, потому что $M\vDash\varphi$ ($\varphi$ — формула соответствующего языка), очевидно, выразим, ну а $R(T, M)$ будет $\forall\varphi.\;\varphi\in T\to M\vDash\varphi$.

Если теория — это $\{\varphi : \mathcal A\vdash\varphi\}$, где $\mathcal A$ — аксиомы, то всё равно получаем то, что выше, потому что $\mathcal A\vdash\varphi$ тоже выражается.

Или можно подумать, что есть проблема в выразимости проверки множества формул на замкнутость по следствию, но нет: $T\vDash\varphi$ — это $\forall I.\;I\vDash T\to I\vDash\varphi$.

Видимо, я или упускаю какую-то деталь, или не понимаю вопрос.

(Во всех случаях можно определить $\vDash,\vdash$ так, чтобы для некорректных аргументов их значением была ложь, так что можно не заботиться о проверке на то, являются ли $M,I$ интерпретациями данного языка, $\varphi$ формулой данного языка и $T$ содержащей только формулы его же.)

[kp9r4d]

arseniiv в сообщении #1116064 писал(а):

потому что $\mathcal A\vdash\varphi$ тоже выражается.

Очень интересно, а как?

[arseniiv]

А, я забыл про нестандартные натуральные числа! И ведь об этом здесь недавно уже писали… Да, они портят проверку на конечность последовательности формул, которую мы бы хотели назвать выводом.

-- Вс апр 17, 2016 20:33:42 --

Но тогда всё плохо для обоих предикатов.

[kp9r4d]

arseniiv
Я не очень понял при чём тут нестандартные натуральные числа. Если у теории $T$ есть конкретный набор констант $c_0,c_1,c_2,...,c_n$, функ. симоволов $f_1,f_2,f_3,...,f_m$ и символов отношений $R_1,R_2,...,R_k$ то любой набор $(S,c_0,c_1,c_2,...,c_n,f_1,f_2,...,f_m,R_1,R_2,...,R_k)$ такой, что он удовлетворят аксиомам $T$ которые мы можем тупо переписать называется моделью. Но вот в случае $R(T,M)$ мы не можем "тупо переписать аксиомы из Т", у нас нет такой штучки, которая бы строку (элемент теории ZFC) превращала бы в аксиому ZFC (не элемент теории ZFC), надеюсь, я достаточно понятно объяснил то, что я не понимаю.

-- 17.04.2016, 17:58 --

Объясню на совсем простом примере, возьмём теорию $T$ "существует ровно 2 элемента" состоящую из 2-х констант $(c_0,c_1)$ и двух аксиом $\forall x (x = c_0 \vee x = c_1)$ и $c_0 \neq c_1$.

Тогда в ZFC предикат будет выглядеть так $R_T(S,c_0,c_1) \Leftrightarrow (c_0 \in S \wedge c_1 \in S) \wedge (\forall x \in S (x = c_0 \vee x = c_1)) \wedge (c_0 \neq c_1)$. Я думаю, из этого примера моя мысль о том, что для любой теории предикат $R_T(M)$ выразим понятна, но можно ли выразить предикат $R(T,M)$?

[arseniiv]

kp9r4d в сообщении #1116086 писал(а):

Я не очень понял при чём тут нестандартные натуральные числа.

Это насчёт определения вывода. Вывод должен быть конечной последовательностью формул, но тут я опять ерунду написал, и всё должно быть нормально.

kp9r4d в сообщении #1116086 писал(а):

Но вот в случае $R(T,M)$ мы не можем "тупо переписать аксиомы из Т", у нас нет такой штучки, которая бы строку (элемент теории ZFC) превращала бы в аксиому ZFC (не элемент теории ZFC), надеюсь, я достаточно понятно объяснил то, что я не понимаю.

Эээ… а зачем нам тут аксиомы ZFC? Можно выразить выводимость одной строки из множества других строк по данному набору правил вывода.

[kp9r4d]

arseniiv в сообщении #1116092 писал(а):

Эээ… а зачем нам тут аксиомы ZFC? Можно выразить выводимость одной строки из множества других строк по данному набору правил вывода.

Допустим можно, и что это даст? Можете с помощью этого предиката записать "M модель Т" на языке ZFC?

[arseniiv]

Ну, он складывается из упомянутого.
1. «$M$ — модель множества формул $T'$»: $\forall\varphi.\;\varphi\in T'\to M\vDash\varphi$
2. «$T'$ — множество выводимых из (аксиом) $\mathcal A$ формул»: $T' = \{\varphi : \mathcal A\vdash\varphi\}$. И берём $\exists T'.\;(1)\wedge(2)$.
$\varphi$ тут везде, конечно, строки-формулы, являющиеся элементами ZFC, а не формулы самой ZFC. Я просто не подумал, что это надо было уточнить.

[kp9r4d]

Ну самое интересное место как раз в $M\vDash\varphi$ как сказать, что строка-формула "$\varphi$" истина в ZFC как формула "$\varphi$"?

arseniiv в сообщении #1116097 писал(а):

$\varphi$ тут везде, конечно, строки-формулы, являющиеся элементами ZFC, а не формулы самой ZFC. Я просто не подумал, что это надо было уточнить.

И даже "внутри" предиката $\vDash$? У меня, в принципе, такой вопрос: мне абсолютно понятно, что, грубо говоря, "теорию формальных систем" можно реализовать средствами ZFC, но мне непонятно, можно ли формализовать теорию моделей средствами ZFC, - непонятно из-за одного места, я не умею в ZFC говорить что "строка-аксиома $\varphi$ верна как аксиома в алгебраической системе $M$ (которое суть просто множество с некоторыми функциями и отношениями, там уже нет никаких строк)".

[arseniiv]

kp9r4d в сообщении #1116102 писал(а):

Ну самое интересное место как раз в $M\vDash\varphi$ как сказать, что строка-формула "$\varphi$" истина в ZFC как формула "$\varphi$"?

Почему «в ZFC»? В $M$ же. ZFC у нас метатеория тут, если я правильно понял, а рассматриваем мы всё, представляя её объектами.

kp9r4d в сообщении #1116102 писал(а):

непонятно из-за одного места, я не умею в ZFC говорить что "строка-аксиома $\varphi$ верна как аксиома в алгебраической системе $M$ (которое суть просто множество с некоторыми функциями и отношениями, там уже нет никаких строк)"

А не в ZFC, на обычном языке? Там ведь тоже модель просто множество с функциями и отношениями, и там тоже нет никаких строк. Потом, я не понимаю, чем тут важна «аксиомность» — просто строка-формула верна (или неверна) в алгебраической системе $M$, а аксиомой она может быть только по отношению к какой-то аксиоматической теории, но не вообще.

[kp9r4d]

arseniiv в сообщении #1116136 писал(а):

Потом, я не понимаю, чем тут важна «аксиомность» — просто строка-формула верна в алгебраической системе $M$

Я не понимаю как это записать.

[mihaild]

kp9r4d в сообщении #1116102 писал(а):

Ну самое интересное место как раз в $M\vDash\varphi$ как сказать, что строка-формула "$\varphi$" истина в ZFC как формула "$\varphi$"?

Определение истинности формулы в интерпретации, кажется, можно проверять изнутри ZFC. Добавим в сигнатуру все элементы $M$, и возьмем минимальное множество $P$, включающее все истинные атомарные формулы, не содержащие переменные (т.е. прообраз $\top$ относительно интерпретации предикатных символов), и замкнутое относительно добавления кванторов и добавления связок (т.е. $\widehat{A \land B} \Leftrightarrow (\widehat{A} \in P \land \widehat{B} \in P})$, $\widehat{\forall x \varphi(x)} \in P \Leftrightarrow \forall a \in M \widehat{\varphi(a)} \in P$ и т.д.).

[arseniiv]

kp9r4d в сообщении #1116137 писал(а):

Я не понимаю как это записать.

Просто перевести обычные индуктивные определения значения терма и формулы на язык теории множеств. Например, вот определение значения $I(t)\colon (V\to S)\to S$ терма $t$ в интерпретации $I$ (пускай также $I$ зовётся функция, сопоставляющая символы языка константам/функциям и предикатам алгебраической системы $M = (S,\ldots)$), где $V$ — множество переменных:
• Если $t \in V$, $I(t)(i) = i(t)$.
• Если $t = f(t_1,\ldots)$, то $I(t)(i) = I(f)(I(t_1)(i),\ldots)$. Сюда может входить или не входить, в зависимости от определений, случай
• Если $t = c$, то $I(t)(i) = I(c)$.
Даже это доводить до точности, конечно, будет немного муторно, а уж структура формулы ещё разнообразнее, и потому там будет не сахар, но препятствий нет.

-- Пн апр 18, 2016 01:11:16 --

И тогда, в конечном итоге, положим $M\vDash\varphi\equiv \forall i\colon V\to S.\;I(\varphi)(i) = \mathsf{true}$.

[kp9r4d]

Как терм проинтерпретировать при помощи $I$ - понятно, а как $I$ будет действовать на логические связки и кванторы?

[arseniiv]

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

Полистал, что у меня есть. Кажется, у Манина, Доказуемое и недоказуемое довольно подробно описано в главе II, §2. Или Xaositect как-то советовал английский перевод (там есть дополнения, но здесь они ни при чём) его другой книги A Course in Mathematical Logic for Mathematicians. Там должно быть практически то же самое по этой теме, но выбор слов может быть немного иным.

-- Пн апр 18, 2016 02:00:53 --

Я бы здесь всё набрал, но лень. Вот, например, конъюнкция и квантор всеобщности:
• Если $\varphi = \alpha\wedge\beta$, то $I(\varphi)(i) = \min(I(\alpha), I(\beta))$, и подразумевается, что $\mathsf{false}<\mathsf{true}$.
• Если $\varphi = \forall v.\,\alpha$, то $I(\varphi)(i) = \min\{I(\alpha)(i'(x)) : x\in S\}$, где

$$i'(x)(u) = \begin{cases} x, & u = v; \\ i(u) & u \ne v. \end{cases}$$