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

[mihaild]

Да, это другое, а именно в каком-то виде $\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))$.

[Tcirkubakin]

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

[KhAl]

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

[Tcirkubakin]

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

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

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

[mihaild]

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

первое означает, что $X\models a$, если для каждой модели X следует, что каждая такая модель удовлетворяет a; второе $X\vdash a$ означает, что из X выводимо a, согласно определ. набору правил

Тут надо смотреть определения обозначений у автора. Иногда слева от двойного штопора ($\models$) вообще ставят модель, а не теорию.

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

переводится, как теорема об исключении?

Как правило говорят "элиминация".

[Tcirkubakin]

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