meow

1 files changed, 0 insertions, 154 deletions

diff --git a/mathematics/logic.md b/mathematics/logic.md
deleted file mode 100644
index b07e867..0000000
--- a/mathematics/logic.md
+++ /dev/null
@@ -1,154 +0,0 @@
----
-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 = ⊤
-```