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

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

«Следствие. Если на последовательности $s$ выполнена формула $\forall x_i \mathcal{A}(x_i)$ и терм $t$ свободен для $x_i$ в $\mathcal{A}(x_i){,}$ то выполнена и формула $\mathcal{A}(t){.}$ Следовательно, формула $\forall x_i \mathcal{A}(x_i) \to \mathcal{A}(t)$ истинна в каждой интерпретации.» Страница 61.

Опять проблемы перевода «...то выполнена и формула $\mathcal{A}(t){.}$» А на какой последовательности? Должно быть: «...то на последовательности $s$ выполнена и формула $\mathcal{A}(t){.}$» Поэтому это следствие должно выглядеть так:

«Следствие. Если на последовательности $s$ выполнена формула $\forall x_i \mathcal{A}(x_i)$ и терм $t$ свободен для $x_i$ в $\mathcal{A}(x_i){,}$ то на последовательности $s$ выполнена и формула $\mathcal{A}(t){.}$ Следовательно, формула $\forall x_i \mathcal{A}(x_i) \to \mathcal{A}(t)$ истинна в каждой интерпретации.»

[Xaositect]

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

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

«... существует последовательность $s'{,}$ быть может, отличающаяся от $s$ одной лишь i-й компонентой, ...»
Да, Вы правы. Употребление "быть может" здесь корректно, но, согласитесь, что
«... существует последовательность $s'{,}$ отличающаяся от $s$ не более чем одной лишь i-й компонентой, ... »
чётче и лучше согласуется с уже использованной лексикой.

С «...то выполнена и формула $\mathcal{A}(t){.}$» согласиться не могу. Формула выполнена или не выполнена на последовательности и только на последовательности. Нет последовательности – нельзя и спрашивать выполнена формула или нет. Кроме того, последовательность упомянута в оригинале.

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

«Формула $\mathcal{A}$ называется выполнимой (в исчислении предикатов), если существует интерпретация, в которой $\mathcal{A}$ выполнима хотя бы на одной последовательности из $\sum{.}$» Страница 62.
А что такое «$\mathcal{A}$ выполнима хотя бы на одной последовательности из $\sum{.}$»? Такого определения не было. Было определение, что значит «...формула $\mathcal{A}$ выполнена на последовательности $s=(b_1,b_2,\dots)$ из $\sum$ при данной интерпретации.» Страница 58.
Смотрим оригинал: «$\mathcal{A}$ is said to be satisfiable if and only if there is an interpretation for which $\mathcal{A}$ is satisfied by at least one sequence in $\sum{.}$» Страница 56 по второму английскому изданию.
«is satisfied» как раз и есть «выполнена». Т. е. должно быть «Формула $\mathcal{A}$ называется выполнимой (в исчислении предикатов), если существует интерпретация, в которой $\mathcal{A}$ выполнена хотя бы на одной последовательности из $\sum{.}$»

-- Чт май 19, 2011 13:43:41 --

И опять о проблеме перевода: «Как мы знаем, во всякой интерпретации всякая замкнутая формула $\mathcal{A}$ или истинна или ложна, т. е. выполнима либо на каждой последовательности, либо ни на одной.» Страница 62.

А должно быть: «Как мы знаем, во всякой интерпретации всякая замкнутая формула $\mathcal{A}$ или истинна или ложна, т. е. выполнена либо на каждой последовательности, либо ни на одной.»

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

Медленное чтение – увлекательная вещь. Правда, по определению происходит оно медленно.

