lection2.tex

\section{Исчисление высказываний}

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

Мы начнём с очень простого предметного языка --- языка исчисления высказываний.
Элементами (строками) данного языка являются некоторые выражения (формулы), по структуре
очень похожие на арифметические, которые называются \emph{высказываниями}.

Каждое высказывание --- это либо \emph{пропозициональная переменная} --- 
большая буква латинского алфавита, возможно, с цифровым индексом, либо 
оно составлено из одного или двух высказываний меньшего размера, соединённых логической связкой.

Связок в языке мы определим 4 (хотя при необходимости этот список может быть
в любой момент изменен).
\begin{itemize}
\item отрицание: если $\alpha$ --- высказывание, то $\neg\alpha$ --- тоже высказывание.
\item конъюнкция: если $\alpha$ и $\beta$ --- высказывания, то $\alpha \& \beta$ --- тоже высказывание.
\item дизъюнкция: если $\alpha$ и $\beta$ --- высказывания, то $\alpha \vee \beta$ --- тоже высказывание.
\item импликация: если $\alpha$ и $\beta$ --- высказывания, то $\alpha \rightarrow \beta$ --- тоже высказывание.
\end{itemize}

Также в языке можно использовать скобки вокруг выражений:
если $\alpha$ --- высказывание, то $(\alpha)$ --- тоже высказывание.
Если из расстановки скобок не следует иное, мы будем учитывать приоритет связок
(связки в перечислении выше указаны в порядке убывания приоритета).
Также, конъюнкцию и дизъюнкцию мы будем считать левоассоциативной (скобки в цепочке
одинаковых связок расставляются слева направо: $(A \vee B) \vee C$), 
а импликацию --- правоассоциативной: $A \rightarrow (B \rightarrow C)$). 

Высказывания, подробности
которых нас не интересуют, мы будем обозначать начальными буквами 
греческого алфавита
($\alpha$, $\beta$, $\gamma$ и т.п.). 
Ещё мы будем называть такие
высказывания \emph{метапеременными}.
Одинаковым буквам всегда соответствуют
одинаковые высказывания, однако разным буквам не обязаны соответствовать
разные высказывания. 
При подстановке выражений вместо метапеременных мы всегда предполагаем,
что эти выражения взяты в скобки.

Покажем эти правила на примере. Выражение
$$\alpha \rightarrow \neg \beta \& \gamma \vee \delta \vee \epsilon \rightarrow \zeta\vee\iota$$
нужно воспринимать так:
$$(\alpha) \rightarrow \left(((((\neg (\beta)) \& (\gamma)) \vee (\delta)) \vee (\epsilon)) \rightarrow ((\zeta)\vee(\iota))\right)$$

\subsection{Оценка высказываний}

Процесс <<вычисления>> значения высказываний имеет совершенно
естественное определение. Мы фиксируем некоторое множество
\emph{истинностных значений} $V$, для начала мы в качестве такого множества возьмем 
множество $\{\texttt{И}, \texttt{Л}\}$, здесь \texttt{И} означает истину, а
\texttt{Л} --- ложь. Всем пропозициональным переменным мы приписываем некоторое
значение, а затем рекурсивно вычисляем значение выражения естественным для указанных
связок образом.

Пусть $P$ --- множество пропозициональных переменных языка.
Тогда функцию $M: P \rightarrow V$, приписывающую истинностное 
значение пропозициональным переменным, мы назовём \emph{моделью} 
(иначе: \emph{интерпретацией} или \emph{оценкой} переменных). 

Функцию, сопоставляющую высказыванию $\alpha$ и модели $M$
истинностное значение, мы назовём \emph{оценкой} высказывания и
будем это записывать так: $\llbracket \alpha \rrbracket ^ M$.
Обычно для указания модели $M$ мы будем перечислять значения
пропозициональных переменных, входящих в формулу:
$\llbracket P \rightarrow Q \rrbracket ^ {P:=\texttt{Л}, Q:=\texttt{И}} = \texttt{И}$.
Если конкретная модель ясна из контекста или несущественна для изложения,
мы можем указание на модель опустить: $\llbracket P \rightarrow P \rrbracket = \texttt{И}$.

