blob: 806875197d8c386eae4d4ae3da778237714774fd (
plain) (
blame)
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
|
# 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 = ⊤
```
|