На страница 65 непосредственно перед введением логических аксиом теории K нам напомнили о символах, введенных ранее. Но в этом списке не оказалось квантора всеобщности $\forall{,}$ а он используется в формулировках 4ой и 5ой аксиом. Как обычно, я полез в оригинал и обнаружил, что квантор всеобщности был восстановлен в своих правах только к 4му изданию. Тут самое время посмотреть, что такое аксиома формальной аксиоматической теории: «(3) Выделено некоторое множество формул, называемых аксиомами $\mathcal{T}{.}$» Страница 36.
Какие же формулы выделены в качестве логических аксиом теории K? «Логические аксиомы: каковы бы ни были формулы $A{,}$ $B$ и $E$ теории K, следующие формулы являются логическими аксиомами теории K:
(1) $A\to (B\to A){;}$
(2) $(A\to (B\to E))\to ((A\to B)\to (A\to E)){;}$
(3) $(\neg B\to \neg A)\to ((\neg B\to A)\to B){;}$
(4) $\forall x_iA(x_i)\to A(t){,}$ где $A(x_i)$ есть формула теории K и $t$ есть терм теории K, свободный для $x_i$ в $A(x_i){.}$ Заметим, что $t$ может совпадать с $x_i{,}$ и тогда мы получаем аксиому $\forall x_iA(x_i)\to A(x_i){.}$
(5) $\forall x_i(A\to B)\to (A\to \forall x_iB){,}$ если формула $A$ не содержит свободных вхождений $x_i{.}$»

Всё это прекрасно, но хотелось бы понять почему именно эти формулы стали аксиомами. Кое-что становится ясным, если неформально переписать первые три формулы как импликации с посылками в виде конъюнций:
(1) $A\to (B\to A)$ $\Longleftrightarrow$ $(A\wedge B)\to A$
(2) $(A\to (B\to E))\to ((A\to B)\to (A\to E))$ $\Longleftrightarrow$
$[(A\to B) \wedge (A\wedge B\to E)]\to (A\to E)$ $\Longleftrightarrow$ $[A\wedge (A\to B) \wedge (A\wedge B\to E)]\to E$
(3) $(\neg B\to \neg A)\to (\neg B\to A)\to B)$ $\Longleftrightarrow$ $[(\neg B\to \neg A)\wedge (\neg B\to A)]\to B$

[Xaositect]

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

Можно их не переписывать. Надо только помнить, что эти аксиомы будут использоваться с правилом Modus Ponens.
Тогда: (1) позволяет из $A$ вывести $B\to A$ (Верное утверждение $A$ следует из любого $B$); (2) позволяет из $A\to B$ и $A\to(B\to C)$ вывести $A\to C$ (Это некоторое "поднятие" MP: если из $A$ следует $B$ и $B\to C$, то из него следует и $C$); (3) позволяет из $\neg B\to A$ и $\neg B\to \neg A$ вывести $B$ (доказательство от противного: если из отрицания $B$ следует два противоречащих друг другу утверждения, то верно $B$); (4) нужно, чтобы из общих утверждений выводить их частные случаи.

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

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

(4) нужно, чтобы из общих утверждений выводить их частные случаи.

Это понятно и приятно. Прокомментируйте, пожалуйста, правило обобщения. Из $A$ следует $\forall A{.}$

[Xaositect]

Правило обобщение соответсвует такому довольно распространенному обороту: "Пусть $x$ - некоторая штука. Тогда <доказательство> получаем $A(x)$. Т.к. $x$ было выбрано произвольно, то для любой штуки $x$ верно $A(x)$"

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

Переводческий детектив. «Как мы увидим позже, логические аксиомы выбраны таким образом, что множество логических следствий (в семантическом смысле, см. стр. 62) аксиом теории К в точности совпадает с множеством теорем теории К.» Страница 66.
А в оригинале: «As we shall see, the logical axioms are so designed that the logical consequences (in the semantic sense, cf. p. 56) of the closure of the axioms of K are precisely the theorems of K.»
В переводе исчезло слово «closure»? Да и что такое «замыкание аксиом»? Найти определение понятия «замыкание аксиом» мне не удалось. Выручили Xaositect и Мендельсон. Xaositect предположил, что «замыкание аксиом» это «Набор предложений, полученный замыканием каждой аксиомы универсальными кванторами.» Я не склонен был с ним согласиться, но обнаружил, что Мендельсон в четвертом издании заменил «closure» на «closures», что с моей точки зрения, доказывает правоту Xaositect. Итак этот кусок по-русски должен звучать: «Как мы увидим позже, логические аксиомы выбраны таким образом, что множество логических следствий (в семантическом смысле, см. стр. 62) замыканий аксиом теории К в точности совпадает с множеством теорем теории К.»
Неформальный вопрос: Зачем нужно понятие замыкания формулы? «Замыканием данной формулы назовем формулу, которая получается приписыванием к $\mathscr A$ спереди знаков кванторов всеобщности, содержащих в порядке убывания индексов все свободные переменные, входящие в $\mathscr A$. Замыканием формулы $\mathscr A$ не содержащей свободных переменных, будем называть саму формулу $\mathscr A$.» Страница 60.

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

