Start propositional logic

1 files changed, 35 insertions, 0 deletions

diff --git a/library/logic/propositional.tex b/library/logic/propositional.tex
new file mode 100644
index 0000000..716de54
--- /dev/null
+++ b/library/logic/propositional.tex
@@ -0,0 +1,35 @@
+\import{set.tex}
+\import{nat.tex}
+
+
+\begin{datatype}
+The set $\propform$ is generated as follows.
+\begin{enumerate}
+    \item if $n\in\naturals$, then $\propvar{n}\in\propform$
+    \item $\propbot\in\propform$
+    \item if $p, q\in\propform$, then $p\propto q\in\propform$
+\end{enumerate}
+\end{datatype}
+
+\begin{abbreviation}
+    $\propnot p = p\propto\propbot$.
+\end{abbreviation}
+
+\begin{inductive}
+    \begin{enumerate}
+        \item (Detachment) If $\deducible{p}$ and $\deducible{p\propto q}$, then $\deducible{q}$
+        \item (Implosion) $\deducible{p\propto q\propto p}$
+        \item (Chain) $\deducible{(p\propto q\propto r)\propto(p\propto q)\propto(p\propto r)}$
+        \item (Negation) $\propnot\propnot p\to p$
+    \end{enumerate}
+\end{inductive}
+
+\begin{lemma}
+    Suppose $\deducible{q}$.
+    Then $\deducible{p\propto q}$.
+\end{lemma}
+
+\begin{primrec}
+    Recursively define a predicate $\propeval{-}{-}$ on $\propform$ as follows.
+    % TODO continue...
+\end{primrec}