The duality between truth and falsity, conjunction and disjunction is a property of classical logic. Proof theory reveals not only the deep reason behind this duality, but also another duality of a more dynamical nature, which relates the two solutions of a certain dilemma in the normalization process of formal proofs. Now, surprisingly, this dilemma relates to the fundamental dilemma that occurs in the execution of functional programs: to evaluate or not the argument of a function. The seminar intends mainly to explain these relationships, which motivate work in progress about the same matters in the case of intuitionistic logic. Time permitting, the preliminary results of that work will be mentioned.
|