Неформальные и формальные аксиоматические теории

[Mr Alexey]

Доброго времени суток. Помогите разобраться, в чем разница между неформальными и формальными аксиоматическими теориями. По определению:

"Множество замкнутых формул, которые логически следуют из
данного множества аксиом, называется неформальной аксиоматической
теорией.
Множество замкнутых формул, которые выводимы в исчислении
предикатов из данного множества аксиом, называется формальной
аксиоматической теорией."

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

[Toucan]

Тема перемещена из форума «Математика (общие вопросы)» в форум «Помогите решить / разобраться (М)»

[Xaositect]

Логическое следование - это когда формула истинна в любой модели нашего множества аксиом.
Какое правило вывода Вы называете Taut?

[Mr Alexey]

Xaositect в сообщении #695739 писал(а):

Какое правило вывода Вы называете Taut?

Правило тавтологического следствия

Xaositect в сообщении #695739 писал(а):

Логическое следование - это когда формула истинна в любой модели нашего множества аксиом.

Это вроде и есть тавтологическое следование. (Для формулы А из того, что все аксиомы верны, следует, что А верна)

[Xaositect]

Терминология в разных учебниках логики, к сожалению, отличается до неузнаваемости. Термин "Правило тавтологического следствия" мне говорит мало. Дайте формальную формулировку.

Для исчисления предикатов эквивалентность логического и дедуктивного следования называется теоремой Геделя о полноте и доказывается нетривиально.

[Mr Alexey]

Xaositect в сообщении #695775 писал(а):

Терминология в разных учебниках логики, к сожалению, отличается до неузнаваемости. Термин "Правило тавтологического следствия" мне говорит мало. Дайте формальную формулировку.

Формулу $B$ возможно вывести из множества формул $A_{1}, ... ,A_{n}$, если формула $A_{1}\& A_{2}\& ...\& A_{n} \mapsto B$ - тавтология.
Взято из учебника: Успенский В.А., Верещагин Н.К., Плиско В.Е. "Вводный курс математической логики"

Xaositect в сообщении #695775 писал(а):

Для исчисления предикатов эквивалентность логического и дедуктивного следования называется теоремой Геделя о полноте и доказывается нетривиально.

До теоремы о полноте я еще не дочитал) Но если логическое и дедуктивное следования эквивалентны, значит формальная и неформальная аксиоматическая теория тоже эквивалентны?

[Xaositect]

Mr Alexey в сообщении #695782 писал(а):

Взято из учебника: Успенский В.А., Верещагин Н.К., Плиско В.Е. "Вводный курс математической логики"

В начале §3 гл.3 (Тавтологическое следствие) приводится определение тавтологии, согласно которому тавтологией называется формула, получающаяся подстановкой из пропозициональной тавтологии. То есть, например, формула $\forall x \neg P(x) \supset \neg \exists x P(x)$ не является тавтологией, несмотря на то, что общезначима, и, значит, $\neg\exists x P(x)$ является логическим следствием $\forall x \neg P(x)$, но не является тавтологическим следствием.

Кстати, это определение тавтологии тоже не общепринято - чаще "общезначимая формула" и "тавтология" означают одно и то же.

-- Пт мар 15, 2013 00:36:54 --

Mr Alexey в сообщении #695782 писал(а):

До теоремы о полноте я еще не дочитал) Но если логическое и дедуктивное следования эквивалентны, значит формальная и неформальная аксиоматическая теория тоже эквивалентны?

Да

[Mr Alexey]

Xaositect, спасибо за помощь, вы мне очень помогли.