Математическая логика (по Мендельсону)

[Виктор Викторов]

Суть первых пяти параграфов второй главы (Теории первого порядка) становится ясна в конце пятого параграфа.

«... для логики предикатов синтаксический метод теорий первого порядка равносилен семантическому методу, использующему понятия интерпретации, модели, логической общезначимости и т. п.» Страница 79.
«Следствие 2.14. (Теорема Гёделя [1930] о полноте.) Во всяком исчислении предикатов первого порядка теоремами являются все те и только те формулы, которые логически общезначимы.» Страница 78.

Жизнь была бы почти прекрасна, если бы о двух методах (синтаксическом и семантическом) нам бы рассказали в начале главы и частенько добавляли что-нибудь вроде: «с синтаксической (семантической) точки зрения ...». Но так как этого не произошло, то изучение этого материала превратилось в чтение детектива. После вводных примеров идут определения термов, формул, кванторов и прочая и прочая. Эти определения нужны, как синтаксической, так и семантической версиям (мы ещё о этом не знаем). Но вот начинается второй параграф. Он весь о семантике (интерпретации, выполнимость и истинность, модели) и сразу неувязка: «Формулы имеют смысл только тогда, когда имеется какая-нибудь интерпретация входящих в нее символов.» Да, конечно, но только с семантической точки зрения, а синтаксическая точка зрения не нуждается в интерпретации (и в частности в области интерпретации). Третий параграф синтаксический. И всё со временем обошлось бы, но вдруг читаем: «Моделью теории первого порядка К называется всякая интерпретация, в которой истинны все аксиомы теории К» страница 66. Модель нам понадобится, но почему семантическое понятие вставлено без какого либо предупреждения в «синтаксический» параграф? И ещё один момент: я где-то уже видел слово «модель». А, вот:
«Данная интерпретация называется моделью для данного множества формул Г, если каждая формула из Г истинна в данной интерпретации» страница 59. Здесь возникают два вопроса:
1. Зачем мне новое определение? Нельзя ли воспользоваться определением на странице 59, добавив, что из-за истинности аксиом истинны и все формулы?
2. Аксиомы истинны в каждой интерпретации. Получается, что каждая интерпретация теории первого порядка К является её моделью? Или я заврался? (Что вполне может быть).

[beroal]

Виктор Викторов в сообщении #466170 писал(а):

1. Зачем мне новое определение? Нельзя ли воспользоваться определением на странице 59, добавив, что из-за истинности аксиом истинны и все формулы?

На странице 59 даётся определение модели множества формул, а на странице 66 — модели теории первого порядка. Просто интерпретация является моделью теории первого порядка $T$ iff она является моделью аксиом $T$. Так что можно выбросить не только определение модели теории первого порядка, но и определение теории первого порядка.

Виктор Викторов в сообщении #466170 писал(а):

2. Аксиомы истинны в каждой интерпретации. Получается, что каждая интерпретация теории первого порядка К является её моделью? Или я заврался? (Что вполне может быть).

Логические аксиомы истинны в каждой интерпретации.

[Виктор Викторов]

beroal в сообщении #466248 писал(а):

Виктор Викторов в сообщении #466170 писал(а):

1. Зачем мне новое определение? Нельзя ли воспользоваться определением на странице 59, добавив, что из-за истинности аксиом истинны и все формулы?

На странице 59 даётся определение модели множества формул, а на странице 66 — модели теории первого порядка. Просто интерпретация является моделью теории первого порядка $T$ iff она является моделью аксиом $T$. Так что можно выбросить не только определение модели теории первого порядка, но и определение теории первого порядка.

А зачем выбрасывать определение теории первого порядка? Это теория с конкретным набором логических аксиом. Чем она (теория) провинилась?

beroal в сообщении #466248 писал(а):

Логические аксиомы истинны в каждой интерпретации.

Правильно! Так и напишите (это к Мендельсону), что для исчисления предикатов первого порядка каждая интерпретация – модель, а острие определения направлено на теории, имеющие также и нелогические аксиомы.

[beroal]

Виктор Викторов в сообщении #466265 писал(а):

Так что можно выбросить не только определение модели теории первого порядка, но и определение теории первого порядка.

