2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему На страницу 1, 2  След.
 
 О консервативных расширениях теорий
Сообщение19.01.2023, 23:08 


26/12/22
52
Явное определение 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)
Не понятно, каким образом отсутствие условия обоснования влияет на консервативность расширения теории с функцией.

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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение20.01.2023, 19:11 


26/12/22
52
Явное определение 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)
Не понятно, каким образом отсутствие условия обоснования влияет на консервативность расширения теории с функцией.
(Прошу простить за флуд, так как преследует злой рок с написанием формул.)

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение20.01.2023, 21:04 


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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение21.01.2023, 17:32 


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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение21.01.2023, 20:24 


26/12/22
52
KhAl в сообщении #1578203 писал(а):
Почему это расширение не консервативно?

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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение21.01.2023, 23:36 


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

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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение22.01.2023, 13:47 


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

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

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

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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение22.01.2023, 23:48 


26/12/22
52
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. Или, я что-то не понял...

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение23.01.2023, 14:13 
Заслуженный участник
Аватара пользователя


16/07/14
8355
Цюрих
Tcirkubakin в сообщении #1578338 писал(а):
А для того, чтобы получилась полноценная теория групп, нам требуется что условие $y \ \circ \ x =e$ обязано выполняться для всех элементов x.
Всё-таки $\exists y(y \circ x = e)$.
Именно для этого нам требовалась обоснованность $\eta_f$ - т.е. что мы уже можем доказать существование и единственность "значения функции" (хотя никакой функции на момент проверки обоснованности еще нет).

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение23.01.2023, 14:53 


26/12/22
52
mihaild в сообщении #1578425 писал(а):
Всё-таки $\exists y(y \circ x = e)$.

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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение23.01.2023, 15:07 
Заслуженный участник
Аватара пользователя


16/07/14
8355
Цюрих
Tcirkubakin в сообщении #1578430 писал(а):
добавления к теории моноидов формулы, определяющей функцию inv достаточно (как я понял, без обосновыв. утверждения) для формирования теории групп(в которой, кроме этого, требуется аксиома $\exists y(y \circ x = e)$, что добавл-мая формула не представляет).
А, понял, в чем вопрос.
Да, если у нас есть функция, то по определению считается, что она определена всюду, и её значение единственно. Более точно, формула $\forall x \exists! y(y=f(x))$ (*) выводится для любого функционального символа $f$ (существование выводится из аксиомы подстановки, единственность - из транзитивности равенства).
А вот если мы добавляем новый функциональный символ, то, чтобы не получить внезапно новых, невыводимых ранее утверждений, нужно чтобы формула, получаемая подстановкой в (*) определения нашего символа, уже заранее выводилась.

(Оффтоп)

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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение24.01.2023, 00:42 


13/01/23
307
Tcirkubakin в сообщении #1578338 писал(а):
Я правильно понимаю, что после добавления функции в язык, а следом в теорию, то она обязана быть определена для всех элементов по определению?
Я уточню. Строго говоря, в язык мы добавляем не саму функцию, а функциональный символ (function symbol, он же operation symbol). На этом уровне нет никакого "определена для всех элементов" по простой причине -- элементов нет. Также нет и функции, как и понятия "определена для".

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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение24.01.2023, 13:43 


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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение24.01.2023, 13:46 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: О консервативных расширениях теорий
Сообщение24.01.2023, 14:03 


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 21 ]  На страницу 1, 2  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: Mikhail_K, tolstopuz


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group