Constructive Logic
The underlying principle of our development of logic (and later type theory) is the separation of judgments from propositions. A judgment is an object of knowledge, while an evident judgment is something we know. Examples of judgments are ``A is a proposition'' and ``A is true''. The meaning of a proposition is determined by what counts as a verification of it. These consideration lead us to introduction and elimination rules for logical connectives, plus the notion of local reduction which verifies that the elimination rules are sound with respect to the introduction rules.
For the purpose of guiding proof search we further introduce the notion of normal deduction. Roughly, a proof is normal if it can be found by using only introduction rules from below (from the goal) and only elimination rules from above (the assumptions). Normal proofs are complete for the propositional fragment (every true proposition has a normal proof). As an application, we can show the independence of certain schematic propositions such as the so-called law of excluded middle.
A common alternative meaning explanation is via notational definitions. We use this, for example, to define negation and equivalence of propositions.
As a final, purely logical concept we consider universal and existential quantification over elements of an unspecified domain. This yields first-order intuitionistic logic. If we also assume the law of excluded middle (which cannot be justified using our machinery of judgments), then we obtain classical logic in which every proposition is assumed to be true or false. This destroys the constructive nature of proofs which is subject of the second part of the course.
Proofs and Programs
We introduce proof terms to directly express the evidence for the truth of a proposition. Proofs terms constitute a small functional programming languages, in which propositions play the role of types. This correspondence is known as the Curry-Howard isomorphism between proofs and programs. The basis for computation are local reductions, expressed as reduction rules on proof terms.
Under this interpretation, implication corresponds to function types, conjunction to product types, and disjunction to disjoint sum types. Thus we have strong logical guidance in the design of programming languages and type systems, which is the first major application of logic in computer science we consider.
To write interesting programs we need specific data types, such as Booleans, natural numbers, and lists. These can be introduced via introduction and elimination rules, following precisely the same methodology as in our development of logic. Elimination rules takes the form of schemas for definition by cases or primitive recursion (elimination on types) and proof by cases or induction (elimination on propositions).
We briefly investigate arithmetic (the theory of natural numbers), but then generalize to other structure data types and discuss various programming concepts. This includes reasoning about data representation (exemplified by an implementation of numbers as bit strings), general recursion (related to complete induction), and reasoning about data structure invariants (captured by dependent types).
With dependent types we have essentially replicated the full structure of propositions at the level of types. In order to avoid excessive redundancy, those concepts are therefore often collapsed, which can be justified by the correspondence between proofs and programs. In general, we see that proofs concerning data types contain computationally uninteresting part, and we show how to consistently eliminating those parts, thereby contracting proofs to programs.
Classical Logic
The standard semantics of classical logic is given by truth assignments. Every proposition is either true or false. The propositional connectives are given their usual intepretation via truth tables, and the quantifiers are given meaning with respect to a model. This semantics is thoroughly non-constructive.
Surprisingly, classical logic also has a constructive interpretation. First, we note that from a constructive point of view, classical logic is a form of constructive logic in which we postulate that every proposition is decidable. This can be expressed by positing that the double negation of a proposition is equivalent to that proposition.
But what is the computational content of this assumption? The astonishing result is that it corresponds to a special control construct similar to a goto statement in an ordinary programming language. Such a construct may be constructivized by a global transformation very similar to one used in many compilers for functional languages, the CPS transformation.
(Intuitionistic) Linear Logic
Just as constructive logic may be seen as a refinement of classical logic, so intuitionistic linear logic is a refinement of constructive logic. Constructive logic is the logic of effective computation with no constraints on the use of resources. In contrast intuitionistic linear logic is the logic of resource-sensitive computation.
Linear logic is resource-sensitive in the sense that it takes account of how many times an assumption is used in a proof. In constructive logic we may use an assumption any number of times, without explicit mention. In linear logic we must use each assumption exactly once. Thus assuming P twice is not the same as assuming it once! However, we may make the assumption ` of course P ', which means ` P, any number of times ' to obtain a controlled relaxation of these strictures.
Linear logic admits many computational interpretations. We will consider a linear functional programming language that provides one such interpretation.