Некоторые логические теоремы

[arseniiv]

Хочу, чтобы проверили меня, нельзя ли укоротить что-нибудь или упростить.

Теорема о правиле Modus Ponens. Пусть $\mathfrak A$ и $\mathfrak A \rightarrow \mathfrak B$ обе тавтологии. Тогда и $\mathfrak B$ — тавтология.
$\square$ Допустим, $\mathfrak B$ опровержима. Тогда есть набор значений переменных, при которых она принимает значение $F$. Тогда на этом наборе значение $\mathfrak A \rightarrow \mathfrak B$ ($T \rightarrow F$) тоже $F$, что невозможно в силу того, что $\mathfrak A \rightarrow \mathfrak B$ тавтология и ни на каком наборе значений переменных значения $F$ не принимает. Значит, $\mathfrak B$ всё-таки тавтология. $\blacksquare$

Более длинную теорему лень переписывать всю (точнее, её длинное доказательство), спрошу только в деталях. Пусть $\mathfrak A$ — правильно построенная формула [ранее её индуктивное определение], не являющаяся пропозиц. переменной. Тогда эта формула может иметь один из видов $\neg \mathfrak B$, $\mathfrak B \wedge \mathfrac C$, $\mathfrak B \vee \mathfrak C$, $\mathfrak B \rightarrow \mathfrak C$, где $\mathfrak B$, $\mathfrak C$ — п. п. ф.. Правильно я понимаю, что надо доказать именно то, что подформулы $\mathfrak B$ и $\mathfrak C$ — правильно построенные? А то мне эта теорема кажется естественным продолжением индуктивного определения, не понял, что от меня требуется. Могу привести и определение, вдруг они различаются в деталях. (Просто пока лень.)

А ещё, какие есть обозначения для замены $\mathfrak B$ в $\mathfrak A$ на $\mathfrak C$ и подстановки $\mathfrak C$ вместо $P$ в $\mathfrak A$? У нас они какие-то неудобоваримые. (Странно, как вообще такие выбирают для использования.)

[mkot]

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

Хочу, чтобы проверили меня, нельзя ли укоротить что-нибудь или упростить.

Теорема о правиле Modus Ponens. Пусть $\mathfrak A$ и $\mathfrak A \rightarrow \mathfrak B$ обе тавтологии. Тогда и $\mathfrak B$ — тавтология.
$\square$ Допустим, $\mathfrak B$ опровержима. Тогда есть набор значений переменных, при которых она принимает значение $F$. Тогда на этом наборе значение $\mathfrak A \rightarrow \mathfrak B$ ($T \rightarrow F$) тоже $F$, что невозможно в силу того, что $\mathfrak A \rightarrow \mathfrak B$ тавтология и ни на каком наборе значений переменных значения $F$ не принимает. Значит, $\mathfrak B$ всё-таки тавтология. $\blacksquare$

Здесь всё сильно просто и в любом случае сводится к определению импликации.

Цитата:

Более длинную теорему лень переписывать всю (точнее, её длинное доказательство), спрошу только в деталях. Пусть $\mathfrak A$ — правильно построенная формула [ранее её индуктивное определение], не являющаяся пропозиц. переменной. Тогда эта формула может иметь один из видов $\neg \mathfrak B$, $\mathfrak B \wedge \mathfrac C$, $\mathfrak B \vee \mathfrak C$, $\mathfrak B \rightarrow \mathfrak C$, где $\mathfrak B$, $\mathfrak C$ — п. п. ф.. Правильно я понимаю, что надо доказать именно то, что подформулы $\mathfrak B$ и $\mathfrak C$ — правильно построенные? А то мне эта теорема кажется естественным продолжением индуктивного определения, не понял, что от меня требуется. Могу привести и определение, вдруг они различаются в деталях. (Просто пока лень.)

Формально говоря, вы формулирируете её неверно, возможно из-за этого и проблемы. Скобки. Скобки! Именно они гарантируют однозначность разбора.
То есть не $A \vee B$, $A \wedge B$, $A \to B$, а $(A \vee B)$, ($A \wedge B$), $(A \to B$). Иначе же если вы скобки опустите в определении, то
например при построении у вас получилась формула $A \vee B \wedge C$, что это? $((A \vee B) \wedge C)$ или $(A \vee (B \wedge C))$. Конечно в жизни вводят приоритет операций (и ещё используя ассоциативность) и большинство скобок не пишут.

