summaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* An exercise on Girard's system F.David A. Madore2024-01-121-2/+209
|
* Exercise on the realizability of Plisko's formula.David A. Madore2024-01-111-1/+90
|
* Dragon riddle.David A. Madore2024-01-111-1/+108
|
* An exercise on refuting Tseitin's formula using open sets in the plane.David A. Madore2024-01-111-0/+153
|
* An exercise on Kleene's recursion theorem with a slight "paradox".David A. Madore2024-01-111-0/+55
|
* Fix a typo and make small improvement noted during lecture on 2024-01-09.David A. Madore2024-01-091-5/+5
|
* The set of theorems is not computable.David A. Madore2024-01-091-5/+37
|
* More around Gödel and whatnot.David A. Madore2024-01-091-13/+159
|
* Gödel's theorem.David A. Madore2024-01-081-3/+168
|
* More about first-order arithmetic.David A. Madore2024-01-081-4/+111
|
* An example proof in Heyting arithmetic.David A. Madore2024-01-081-5/+43
|
* Start writing about first-order arithmetic.David A. Madore2024-01-081-0/+71
|
* Curry-Howard and equality for first-order logic.David A. Madore2024-01-081-0/+98
|
* Try to improve explanations of what sort of quantifications are allowed.David A. Madore2024-01-081-23/+92
|
* Add minor clarifications here and there.David A. Madore2024-01-081-9/+17
|
* An exercise that will be used as a lemma for a later exercise.David A. Madore2024-01-081-0/+72
|
* Rework presentation of first-order logic.David A. Madore2024-01-071-103/+165
|
* Slightly rework slide on \exists versus sum types.David A. Madore2024-01-071-1/+19
|
* Continue reworking the introduction to quantifiers (maybe done?).David A. Madore2024-01-061-1/+156
|
* Rework the introduction to quantifiers (work in progress!).David A. Madore2024-01-061-23/+162
|
* An exercise about proving the Medvedev-validity of the Kreisel-Putnam formula.David A. Madore2024-01-051-0/+75
|
* An exercise about proving the irrealizability of the Kreisel-Putnam formula.David A. Madore2024-01-051-1/+119
|
* Another exercise on Kripke semantics.David A. Madore2024-01-051-4/+106
|
* Two more exercises on intuitionistic propositional calculus.David A. Madore2024-01-051-10/+145
|
* A simple exercise on Kripke semantics.David A. Madore2024-01-041-1/+79
|
* Exercise on comparison of double-negation elimination and excluded middle.David A. Madore2023-12-281-0/+243
|
* Forgotten braces.David A. Madore2023-12-281-2/+2
|
* Fix a number of typos / thinkos / notational blunders in an exercise.David A. Madore2023-12-281-4/+4
|
* Fix various mistakes and make some improvements noted during lecture on ↵David A. Madore2023-12-202-63/+85
| | | | 2023-12-19.
* Change my mind about name of third part.David A. Madore2023-12-191-1/+1
|
* Say something about existentials versus sum types.David A. Madore2023-12-191-0/+42
|
* Add a slide on impredicativity.David A. Madore2023-12-191-0/+52
|
* Slight clarification.David A. Madore2023-12-181-3/+4
|
* The problem of the inhabitedness of the domain.David A. Madore2023-12-181-6/+57
|
* Example proof in first-order logic.David A. Madore2023-12-181-8/+86
|
* The rules of first-order logic.David A. Madore2023-12-171-0/+121
|
* Start talking about first-order logic.David A. Madore2023-12-171-2/+111
|
* Start a basic set of slides on higher order logic(s).David A. Madore2023-12-171-0/+227
|
* Give the proof in Coq as well.David A. Madore2023-12-161-0/+29
|
* More exercises in intiotionistic propositional logic.David A. Madore2023-12-161-1/+87
|
* Say something about the value restriction.David A. Madore2023-12-161-3/+37
|
* Briefly mention the problem of let-bound polymorphism.David A. Madore2023-12-161-0/+84
|
* Summarize properties of Hindley-Milner.David A. Madore2023-12-161-0/+46
|
* An example of the full H-M algorithm.David A. Madore2023-12-161-5/+58
|
* Description of the unification phase of Hindley-Milner.David A. Madore2023-12-161-1/+35
|
* Start describing the Hindley-Milner algorithm.David A. Madore2023-12-161-4/+113
|
* An exercise involving call/cc.David A. Madore2023-12-151-0/+42
|
* An exercise on Curry-Howard.David A. Madore2023-12-151-0/+109
|
* Decide that label strings should be in English.David A. Madore2023-12-151-14/+14
|
* Note the disjunction property for realizability semantics.David A. Madore2023-12-151-1/+8
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-23 03:05:39 +0000