meow

1 files changed, 132 insertions, 0 deletions

diff --git a/mathematics/logic.md b/mathematics/logic.md
new file mode 100644
index 0000000..8068751
--- /dev/null
+++ b/mathematics/logic.md
@@ -0,0 +1,132 @@
+# sparse notes on logic, mathematics, and that around and 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](https://ncatlab.org/nlab/show/propositional+logic)
+
+**propositional logic** or *0th-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.
+
+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.
+
+### [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
+
+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 = ⊤
+```