Цитата:

А ещё, какие есть обозначения для замены $\mathfrak B$ в $\mathfrak A$ на $\mathfrak C$ и подстановки $\mathfrak C$ вместо $P$ в $\mathfrak A$? У нас они какие-то неудобоваримые. (Странно, как вообще такие выбирают для использования.)

А и общепринятого-то нет. Какое у вас? $A(x)[C // x]$? $A(B/x)$? или ещё что-то?

[arseniiv]

mkot в сообщении #357866 писал(а):

Скобки! Именно они гарантируют однозначность разбора.

Да, я забыл про них, когда печатал, но так они есть, я понимаю, что пока эквивалентные формулы не введены, $((A \vee B) \vee C)$ имеет мало общего с $(A \vee (B \vee C))$. А уж когда вводится приоритет и учитывается ассоциативность, можно опускать многие скобки.

mkot в сообщении #357866 писал(а):

Конечно в жизни вводят приоритет операций (и ещё используя ассоциативность) и большинство скобок не пишут.

А, ну вот, да-да. Сначала не дочитал.

mkot в сообщении #357866 писал(а):

А и общепринятого-то нет. Какое у вас? $A(x)[C // x]$? $A(B/x)$? или ещё что-то?

Такому бы рад, его запомнить легче, оно "неоднородно" (и используется в одной настольной книге). У нас (по-моему, ужасные) $R\begin{smallmatrix} a \\ b \\ c \end{smallmatrix}$ и $S\begin{smallmatrix} a \\ b \\ c \end{smallmatrix}$, даже не помню, что где там стоит (ведь это важно, а такая "однородная" запись всё портит).

[mkot]

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

mkot в сообщении #357866 писал(а):

Скобки! Именно они гарантируют однозначность разбора.

Да, я забыл про них, когда печатал, но так они есть, я понимаю, что пока эквивалентные формулы не введены, $((A \vee B) \vee C)$ имеет мало общего с $(A \vee (B \vee C))$.

Ещё кстати, слов о том что эти части восстанавливаются однозначно не хватает. А так, да, теорема несложная и очевидная, и описывает как вы, например, компьютеру объясните что у вас за формула.

Цитата:

У нас (по-моему, ужасные) $R\begin{smallmatrix} a \\ b \\ c \end{smallmatrix}$ и $S\begin{smallmatrix} a \\ b \\ c \end{smallmatrix}$, даже не помню, что где там стоит (ведь это важно, а такая "однородная" запись всё портит).

Эх, даже не знаю, можно что угодно понаписать $A(x)[x \leftarrow B], A\big(\begin{smallmatrix}B \\ x\end{smallmatrix}\big), \ldots$ тут ничё стандартного нет.

А ещё, почему вы формулы готическими буквами обозначаете? Это ж неудобно.

[arseniiv]

Да, действительно, всё время \mathfrak, \mathfrak, \mathfrak писать неудобно… Тогда как я буду обозначать переменные (и значения)? Могу здесь обозначать их маленькими буквами, сойдёт? (Думал, вдруг кто-нибудь не поймёт.)

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

[mkot]

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

Правильно понимаю, что можно понимать эту теорему как способ выделения "верхней" связки в формулах (записанных без вольностей)?

Ага, верхней связки и её аргуметнов (всё однозначно выделяется!); например, у Верещагина и Шеня эта теорема так и называется об однозначности разбора. Кстати, эту книгу (Языки и исчисления) очень рекомендую.

(Оффтоп)

Я по-моему на этом форуме только тем и занимаюсь, что в половине ответов рекомендую Линейную алгебру Мальцева, а в другой половине Языки и исчисления Верещанина и Шеня.

[arseniiv]

mkot в сообщении #358045 писал(а):

Ага, верхней связки и её аргуметнов (всё однозначно выделяется!)

Ура! Теперь всё ясно на 100%. Как-нибудь, может, ещё теоремы попрошу поразбирать в этой теме.

mkot в сообщении #358045 писал(а):

стати, эту книгу (Языки и исчисления) очень рекомендую.

Посмотрю!

[Профессор Снэйп]

Масло масляное...

Как выражался наш преподаватель философии, утверждение "снег является белым" истинно, если снег является белым.

[arseniiv]