--- 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.
aside: nand and nor 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 | ...
### [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 = ⊤ ```