Формулы

[Z1X]

Цитата:

Заглавные латинские буквы $A, B$ и другие, которые употребляются в определении формулы, принадлежат не языку логики высказываний, а его метаязыку, то есть языку, который используется для описания самого языка логики высказываний. Содержащие метабуквы выражения $\neg A$, $(A\to B)$ и другие — не пропозициональные формулы, а схемы формул. Например, выражение $(A\wedge B)$ есть схема, под которую подходят формулы $(p\wedge q), (p\wedge (r\vee s))$ и другие.

Совершенно не понимаю, зачем проводить такие различия и плодить бесконечное множество аксиом. Проще в индуктивное определение формулы добавить, что подстановка одной формулы в другую дает формулу. Какие могут быть проблемы?

Теперь пусть в предикатной логике я хочу сказать, что в $\varphi$ есть вхождение переменной $x$. По-моему, это можно просто обозначить как $\varphi (x)$. А вот если требуется наоборот показать, что вхождений нет, то как это обозначить символьно?

[arseniiv]

Z1X в сообщении #1234037 писал(а):

Проще в индуктивное определение формулы добавить, что подстановка одной формулы в другую дает формулу.

И получится не очень индуктивное определение. В любом случае просто доказать, что $\varphi[\psi/x]$ для формул $\varphi,\psi$ и переменной $x$ — формула, но нам-то надо другое: чтобы подстановка в аксиому давала аксиому. Это не связано с определением формулы.

Z1X в сообщении #1234037 писал(а):

Совершенно не понимаю, зачем проводить такие различия и плодить бесконечное множество аксиом.

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

Z1X в сообщении #1234037 писал(а):

А вот если требуется наоборот показать, что вхождений нет, то как это обозначить символьно?

Можно попробовать $\varphi(\hat x)$ — я видел несколько контекстов, где это обозначает, что $x$ пропускается, когда без крышки входил бы. В любом случае понадобится пояснение, даже для $\varphi(x)$. К тому же, бывает всё-таки проще писать явно $x\in\mathrm{FV}(\varphi), x\notin\mathrm{FV}(\varphi)$.

[Z1X]

arseniiv в сообщении #1234156 писал(а):

нам-то надо другое: чтобы подстановка в аксиому давала аксиому

Ну, считаем, что подстановка в аксиому или теорему всегда дает теорему, а правило подстановки — одно из правил вывода. Годится?

arseniiv в сообщении #1234156 писал(а):

$x\in\mathrm{FV}(\varphi), x\notin\mathrm{FV}(\varphi)$

Что обозначено через $\mathrm{FV}$ ? Множество всех символов, используемых в формуле?

[arseniiv]

Z1X в сообщении #1234222 писал(а):

Ну, считаем, что подстановка в аксиому или теорему всегда дает теорему, а правило подстановки — одно из правил вывода. Годится?

Ну, как и с любым правилом вывода, надо сначала доказать, что если все посылки ($\varphi$) тождественно истинны, таково и заключение ($\varphi[\psi/x]$, хотя для полноты можно предложить рассмотреть одновременные подстановки сразу вместо нескольких переменных — то, что они сводятся к повторным, не совсем уж и тривиально). Потом пожалуйста.

Z1X в сообщении #1234222 писал(а):

Что обозначено через $\mathrm{FV}$ ? Множество всех символов, используемых в формуле?

Множество свободных переменных в формуле. В пропозициональном языке, конечно, они все свободные, но это ведь лишь пока, а понятие используется много где и почти везде обозначается так (этимология — free variables).

-- Пн июл 17, 2017 23:44:19 --

В любом случае, от метапеременных никуда не деться при рассмотрении интересных теорий первого порядка, где обычно хотя бы одна схема с пропозициональной метапеременной есть. Можно не говорить «метапеременная», но человеческое описание всей схемы конечным набором символов всё равно будет включать её.

[Z1X]

arseniiv в сообщении #1234235 писал(а):

надо сначала доказать, что если все посылки ($\varphi$) тождественно истинны, таково и заключение

Почему сначала? Сначала мы все определяем, затем разбираемся в истинности.

Предположим, что формулы $\varphi$ и $\psi$ общезначимы. Тогда $\varphi[\psi/x] \leftrightarrow \varphi[1/x] \leftrightarrow \varphi[x/x]$. Это и есть нужное доказательство?

arseniiv в сообщении #1234235 писал(а):

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

В схемах обычно бывает то самое $\varphi (x)$ или $\varphi (x,y)$. Здесь просто надо пояснить, что подстановка вместо пропозициональной переменной ограничена лишь теми высказывательными формами, которые содержат свободно $x$ или $x,y$ соответственно. Где и зачем тут метапеременные?

[arseniiv]

Z1X в сообщении #1234245 писал(а):

Почему сначала? Сначала мы все определяем, затем разбираемся в истинности.

Ну, главное не до того, как мы объявим, что всё выводимое тождественно истинно.

Z1X в сообщении #1234245 писал(а):

