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  След.

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



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

Сейчас этот форум просматривают: нет зарегистрированных пользователей


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

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