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