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

[Xaositect]

epros в сообщении #463007 писал(а):

Ой, а напомните пожалуйста: Что именно является "истинным в классе всех возможных интерпретаций" (т.е. "логически общезначимым")? Вопрос в том, что предложение в языке исчисления предикатов можно сформулировать только тогда, когда определён хотя бы один функциональный символ и хотя бы один - предикатный. Т.е. мы должны считать, что определено столько функциональных и предикатных символов, а также переменных, сколько нам нужно (хотя прикладных аксиом в системе нет)?

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

[epros]

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

В Вашем же комментарии нужны ещё и собственные аксиомы.

Нет, я как раз говорил о формальной системе без прикладных аксиом.

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

Если нет формул, то все формулы истинны на всех интерпретациях и, соответственно, общезначимы. Вырожденный случай.

Почему-то мне кажется, что тот, кто давал определение, вовсе не этот случай имел в виду.

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

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

Это всё понятно, но вопрос был с дальним прицелом, чуть позже я поясню... Я прекрасно вижу, что формула:
$\forall x,y,z ~ (x+y=z \to y+x=z)$
не является общезначимой, поскольку может быть такая интерпретация операции сложения, согласно которой оно не является коммутативным. Нашли интерпретацию, в которой формула ложна, - значит она не общезначима, всё понятно.

Вопрос в том, как мы можем понять, что формула общезначима, если она такова. Например, формула
$\forall x,y,z ~ (x+y=z \to x+y=z)$
судя по всему является общезначимой, поскольку это утверждение не опирается ни на какие свойства операции сложения и ни на какие свойства отношения равенства. Т.е. именно "её истинность не зависит от смысла входящих в неё предикатных и функциональных символов". Но это что, чисто интуитивный вывод? Как это доказать? Если буквально следовать определению, то мы должны проверить все возможные интерпретации. Не могу себе представить, чтобы это было возможно.

Теперь про "дальный прицел". Известно, что для логики второго порядка нет аналога теоремы полноты. Т.е. среди формул второго порядка имеются логически общезначимые, но невыводимые. Поэтому очень любопытно было бы:
1) Найти пример такой формулы.
2) Доказать, что она - логически общезначима (хотя бы понять, как это делается).
3) Доказать, что она невыводима в исчислении предикатов второго порядка (без прикладных аксиом).

[Xaositect]

epros в сообщении #463299 писал(а):

Если буквально следовать определению, то мы должны проверить все возможные интерпретации. Не могу себе представить, чтобы это было возможно.

Ну как же. Пусть $I$ - некоторая интерпретация с областью $D$, оценкой $eq\subset D^2$ предиката $=$ и оценкой $add\colon D^2\to D$ функтора $+$. Формула истинна в интерпретации тогда и только тогда, когда для любых $X, Y, Z\in D$ истинностное значение $eq(add(X, Y), Z)$ меньше или равно истинностному значению $eq(add(X, Y), Z)$, что, очевидно, верно.

[epros]

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

что, очевидно, верно

Любопытное рассуждение. Вам это "очевидно" потому, что это соответствует Вашему интуитивному представлению о множествах (в частности, о том, что такое "оценка предиката" и "оценка функтора")? А если у кого-то другая интуиция, например, если в его интуиции отсутствует аксиома экстенсиональности? Я ведь могу себе вообразить интерпретацию понятия "множества", в которой разные множества могут состоять из одних и тех же элементов?

Я это к тому, что все эти "семантические" представления о полноте, которые привлекают понятие интерпретации, неявным образом опираются на какую-то достаточно сильную теоретико-множественную аксиоматику. Причём самое печальное то, что нам никто не сказал, на какую именно...

[Xaositect]

epros в сообщении #463394 писал(а):

Я это к тому, что все эти "семантические" представления о полноте, которые привлекают понятие интерпретации, неявным образом опираются на какую-то достаточно сильную теоретико-множественную аксиоматику. Причём самое печальное то, что нам никто не сказал, на какую именно...

Разумеется. Для работы с интерпретациями нам нужна теория множеств в метатеории. В данном конкретном случае, правда, от нее не так много требуется.

[epros]

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

В данном конкретном случае, правда, от нее не так много требуется.

Угу, потому-что случай достаточно простой. А если рассмотреть пример недоказуемой общезначимой формулы второго порядка? Любопытно, что нам потребуется в метатеории?

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