(Оффтоп)

Я много лет не читал детективов. Теперь я изучаю некоторые математические книги как будто читаю детектив.

«... мы теперь обращаемся к рассмотрению теорий первого порядка ...» Страница 65. Что такое теории первого порядка Мендельсон не рассказывает. Он просто сообщает, чем мы при этом будем пользоваться из уже определённого, забыв при этом про кванторы, (о чем я уже писал). Дальше идет слово: «Аксиомы» и ещё через пару страниц: «теорема», «непротиворечивость» и, наконец, показался значок «$\vdash$». Никаких упоминаний об этих терминах для исчисления первого порядка нет. И тут-то и разворачивается глава из детектива. Я помню, что все эти термины определялись в исчислении высказываний. Лезу в параграф 4 главы первой. Параграф озаглавлен «Система аксиом для исчисления высказываний» страница 36 и читаю:

«Формальная (аксиоматическая) теория $\mathscr G$ считается определенной, если выполнены следующие условия:
(1) Задано некоторое счетное множество символов — символов теории $\mathscr G$. Конечные последовательности символов теории $\mathscr G$ называются выражениями теории $\mathscr G$.
(2) Имеется подмножество выражений теории $\mathscr G$, называемых формулами теории $\mathscr G$. ...
(3) Выделено некоторое множество формул, называемых аксиомами теории $\mathscr G$. ...
(4) Имеется конечное множество $R_1, \cdots, R_n$ отношений между формулами, называемых правилами вывода. Для каждого $R_i$ - существует целое положительное $j$ такое, что для каждого множества, состоящего из $j$ формул, и для каждой формулы $\mathscr A$ эффективно решается вопрос о том, находятся ли данные $j$ формул в отношении $R_i$ с формулой $\mathscr A$, и если да, то $\mathscr A$ называется непосредственным следствием данных $j$ формул по правилу $R_i$.»

И вдруг я осознаю, что от начала параграфа и до этого определения и во время этого определения никто не указал, что те из определяемых символов, которые будут буквы обязаны быть пропозициональными буквами. Итак, появились «аксиомы», дальше «теоремы», «вывод», «следствие множества формул», «свойства выводимости». Мне уже стало интересно, ведь, скоро теорема о дедукции, а она для исчисления предикатов выглядит иначе чем для исчисления высказываний. Но в самом конце следующей страницы 37 детектив прервался и громкий голос сказал: «Мы введем теперь формальную аксиоматическую теорию L для исчисления высказываний.» Интересно, если бы автор хотя бы упомянул, говоря теориях первого порядка, о том, что все определения и выводы о понятии формальной (аксиоматической) теории нужно брать в главе об исчислении высказываний, то материал усваивался бы хуже? На днях получу пятое издание посмотрим, что там делается.

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

В самом конце страницы 67 всё-таки нашлась ссылка на определение формальной теории: «Заметим, что всякая теория первого порядка является формальной теорией (см. стр. 36).»

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

Правило обобщение соответсвует такому довольно распространенному обороту: "Пусть $x$ - некоторая штука. Тогда <доказательство> получаем $A(x)$. Т.к. $x$ было выбрано произвольно, то для любой штуки $x$ верно $A(x)$"

«В силу (III) и (VI) на стр. 59—60, если правила modus ponens и обобщения применяются к истинным в данной интерпретации формулам, то результатом являются формулы, также истинные в той же интерпретации.» Страница 66.

