Schedule and Lecture Notes

Here is a list of the lectures planned for the course. Note that topics are subject to change.

Date Topic Lecture Notes and Readings
Jan 25

Course Introduction, the story of logic


Lecture 1: pdf
Jan 27 Ways of defining logics formally, recursive types Lecture 2: pdf
Feb 1

Boolean logics-- propositional, first order (FOL)

Lecture 3: pdf
Feb 3 Computational logics -- first order Lecture 4: pdf


Feb 8

Evidence semantics

Lecture 5: pdf

Feb 10 Evidence semantics continued Lecture 6: pdf
Feb 15 Consistency and completeness issues

Lecture 7: pdf

Feb 17 Types and sets

Lecture 8: pdf

Feb 22 First-Order theories-- PA, HA Lecture 9: pdf
Feb 24 Peano Arith (PA) and Heyting Arithmetic (HA) Lecture 10: pdf
Mar 1 Godel translation of PA into HA Lecture 11: pdf
Mar 3 Markov's Principle Lecture 12: pdf
Mar 8 Marvov's Principle (MP) and Hoare While Rule  
Mar 10 Consistency of Markov's Principle Lecture 13: pdf
Mar 15

Godel system T, higher-order functions

Lecture 14: pdf
Mar 17 Translating classical proofs to constructive proofs, Murthy results

Lecture 15: pdf


Problem Set 3
Mar 22 **Spring Break**
Mar 24 **Spring Break**
Mar 29 Brouwer ordinals and W-types

Lecture 16: pdf

Mar 31


Lecture 17: pdf

Apr 5

Kleene theorem on recursive fans, Continuity principles

Lecture 18:

pdf, pdf, pdf, pdf

Apr 7

Brouwer's Bar Theorem, Kleene realizability

Lecture 19: pdf

pdf, pdf

Apr 12

Martin-Lof's Intuitionistic Type Theory (ITT)

Lecture 20: pdf


Apr 14

Realizing Bar Induction

Lecture 21: pdf
Apr 19 Howe's computational equality and Howe's trick Lecture 22: pdf
Apr 21 Partial equivalence relation (per) semantics

Lecture 23: pdf pdf

Apr 26

Richer types -- dependent records

Lecture 24:pdf pdf pdf pdf

Apr 28 Bar types and unsolvable problems Lecture 25: pdf

May 3

May 5

Process type

Unsolvability without Church's Thesis (CT)

Lecture 26: pdf

Lecture 27: pdf