Driven by the question, 'What is the computational content of a (formal) proof?', this book studies fundamental interactions between proof theory and computability. It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science. Part I covers basic proof theory, computability and Gödel's theorems. Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to Π11-CA0. Ordinal analysis and the (Schwichtenberg-Wainer) subrecursive hierarchies play a central role and are (...) used in proving the 'modified finite Ramsey' and 'extended Kruskal' independence results for PA and Π11-CA0. Part III develops the theoretical underpinnings of the first author's proof assistant MINLOG. Three chapters cover higher-type computability via information systems, a constructive theory TCF of computable functionals, realizability, Dialectica interpretation, computationally significant quantifiers and connectives and polytime complexity in a two-sorted, higher-type arithmetic with linear logic. (shrink)

Let A be a formula without implications, and Γ consist of formulas containing disjunction and falsity only negatively and implication only positively. Orevkov and Nadathur proved that classical derivability of A from Γ implies intuitionistic derivability, by a transformation of derivations in sequent calculi. We give a new proof of this result , where the input data are natural deduction proofs in long normal form involving stability axioms for relations; the proof gives a quadratic algorithm to remove the stability axioms. (...) This can be of interest for computational uses of classical proofs. (shrink)

From a classical proof that the gcd of natural numbers a1 and a2 is a linear combination of the two, we extract by Gödel's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well-founded recursion can be used to Dialectica interpret well-founded induction, which is needed in the proof of the minimum principle. In the special case of the example above it turns out that we obtain a reasonable extracted term, representing an (...) algorithm close to Euclid's. (shrink)

Buchholz presented a method to build notation systems for infinite sequent-style derivations, analogous to well-known systems of notation for ordinals. The essential feature is that from a notation one can read off by a primitive recursive function its n th predecessor and, e.g. the last rule applied. Here we extend the method to the more general setting of infinite terms, in order to make it applicable in other proof-theoretic contexts as well as in recursion theory. As examples, we use the (...) method to 1. give a new proof of a well-known trade-off theorem , which says that detours through higher types can be eliminated by the use of transfinite recursion along higher ordinals, and 2. construct a continuous normalization operator with an explicit modulus of continuity. (shrink)

Several properties of monotone functionals (MF) and monotone majorizable functionals (MMF) used in the earlier work by the author and van de Pol are proved. It turns out that the terms of the simply typed lambda-calculus define MF, but adding primitive recursion, and even monotonic primitive recursion changes the situation: already Z.Z(1 — sg) is not MMF. It is proved that extensionality is not Dialectica-realizable by MMF, and a simple example of a MF which is not hereditarily majorizable is given.

The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula.

Consider the problem which set V of propositional variables suffices for whenever, where, and ⊢c and ⊢i denote derivability in classical and intuitionistic implicational logic, respectively. We give a direct proof that stability for the final propositional variable of the (implicational) formula A is sufficient; as a corollary one obtains Glivenko's theorem. Conversely, using Glivenko's theorem one can give an alternative proof of our result. As an alternative to stability we then consider the Peirce formula. It is an easy consequence (...) of the result above that adding a single instance of the Peirce formula suffices to move from classical to intuitionistic derivability. Finally we consider the question whether one could do the same for minimal logic. Given a classical derivation of a propositional formula not involving ⊥, which instances of the Peirce formula suffice as additional premises to ensure derivability in minimal logic? We define a set of such Peirce formulas, and show that in general an unbounded number of them is necessary. (shrink)

Proceedings of the NATO Advanced Study Institute on Proof and Computation, held in Marktoberdorf, Germany, July 20 - August 1, 1993.

This is a tutorial for the Minlog Proof Assistant, version 5.0.

Constructive mathematics – mathematics in which ‘there exists’ always means ‘we can construct’ – is enjoying a renaissance. Fifty years on from Bishop’s groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject’s myriad aspects. Major themes include: constructive algebra and geometry, constructive analysis, constructive topology, (...) constructive logic and foundations of mathematics, and computational aspects of constructive mathematics. A series of introductory chapters provides graduate students and other newcomers to the subject with foundations for the surveys that follow. Edited by four of the most eminent experts in the field, this is an indispensable reference for constructive mathematicians and a fascinating vista of modern constructivism for the increasing number of researchers interested in constructive approaches. (shrink)

This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.

It is shown how to restrict recursion on notation in all finite types so as to characterize the polynomial-time computable functions. The restrictions are obtained by using a ramified type structure, and by adding linear concepts to the lambda calculus.

