2014 dxdy logo

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

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


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


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



Начать новую тему Ответить на тему На страницу Пред.  1, 2
 
 Re: О консервативных расширениях теорий
Сообщение24.01.2023, 15:20 
Заслуженный участник
Аватара пользователя


16/07/14
9545
Цюрих
Да, это другое, а именно в каком-то виде $\forall x \varphi \vdash \varphi \frac{t}{x}$ - т.е. что если мы доказали, что $\varphi$ выполнена для любого аргумента, то $\varphi$ выполнена и для $t$. Теперь как-нибудь выведем $\forall z \exists y(y = z)$, и подстановкой $f(x)$ вместо $z$ получим $\exists y (y = f(x))$.

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


26/12/22
52
Похожая формула выводилась в учебнике: $\forall \vec{x} \varphi \models \varphi \frac{\vec t}{\vec x}$

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


13/01/23
307
Tcirkubakin
хм. а в этом учебнике и истинность (в любой модели) и выводимость обозначаются одним символом, что ли? понимаете ли вы разницу между этими понятиями?

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


26/12/22
52
KhAl в сообщении #1579249 писал(а):
Tcirkubakin
хм. а в этом учебнике и истинность (в любой модели) и выводимость обозначаются одним символом, что ли? понимаете ли вы разницу между этими понятиями?

Нет, обозначаются разными и подразумевается различие (написал "похожее", т.к. для пропозициональной логики(кажется так называется) доказывается их эквивалентность(в учебнике Completeness theorem), хотя я не знаю их эквивалентность в логике первого порядка(пока не дошёл до этого)). Надеюсь, что разницу понимаю(первое означает, что $X\models a$, если для каждой модели X следует, что каждая такая модель удовлетворяет a; второе $X\vdash a$ означает, что из X выводимо a, согласно определ. набору правил).
Сейчас пытаюсь понять теорему 6.1 второй главы (Elimination theorem(переводится, как теорема об исключении?)) для расширений с функциональными символами и константами.

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


16/07/14
9545
Цюрих
Tcirkubakin в сообщении #1579435 писал(а):
первое означает, что $X\models a$, если для каждой модели X следует, что каждая такая модель удовлетворяет a; второе $X\vdash a$ означает, что из X выводимо a, согласно определ. набору правил
Тут надо смотреть определения обозначений у автора. Иногда слева от двойного штопора ($\models$) вообще ставят модель, а не теорию.
Tcirkubakin в сообщении #1579435 писал(а):
переводится, как теорема об исключении?
Как правило говорят "элиминация".

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


26/12/22
52
Слева от двойного штопора под X я подразумевал множество формул (в пункте 3 главы о пропозиц. исчислении(1 главы) автор подразумевает это ). Модели слева от двойного штопора у автора также встречаются.

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

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



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

Сейчас этот форум просматривают: Alex Krylov


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

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