1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
---
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
[**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 = ⊤
```
|
