| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | A tedious exercise in using Peano's axioms. | David A. Madore | 2024-01-12 | 1 | -0/+53 |
| * | Be more consistent about abbreviating logical rules. | David A. Madore | 2024-01-12 | 1 | -2/+2 |
| * | Two exercises on Löb's theorem. | David A. Madore | 2024-01-12 | 1 | -0/+146 |
| * | An easy exercise on first-order logic. | David A. Madore | 2024-01-12 | 1 | -0/+53 |
| * | An exercise on Girard's system F. | David A. Madore | 2024-01-12 | 1 | -2/+209 |
| * | Exercise on the realizability of Plisko's formula. | David A. Madore | 2024-01-11 | 1 | -1/+90 |
| * | Dragon riddle. | David A. Madore | 2024-01-11 | 1 | -1/+108 |
| * | An exercise on refuting Tseitin's formula using open sets in the plane. | David A. Madore | 2024-01-11 | 1 | -0/+153 |
| * | An exercise on Kleene's recursion theorem with a slight "paradox". | David A. Madore | 2024-01-11 | 1 | -0/+55 |
| * | Fix a typo and make small improvement noted during lecture on 2024-01-09. | David A. Madore | 2024-01-09 | 1 | -5/+5 |
| * | The set of theorems is not computable. | David A. Madore | 2024-01-09 | 1 | -5/+37 |
| * | More around Gödel and whatnot. | David A. Madore | 2024-01-09 | 1 | -13/+159 |
| * | Gödel's theorem. | David A. Madore | 2024-01-08 | 1 | -3/+168 |
| * | More about first-order arithmetic. | David A. Madore | 2024-01-08 | 1 | -4/+111 |
| * | An example proof in Heyting arithmetic. | David A. Madore | 2024-01-08 | 1 | -5/+43 |
| * | Start writing about first-order arithmetic. | David A. Madore | 2024-01-08 | 1 | -0/+71 |
| * | Curry-Howard and equality for first-order logic. | David A. Madore | 2024-01-08 | 1 | -0/+98 |
| * | Try to improve explanations of what sort of quantifications are allowed. | David A. Madore | 2024-01-08 | 1 | -23/+92 |
| * | Add minor clarifications here and there. | David A. Madore | 2024-01-08 | 1 | -9/+17 |
| * | An exercise that will be used as a lemma for a later exercise. | David A. Madore | 2024-01-08 | 1 | -0/+72 |
| * | Rework presentation of first-order logic. | David A. Madore | 2024-01-07 | 1 | -103/+165 |
| * | Slightly rework slide on \exists versus sum types. | David A. Madore | 2024-01-07 | 1 | -1/+19 |
| * | Continue reworking the introduction to quantifiers (maybe done?). | David A. Madore | 2024-01-06 | 1 | -1/+156 |
| * | Rework the introduction to quantifiers (work in progress!). | David A. Madore | 2024-01-06 | 1 | -23/+162 |
| * | An exercise about proving the Medvedev-validity of the Kreisel-Putnam formula. | David A. Madore | 2024-01-05 | 1 | -0/+75 |
| * | An exercise about proving the irrealizability of the Kreisel-Putnam formula. | David A. Madore | 2024-01-05 | 1 | -1/+119 |
| * | Another exercise on Kripke semantics. | David A. Madore | 2024-01-05 | 1 | -4/+106 |
| * | Two more exercises on intuitionistic propositional calculus. | David A. Madore | 2024-01-05 | 1 | -10/+145 |
| * | A simple exercise on Kripke semantics. | David A. Madore | 2024-01-04 | 1 | -1/+79 |
| * | Exercise on comparison of double-negation elimination and excluded middle. | David A. Madore | 2023-12-28 | 1 | -0/+243 |
| * | Forgotten braces. | David A. Madore | 2023-12-28 | 1 | -2/+2 |
| * | Fix a number of typos / thinkos / notational blunders in an exercise. | David A. Madore | 2023-12-28 | 1 | -4/+4 |
| * | Fix various mistakes and make some improvements noted during lecture on 2023-... | David A. Madore | 2023-12-20 | 2 | -63/+85 |
| * | Change my mind about name of third part. | David A. Madore | 2023-12-19 | 1 | -1/+1 |
| * | Say something about existentials versus sum types. | David A. Madore | 2023-12-19 | 1 | -0/+42 |
| * | Add a slide on impredicativity. | David A. Madore | 2023-12-19 | 1 | -0/+52 |
| * | Slight clarification. | David A. Madore | 2023-12-18 | 1 | -3/+4 |
| * | The problem of the inhabitedness of the domain. | David A. Madore | 2023-12-18 | 1 | -6/+57 |
| * | Example proof in first-order logic. | David A. Madore | 2023-12-18 | 1 | -8/+86 |
| * | The rules of first-order logic. | David A. Madore | 2023-12-17 | 1 | -0/+121 |
| * | Start talking about first-order logic. | David A. Madore | 2023-12-17 | 1 | -2/+111 |
| * | Start a basic set of slides on higher order logic(s). | David A. Madore | 2023-12-17 | 1 | -0/+227 |
| * | Give the proof in Coq as well. | David A. Madore | 2023-12-16 | 1 | -0/+29 |
| * | More exercises in intiotionistic propositional logic. | David A. Madore | 2023-12-16 | 1 | -1/+87 |
| * | Say something about the value restriction. | David A. Madore | 2023-12-16 | 1 | -3/+37 |
| * | Briefly mention the problem of let-bound polymorphism. | David A. Madore | 2023-12-16 | 1 | -0/+84 |
| * | Summarize properties of Hindley-Milner. | David A. Madore | 2023-12-16 | 1 | -0/+46 |
| * | An example of the full H-M algorithm. | David A. Madore | 2023-12-16 | 1 | -5/+58 |
| * | Description of the unification phase of Hindley-Milner. | David A. Madore | 2023-12-16 | 1 | -1/+35 |
| * | Start describing the Hindley-Milner algorithm. | David A. Madore | 2023-12-16 | 1 | -4/+113 |
