О консервативных расширениях теорий

[Tcirkubakin]

Явное определение n-арной функции не встречающейся в языке $\mathscr{L}$ задаётся формулой вида:
$\eta_{f}:\quad y=\,f\,\overrightarrow{x}\leftrightarrow \delta\left( \overrightarrow{x},y \right)\quad \left( \delta\in \mathscr{L}\: \right)$
$\eta_{f}$ называется обоснованной в теории $\mathrm{T}\subseteq \mathscr{L}$ , если $\mathrm{T}\models\:\forall\overrightarrow{x}\,\exists !y\delta$. Тогда расширение теории $\mathrm{T}_{f}\: :=\mathrm{T}\:+\:\eta_{f}^{g}$ (где $\eta^{g}$ предложение вида $\forall x_{1}\cdots \forall x_{m}\eta$, где $x_{1},\cdots x_{m}$ перечисление свободных переменных формулы $\eta$) является консервативным т.е.

$$T^{\prime} \supseteq T$ in $\mathcal{L}^{\prime} \supseteq \mathcal{L}$ such that $T^{\prime} \cap \mathcal{L}=T$$

(L штрих обозначает язык L с добавленной операцией f)
Не понятно, каким образом отсутствие условия обоснования влияет на консервативность расширения теории с функцией.

П.С. Формулы опять не отобразились... Попытаюсь исправить.

[Tcirkubakin]

Явное определение n-арной функции не встречающейся в языке $\mathscr{L}$ задаётся формулой вида:
$\eta_f\quad y=f\vec{x}\leftrightarrow\delta(\vec{x},y)\quad (\delta\in \mathscr{L})$
$\eta_{f}$ называется обоснованной в теории $\mathrm{T}\subseteq \mathscr{L}$ , если $\mathrm{T}\models\:\forall\vec{x}\,\exists !y\delta$. Тогда расширение теории $\mathrm{T}_{f}\: :=\mathrm{T}\:+\:\eta_{f}^{g}$ (где $\eta^{g}$ предложение вида $\forall x_{1}\cdots \forall x_{m}\eta$, где $x_{1},\cdots x_{m}$ перечисление свободных переменных формулы $\eta$) является консервативным т.е. $T^{\prime} \supseteq T \ \ \text{in} \ \mathcal{L}^{\prime} \supseteq \mathcal{L} \ \ \text{such that} \ T^{\prime} \cap \mathcal{L}=T$(L штрих обозначает язык L с добавленной операцией f)
Не понятно, каким образом отсутствие условия обоснования влияет на консервативность расширения теории с функцией.
(Прошу простить за флуд, так как преследует злой рок с написанием формул.)

[Tcirkubakin]

Расширением теории является теория вида $\mathrm{T} + \eta_{f}^{g}$ (в прошлом сообщении неправильно ввёл). В учебнике под "T'=T+a" понимается минимальная теория, расширяющая теорию T и содержащая формулу a

[KhAl]

Если знаете, что такое группа, то представьте себе теорию полугрупп с единицей (это как группы, только нет условия обратимости любого элемента, см. Википедию) и попробуйте её расширить функцией $inv(x)$ с $y = inv(x) \leftrightarrow xy = 1$. Что получится? Почему это расширение не консервативно?

[Tcirkubakin]

KhAl в сообщении #1578203 писал(а):

Почему это расширение не консервативно?

Кажется понял(с помощью википедии), но если я ошибся, то можете поправить.
Для контрпримера можно взять непротивор. теорию. В любой непротиворечивой теории предложение одновременно с его отрицанием не выводимо(у меня в учебнике под теориями понимается прежде всего множество предложений). То есть, если мы рассматриваем непротивореч. теорию моноидов, то в ней также не выводимо некое предложение. Существуют моноиды, в которых есть элементы a и b, такие что $ab = a$ и при этом b не является нейтральным элементом (в моноиде не выводимо обосновывающее утверждение о функции обратного элемента, т.е. он не обязан являться группой). Тогда в получившейся теории выводимо противоречие (мы могли бы домножить обе части равенства $ab = a$ на обратный к a элемент слева и получили бы противоречие). Таким образом(из-за противоречия), из расширенной теории выводимо любое предложение из нерасширенного языка, в частности предложения, невыводимые в теории моноидов, т.е консервативность была бы нарушена(пересечение новой теории со нерасш. языком не совпадало бы с изначальной теорией)
Есть еще недопонимание по теме явных определений, возможно зададу вопрос(ы) позднее.

[KhAl]

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

Тогда в получившейся теории выводимо противоречие

Ну, я имел в виду чуть более простую конструкцию: взять теорию, описывающую моноиды (на 65 странице Раутенберга есть аксиомы групп, осталось убрать оттуда обратимость и получатся аксиомы для моноидов). После добавления $inv$ получится теория, описывающая группы. Противоречия там не будет, просто утверждение "любой элемент обратим", необщезначимое для моноидов, оказывается общезначимым для групп.

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

