summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--mathematics/logic.md9
1 files changed, 7 insertions, 2 deletions
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