А зачем выбрасывать определение теории первого порядка? Это теория с конкретным набором логических аксиом. Чем она (теория) провинилась?[/quote]
Вместо теории первого порядка можно использовать просто множество формул. Тогда теорема теории первого порядка $T$ определяется как формула, выведенная из $T$ и логических аксиом.

beroal в сообщении #466248 писал(а):

Логические аксиомы истинны в каждой интерпретации.

Правильно! Так и напишите (это к Мендельсону), что для исчисления предикатов первого порядка каждая интерпретация – модель, а острие определения направлено на теории, имеющие также и нелогические аксиомы.[/quote]
Это я вам написал. Термин «аксиома» не однозначный — логические аксиомы, аксиомы теории первого порядка. Неверно, что каждая интерпретация является моделью каждой теории первого порядка.

-- Fri Jul 08, 2011 16:08:59 --

Виктор Викторов в сообщении #466265 писал(а):

beroal в сообщении #466248 писал(а):

Виктор Викторов в сообщении #466170 писал(а):

1. Зачем мне новое определение? Нельзя ли воспользоваться определением на странице 59, добавив, что из-за истинности аксиом истинны и все формулы?

На странице 59 даётся определение модели множества формул, а на странице 66 — модели теории первого порядка. Просто интерпретация является моделью теории первого порядка $T$ iff она является моделью аксиом $T$. Так что можно выбросить не только определение модели теории первого порядка, но и определение теории первого порядка.

А зачем выбрасывать определение теории первого порядка? Это теория с конкретным набором логических аксиом. Чем она (теория) провинилась?

beroal в сообщении #466248 писал(а):

Логические аксиомы истинны в каждой интерпретации.

Правильно! Так и напишите (это к Мендельсону), что для исчисления предикатов первого порядка каждая интерпретация – модель, а острие определения направлено на теории, имеющие также и нелогические аксиомы.

[Виктор Викторов]

beroal в сообщении #466248 писал(а):

Так что можно выбросить не только определение модели теории первого порядка, но и определение теории первого порядка.

Виктор Викторов в сообщении #466265 писал(а):

А зачем выбрасывать определение теории первого порядка? Это теория с конкретным набором логических аксиом. Чем она (теория) провинилась?

beroal в сообщении #466468 писал(а):

Вместо теории первого порядка можно использовать просто множество формул. Тогда теорема теории первого порядка $T$ определяется как формула, выведенная из $T$ и логических аксиом.

В принципе, да. Но выделение специального списка логических аксиом и места для нелогических аксиом смотрится разумным.

-- Пт июл 08, 2011 10:15:30 --

beroal в сообщении #466468 писал(а):

Неверно, что каждая интерпретация является моделью каждой теории первого порядка.

Я имел в виду исчисление предикатов первого порядка. «Теория первого порядка, не содержащая собственных аксиом, называется исчислением предикатов первого порядка.» Страница 66.

Виктор Викторов в сообщении #466265 писал(а):

...для исчисления предикатов первого порядка каждая интерпретация – модель...

[Виктор Викторов]

«Пусть К — теория первого порядка, в числе предикатных букв которой имеется $A_1^2$. Будем для сокращения писать $t = s$ вместо $A_1^2$ и $t\neq s$ вместо $\neg A_1^2(t, s)$. Теория К называется теорией первого порядка с равенством, если следующие формулы являются теоремами К:

(6)*) $\forall x_1(x_1 = x_1)$ (рефлексивность равенства);
(7) $(x=y)\to (\mathscr A(x, x)\to \mathscr A(x, y))$ (подстановочность равенства),

где $x$ и $y$ — предметные переменные, $\mathscr A(x, x)$ — произвольная формула, a $\mathscr A(x, y)$ получается из $\mathscr A(x, x)$ заменой каких-нибудь (не обязательно всех) свободных вхождений $x$ вхождениями $y$, с соблюдением условия, чтобы $y$ было свободно для тех вхождений $x$, которые заменяются. Таким образом, в одних случаях $\mathscr A(x, y)$ может иметь свободные вхождения $x$, в других случаях таких вхождений может уже не быть.» Страницы 86-87

И сноска на странице 86 «*) Мы здесь продолжаем нумерацию логических аксиом на стр. 65—66.»