epros в сообщении #463299 писал(а):

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

В Вашем же комментарии нужны ещё и собственные аксиомы.

Нет, я как раз говорил о формальной системе без прикладных аксиом.

«Аксиомы теории К разбиваются на два класса: логические аксиомы и собственные (или нелогические) аксиомы.» Страница 65.

epros в сообщении #463118 писал(а):

Значит, мы можем смело считать "логически общезначимыми", например, такие вещи, как: $\forall x,y,z ~ (x+y=z \to x+y=z)$

А что с утра сложение перевели в логические аксиомы?

[epros]

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

А что с утра сложение перевели в логические аксиомы?

Где Вы тут видите какие-то аксиомы? Это просто функциональный символ. Вместо него можно было написать $\times$ или $\circ$, или $\bullet$, или что угодно ещё.

[Xaositect]

По поводу логики второго порядка - в ней можно выразить понятия конечной бинарной строки и алгоритма(МТ). При этом доказать все утверждения вида "Машина $M$ на строке $x$ зацикливается" не получится, так как множество таких утверждений неперечислимо.

[epros]

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

По поводу логики второго порядка - в ней можно выразить понятия конечной бинарной строки и алгоритма(МТ). При этом доказать все утверждения вида "Машина $M$ на строке $x$ зацикливается" не получится, так как множество таких утверждений неперечислимо.

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

Может Вы хотели сказать, что нет общего алгоритма доказательства?

[epros]

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

По поводу логики второго порядка ..

Любопытен ответ, который дал автор статьи английской википедии про логику второго порядка, на мой вопрос: "Есть ли пример недоказуемого общезначимого утверждения второго порядка?"

Он сходу сформулировал такое утверждение: "Если X - несчётное множество, на котором определена аксиоматика непрерывного упорядоченного поля, то для любого несчётного множества Y существует сюръекция его в X". Далее он заявил, что если верна гипотеза континуума, то данное утверждение - общезначимо (но недоказуемо). А если гипотеза континуума неверна, то общезначимо отрицание данного утверждения.

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

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

(Оффтоп)

«Поиски прошлого».

Опять возвращаюсь к началу второй главы. Страница 53. «Если $P(x)$ означает, что $x$ обладает свойством $P$, то договоримся посредством $\forall xP(x)$ обозначать утверждение: «для всякого предмета $x$ свойство $P$ выполнено»,...» Итак, мы договорились об обозначении. И чуть ниже: «В выражении $\forall xP(x)$ часть $\forall x$ называется квантором всеобщности, ...» и вдруг: «Изучение кванторов как логических операций и связанных с ними понятий и составляет основной предмет этой главы...» Что такое логическая операция? Эта комбинация слов употребляется впервые в этой книге. Но чтобы из себя эта самая логическая операция не представляла, пока $\forall x$ только лишь обозначение. Но посмотрим в оригинале: «The study of quantifiers and related concepts is the principal subject of this chapter; ...» Т. е. «Изучение кванторов [] и связанных с ними понятий составляет основной предмет этой главы...» и никаких «логических операций».

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

Ещё один «кванторный» сюжет. Квантор всеобщности на интерпретации с конечной областью – конъюнкция различных значений одной и той же формулы. Квантор всеобщности – обобщение конъюнкции на бесконечную область и также на пустое множество и множество из одного элемента . (Смотрите книгу «Введение в современную математику» Юрия Шихановича страница 148). Иногда полезно для понимания взять конечную область интерпретации и заменить квантор всеобщности на конъюнкцию.

[beroal]

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

Квантор всеобщности на интерпретации с конечной областью – конъюнкция различных значений одной и той же формулы. Квантор всеобщности – обобщение конъюнкции на бесконечную область и также на пустое множество и множество из одного элемента.

$\varnothing$ и синглетоны являются конечными множествами. Я бы сначала обобщил конъюнкцию на конечные множества, затем на бесконечные.

-- Wed Jul 06, 2011 20:46:46 --

И не забываем, что $\exists$ есть обобщение дизъюнкции.

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

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

$\varnothing$ и синглетоны являются конечными множествами. Я бы сначала обобщил конъюнкцию на конечные множества, затем на бесконечные.

Дело вкуса.

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

И не забываем, что $\exists$ есть обобщение дизъюнкции.

Вы правы, но мне было лень это делать. Поэтому по аналогии.