\documentclass[12pt]{article}

\usepackage{fontspec}
\usepackage{polyglossia}
\usepackage{tikz}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{float}
\usepackage{tabularx}
\usepackage{bussproofs}
\usepackage{minted}
\usepackage{indentfirst}

\setdefaultlanguage{russian}

\setmainfont{CMU Serif}           %% задаёт основной шрифт документа
\setsansfont{CMU Sans Serif}      %% задаёт шрифт без засечек
\setmonofont{CMU Typewriter Text}

\title{Математическая логика}
\author{Практика 3, 4}
\date{22/03/2018}

\begin{document}

\maketitle

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

\noindent Правила вывода:

\textit{Правило введения импликации}
\begin{center}
  \RightLabel{($\to$ intro)}
  \AxiomC{$\Gamma , A \vdash B$}
  \UnaryInfC{$\Gamma \vdash A \to B$}
  \DisplayProof{}
\end{center}

\textit{Правило удаления импликации(Modus Ponens)}
\begin{center}
  \AxiomC{$\Gamma \vdash A \to B$}
  \AxiomC{$\Gamma \vdash A$}
  \RightLabel{($\to$ elim)}
  \BinaryInfC{$\Gamma \vdash B$}
  \DisplayProof{}
\end{center}

\textit{Правило введения конъюнкции}
\begin{center}
  \AxiomC{$\Gamma \vdash A$}
  \AxiomC{$\Gamma \vdash B$}
  \RightLabel{($\land$ intro)}
  \BinaryInfC{$\Gamma \vdash A \land B$}
  \DisplayProof{}
\end{center}

\textit{Правила удаления конъюнкции}
\begin{center}
  \RightLabel{($\land$ elimI)}
  \AxiomC{$\Gamma \vdash A \land B$}
  \UnaryInfC{$\Gamma \vdash A$}
  \DisplayProof{}
  \hspace{1em}
  \RightLabel{($\land$ elimII)}
  \AxiomC{$\Gamma \vdash A \land B$}
  \UnaryInfC{$\Gamma \vdash B$}
  \DisplayProof{}
\end{center}

\textit{Правила введения дизъюнкции}
\begin{center}
  \RightLabel{($\lor$ introI)}
  \AxiomC{$\Gamma \vdash A$}
  \UnaryInfC{$\Gamma \vdash A \lor B$}
  \DisplayProof{}
  \hspace{1em}
  \RightLabel{($\lor$ introII)}
  \AxiomC{$\Gamma \vdash B$}
  \UnaryInfC{$\Gamma \vdash A \lor B$}
  \DisplayProof{}
\end{center}

\textit{Правило разбора случаев}
\begin{center}
  \AxiomC{$\Gamma, A \vdash C$}
  \AxiomC{$\Gamma, B \vdash C$}
  \RightLabel{(case analisys)}
  \BinaryInfC{$\Gamma, A \lor B \vdash C$}
  \DisplayProof{}
\end{center}

\textit{Правило удаления дизъюнкции}
\begin{center}
  \AxiomC{$\Gamma \vdash A \lor B$}
  \AxiomC{$\Gamma, A \vdash C$}
  \AxiomC{$\Gamma, B \vdash C$}
  \RightLabel{($\lor$ elim)}
  \TrinaryInfC{$\Gamma \vdash C$}
  \DisplayProof{}
\end{center}

\textit{Вывод чего угодно из противоречия}
\begin{center}
  \AxiomC{$\Gamma \vdash A$}
  \AxiomC{$\Gamma \vdash \lnot A$}
  \RightLabel{($\lnot$ elim)}
  \BinaryInfC{$\Gamma \vdash B$}
  \DisplayProof{}
\end{center}

\textit{Правило введения отрицания}
\begin{center}
  \AxiomC{$\Gamma, A \vdash B$}
  \AxiomC{$\Gamma, A \vdash \lnot B$}
  \RightLabel{($\lnot$ intro)}
  \BinaryInfC{$\Gamma \vdash \lnot A$}
  \DisplayProof{}
\end{center}

\textit{Закон снятия двойного отрицания}
\begin{center}
  \AxiomC{$\Gamma \vdash \lnot \lnot A$}
  \RightLabel{($\lnot$ elimII)}
  \UnaryInfC{$\Gamma \vdash A$}
  \DisplayProof{}
\end{center}

На всякий случай, некоторые полезные конструкции в лямбда-исчислении и правила их типизации, по соответствию Карри-Говарда:

Множество типов лямбда исчисления:
\begin{center}
  \AxiomC{$t \in Var$}
  \UnaryInfC{$t \in Type$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$A \in Type$}
  \AxiomC{$B \in Type$}
  \BinaryInfC{$A \to B \in Type$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$A \in Type$}
  \AxiomC{$B \in Type$}
  \BinaryInfC{$A \times B \in Type$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$A \in Type$}
  \AxiomC{$B \in Type$}
  \BinaryInfC{$A \coprod B \in Type$}
  \DisplayProof{}
\end{center}

Множество предтермов лямбда-исчисления (мы используем разные множества для переменных в типах и переменных в термах):
\begin{center}
  \AxiomC{$x \in Var'$}
  \UnaryInfC{$x \in Term$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$M \in Term$}
  \AxiomC{$N \in Term$}
  \BinaryInfC{$M\ N \in Term$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$M \in Term$}
  \AxiomC{$x \in Var'$}
  \BinaryInfC{$\lambda x.\ M \in Term$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$M \in Term$}
  \AxiomC{$N \in Term$}
  \BinaryInfC{$(M, N) \in Term$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$P \in Term$}
  \UnaryInfC{$fst\ P \in Term$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$P \in Term$}
  \UnaryInfC{$snd\ P \in Term$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$M \in Term$}
  \UnaryInfC{$inl\ M \in Term$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$M \in Term$}
  \UnaryInfC{$inr\ M \in Term$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$E \in Term$}
  \AxiomC{$M \in Term$}
  \AxiomC{$N \in Term$}
  \RightLabel{, $x,y \in Var'$}
  \TrinaryInfC{$\mathbf{case}\,E\ \mathbf{of}\ \{\,inl\ x \to M; inr\ y \to N\} \in Term$}
  \DisplayProof{}
\end{center}

Правила типизации:
\begin{center}
  \AxiomC{$(x : A) \in \Gamma$}
  \UnaryInfC{$\Gamma \vdash x : A$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$\Gamma \vdash M : A \to B$}
  \AxiomC{$\Gamma \vdash N : A$}
  \BinaryInfC{$\Gamma \vdash M\ N : B$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$\Gamma, x : A \vdash M : B$}
  \UnaryInfC{$\Gamma \vdash \lambda x.\ M : A \to B$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$\Gamma \vdash M : A$}
  \AxiomC{$\Gamma \vdash N : B$}
  \BinaryInfC{$\Gamma \vdash (M, N) : A \times B$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$\Gamma \vdash P : A \times B$}
  \UnaryInfC{$\Gamma \vdash fst\ P : A$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$\Gamma \vdash P : A \times B$}
  \UnaryInfC{$\Gamma \vdash snd\ P : B$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$\Gamma \vdash M : A$}
  \UnaryInfC{$\Gamma \vdash inl\ M : A \coprod B$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$\Gamma \vdash N : B$}
  \UnaryInfC{$\Gamma \vdash inr\ N : A \coprod B$}
  \DisplayProof{}
\end{center}

\begin{center}
  \AxiomC{$\Gamma \vdash E : A \coprod B$}
  \AxiomC{$\Gamma, x : A \vdash M : C$}
  \AxiomC{$\Gamma, y : B \vdash N : C$}
  \TrinaryInfC{$\Gamma \vdash \mathbf{case}\ E\ \mathbf{of}\{inl\ x \to M; inr\ y \to N\} : C$}
  \DisplayProof{}
\end{center}

\noindent Задания:

\begin{itemize}
  \item Покажите, что следующие правила являются допустимыми в исчислении высказываний:
    \begin{enumerate}
      \item Правило объединения посылок
        \begin{center}
          \AxiomC{$\Gamma, A, B \vdash C$}
          \UnaryInfC{$\Gamma, A \land B \vdash C$}
          \DisplayProof{}
        \end{center}
      \item Правило расщепления посылок
        \begin{center}
          \AxiomC{$\Gamma, A \land B \vdash C$}
          \UnaryInfC{$\Gamma, A, B \vdash C$}
          \DisplayProof{}
        \end{center}
      \item Правила
        \begin{center}
          \AxiomC{$\Gamma, A \vdash B$}
          \UnaryInfC{$\Gamma, A \land C \vdash B \land C$}
          \DisplayProof{}
          \hspace{1cm}
          \AxiomC{$\Gamma, A \vdash B$}
          \UnaryInfC{$\Gamma, A \lor C \vdash B \lor C$}
          \DisplayProof{}
        \end{center}
      \item Доказательство от противного
        \begin{center}
          \AxiomC{$\Gamma, \lnot B \vdash \lnot A$}
          \UnaryInfC{$\Gamma, A \vdash B$}
          \DisplayProof{}
        \end{center}
    \end{enumerate}
  \item Докажите, что следующие формулы являются теоремами исчисления высказываний
    \begin{enumerate}
      \item $\vdash (A \to C) \land (B \to C) \to (A \lor B) \to C$
      \item $\vdash (A \lor B) \land C \to A \land C \lor B \land C$
      \item $\vdash A \to \lnot \lnot A$
      \item $\lnot A, \lnot B \vdash A \to B$
    \end{enumerate}

\end{itemize}

\section*{Исчисление секвенций}

\indent \textit{Схема аксиом:}
$$ A, \Gamma \vdash A, \Delta $$

\textit{Правила введения конъюнкции в антецедент и сукцедент:}
\begin{center}
  \AxiomC{$A, B, \Gamma \vdash \Delta$}
  \RightLabel{$(\land \vdash)$}
  \UnaryInfC{$A \land B, \Gamma \vdash \Delta$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$\Gamma \vdash A, \Delta$}
  \AxiomC{$\Gamma \vdash B, \Delta$}
  \RightLabel{$(\vdash \land)$}
  \BinaryInfC{$\Gamma \vdash A \land B, \Delta$}
  \DisplayProof{}
\end{center}

\textit{Правила введения дизъюнкции в антецедент и сукцедент:}
\begin{center}
  \AxiomC{$A, \Gamma \vdash \Delta$}
  \AxiomC{$B, \Gamma \vdash \Delta$}
  \RightLabel{$(\lor \vdash)$}
  \BinaryInfC{$A \lor B, \Gamma \vdash \Delta$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$\Gamma \vdash A, B, \Delta$}
  \RightLabel{$(\vdash \lor)$}
  \UnaryInfC{$\Gamma \vdash A \lor B, \Delta$}
  \DisplayProof{}
\end{center}

\textit{Правила введения импликации в антецедент и сукцедент:}
\begin{center}
  \AxiomC{$\Gamma \vdash A, \Delta$}
  \AxiomC{$B, \Gamma \vdash \Delta$}
  \RightLabel{$(\to \vdash)$}
  \BinaryInfC{$A \to B, \Gamma \vdash \Delta$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$A, \Gamma \vdash B, \Delta$}
  \RightLabel{$(\vdash \to)$}
  \UnaryInfC{$\Gamma \vdash A \to B, \Delta$}
  \DisplayProof{}
\end{center}

\textit{Правила введения отрицания в антецедент и сукцедент:}
\begin{center}
  \AxiomC{$\Gamma \vdash A, \Delta$}
  \RightLabel{$(\lnot \vdash)$}
  \UnaryInfC{$\lnot A, \Gamma \vdash \Delta$}
  \DisplayProof{}
  \hspace{1cm}
  \AxiomC{$A, \Gamma \vdash \Delta$}
  \RightLabel{$(\vdash \lnot)$}
  \UnaryInfC{$\Gamma \vdash \lnot A, \Delta$}
  \DisplayProof{}
\end{center}

\noindent Задания:
\begin{itemize}
  \item Постройте вывод формулы или контрпример:
      \begin{enumerate}
        \item $((p \to q) \to q) \to q$
        \item $p \to q \vdash r \lor p \to r \lor q$
      \end{enumerate}
\end{itemize}

\section*{Домашнее задание}
\begin{enumerate}
  \item Покажите, что следующие формулы являются теоремами исчисления высказываний. Напишите вывод этих формул(или дерево вывода, как вам удобно) и лямбда-термы, доказывающие эти формулы:
    \begin{enumerate}
      \item (1б.) $\vdash A \land B \lor C \to (A \lor C) \land (B \lor C)$
      \item (1б.) $\vdash A \land C \lor B \land C \to (A \lor B) \land C$
      \item (1б.) $\vdash (A \lor C) \land (B \lor C) \to A \land B \lor C$
      \item (2б.) $\vdash ((((A \to B) \to A) \to A) \to B) \to B$
    \end{enumerate}
  \item (2б.) Покажите, что закон Де Моргана является теоремой исчисления высказываний
   $$ \vdash \lnot (A \lor B) \to \lnot A \land \lnot B $$
  \item (2б.) Опишите правила введения и удаления связки $\leftrightarrow$
  \item Постройте вывод формул или приведите контрпример
    \begin{enumerate}
      \item (1б.) $\vdash (((p \to q) \to q) \to q) \to p$
      \item (1б.) $p \to q \vdash (p \to r) \to q \to r$
      \item (2б.) $p \leftrightarrow q \vdash (p \land r) \leftrightarrow q \land r$
    \end{enumerate}
  \item (3б.) Выведите правила введения, сложения по модулю 2($\oplus$), стрелки Пирса и штриха Шеффера в антецедент и сукцедент секвенции.
\end{enumerate}


\end{document}