[Tcirkubakin]

KhAl в сообщении #1578237 писал(а):

Ну, я имел в виду чуть более простую конструкцию: взять теорию, описывающую моноиды (на 65 странице Раутенберга есть аксиомы групп, осталось убрать оттуда обратимость и получатся аксиомы для моноидов). После добавления $inv$ получится теория, описывающая группы. Противоречия там не будет, просто утверждение "любой элемент обратим", необщезначимое для моноидов, оказывается общезначимым для групп.

Да, так весьма лаконичнее.

KhAl в сообщении #1578237 писал(а):

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

Да, это я и хотел сделать.

[Tcirkubakin]

KhAl в сообщении #1578237 писал(а):

После добавления $inv$ получится теория, описывающая группы.

Я правильно понимаю, что после добавления функции в язык, а следом в теорию, то она обязана быть определена для всех элементов по определению? Просто после добавления к теории формулы $\eta_{f}^{g} \colon \ \forall x \forall y \left( y=x^{-1}\leftrightarrow x \ \circ \ y = e \right)$ , она будет утверждать, что условие определенности функции обратного элемента равноценно тому что операция x с обратным элементом y равна e(т.е. если функция не задана, то и $y \ \circ \ x =e$ выполняться не обязано). А для того, чтобы получилась полноценная теория групп, нам требуется что условие $y \ \circ \ x =e$ обязано выполняться для всех элементов x. Или, я что-то не понял...

[mihaild]

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

А для того, чтобы получилась полноценная теория групп, нам требуется что условие $y \ \circ \ x =e$ обязано выполняться для всех элементов x.

Всё-таки $\exists y(y \circ x = e)$.
Именно для этого нам требовалась обоснованность $\eta_f$ - т.е. что мы уже можем доказать существование и единственность "значения функции" (хотя никакой функции на момент проверки обоснованности еще нет).

[Tcirkubakin]

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

Всё-таки $\exists y(y \circ x = e)$.

Извиняюсь, написал неточно.
Вопрос о определенности функции возник после сообщения Khaidа о том, что добавления к теории моноидов формулы, определяющей функцию inv достаточно (как я понял, без обосновыв. утверждения) для формирования теории групп(в которой, кроме этого, требуется аксиома $\exists y(y \circ x = e)$, что добавл-мая формула не представляет). Прошу не злиться на моё тугоумие, стараюсь понять, как могу. Или мне как-то по другому надо понимать сообщение Khaidа о доказательстве необходимости обоснов. утверждения для консервативности расширения теории?

[mihaild]

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

добавления к теории моноидов формулы, определяющей функцию inv достаточно (как я понял, без обосновыв. утверждения) для формирования теории групп(в которой, кроме этого, требуется аксиома $\exists y(y \circ x = e)$, что добавл-мая формула не представляет).

А, понял, в чем вопрос.
Да, если у нас есть функция, то по определению считается, что она определена всюду, и её значение единственно. Более точно, формула $\forall x \exists! y(y=f(x))$ (*) выводится для любого функционального символа $f$ (существование выводится из аксиомы подстановки, единственность - из транзитивности равенства).
А вот если мы добавляем новый функциональный символ, то, чтобы не получить внезапно новых, невыводимых ранее утверждений, нужно чтобы формула, получаемая подстановкой в (*) определения нашего символа, уже заранее выводилась.

(Оффтоп)

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

[KhAl]

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

Я правильно понимаю, что после добавления функции в язык, а следом в теорию, то она обязана быть определена для всех элементов по определению?

Я уточню. Строго говоря, в язык мы добавляем не саму функцию, а функциональный символ (function symbol, он же operation symbol). На этом уровне нет никакого "определена для всех элементов" по простой причине -- элементов нет. Также нет и функции, как и понятия "определена для".

Но mihaild правильно заметил, что как только язык содержит функциональный символ $f$, так сразу в любой теории этого языка выводима формула $\forall x \exists! y(y=f(x))$, что можно считать строгим выражением цитированного утверждения. (впрочем, если вы хотели сказать что-то существенно другое, то прошу)

[Tcirkubakin]

Возможно, у меня возникли проблемы из-за незнания аксиом ZF(кажется, их Вольфганг будет обсуждать в 3 главе). Что ж, если снова возникнет недопонимание, напишу снова.

[mihaild]

Как раз ZF тут не нужно, это более базовая вещь, на которой строится в том числе теория множеств (хотя тут и есть цикл: модели строятся из множеств). Хотя для примера может быть полезна.

[Tcirkubakin]

Разве аксиома замены(подстановки) не принадлежит ZF, или это что-то другое?