1 files changed, 154 insertions, 0 deletions
diff --git a/math/logic.md b/math/logic.md
new file mode 100644
index 0000000..b07e867
--- /dev/null
+++ b/math/logic.md
@@ -0,0 +1,154 @@
+---
+layout: foundations
+title: mathematics/logic
+---
+
+# logic, mathematics, & that around + in between
+
+## kinds of logic
+
+there are different types of logic!
+
+some such systems:
+- classical logic
+- intuitionistic logic
+- paraconsistent logic
+
+and many others.
+
+## orders of logic
+
+### propositional logic
+
+[**propositional logic**](https://ncatlab.org/nlab/show/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. in non-classical logics, this can differ.
+
+the basic foundations of propositional logic are as follows:
+
+notation | definition
+---------|--------------
+0        | *false*
+1        | *true*
+p        | a *proposition*
+¬p       | *not* p
+p → q   | *if* p *then* q, p *implies* q
+
+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*
+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 markdown="block">
+<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:
+* ∀x: for all x
+* ∃y: there exists a y
+
+these additions are enough to serve as a foundation of mathematics...
+
+## philosophy of mathematics
+
+what mathematics *is* is not universally agreed upon.
+
+there are two primary
+
+
+logicism is generally widely regarded as correct
+
+these philosophies
+
+there are others, but none that i am interested in.
+
+## foundations of mathematics
+
+### set theory
+
+there have been a number of set theories, of varying consistency
+
+
+naive set theory was shown inconsistent
+
+
+### type theory
+
+*type theories* can serve as an alternative (equivalent) foundation of mathematics.
+
+
+but what is the point in fashioning equivalent foundations when standard ZFC works just fine?
+
+an alternative (equivalent) foundation of mathematics are *type theories*.
+
+
+## the curry-howard correspondence
+
+the **curry-howard correspondence** or *propositions-as-types*
+
+
+symbol | logic | types
+---|-------------|--------------
+⊤  | true        | top type
+⊥  | false       | bottom type
+→  | implication | function type
+∧  | conjunction | product type
+∨  | 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 
+you MUST have a constructed thing with a type
+
+no negation??
+don't fully understand the distinction between dependent and nondependent types
+implication over types?
+
+
+
+## [principle of explosion](https://en.wikipedia.org/wiki/Principle_of_explosion)
+
+what's wrong with inconsistency, anyway?
+
+it may or may not be intuitive that a contradiction can lead to further contradictions.
+either way, an example can be helpful.
+the following logic proves any arbitrary statement B:
+
+```logic
+A = ⊤, ¬A = ⊤
+A ∨ B = ⊤
+¬A ⇒ A = ⊥
+⊥ ∨ B ⇒ B = ⊤
+```