Proof Theory Foundations, Lecture 1

Frank Pfenning - Proof Theory Foundations, Lecture 1, Oregon Programming Languages Summer School 2012, University of Oregon

[bobl]

I don't know if it's just me but I had several failed attempts trying to understand this video. At first I thought it was because I lacked enough background for understanding this but after I did more reading on this subject and watched this video again, I realized that there are a lot of hand-waving (discharging of assumption was not mentioned at all, which is crucial to some completeness proofs). The video is still valuable and serves as a good complement to the readings I had, but my suggestion is that you shouldn't use this video as a self-contained introduction to proof theory. Ignore this comment if you are actually able to follow it, I just don't want anyone else getting as frustrated as I were when getting totally confused ;-)

[JeanIbarz]

I don't really agree with the explanation of why we can deduce something from the conjunction introduced around 20-25min of the lecture. In my opinion, the definition can be interpreted as "A true, B true" implies "(A and B) is true". In this case, we can't deduce anything from the judgement "(A and B) is true", because we should have an "if and only if" relation from the definition : something other than "A true, B true" could implies "(A and B) is true". I think the deduction can only be assumed if the definition is interpreted as "(A true, B true) is equivalent to (A and B) is true", in which case we can guess the left to right implication and the right to left implication (what you call the "deduction").

[CaptainPumpkin]

To who record this, sorry, I cant see the whiteboard.

[ThorkilKowalski]

Is there a place where you can find the exercises that he describes in this lecture?