Итак, мы дожили до «Теории первого порядка с равенством», но это определение порождает ряд вопросов:
1. Начну со сноски: (6) и (7) – логические аксиомы?
2. Это как можно требовать, чтобы (6) и (7) были теоремами? Один случай очевиден: если они аксиомы. А другие случаи требуют дополнительных аксиом. Т. е. получается, что мы собрались работать с неназванными нелогическими аксиомами. Как это?
3. Почему так существенен вопрос о свободных и связанных переменных в (7)?

[Xaositect]

Виктор Викторов в сообщении #466899 писал(а):

1. Начну со сноски: (6) и (7) – логические аксиомы?
2. Это как можно требовать, чтобы (6) и (7) были теоремами? Один случай очевиден: если они аксиомы. А другие случаи требуют дополнительных аксиом. Т. е. получается, что мы собрались работать с неназванными нелогическими аксиомами. Как это?

Ну тут вообще надо подумать, чем логические аксиомы отличаются от нелогических. И тут никакого разумного определения я не вижу, кроме как сказать, что у нас есть много теорий первого порядка, и логическими называются те аксиомы, которые позволяют доказывать общие для них всех утверждения.
Так что, если мы вместо всех теорий первого порядка возьмем теори с равенством, а правильными интерпретациями будем считать только те интерпретации, в которых предикату равенства соответствует диагональное отношение, то да, эти аксиомы будут логическими в выше указанном смысле.
А по поводу теорем - часто в специальных теориях (6) и (7) выводятся из нелогических аксиом, но если рассматривать всю совокупность теорий с равенством, то все-таки их надо, вообще говоря, добавлять как аксиомы.

Виктор Викторов в сообщении #466899 писал(а):

3. Почему так существенен вопрос о свободных и связанных переменных в (7)?

Ну, допустим, у нас есть функциональный символ $f$ арности 2. Тогда для того, чтобы доказать $x=y\to f(x,x) = f(x,y)$ нам нужно заменить не все свободные вхождения в формуле $f(x,x) = f(x,x)$.

[Виктор Викторов]

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

Так что, если мы вместо всех теорий первого порядка возьмем теории с равенством, а правильными интерпретациями будем считать только те интерпретации, в которых предикату равенства соответствует диагональное отношение, то да, эти аксиомы будут логическими в выше указанном смысле.
А по поводу теорем - часто в специальных теориях (6) и (7) выводятся из нелогических аксиом, но если рассматривать всю совокупность теорий с равенством, то все-таки их надо, вообще говоря, добавлять как аксиомы.

Этот кусок мне стал ясен и, по крайней мере, теперь я могу двигаться дальше. Огромное спасибо.

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

Ну тут вообще надо подумать, чем логические аксиомы отличаются от нелогических. И тут никакого разумного определения я не вижу, кроме как сказать, что у нас есть много теорий первого порядка, и логическими называются те аксиомы, которые позволяют доказывать общие для них всех утверждения.

Это очень интересный вопрос. Вот что пишет Мендельсон: «Аксиомы теории К разбиваются на два класса: логические аксиомы и собственные (или нелогические) аксиомы.
Логические аксиомы: каковы бы ни были формулы $\mathscr A$, $\mathscr B$ и $\mathscr E$ теории К, следующие формулы являются логическими аксиомами теории К:» Страница 65 и дальше идут уже много раз цитированные аксиомы. Возникает ощущение, что только эти пять аксиом и являются логическими. Таким образом, моё ощущение явно ошибочно.
Но читаем дальше: «Собственные аксиомы: таковые не могут быть сформулированы в общем случае, ибо меняются от теории к теории. Теория первого порядка, не содержащая собственных аксиом, называется исчисление предикатов первого порядка.» Страница 66. После Вашего замечания возникает вопрос, а что же тогда такое исчисление предикатов первого порядка? Я думал, что это пять этих аксиом плюс два правила вывода.

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

Виктор Викторов в сообщении #466899 писал(а):

3. Почему так существенен вопрос о свободных и связанных переменных в (7)?

Ну, допустим, у нас есть функциональный символ $f$ арности 2. Тогда для того, чтобы доказать $x=y\to f(x,x) = f(x,y)$ нам нужно заменить не все свободные вхождения в формуле $f(x,x) = f(x,x)$.

То, что менять можно не все свободные переменные, а по выбору, я понимаю. Причем здесь замечание про связанные переменные – вот мой вопрос.

[Xaositect]

Виктор Викторов в сообщении #467195 писал(а):

То, что менять можно не все свободные переменные, а по выбору, я понимаю. Причем здесь замечание про связанные переменные – вот мой вопрос.

