From f41200967e489fb7e1fe14e189080a48903a0674 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 27 Nov 2023 23:44:20 +0100
Subject: Rules of inuitionistic propositional calculus in natural deduction
 style.

---
 transp-inf110-02-typage.tex | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 45d1ca2..7df864b 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1333,6 +1333,45 @@ On distingue {\footnotesize (les règles précises seront décrites plus
 \vdash Q$ s'appelle un \textbf{séquent}, à comprendre comme « sous les
 hypothèses $P_1,\ldots,P_r$, on a $Q$ ».
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le calcul propositionnel intuitionniste : survol des règles}
+
+Axiomes : si $Q \in \{P_1,\ldots,P_r\}$ alors $P_1,\ldots,P_r \vdash Q$.
+
+\bigskip
+
+Introduction et élimination des connecteurs (style « déduction naturelle ») :
+
+\smallskip
+
+\begin{tabular}{c|c|c}
+&Intro&Élim\\\hline
+$\Rightarrow$
+&$\inferrule{\Gamma,P\vdash Q}{\Gamma\vdash P\Rightarrow Q}$
+&$\inferrule{\Gamma\vdash P\Rightarrow Q\\\Gamma\vdash P}{\Gamma\vdash Q}$
+\\\hline
+$\land$
+&$\inferrule{\Gamma\vdash Q_1\\\Gamma\vdash Q_2}{\Gamma\vdash Q_1\land Q_2}$
+&$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_1}$
+\quad$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_2}$
+\\\hline
+$\lor$
+&$\inferrule{\Gamma\vdash Q_1}{\Gamma\vdash Q_1\lor Q_2}$
+\quad$\inferrule{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$
+&$\inferrule{\Gamma\vdash P_1\lor P_2\\\Gamma,P_1\vdash Q\\\Gamma,P_2\vdash Q}{\Gamma\vdash Q}$
+\\\hline
+$\top$
+&$\inferrule{\strut}{\Gamma\vdash \top}$
+&(néant)
+\\\hline
+$\bot$
+&(néant)
+&$\inferrule{\Gamma\vdash \bot}{\Gamma\vdash Q}$
+\\
+\end{tabular}
+
 \end{frame}
 %
 \end{document}
-- 
cgit v1.2.3