lection2.tex

\section{Общие замечания}

Данный текст представляет из себя краткий конспект лекций по курсу
<<Математическая логика>>, рассказанных студентам ИТМО (группы 2537-2539)
в 2013-2014 учебном году.

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

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

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

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

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

Высказывания, подробности
которых нас не интересуют, мы будем обозначать начальными буквами греческого алфавита
($\alpha$, $\beta$, $\gamma$ и т.п.).

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

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

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

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

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

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

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

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

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

\begin{tabular}{ll}
(1) & $(\phi) \rightarrow ((\psi) \rightarrow (\phi))$ \\
(2) & $((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow (\psi) \rightarrow (\pi)) \rightarrow ((\phi) \rightarrow (\pi))$ \\
(3) & $(\phi) \rightarrow (\psi) \rightarrow (\phi) \with (\psi)$\\
(4) & $(\phi) \with (\psi) \rightarrow (\phi)$\\
(5) & $(\phi) \with (\psi) \rightarrow (\psi)$\\
(6) & $(\phi) \rightarrow (\phi) \vee (\psi)$\\
(7) & $(\psi) \rightarrow (\phi) \vee (\psi)$\\
(8) & $((\phi) \rightarrow (\pi)) \rightarrow ((\psi) \rightarrow (\pi)) \rightarrow ((\phi) \vee (\psi) \rightarrow (\pi))$\\
(9) & $((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow \neg (\psi)) \rightarrow \neg (\phi)$\\
(10) & $\neg \neg (\phi) \rightarrow (\phi)$
\end{tabular}

Помимо аксиом, нам требуется каким-то образом научиться преобразовывать одни верные утверждения
в другие.
Сделаем это с помощью правил вывода. У нас пока будет одно правило вывода --- 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{\psi}{\phi & (\phi) \rightarrow (\psi)}$$