Я не вижу в цитированном замечании ничего про связанные переменные, только про свободные. В принципе и так понятно, что заменять имеет смысл только свободные переменные, и $y$ должно быть свободно для заменяемых вхождений.

Виктор Викторов в сообщении #467195 писал(а):

Но читаем дальше: «Собственные аксиомы: таковые не могут быть сформулированы в общем случае, ибо меняются от теории к теории. Теория первого порядка, не содержащая собственных аксиом, называется исчисление предикатов первого порядка.» Страница 66. После Вашего замечания возникает вопрос, а что же тогда такое исчисление предикатов первого порядка? Я думал, что это пять этих аксиом плюс два правила вывода.

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

[Виктор Викторов]

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

Виктор Викторов в сообщении #467195 писал(а):

То, что менять можно не все свободные переменные, а по выбору, я понимаю. Причем здесь замечание про связанные переменные – вот мой вопрос.

Я не вижу в цитированном замечании ничего про связанные переменные, только про свободные. В принципе и так понятно, что заменять имеет смысл только свободные переменные, и $y$ должно быть свободно для заменяемых вхождений.

Вот тот кусок: «Таким образом, в одних случаях $\mathscr A(x, y)$ может иметь свободные вхождения $x$, в других случаях таких вхождений может уже не быть.» Страница 87.

[Xaositect]

Виктор Викторов в сообщении #467202 писал(а):

Вот тот кусок: «Таким образом, в одних случаях $\mathscr A(x,y)$ может иметь свободные вхождения , в других случаях таких вхождений может уже не быть.» Страница 87.

Ну тут просто говорится, что может быть и так, что заменяются все вхождения $x$.

[Виктор Викторов]

Спасибо! "На всякого мудреца довольно простоты".

[beroal]

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

А по поводу теорем - часто в специальных теориях (6) и (7) выводятся из нелогических аксиом, но если рассматривать всю совокупность теорий с равенством, то все-таки их надо, вообще говоря, добавлять как аксиомы.

Например, из аксиомы объёмности теории ZF следует подстановочность равенства.

-- Mon Jul 11, 2011 11:47:21 --

Виктор Викторов в сообщении #467195 писал(а):

Возникает ощущение, что только эти пять аксиом и являются логическими. Таким образом, моё ощущение явно ошибочно.
Но читаем дальше: «Собственные аксиомы: таковые не могут быть сформулированы в общем случае, ибо меняются от теории к теории. Теория первого порядка, не содержащая собственных аксиом, называется исчисление предикатов первого порядка.» Страница 66. После Вашего замечания возникает вопрос, а что же тогда такое исчисление предикатов первого порядка? Я думал, что это пять этих аксиом плюс два правила вывода.

Ну, я бы сказал, что исчисление предикатов первого порядка включает аксиомы 1-5, а исчисление предикатов первого порядка с равенством включает аксиомы 1-7.

[beroal]

Виктор Викторов в сообщении #466899 писал(а):

3. Почему так существенен вопрос о свободных и связанных переменных в (7)?

Это обычное правило подстановки термов, не специфичное для логики (например, смотри лямбда-исчисление). Если нарушить его, тогда $\forall x y(x=y\to \forall y(x=\varnothing)\to \forall y(y=\varnothing))$, следовательно, все множества пустые.

[Виктор Викторов]

beroal в сообщении #467262 писал(а):

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

А по поводу теорем - часто в специальных теориях (6) и (7) выводятся из нелогических аксиом, но если рассматривать всю совокупность теорий с равенством, то все-таки их надо, вообще говоря, добавлять как аксиомы.

Например, из аксиомы объёмности теории ZF следует подстановочность равенства.

Тут Вы меня за живое задели. Я-то хочу как раз наоборот!
«Относительно того, какое место в нашей системе занимает отношение равенства, можно занять одну из следующих трех позиций.
a) Отношение равенства считается принадлежащим к лежащей в основе логике. В нашем случае в качестве лежащей в основе теории может быть, очевидно, взято функциональное исчисление первого порядка с равенством.» Абрахам Френкель, Иегоша Бар-Хиллел "Основания теории множеств". Издательство "Мир" Москва 1966. Страница 43.
Именно поэтому я и отношусь столь трепетно к исчислению предикатов первого порядка с равенством.