summaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Second pass of proofreading.David A. Madore2024-01-221-124/+133
* First pass of proofreading.David A. Madore2024-01-221-112/+145
* A simple exercise about Coq.David A. Madore2024-01-221-0/+62
* An exercise on Gödel's theorem.David A. Madore2024-01-221-0/+79
* An exercise on Hindley-Milner.David A. Madore2024-01-221-0/+63
* Improve that last exercise.David A. Madore2024-01-221-3/+25
* An exercise on simple reading of lambda-terms.David A. Madore2024-01-221-0/+48
* An exercise on semantics.David A. Madore2024-01-221-0/+145
* First version of test for 2024-01-26.David A. Madore2024-01-221-0/+625
* Typo.David A. Madore2024-01-221-1/+1
* Simple exercise illustrating the s-m-n theorem for programmatic composition.David A. Madore2024-01-201-0/+40
* Clarification over previous addition.David A. Madore2024-01-201-1/+4
* Give another presentation of a proof in an exercise (at a student's request).David A. Madore2024-01-201-0/+70
* Adjust TeX sources to make compilation as handout with beamerarticle easier.David A. Madore2024-01-203-10/+39
* Typeset course syllabus.David A. Madore2024-01-191-0/+160
* An exercise on computing a large number.David A. Madore2024-01-191-0/+130
* Fix wrong environment.David A. Madore2024-01-191-2/+2
* Fix small mistakes noted during lecture on 2024-01-17.David A. Madore2024-01-171-3/+3
* A tedious exercise in using Peano's axioms.David A. Madore2024-01-121-0/+53
* Be more consistent about abbreviating logical rules.David A. Madore2024-01-121-2/+2
* Two exercises on Löb's theorem.David A. Madore2024-01-121-0/+146
* An easy exercise on first-order logic.David A. Madore2024-01-121-0/+53
* 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