We show that the number-theoretic functions definable in the atomic polymorphic system are exactly the extended polynomials. Two proofs of the above result are presented: one, reducing the functions’ definability problem in ${\mathbf{F}}_{\mathbf{at}}$ to definability in the simply typed lambda calculus and the other, directly adapting Helmut Schwichtenberg’s strategy for definability in $\lambda ^{\rightarrow }$ to the atomic polymorphic setting. The uniformity granted in the polymorphic system, when compared with the simply typed lambda calculus, is emphasized.

Analyzes the philosophical ideas of two famous neo-Kantian philosophers, Hermann Cohen and Paul Natorp, who worked together in the Marburger Schule research institute from 1880 to 1912. In volume 1, mentions differences of opinion between them, partly due to Cohen's Jewishness, noting that Cohen resented the prevalence of antisemitism and discrimination. Cohen felt that Natorp's opposition to his ideas was motivated by antisemitism. The second volume is a collection of documents and correspondence between the two and others, where antisemitism is (...) frequently mentioned (see the index). (shrink)

This essay introduces ideas from Confucius, Xunzi, the Six Dynasties, and Kant about beauty, music, morality, and what we might today call “aesthetic education.” It asks how beauty and morality are related and how they ideally should be related to each other. We know that beauty and morality can drift apart, and we may wonder how aesthetic education might work best. Should the arts be a means for developing morality? Or should it be the other way around? These questions are (...) still relevant today. But our world has changed, not only since Confucius, but also since Kant. We may ask what to make of their ideas in our present time. I argue that there are good reasons for keeping morality and aesthetics apart, somewhat in the spirit of Kant, and in opposition to the idea of “fusing” the two. (shrink)

Jakob Friedrich Fries (1773–1843) was the most prolific German philosopher of science in the nineteenth century who strived to synthesize Kant’s philosophical foundation of science and mathematics and the needs or practised science and mathematics in order to gain more comprehensive conceptual frameworks and greater methodological flexibility for those two disciplines. His original contributions anticipated later developments, to some extent, though they received comparatively little notice in the later course of the nineteenth century—a fate which partly can be explained by (...) the unfortunate development of the so-called ‘First Friesian School,’ founded by E. F. Apelt, M. J. Schleiden and O. X. Schlömilch. This situation changed temporarily when Leonard Nelson (1882–1927) arrived on the philosophical stage and founded a second, so-called, ‘New Friesian School’ in 1903. In the following two decades, Fries’ specific transformation of Kantian philosophy gained influence within the vigorous discussions about ‘new’ foundations of mathematics and, thus, also played a role within the Berlin Group surrounding Hans Reichenbach, though his work had no direct impact on the philosophy of physics being expounded therein. -/- This essay will first outline some characteristics of Fries’ development of the Kantian approach. Then it will point out the limited impact of the ‘New Friesian School’ on the Berlin Group, while highlighting some missed chances for fruitful exchange. As the originality of this school and its importance for the development of logic and philosophy of mathematics—by and large merits of its early members Walter Dubislav and Kurt Grelling —is dealt with in separate chapters of this volume, and elsewhere, this article will focus on what Fries called the ‘mathematical philosophy of nature’ (i. e. the philosophical foundations of physics). More specifically, it will show how the New Friesian School reacted to Einstein’s theories of relativity, in a way that contrasts with the approach of the Berlin Group. This discussion about relativity will also be used to reveal different understandings of the nature of ‘scientific philosophy’ in general, as well as different models of how philosophy and the empirical sciences should interact. (shrink)

In the yeast Saccharomyces cerevisiae three positive transcriptional control elements are activated by stress conditions: heat shock elements (HSEs), stress response elements (STREs) and AP‐1 responsive elements (AREs). HSEs bind heat shock transcription factor (HSF), which is activated by stress conditions causing accumulation of abnormal proteins. STREs mediate transcriptional activation by multiple stress conditions. They are controlled by high osmolarity via the HOG signal pathway, which comprises a MAP kinase module and a two‐component system homologous to prokaryotic signal transducers. AREs (...) bind the transcription factor Yap1p. The three types of control elements seem to have overlapping, but distinct functions. Some stress proteins encoded by HSE‐regulated genes are necessary for growth of yeast under moderate stress, products of STRE‐activated genes appear to be important for survival under severe stress and ARE‐controlled genes may mainly function during oxidative stress and in the response to toxic conditions, such as caused by heavy metal ions. (shrink)