From 30d6d7dc63fe117b7acef1ad88678f6258211295 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Fri, 4 Jul 2025 02:11:44 +0200
Subject: Start propositional logic

---
 library/logic/propositional.tex | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 library/logic/propositional.tex

(limited to 'library/logic/propositional.tex')

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}
-- 
cgit v1.2.3

