Исчисления предикатов

[bonika]

Здравствуйте,
задали решить задачку, но я что-то никак не могу разобраться с чего начинать и как доказать.
Текст задачи: Доказать, что если Г├ А в ИП, то Г |= А

Я начала решать так:
Г |= А. Формула А является общезначимой если А истинна в любой интерпретации.

Г├ А. Выводом формулы А из формул Г в ИП называется конечная последовательность формул А1, А2, …, An, в которой An = Ầ и каждая из формул Ai, является или аксиомой, или формулой из Г (исходной формулой), или получается по некоторому правилу вывода из предыдущих формул последовательности.

А как само доказательство проводить даже не представляю.
Подскажите пожалйста

[cyb12]

bonika в сообщении #378925 писал(а):

Г |= А. Формула А является общезначимой если А истинна в любой интерпретации.

При чём здесь общезначимость формулы? Это же не $\models A$, а $\Gamma\models A.$

[bonika]

$\Gamma\models A.$ ну да Это логическое следствие, а значит если все формулы Г истинны, то и заключение А истинно

[cyb12]

Maslov в сообщении #378959 писал(а):

(Правда, не очень понятно, при чём здесь предикаты).

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

[Maslov]

cyb12 в сообщении #378964 писал(а):

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

Да Вы правы (извините, удалил своё сообщение).

Доказываемое утверждение -- "половина" теоремы об адекватности для ИП: Формула $F$ синтаксически выводима из множества формул $\Phi$ тогда и только тогда, когда она семантически выводима из $\Phi$: $\Phi \vdash F \Leftrightarrow \Phi \models F$.

В Игошине (издание 2004 г) это теорема 29.3.

[bonika]

Maslov в сообщении #378967 писал(а):

cyb12 в сообщении #378964 писал(а):

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

Да Вы правы (извините, удалил своё сообщение).

Доказываемое утверждение -- "половина" теоремы об адекватности для ИП: Формула $F$ синтаксически выводима из множества формул $\Phi$ тогда и только тогда, когда она семантически выводима из $\Phi$: $\Phi \vdash F \Leftrightarrow \Phi \models F$.

В Игошине (издание 2004 г) это теорема 29.3.

Спасибо Огромное!!! Вы мне очень-очень помогли!!!

[bonika]

Еще раз спасибо, скачала книжку и сразу нашла доказательство из двух теорем, вообщем там все просто и по полочкам изложено.
А можно еще вопросик, у меня просто было три задачки, одну я доказала сама, одну вы мне подсказали где найти, т.е. тоже доказана, осталась еще одна: Доказать, что все выводимые в ИП формулы тождествнно истинны

Ясно, что формула А ИП является тождественно истинной, если она истинна во всех интерператация ИП. А выводимые являются или аксиомой, или формулой из Г (исходной формулой), или получается по некоторому правилу вывода из предыдущих формул последовательности. И по идее строить доказательство нужно как в предыдущей задаче. рассмотреть три правила МР, правило всеобщности и существования. а дальше строить предположения.
Но возможно эта теорема тоже уже была доказана. если да то, не могли бы припомнить в каком учебнике Заранее спасибо

[Maslov]

bonika в сообщении #378999 писал(а):

Доказать, что все выводимые в ИП формулы тождествнно истинны
...
Но возможно эта теорема тоже уже была доказана.

А что получится, если в уже доказанное $\Phi \vdash F \Rightarrow \Phi \models F$ подставить вместо $\Phi$ пустое множество формул?