Предположим, что формулы $\varphi$ и $\psi$ общезначимы. Тогда $\varphi[\psi/x] \leftrightarrow \varphi[1/x] \leftrightarrow \varphi[x/x]$. Это и есть нужное доказательство?

Нет, конечно. Это вообще некорректная запись. Тут всё механически по определениям можно доказать.

Z1X в сообщении #1234245 писал(а):

В схемах обычно бывает то самое $\varphi (x)$ или $\varphi (x,y)$. Здесь просто надо пояснить, что подстановка вместо пропозициональной переменной ограничена лишь теми высказывательными формами, которые содержат свободно $x$ или $x,y$ соответственно. Где и зачем тут метапеременные?

Вот это самое $\varphi(x, y)$ и будет метапеременной. Но вообще я вам навязывать видеть или явно использовать где-то метапеременные не собираюсь.

[Z1X]

arseniiv в сообщении #1234268 писал(а):

Тут всё механически по определениям можно доказать.

Я пока не осознал, как доказать. Подставляемая формула может иметь то или иное истинностное значение. Тавтология всегда истинна. Подстановка в тавтологию формулы эквивалентна подстановке ее истинностного значения. Вроде ж верно все?

-- 17.07.2017, 19:37 --

arseniiv в сообщении #1234268 писал(а):

Вот это самое $\varphi(x, y)$ и будет метапеременной. Но вообще я вам навязывать видеть или явно использовать где-то метапеременные не собираюсь.

Вопрос в другом: можно ли без них обойтись? Вот у нас есть схема $A \rightarrow (B \rightarrow A)$. Почему мы сразу по умолчанию должны считать, что подстановка метаформул вместо метапеременных в схему сохраняет истинность схемы?

[arseniiv]

Не должны, конечно. Вопрос с подстановкой что тут, что там одинаковый.

Z1X в сообщении #1234272 писал(а):

Подстановка в тавтологию формулы эквивалентна подстановке ее истинностного значения. Вроде ж верно все?

Надо аккуратнее, потому что значение формулы — это функция значений параметров, и просто так подставлять истинностное значение в формулу нельзя (определение мешает). Пусть $\mathbb B$ — множество лог. значений, $V$ — переменных, $I(\varphi)\colon\mathbb B^V\to\mathbb B$ — значение формулы $\varphi$. Достаточно показать, что $I(\varphi[\psi/x]) = I(\varphi)\circ(a\mapsto v\mapsto\textsf{if } v=x \textsf{ then } I(\psi)(a) \textsf{ else } a(v))$. Тогда если $I(\varphi)$ константа, она и останется константой, что бы там к ней справа не прикомпозировали. А доказывается по индукции.

[Z1X]

Я читаю "Языки и исчисления" Верещагина, Шеня, с. 42, Лемма 1., доказательство ч.1:
$(D \rightarrow ((D \rightarrow D) \rightarrow D)) \rightarrow ((D \rightarrow (D \rightarrow D)) \rightarrow (D \rightarrow D))$ получается из аксиомы $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ при $A=D, B=(D \rightarrow D), C=D$
Верещагин и Шень видимо по умолчанию считают, что такая подстановка в схему даст истинную схему.

Короче, я не вижу во всех этих метаобозначениях решения проблемы. Проблема просто переносится на уровень метатеории. Так для чего это делать, если на новом уровне ее все равно придется решать? Не лучше ли все побрить бритвой Оккама и вернуться, собственно, на уровень исчисления?

arseniiv в сообщении #1234280 писал(а):

Достаточно показать, что $I(\varphi[\psi/x]) = I(\varphi)\circ(a\mapsto v\mapsto\textsf{if } v=x \textsf{ then } I(\psi)(a) \textsf{ else } a(v))$. Тогда если $I(\varphi)$ константа, она и останется константой, что бы там к ней справа не прикомпозировали. А доказывается по индукции.

Сначала мне предстоит понять, что там такое справа прикомпозировано. Как правильно читается выражение $(a\mapsto v\mapsto\textsf{if } v=x \textsf{ then } I(\psi)(a) \textsf{ else } a(v))$ ?

[Portnov]

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

[arseniiv]

Z1X в сообщении #1234289 писал(а):

Верещагин и Шень видимо по умолчанию считают, что такая подстановка в схему даст истинную схему.

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

Z1X в сообщении #1234289 писал(а):

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

Не придётся, если она неформальная.

Z1X в сообщении #1234289 писал(а):

Сначала мне предстоит понять, что там такое справа прикомпозировано. Как правильно читается выражение $(a\mapsto v\mapsto\textsf{if } v=x \textsf{ then } I(\psi)(a) \textsf{ else } a(v))$ ?

В общем, это функция, которая оценке $a\colon V\to\mathbb B$ ставит в соответствие оценку, которая не отличается от неё на всех переменных кроме $x$, а на $x$ равна $I(\psi)(a)$ — то, что мы и ожидаем от «подстановки» логического значения вместо $x$, только действует эта «подстановка» не на формуле $\varphi$, а на оценке переменных, с которой мы будем вычислять значение формулы.