From 43a1015cb0c7e64ac01efde1a38ccfc3f305d9fb Mon Sep 17 00:00:00 2001
From: eggy <d7chen@uwaterloo.ca>
Date: Mon, 27 May 2024 11:44:39 -0400
Subject: [PATCH] ece208: add formulas

---
 docs/2b/ece208.md | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/docs/2b/ece208.md b/docs/2b/ece208.md
index 73b2512..859ad50 100644
--- a/docs/2b/ece208.md
+++ b/docs/2b/ece208.md
@@ -1,3 +1,22 @@
 # ECE 208: Discrete Math 2
 
+## Hilbert system rules
 
+**Axioms:**
+
+- $\vdash (A\implies (B\implies A))$
+- $\vdash (A\implies (B\implies C))\implies ((A\implies B)\implies (A\implies C))$
+- $\vdash (\neg B\implies\neg A)\implies (A\implies B))$
+
+**Inference (MP):**
+
+- $\frac{\vdash A, \vdash A\implies B}{\vdash B}$
+
+**Derived rules:**
+
+- Deduction: $\frac{U\cup \{A\}\vdash B}{U\vdash A\implies B}$
+- Contrapositive: $\frac{U\vdash \neg B\implies\neg A}{U\vdash A\implies B}$ (and vice versa)
+- Transitivity: $\frac{u\vdash A\implies B, U\vdash B\implies C}{U\vdash A\implies C}$
+- Exchange of antecedent: $\frac{U\vdash A\implies (B\implies C)}{U\vdash B\implies (A\implies C)}$
+- Double negation: $\frac{U\vdash \neg\neg A}{U\vdash A}$ (and vice versa)
+- Reductio ad absurdum: $\frac{U\vdash\neg A\implies false}{U\vdash A}$