This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...) more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)
The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi.
The paper discusses the transition from informal concepts to mathematically precise notions; examples are given, and in some detail the case of lawless sequences, a concept of intuitionistic mathematics, is discussed. A final section comments on philosophical discussions concerning intuitionistic logic in connection with a ‘theory of meaning’.
In this paper we discuss a particular example of the passage from the informal, but rigorous description of a concept to the axiomatic formulation of principles holding for the concept; in particular, we look at the principles of continuity and lawlike choice in the theory of lawless sequences. Our discussion also leads to a better understanding of the rôle of the so-called density axiom for lawless sequences.
This paper studies, by way of an example, the intuitionistic propositional connective * defined in the language of second order propositional logic by. In full topological models * is not generally definable, but over Cantor-space and the reals it can be classically shown that; on the other hand, this is false constructively, i.e. a contradiction with Church's thesis is obtained. This is comparable with some well-known results on the completeness of intuitionistic first-order predicate logic.Over [0, 1], the operator * is (...) (constructively and classically) undefinable. We show how to recast this argument in terms of intuitive intuitionistic validity in some parameter. The undefinability argument essentially uses the connectedness of [0, 1]; most of the work of recasting consists in the choice of a suitable intuitionistically meaningful parameter, so as to imitate the effect of connectedness. (shrink)