\documentclass{article}
\usepackage{amssymb, amsmath, geometry, multicol, stmaryrd}
\usepackage{ebproof}
\geometry{tmargin=.5in, bmargin=.75in, lmargin=.75in, rmargin = .75in}

\begin{document}
\setlength{\parindent}{0mm}
\renewcommand{\baselinestretch}{0.8}
\newcommand{\non}{^\neg\!\!}
\newcommand{\prouve}{\vdash}

\title{Preuves}
\author{Aubin SIONVILLE}
\date{MPI Clemenceau - 2021-2023}
\maketitle
\centering

\section*{Déduction naturelle intuitionniste}

    \begin{multicols}{2}
        
        \textbf{Règle d'Axiome :} \quad
        \begin{prooftree}
            \hypo{}
            \infer1[Ax]{\Gamma, \varphi \prouve \varphi}
        \end{prooftree}
        
        \textbf{Règle d'Affaissement :} \quad
        \begin{prooftree}
            \hypo{\Gamma' \prouve \varphi}
            \infer1[Aff]{\Gamma \prouve \varphi}
        \end{prooftree} \quad ($\Gamma' \subset \Gamma$)
        
    \end{multicols}    
    \begin{multicols}{3}

        \[\top\]

        \[\bot\]

        \[\neg\]

        \[\rightarrow\]

        \[\wedge\]

        \[\vee\]


        \[\begin{prooftree}
            \hypo{}
            \infer1[$\top$i]{\Gamma \prouve \top}
        \end{prooftree}\]

        \[\varnothing\]
        
        \[\begin{prooftree}
            \hypo{\Gamma, G \prouve \bot}
            \infer1[$\neg$i]{\Gamma, G \neg G}
        \end{prooftree}\]

        \[\begin{prooftree}
            \hypo{\Gamma, G \prouve H}
            \infer1[$\rightarrow$i]{\Gamma \prouve G \rightarrow H}
        \end{prooftree}\]

        \[\begin{prooftree}
            \hypo{\Gamma \prouve G \quad \Gamma \prouve H}
            \infer1[$\wedge$i]{\Gamma \prouve G \wedge H}
        \end{prooftree}\]

        \[\begin{prooftree}
            \hypo{\Gamma \prouve G}
            \infer1[$\vee$i,g]{\Gamma \prouve G \vee H}
        \end{prooftree}
        \quad\quad
        \begin{prooftree}
            \hypo{\Gamma \prouve H}
            \infer1[$\vee$i,d]{\Gamma \prouve G \vee H}
        \end{prooftree}\]


        \[\varnothing\]

        \[\begin{prooftree}
            \hypo{\Gamma \prouve \bot}
            \infer1[$\bot$e]{\Gamma \prouve G}
        \end{prooftree}\]

        \[\begin{prooftree}
            \hypo{\Gamma \prouve G \quad \Gamma \prouve \non G}
            \infer1[$\neg$e]{\Gamma \prouve \bot}
        \end{prooftree}\]

        \[\begin{prooftree}
            \hypo{\Gamma \prouve G \rightarrow H \quad \Gamma \prouve G}
            \infer1[$\rightarrow$e]{\Gamma \prouve H}
        \end{prooftree}\]

        \[\begin{prooftree}
            \hypo{\Gamma \prouve G \wedge H}
            \infer1[$\wedge$e,g]{\Gamma \prouve G}
        \end{prooftree}
        \quad\quad
        \begin{prooftree}
            \hypo{\Gamma \prouve G \wedge H}
            \infer1[$\wedge$e,d]{\Gamma \prouve H}
        \end{prooftree}\]

        \[\begin{prooftree}
            \hypo{\Gamma \prouve A \vee B \quad \Gamma, A \prouve G \quad \Gamma, B \prouve G}
            \infer1[$\vee$e]{\Gamma \prouve G}
        \end{prooftree}\]
    \end{multicols}
\vspace*{0cm}
\section*{Déduction naturelle classique}

    \begin{multicols}{3}
        Tiers Exclu

        \[\begin{prooftree}
            \hypo{}
            \infer1[TE]{\Gamma \prouve G \vee \non G}
        \end{prooftree}\]

        Double Négation

        \[\begin{prooftree}
            \hypo{\Gamma \prouve \non \non G}
            \infer1[$\neg\neg$e]{\Gamma \prouve G}
        \end{prooftree}\]

        Absurde

        \[\begin{prooftree}
            \hypo{\Gamma, \non G \prouve \bot}
            \infer1[Abs]{\Gamma \prouve G}
        \end{prooftree}\]
    \end{multicols}

\vspace*{0cm}

\section*{Premier order de la deduction naturelle}

    \begin{multicols}{3}
        \[\forall\]

        \[\exists\]

        \[\underset{\text{Avec } x \notin FV(\Gamma)}{\begin{prooftree}
            \hypo{\Gamma \prouve G}
            \infer1[$\forall$i]{\Gamma \prouve \forall x\ G}
        \end{prooftree}}\]

        \[\begin{prooftree}
            \hypo{\Gamma \prouve G[x \mapsto t]}
            \infer1[$\exists$i]{\Gamma \prouve \exists x\ G }
        \end{prooftree}\]

        \[\underset{\text{Avec }vars(t)\cap BV(G)=\varnothing}{\begin{prooftree}
            \hypo{\Gamma, \prouve \forall x\ G}
            \infer1[$\forall$e]{\Gamma \prouve G[x \mapsto t]}
        \end{prooftree}}\]

        \[\underset{\text{Avec } x\notin FV(\Gamma)\cup FV(G)}{\begin{prooftree}
            \hypo{\Gamma \prouve \exists x\ H \quad \Gamma, H \prouve G}
            \infer1[$\exists$e]{\Gamma \prouve G}
        \end{prooftree}}\]
    \end{multicols}

\end{document}