| Commit message (Expand) | Author | Age | Files | Lines |
* | Comments on negation and double negation. | David A. Madore | 2023-12-04 | 1 | -0/+40 |
* | Curry-Howard: a recapitulation. | David A. Madore | 2023-12-04 | 1 | -4/+47 |
* | Various minor changes or additions. | David A. Madore | 2023-12-04 | 1 | -1/+21 |
* | More discussion of the logical connectors. | David A. Madore | 2023-12-04 | 1 | -4/+53 |
* | Non-uniqueness of proofs. | David A. Madore | 2023-12-03 | 1 | -1/+57 |
* | Various examples of Curry-Howard. | David A. Madore | 2023-12-03 | 1 | -1/+81 |
* | Curry-Howard correspondence for true and false. | David A. Madore | 2023-12-03 | 1 | -1/+32 |
* | An example of Curry-Howard with disjunction. | David A. Madore | 2023-12-03 | 1 | -0/+41 |
* | Remarks on products and sums. | David A. Madore | 2023-12-03 | 1 | -2/+44 |
* | Curry-Howard correspondence for disjunction. | David A. Madore | 2023-12-03 | 1 | -0/+31 |
* | An example of Curry-Howard with implication. | David A. Madore | 2023-12-03 | 1 | -0/+31 |
* | An example of Curry-Howard with conjunction. | David A. Madore | 2023-12-03 | 1 | -4/+74 |
* | Curry-Howard correspondence for implication alone. | David A. Madore | 2023-12-03 | 1 | -0/+44 |
* | Brouwer-Heyting-Kolmogorov interpretation of logical connectives. | David A. Madore | 2023-12-03 | 1 | -1/+28 |
* | A few more important tautologies. | David A. Madore | 2023-12-03 | 1 | -1/+5 |
* | Various informal explanations of constructive math / intuitionism. | David A. Madore | 2023-12-02 | 1 | -0/+142 |
* | Classical logic. | David A. Madore | 2023-12-02 | 1 | -3/+71 |
* | Proof of negation vs reduction ad absurdum. | David A. Madore | 2023-12-02 | 1 | -0/+54 |
* | Examples of non-tautologies. | David A. Madore | 2023-12-02 | 1 | -3/+37 |
* | Some important tautologies. | David A. Madore | 2023-12-02 | 1 | -0/+58 |
* | Yet another presentation of natural deduction proofs (flag presentation). | David A. Madore | 2023-12-02 | 1 | -2/+38 |
* | Another presentation of natural deduction proofs. | David A. Madore | 2023-12-02 | 1 | -2/+49 |
* | Give two examples of natural deduction proofs (written in sequent style). | David A. Madore | 2023-11-30 | 1 | -0/+41 |
* | Minor fixes. | David A. Madore | 2023-11-30 | 1 | -3/+3 |
* | Highlight discharged hypotheses in natural deduction presentation. | David A. Madore | 2023-11-28 | 1 | -3/+7 |
* | Alternative notation for multiple lambdas. | David A. Madore | 2023-11-28 | 1 | -2/+3 |
* | Avoid speaking of type "constructors", a word which might cause confusion. | David A. Madore | 2023-11-28 | 1 | -4/+4 |
* | Rules of inuitionistic propositional calculus in natural deduction style. | David A. Madore | 2023-11-27 | 1 | -0/+39 |
* | Syntax of propositional calculus. | David A. Madore | 2023-11-27 | 1 | -2/+39 |
* | Quick overview of intuitionistic propositional calculus. | David A. Madore | 2023-11-27 | 1 | -0/+38 |
* | A (humorous) graphical representation of the Curry-Howard correspondence. | David A. Madore | 2023-11-24 | 1 | -4/+27 |
* | Graphical representation of typing rules. | David A. Madore | 2023-11-22 | 1 | -8/+35 |
* | Brief summary of Tait's proof of normalization of the STLC. | David A. Madore | 2023-11-22 | 1 | -5/+42 |
* | Clarification on how to read a derivation tree. | David A. Madore | 2023-11-22 | 1 | -0/+8 |
* | Give some examples of terms and types in the STLC before formalizing. | David A. Madore | 2023-11-22 | 1 | -4/+44 |
* | A first taste of the Curry-Howard correspondence. | David A. Madore | 2023-11-22 | 1 | -1/+34 |
* | Beta-reduction and strong normalization (to be continued). | David A. Madore | 2023-11-16 | 1 | -0/+41 |
* | More properties of typing, incl. the substitution lemma. | David A. Madore | 2023-11-16 | 1 | -6/+97 |
* | Some properties of derivation in simply-typed lambda-calculus. | David A. Madore | 2023-11-16 | 1 | -0/+111 |
* | Give an example of a fully written out derivation tree. | David A. Madore | 2023-11-15 | 1 | -0/+39 |
* | Rules of the simply-typed lambda-calculus. | David A. Madore | 2023-11-15 | 1 | -3/+122 |
* | Various curiosities. | David A. Madore | 2023-11-15 | 1 | -3/+32 |
* | Type systems for logic. | David A. Madore | 2023-11-15 | 1 | -1/+67 |
* | Curry's paradox (an interlude). | David A. Madore | 2023-11-15 | 1 | -0/+88 |
* | Typing and termination. | David A. Madore | 2023-11-15 | 1 | -0/+41 |
* | Tasks in a typing system. | David A. Madore | 2023-11-15 | 1 | -1/+45 |
* | More examples of languages with interesting type systems. | David A. Madore | 2023-11-15 | 1 | -4/+47 |
* | Use of typing systems beyond value control. | David A. Madore | 2023-11-15 | 1 | -0/+36 |
* | Minor clarification. | David A. Madore | 2023-11-14 | 1 | -2/+3 |
* | Generalities about polymorphism. | David A. Madore | 2023-11-14 | 1 | -14/+64 |