From 5ffac59a93388e16e90dbdd1c4f68d6a2f2c057a Mon Sep 17 00:00:00 2001
From: JJ
Date: Sat, 2 Dec 2023 19:17:23 -0800
Subject: meow

---
 mathematics/logic.md | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'mathematics')

diff --git a/mathematics/logic.md b/mathematics/logic.md
index 3be55f0..dca0cac 100644
--- a/mathematics/logic.md
+++ b/mathematics/logic.md
@@ -3,7 +3,7 @@ layout: foundations
 title: mathematics/foundations/logic
 ---
 
-# sparse notes on logic, mathematics, and that around and in between
+# logic, mathematics, & that around + in between
 
 ## kinds of logic
 
@@ -25,6 +25,8 @@ and many others.
 truth values are classically either true or false. i'm not quite sure if there are alternative approaches that change this.
 
 the basic foundations of propositional logic are as follows:
+
+ |
 ------|--------------
 p     | a proposition
 ¬p    | not p
@@ -34,6 +36,8 @@ p → q | p implies q
 ⊢     | derives/yields
 
 several logical concepts are *derivable* from the above:
+
+ |
 ------|--------------------|----
 p ∨ q | ¬p → q             | or
 p ∧ q | ¬(p → ¬q)          | and
@@ -42,7 +46,7 @@ p ⊕ q | (p ∨ q) ∧ ¬(p ∧ q) | xor
 
 to do anything interesting, several rules must exist:
 
-replacement rules
+replacement rules |
 ------------------------------------|----------------
 ((p ∨ q) ∨ r) → (p ∨ (q ∨ r))       | associative
 (p ∧ q) → (q ∧ p)                   | commutative
@@ -110,6 +114,7 @@ symbol | logic | types
 ∨  | disjunction | sum type
 ∀  | universal   | dependent product type
 ∃  | existential | dependent sum type
+¬  | negation    | many such representations
 
 a couple of other notes.
 programs as proofs comes into play when 
-- 
cgit v1.2.3-70-g09d2