И после этих разъяснений идет использование принципа обобщения: «Например, $\mathscr A\vdash _K\forall x_1\mathscr A$ для любой формулы $\mathscr A$, однако отнюдь не всегда $\mathscr A\vdash _K\forall x_1\mathscr A$. В самом деле, рассмотрим область, содержащую по меньшей мере два элемента $c$ и $d$. Пусть К есть некоторое исчисление предикатов, и пусть $\mathscr A$ есть $A_1^1(x_1)$. Проинтерпретируем $A_1^1$ каким-нибудь свойством, которым обладает только элемент $c$. Тогда $A_1^1(x_1)$ выполнено на всякой последовательности $s = (b_1, b_2, \cdots)$, где $b_1=c$, однако $\forall x_1A(x_1)$ не выполнено вообще ни на какой последовательности. Следовательно, формула $A(x_1)\to \forall x_1A(x_1)$ не истинна в этой интерпретации и потому не является логически общезначимой.»

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

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

«Моделью теории первого порядка К называется всякая интерпретация, в которой истинны все аксиомы теории К. В силу (III) и (VI) на стр. 59—60, если правила modus ponens и обобщения применяются к истинным в данной интерпретации формулам, то результатом являются формулы, также истинные в той же интерпретации. Следовательно, и всякая теорема теории К истинна во всякой ее модели.» Страница 66.

Если нас интересуют только модели теории К, то у нас нет трудностей в применении правила обобщения. Но... зачем оно нам при этом вообще нужно? Ведь если $\mathscr A$ истинна в данной интерпретации, то и $\mathscr A\to \forall x_1\mathscr A$ истинна в той же интерпретации. И по modus ponens $\forall x_i\mathscr A$ истинна и без правила обобщения. С другой стороны, пример $\mathscr A\vdash _K\forall x_1\mathscr A$ рассмотрен не на модели и как раз такое применение правила обобщения мне непонятно. Что же касается modus ponens, то в интерпретации, где $\mathscr A$ выполнена на одних последовательностях и не выполнена на других, формула $\mathscr A\to \forall x_1\mathscr A$ также выполнена на одних последовательностях и не выполнена на других. Интересно заметить, что тогда формула $\forall x_i\mathscr A$ ложна.

[epros]

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

...в интерпретации, где $\mathscr A$ выполнена на одних последовательностях и не выполнена на других, формула $\mathscr A\to \forall x_1\mathscr A$ также выполнена на одних последовательностях и не выполнена на других. Интересно заметить, что тогда формула $\forall x_i\mathscr A$ ложна.

В связи с этим вспомнилось понятие $\omega$-противоречивой теории. Это такая теория, в которой некоторое свойство $\varphi(n)$ можно отдельно доказать для каждого натурального $n$, однако утверждение $\forall n ~ \varphi(n)$ в этой теории опровержимо. Может быть как раз правило обобщения помешает построить модель такой теории?

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

Сравнивая правила modus ponens и обобщения, я вполне освоился с правилом обобщения. В конце концов, modus ponens работает в модели и правило обобщения работает в модели. Если же интерпретация не является моделью, заключение и по modus ponens и по правилу обобщения может быть ложным.

Ещё один переводческий ляп. Так как тег не позволяет использовать кириллицу, то букву «Г» я везде заменяю на «G». На странице 70 несколько раз говорится о выводе $\mathscr B$ из $\left\{G, \mathscr A}\right\}$ т. е. речь идет о выводе $\mathscr B$ из двух формул $G$ и $\mathscr A$. Но на самом деле $\mathscr A$ -- формула, а $G$ -- множество формул. И, конечно, писать надо без скобок «вывод $\mathscr B$ из $G, \mathscr A$» или $G, \mathscr A \vdash\mathscr B$, как и сделано в оригинале.

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

Ещё один вопрос. «Формула $\mathscr A$ называется логически общезначимой (в исчислении предикатов), если она истинна в каждой интерпретации.» Страница 62. Если какой-нибудь универсум, из которого мы черпаем область интерпретации? Запахло множеством всех множеств, но сваливаться в эту бездну у меня сейчас желания нет. Я догадываюсь, что есть договоренность на сей счет, но Мендельсон о ней не пишет.