Если $\llbracket \alpha \rrbracket ^ M = \texttt{И}$, то мы будем 
говорить, что высказывание $\alpha$ истинно в модели $M$, или, иными словами,
\emph{$M$ --- модель высказывания $\alpha$}.

\emph{Тавтологией} или 
\emph{общезначимым высказыванием} мы назовём высказывание, истинное в любой модели.
На языке исследователя общезначимость высказывания $\alpha$ можно кратко 
записать как $\models \alpha$. 

Указанный способ оценки высказываний мы будем называть классическим.
В дальнейшем мы будем брать необычные множества истинностных значений и будем давать
неожиданный смысл связкам, однако, классический способ будет всегда подразумеваться, 
если не указано иного. Если же мы захотим сделать на этом акцент, мы будем говорить
о \emph{классических моделях исчисления высказываний}, подразумевая, что
если мы приписываем переменным классические значения истина и ложь, 
то и высказывание целиком мы оцениваем тоже по классическим правилам.

\subsection{Доказательства}

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

Для решения вопроса мы введём понятие \emph{схемы аксиом} --- некоторого обобщённого
шаблона, подставляя значения в который, мы получаем различные, но схожие аксиомы. 
Например, схема аксиом $\alpha \& \beta \rightarrow \alpha$ позволяет получить как
аксиому $A \& B \rightarrow A$ (при подстановке $\alpha := A, \beta := B$), так и
аксиому $B \& A \rightarrow B$.

Возьмем следующие схемы аксиом для исчисления высказываний:

\begin{tabular}{ll}
(1) & $\alpha \rightarrow \beta \rightarrow \alpha$ \\
(2) & $(\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow \gamma)$ \\
(3) & $\alpha \rightarrow \beta \rightarrow \alpha \& \beta$\\
(4) & $\alpha \& \beta \rightarrow \alpha$\\
(5) & $\alpha \& \beta \rightarrow \beta$\\
(6) & $\alpha \rightarrow \alpha \vee \beta$\\
(7) & $\beta \rightarrow \alpha \vee \beta$\\
(8) & $(\alpha \rightarrow \gamma) \rightarrow (\beta \rightarrow \gamma) \rightarrow (\alpha \vee \beta \rightarrow \gamma)$\\
(9) & $(\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \neg \beta) \rightarrow \neg \alpha$\\
(10) & $\neg \neg \alpha \rightarrow \alpha$
\end{tabular}

Напомним, что импликация --- правоассоциативная операция, поэтому
скобки в схеме аксиом 1, например, расставляются так:
$(\alpha) \rightarrow ((\beta) \rightarrow (\alpha))$

Помимо аксиом, нам требуется каким-то образом научиться преобразовывать одни верные утверждения
в другие.
Сделаем это с помощью правил вывода. У нас пока будет одно правило вывода --- Modus Ponens.
Это также схема, она позволяет при доказанности двух формул $\psi$ и $\psi \rightarrow \phi$
считать доказанной формулу $\phi$.

\begin{definition} \emph{Доказательство} в исчислении высказываний --- 
это некоторая конечная последовательность выражений 
$\alpha_1$, $\alpha_2$ \dots $\alpha_n$
из языка $L$ такая, что каждое из утверждений $\alpha_i (1 \le i \le n)$
либо является аксиомой, либо получается из других
утверждений $\alpha_{P_1}$, $\alpha_{P_2}$ \dots $\alpha_{P_k}$ 
($P_1 \dots P_k < i$) по правилу вывода.
\end{definition}

\begin{definition} Высказывание $\alpha$ называется доказуемым, если 
существует доказательство $\alpha_1$, $\alpha_2$ \dots $\alpha_k$, и в нем
$\alpha_k$ совпадает с $\alpha$. 
\end{definition}

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

В качестве сокращения записи в языке исследователя мы будем писать $\vdash \alpha$,
чтобы сказать, что $\alpha$ доказуемо.

Традиционно правило вывода Modus Ponens записывают так:
$$\infer{\beta}{\alpha & \alpha \rightarrow \beta}$$