meow

1 files changed, 47 insertions, 35 deletions

diff --git a/mathematics/logic.md b/mathematics/logic.md
index dca0cac..e19cb52 100644
--- a/mathematics/logic.md
+++ b/mathematics/logic.md
@@ -20,48 +20,60 @@ and many others.
 
 ### [propositional logic](https://ncatlab.org/nlab/show/propositional+logic)
 
-**propositional logic** or *0th-order logic* deals with raw *propositions*.
+**propositional logic** or **zeroth-order logic** deals with raw *propositions*.
 **propositions** are statements that *reduce* to a **truth value**.
-truth values are classically either true or false. i'm not quite sure if there are alternative approaches that change this.
+truth values are classically either true or false. in non-classical logics, this can differ.
 
 the basic foundations of propositional logic are as follows:
 
- |
-------|--------------
-p     | a proposition
-¬p    | not p
-p → q | p implies q
-⊤     | true
-⊥     | false
-⊢     | derives/yields
-
-several logical concepts are *derivable* from the above:
-
- |
-------|--------------------|----
-p ∨ q | ¬p → q             | or
-p ∧ q | ¬(p → ¬q)          | and
-p ⟺ q | (p → q) ∧ (q → p)  | iff
-p ⊕ q | (p ∨ q) ∧ ¬(p ∧ q) | xor
-
-to do anything interesting, several rules must exist:
-
-replacement rules |
-------------------------------------|----------------
-((p ∨ q) ∨ r) → (p ∨ (q ∨ r))       | associative
-(p ∧ q) → (q ∧ p)                   | commutative
-((p ∧ q) → r) → (p → (q → r))       | exportation
-(p → q) → (¬q → ¬p)                 | transposition
-(p → q) → (¬p ∨ q)                  | implication
-((p ∨ q) ∨ r) → ((p ∧ r) ∨ (q ∧ r)) | distributive
-((p) ∧ (q)) → (p ∧ q)               | conjunction
-p ⟺ (¬¬p)                           | double negation
-
-double negation is not allowed in intuistionistic logic systems.
+notation | definition
+---------|--------------
+p        | a *proposition*
+¬p       | *not* p
+p → q   | *if* p *then* q, p *implies* q
+0        | *false*
+1        | *true*
+
+several logical connectives are *derivable* from the above:
+
+notation | derivation | definition
+------|---------------------|----
+p ∨ q | ¬p → q             | p *or* q, *disjunction*
+p ∧ q | ¬(p → ¬q)          | p *and* q, *conjunction*
+p → q | ¬p ∨ q             | p *implies* q, (material) *implication* (again)
+p ↔ q | (p → q) ∧ (q → p) | p *if and only if* q, p *iff* q
+p ⊕ q | (p ∨ q) ∧ ¬(p ∧ q) | p *exclusively or* q, p *xor* q
+p ↑ q | ¬(p ∧ q)           | p *not both* q, p *nand* q
+p ↓ q | ¬(p ∨ q)           | *neither* p *nor* q, p *nor* q
+
+note that several of these definitions are circular.
+our choice in $¬$ and $→$ as the primitive connectives is thus arbitrary.
+interestingly, ↑ and ↓ are *functionally complete*: we may define all other connectives in terms of them.
+
+<details>
+<summary>aside: nand and nor</summary>
+
+notation | definition
+---------|-----------
+¬p       | p ↑ p
+p → q    | p ↑ ¬q
+p ∨ q    | ¬p ↑ ¬q
+p ∧ q    | (p ↑ q) ↑ (p ↑ q)
+p ↔ q    | (p ↑ q) ↑ (p ∨ q)
+
+notation | definition
+---------|-----------
+¬p       | p ↓ p
+p → q    | (¬p ↓ q) ↓ (¬p ↓ q)
+p ∨ q    | (p ↓ q) ↓ (p ↓ q)
+p ∧ q    | ¬p ↓ ¬q
+p ↔ q    | ...
+
+</details>
 
 ### [predicate logic](https://ncatlab.org/nlab/show/predicate+logic)
 
-**predicate logic** or *first-order logic* adds variables and quantifiers to propositions:
+**predicate logic** or **first-order logic** adds variables and quantifiers to propositions:
 * ∀x: for all x
 * ∃y: there exists a y