---
layout: foundations
title: mathematics/foundations/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](https://ncatlab.org/nlab/show/propositional+logic)

**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
---------|--------------
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:
* ∀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 = ⊤
```