summaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* Slightly expand slide on Hilbert system.David A. Madore2023-12-121-2/+13
|
* A brief word about the S,K,I combinators.David A. Madore2023-12-121-0/+44
|
* A brief word on Curry-Howard for sequent calculus, and the lambda-bar-calculus.David A. Madore2023-12-121-0/+62
|
* Sketch of proof of cut elimination, and applications thereof.David A. Madore2023-12-121-6/+91
|
* Better use of mathpartir.David A. Madore2023-12-121-88/+88
|
* Examples of cut elimination steps.David A. Madore2023-12-121-15/+76
|
* Start talking about cut elimination.David A. Madore2023-12-111-0/+79
|
* Equivalence of sequent calculus with natural deduction.David A. Madore2023-12-111-0/+55
|
* Sequent calculus: better discuss structural rules.David A. Madore2023-12-111-0/+38
|
* Make the fix less confusing.David A. Madore2023-12-111-6/+3
|
* Fix a mistake: contraction rule cannot be dispensed with.David A. Madore2023-12-091-10/+7
| | | | | | (See discussion in example 3.1.3 in Troelstra & Schwichtenberg: the system I presented is essentially their G2i, and the contraction rule is necessary.)
* Fix various mistakes noted during lecture on 2023-12-08.David A. Madore2023-12-081-9/+12
|
* Thinko.David A. Madore2023-12-051-1/+1
|
* Various minor changes (upon re-reading).David A. Madore2023-12-051-17/+28
|
* Examples of sequent calculus proofs.David A. Madore2023-12-041-3/+74
|
* The rules of sequent calculus.David A. Madore2023-12-041-0/+84
|
* Functoriality of connectors and of logical formulae.David A. Madore2023-12-041-24/+123
|
* Positive and negative occurrences.David A. Madore2023-12-041-0/+43
|
* A start of polymorphism, and substitution for type/prop variables.David A. Madore2023-12-041-2/+35
|
* Comments on negation and double negation.David A. Madore2023-12-041-0/+40
|
* Curry-Howard: a recapitulation.David A. Madore2023-12-041-4/+47
|
* Various minor changes or additions.David A. Madore2023-12-041-1/+21
|
* More discussion of the logical connectors.David A. Madore2023-12-041-4/+53
|
* Non-uniqueness of proofs.David A. Madore2023-12-031-1/+57
|
* Various examples of Curry-Howard.David A. Madore2023-12-031-1/+81
|
* Curry-Howard correspondence for true and false.David A. Madore2023-12-031-1/+32
|
* An example of Curry-Howard with disjunction.David A. Madore2023-12-031-0/+41
|
* Remarks on products and sums.David A. Madore2023-12-031-2/+44
|
* Curry-Howard correspondence for disjunction.David A. Madore2023-12-031-0/+31
|
* An example of Curry-Howard with implication.David A. Madore2023-12-031-0/+31
|
* An example of Curry-Howard with conjunction.David A. Madore2023-12-031-4/+74
|
* Curry-Howard correspondence for implication alone.David A. Madore2023-12-031-0/+44
|
* Brouwer-Heyting-Kolmogorov interpretation of logical connectives.David A. Madore2023-12-031-1/+28
|
* A few more important tautologies.David A. Madore2023-12-031-1/+5
|
* Various informal explanations of constructive math / intuitionism.David A. Madore2023-12-021-0/+142
|
* Classical logic.David A. Madore2023-12-021-3/+71
|
* Proof of negation vs reduction ad absurdum.David A. Madore2023-12-021-0/+54
|
* Examples of non-tautologies.David A. Madore2023-12-021-3/+37
|
* Some important tautologies.David A. Madore2023-12-021-0/+58
|
* Yet another presentation of natural deduction proofs (flag presentation).David A. Madore2023-12-021-2/+38
|
* Another presentation of natural deduction proofs.David A. Madore2023-12-021-2/+49
|
* An exercise on a possible representation of pairs in functional programming ↵David A. Madore2023-12-011-5/+146
| | | | languages.
* Another exercise on various "loopy" reductions.David A. Madore2023-12-011-1/+120
|
* Give two examples of natural deduction proofs (written in sequent style).David A. Madore2023-11-301-0/+41
|
* Some exercises on the untyped lambda-calculus.David A. Madore2023-11-301-0/+286
|
* Minor fixes.David A. Madore2023-11-301-3/+3
|
* Much longer explanation of the Y (and also Z) combinator.David A. Madore2023-11-281-5/+139
|
* Highlight discharged hypotheses in natural deduction presentation.David A. Madore2023-11-281-3/+7
|
* Fix various small mistakes or unclear points.David A. Madore2023-11-281-9/+8
|
* Alternative notation for multiple lambdas.David A. Madore2023-11-281-2/+3
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-23 18:59:01 +0000